[Haskell] A question about fundeps <-> GADT interaction

[Tomasz Zielonka]

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