RE: [Haskell] A question about fundeps <-> GADT interaction
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@haskell.org [mailto:haskell-bounces@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell
On Thu, Dec 29, 2005 at 09:48:04AM -0000, Simon Peyton-Jones wrote:
Intriguing! I'm afraid it'll be some time before your code works, though.
No problem, I can wait.
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.
I wonder if my problem can't be solved with Associated Type Synonyms. But was interaction of ATS and GADT explored at all?
As of today, if it works at all, it's quite amazing.
I am amazed too. After all, Oleg found a way to make "untype" compile (but there are still problems with more complicated functions). There is also his idea for doing it in a different way, but haven't tested it yet. 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
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
On Thu, Dec 29, 2005 at 12:39:01PM +0000, Bruno Oliveira wrote:
A second alternative would be to simulate your GADT with a type class and your constructors with the functions of that type class:
[...]
As a remark, this is a church encoding of the GADT.
[...]
Now you can encode functions on the GADT as instances of this type class:
This is very interesting. Thanks! I'll try to apply this technique to my problem. 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
participants (3)
-
Bruno Oliveira -
Simon Peyton-Jones -
Tomasz Zielonka