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

[Simon Peyton-Jones]

Tomasz

Intriguing!  I'm afraid it'll be some time before your code works,
though.

First I have to get GADTs and type classes to play together nicely,
which I am hoping to do during Jan/Feb.  Then I'll have to think about
the interaction between GADTs and fundeps. 

As of today, if it works at all, it's quite amazing.

Simon

| -----Original Message-----
| From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org]
On Behalf Of Tomasz
| Zielonka
| Sent: 22 December 2005 14:16
| To: Haskell Mailing List
| Subject: [Haskell] A question about fundeps <-> GADT interaction
| 
| 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
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell