Add Zero (Succ n) ~ Succ n “Equality Axiom” Type Family instance …compiles to There is no “type computation”! (only solving of equality constraints) Add Int Bool ~ Add Int Bool
a -> List a append :: Vect n a -> Vect m a -> Vect (n + m) a index :: n -> List a -> a index :: Upto n -> Vect n a -> a transpose :: Matrix a -> Matrix a transpose :: Matrix m n a -> Matrix n m a take :: Nat -> List a -> List a take :: (n::Nat) -> Vect (n + m) a -> Vect m a
Nat -> Nat -> Nat add Zero n = Zero add (Succ n) m = Succ (add n m) length :: Vect n a -> n length {n} _ = n replicate :: n -> a -> Vect n a replicate Zero _ = Nil replicate (Succ n) x = Cons x (replicate n x)