[Haskell-cafe] Combine type family return value

9 Oct 2014

      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 <KAction@gnu.org>,
Free Software supporter, esperantisto and netiquette guardian.
GPG: 54B7F00D