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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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 | [email protected] | http://www.haskell.org/mailman/listinfo/haskell _______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
