Type Checking with Indexed Type Synonyms

This is OLD and OUT OF DATE material.

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.

Last modified 10 years ago Last modified on Apr 6, 2008 8:29:49 AM