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

[Bruno Oliveira]

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