EvaluateType.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}

data Nat = Z | S Nat

data Expr = Num Nat
           | Add Expr Expr

type family Eval (expr :: Expr)  :: Nat where
  Eval ('Num n) = n
  Eval ('Add e e) = Add (Eval e) (Eval e)

type family Add (x :: Nat) (y :: Nat) :: Nat where
  Add 'Z     y = y
  Add ('S x) y = 'S (Add x y)

-- *Main> :kind! Eval ('Add ('Num ('S 'Z)) ('Num ('Z)))
--  Eval ('Add ('Num ('S 'Z)) ('Num ('Z))) :: Nat
--  = Eval ('Add ('Num ('S 'Z)) ('Num 'Z))