Hello! (This message is a literate Haskell module)

{-# OPTIONS -fglasgow-exts -fno-warn-missing-methods #-} module Term where

The papers on GADTs have an example showing how you can transform, traverse and evaluate ASTs (or terms) with more type safety. I've used such an approach in one of my applications and it works remarkably well. However, I would like to be able to "turn off" that type-safety in some parts of code, for example to separate parsing from typing. I thought I found a way to do this, because I was able to create Typed (with all consistency checking) and Untyped (without consistency checking) terms. Unfortunately I seem to be unable to write any useful function on such terms - GHC complains that there are type errors. I think this is because of the known problem with current GADT implementation in GHC, namely - bad GADT / type-classes interaction. I would be very happy to hear that it will be solved in GHC 6.6. I use an additional type parameter for Term that determines whether the Term is used as Typed or Untyped. Typed terms will have types (Term Typed Int), (Term Typed Bool), ..., but Untyped terms only one type: (Term Untyped ()) I use a multiparameter type-class with fundeps to describe a relation between the Typed/Untyped tag used, the types actually used in data constructors and the resulting "phantom" type.

class F f a b | f a -> b where -- these methods are just for experiments in GHCi a2b :: f -> a -> b b2a :: f -> b -> a

data Typed = Typed instance F Typed a a where

data Untyped = Untyped instance F Untyped a () where

data Term f a where Lit :: (F f Int int) => Int -> Term f int Succ :: (F f Int int) => Term f int -> Term f int IsZero :: (F f Int int, F f Bool bool) => Term f int -> Term f bool If :: (F f Bool bool, F f a a') => Term f bool -> Term f a' -> Term f a' -> Term f a'

Some examples: a typeable term

ex1 :: Term Untyped () ex1 = If (IsZero (Succ (Lit 0))) (Lit 1) (Lit 2)

the same as ex1, but Typed

ex1' :: Term Typed Int ex1' = If (IsZero (Succ (Lit 0))) (Lit 1) (Lit 2)

a term that has type bug, but will be accepted as Untyped

ex2 :: Term Untyped () ex2 = If (IsZero (Succ (Lit 0))) (Lit 1) (IsZero (Lit 2))

Here is the function that doesn't type check (you can comment it out to get the rest of code to compile).

-- A simple cast from typed terms to untyped terms untype :: Term Typed a -> Term Untyped () untype (Lit x) = Lit x untype (IsZero t) = IsZero (untype t) untype (Succ t) = Succ (untype t) untype (If c t e) = If (untype c) (untype t) (untype e)

The error given by GHC (for the commented "untype" function) is: T.hs:52:8: Couldn't match the rigid variable `a' against `Int' `a' is bound by the type signature for `untype' Expected type: Int Inferred type: a When using functional dependencies to combine F Typed a a, arising from the instance declaration at T.hs:13:0 F Typed Int a, arising from the pattern for `Lit' at T.hs:52:8-12 at T.hs:52:8-12 In the definition of `untype': untype (Lit x) = Lit x Failed, modules loaded: none. So it seems it can't infer that the 'a' in (F Typed Int a) is Int. At the same time... *T> :t a2b a2b :: (F f a b) => f -> a -> b *T> :t a2b Untyped a2b Untyped :: a -> () *T> :t a2b Typed a2b Typed :: b -> b -- see? it knows a and b are equal! *T> :t b2a Typed b2a Typed :: b -> b If there is another way to do this right now (conveniently, Oleg! ;-), I would be more than happy to hear about it. If this worked, it would be a cool trick and a nice example for GADT use. Let me know if it was proposed before. Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland