Замена однотипных типов данных с помощью семейства данных

Question

Итак, в моем текущем проекте я нахожу, что я делаю кучу логики уровня типа с одноточечными типами.

Например:

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE GADTs #-} 
module TypeBools where 

type family (||) (a :: Bool) (b :: Bool) :: Bool where 
    'False || 'False = 'False 
    'False || 'True = 'True 
    'True || 'False = 'True 
    'True || 'True = 'True 

data OrProof (a :: Bool) (b :: Bool) (c :: Bool) where 
    OrProof :: SBool (a || b) -> OrProof a b (a || b) 

data SBool (b :: Bool) where 
    SFalse :: SBool 'False 
    STrue :: SBool 'True 

class Boolean b where 
    sBool :: SBool b 
instance Boolean 'False where 
    sBool = SFalse 
instance Boolean 'True where 
    sBool = STrue 

orProof :: (Boolean a, Boolean b) => OrProof a b (a || b) 
orProof = go sBool sBool where 

    go :: SBool a -> SBool b -> OrProof a b (a || b) 
    go SFalse SFalse = OrProof SFalse 
    go SFalse STrue = OrProof STrue 
    go STrue SFalse = OrProof STrue 
    go STrue STrue = OrProof STrue 

И это работает очень хорошо для меня. Мне не нравится кататься по одиночным путям вручную, имея возможность вызвать их при необходимости через класс (например, класс Boolean), но это привело к появлению довольно похожих моделей , которые существуют только для того, чтобы тип как одноточечные данные.

Я подумал, что я мог бы абстрактное эти несколько классов типов в одной семье типа, , например, замену SBool и Boolean выше с:

{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE ConstraintKinds #-} 
-- ... 
class Singleton (t :: k) where 
    data Sing t 
    sing :: Sing t 

instance Singleton 'False where 
    data Sing 'False = SFalse 
    sing = SFalse 

instance Singleton 'True where 
    data Sing 'True = STrue 
    sing = STrue 

type SBool b = Sing (b :: Bool) 

type Boolean b = Singleton (b :: Bool) 
sBool :: Boolean b => SBool b 
sBool = sing 

Но тогда я получаю шаблоны ошибок матча:

TypeBools2.hs:42:13: 
    Couldn't match type ‘b1’ with ‘'True’ 
     ‘b1’ is a rigid type variable bound by 
      the type signature for 
      go :: SBool a1 -> SBool b1 -> OrProof a1 b1 (a1 || b1) 
      at TypeBools2.hs:40:9 
    Expected type: SBool b1 
     Actual type: Sing 'True 
    Relevant bindings include 
     go :: SBool a1 -> SBool b1 -> OrProof a1 b1 (a1 || b1) 
     (bound at TypeBools2.hs:41:3) 
    In the pattern: STrue 
    In an equation for ‘go’: go SFalse STrue = OrProof STrue 
    In an equation for ‘orProof’: 
     orProof 
      = go sBool sBool 
      where 
       go :: SBool a -> SBool b -> OrProof a b (a || b) 
       go SFalse SFalse = OrProof SFalse 
       go SFalse STrue = OrProof STrue 
       go STrue SFalse = OrProof STrue 
       go STrue STrue = OrProof STrue 

Я не уверен, есть ли что-то еще, я могу убедить компилятор в том, что b1 должен иметь вид Bool, или если Я просто лаем по неправильному дереву здесь.

Answer 1

Ваша запрашиваемая функция и многое другое можно найти в singletons. Он был окончательным шаблоном для программирования на уровне шрифта довольно долгое время. Вы должны либо использовать его, либо скопировать реализацию. Во всяком случае, я сделаю здесь краткую презентацию для упрощенного решения singletons.

Ваш шаблон не работает, потому что STrue и SFalse находятся в разных определениях данных, и для начала это не GADT. Согласование шаблонов только уточняет типы, когда они выполняются на соответствующих GADT-с. Нам нужно отправить по виды, чтобы иметь возможность группировать все одиночные конструкторы одного типа.

Мы можем сделать это либо с надлежащим классом вида, либо с семейством данных верхнего уровня. Последнее проще для наших целей сейчас, так что давайте сделаем это:

data family Sing (x :: k) 

data instance Sing (b :: Bool) where 
    STrue :: Sing True 
    SFalse :: Sing False 

С sing нам не нужен родом отправка, потому что мы только использовать его для получения конкретных поднимаемых значений, поэтому следующие работ:

class SingI (x :: k) where 
    sing :: Sing x 

instance SingI True where sing = STrue 
instance SingI False where sing = SFalse 

Что касается orProof, то мы хотели бы иметь одноэлементный тип для 0-го уровня (||), который наиболее прост в достижении следующего уровня: Sing b1-> Sing b2 -> Sing (b1 || b2). Мы назовем его (%:||), в соответствии с иероглифической практикой именования singletons.

type family (:||) (b1 :: Bool) (b2 :: Bool) :: Bool where 
    True :|| b = True 
    False :|| b = b 

(%:||) :: Sing b1 -> Sing b2 -> Sing (b1 :|| b2) 
(%:||) STrue b2 = STrue 
(%:||) SFalse b2 = b2 

OrProof не очень полезно, так как это просто специальный тип равенства наряду с SingI ограничением или простой Sing c:

type OrProof a b c = SingI c => c :~: (a :|| b) 
type OrProof' a b c = (Sing c, c :~: (a :|| b))