Hello! Following code is my attempt to comprehend type families and data
kinds.
I want to annotate boolean formula with variables it contains, so
I get function `value` checked at compile time.
`value` should return Bool, if no variables are present in formula,
list of variables otherwise.
Of course, `value` can just return Either [Var] Bool, but
I want to get Type-level programming-fu.
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat
type family Plus (x :: Nat) (y :: Nat) :: Nat
type instance Plus Zero x = x
type instance Plus (Succ x) y = Plus x (Succ y)
type family Multi (x :: Nat) (y :: Nat) :: Nat
type instance Multi Zero x = Zero
type instance Multi (Succ x) y = Plus y (Multi x y)
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Power2 a = Power Two a
type family Power (n :: Nat) (k :: Nat) :: Nat
type instance Power n Zero = One
type instance Power n (Succ x) = Multi n (Power n x)
data Var = Pv | Qv | Rv
type family PEncode (v :: Var) :: Nat
type instance PEncode Pv = Power2 Zero
type instance PEncode Qv = Power2 One
type instance PEncode Rv = Power2 Two
-- type instance PDecode (v :: Nat) :: *
data Formula (n :: Nat) where
P :: Formula (PEncode Pv)
Q :: Formula (PEncode Qv)
R :: Formula (PEncode Rv)
Const :: Bool -> Formula Zero
Conj :: Formula n -> Formula m -> Formula (Plus n m)
type family FormulaValue (x :: Nat) :: *
type instance FormulaValue Zero = Bool
type instance FormulaValue (Succ n) = [Var]
value :: Formula n -> FormulaValue n
value (Const v) = v
value P = [Pv]
value Q = [Pv]
value R = [Pv]
value (Conj x y) = {- I have no idea -}
deriving instance Show (Formula n)
main = print $ Conj P Q
--
Best regards, Dmitry Bogatov