[Haskell] A question about fundeps <-> GADT interaction
Bruno Oliveira
bruno.oliveira at comlab.ox.ac.uk
Thu Dec 29 07:39:01 EST 2005
Hello Tomasz,
Unfortunatelly I have only seen your message after Simon answered to it.
I am sorry for the late answer!
>| 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.
Well, it is true that GADTs and type classes functional depencies do not
work well, but there is no problem if you only use type classes.
The first alternative would be using a multiple parameter type classes with
functional dependencies. This would be something that Oleg would be likely
to propose you. But I think you do not want this :)
A second alternative would be to simulate your GADT with a type class and
your constructors with the functions of that type class:
> class Term g where
> lit :: F f Int int => Int -> g f int
> suc :: F f Int int => g f int -> g f int
> isZero :: (F f Int int, F f Bool bool) =>
> g f int -> g f bool
> iff :: (F f Bool bool, F f a a') =>
> g f bool -> g f a' -> g f a' -> g f a'
As a remark, this is a church encoding of the GADT.
Your examples:
> ex1 :: Term g => g Untyped ()
> ex1 =
> iff (isZero (suc (lit 0)))
> (lit 1)
> (lit 2)
| the same as ex1, but Typed
> ex1' :: Term g => g Typed Int
> ex1' =
> iff (isZero (suc (lit 0)))
> (lit 1)
> (lit 2)
| a term that has type bug, but will be accepted as Untyped
> ex2 :: Term g => g Untyped ()
> ex2 =
> iff (isZero (suc (lit 0)))
> (lit 1)
> (isZero (lit 2))
Now you can encode functions on the GADT as instances of this type class:
> newtype Untype g b a = Untype {untype :: g Untyped ()}
> instance Term g => Term (Untype g) where
> lit x = Untype (lit x)
> suc t = Untype (suc (untype t))
> isZero t = Untype (isZero (untype t))
> iff c t e = Untype (iff (untype c) (untype t) (untype e))
This should suffice for encoding your untype.
Although this might look like a bit puzzling at first glance, the translation
of the GADT code into the type class version (and vice versa) is quite
straighforward and mechanical.
The advantages of this encoding in relation to GADTs are that:
1) It does not have the GADTs <-> fundeps problem;
2) It does not require any heavy machinary from the compiler
(if it would not be for your F class, it would be Haskell 98).
The main disadvantage is that in some functions that you can define
with GADT might not be easily definable with this encoding. I must
say that, from my experience, that functions of this kind do not occur
often.
Until GHC fixes the problem of the interaction between fundeps and
GADTs, you might want to consider using this. All code you develop
with this encoding can be very easily translated to GADT form once the
problem is solved.
If you want further references to this technique check this:
http://www.mail-archive.com/haskell-cafe@haskell.org/msg10047.html
The original thread by Conor is:
http://www.mail-archive.com/haskell-cafe@haskell.org/msg10033.html
The discussion that derived from this thread is quite interesting.
Cheers,
Bruno
More information about the Haskell
mailing list