Presented at IFL 2007.
Abstract
We report on an extension of Haskell with type(-level) functions and equality
constraints. We illustrate their usefulness in the context of phantom types,
GADTs and type classes. Problems in the context of type checking are identified
and we sketch our solution: a decidable type checking algorithm for a
restricted class of type functions. Moreover, functional dependencies are now
obsolete: we show how they can be encoded as type functions.
DRAFT PDF (19 pages)
This page is part of Manuel Chakravarty's WWW-stuff.