you can also write an interpreter in haskell that will typecheck using GADT's http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf http://www.haskell.org/pipermail/haskell/2005-May/015815.html