[Haskell] A question about fundeps <> GADT interaction
Simon PeytonJones
simonpj at microsoft.com
Thu Dec 29 04:48:04 EST 2005
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: haskellbounces at haskell.org [mailto:haskellbounces 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 fglasgowexts fnowarnmissingmethods #}
 > 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 typesafety
 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 / typeclasses 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 typeclass 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:812 at
T.hs:52:812
 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
More information about the Haskell
mailing list