Version 28 (modified by simonpj, 11 years ago) (diff)


Type Checking with Indexed Type Synonyms

GHC has now FC as its typed intermediate language. In a next step, we wish to add type functions to GHC's source language. Type functions in combination with type annotations and GADTs allow us to type check some interesting programs.

data Zero
data Succ n
data List a n where
  Nil  :: List a Zero
  Cons :: a -> List a m -> List a (Succ m)

type family Add :: * -> * -> *
type instance Add Zero     y = y
type instance Add (Succ x) y = Succ (Add x y)

append :: List a l -> List a m -> List a (Add l m)
append Nil xs = xs
append (Cons x xs) ys = Cons x (append xs ys)

However, type checking with type functions is challenging.