Type Families - WIP

TypeFamilies.hs

{-# LANGUAGE TypeFamilies
           , DataKinds
           , PolyKinds
           , TypeInType
           , TypeOperators
           , UndecidableInstances
           , RankNTypes
  #-}


module TypeFamilies where

import Data.Kind (Type)
import GHC.TypeNats (Nat, type (+))
import GHC.Types

type Expr a = a -> Type

type family Eval (e :: Expr a) :: a

data Lit :: a -> Expr a
type instance Eval (Lit x) = x

data Add:: Expr Nat -> Expr Nat -> Expr Nat
type instance Eval (Add l r ) = Eval l + Eval r

data Succ :: Expr Nat -> Expr Nat
type instance Eval (Succ x) =  1 + Eval x

data IsZero :: Expr Nat -> Expr Bool
type instance Eval (IsZero (Lit 0)) =  Eval (Lit 'True)
--type instance Eval (IsZero _) =  Eval (Lit 'False)


data If :: Expr Bool -> Expr a -> Expr a -> Expr a
type instance Eval (If (Lit True) t e ) = Eval t
type instance Eval (If (Lit False) t e ) = Eval e