GADTs and functional dependencies

newer
Re: newSession gone from GHC API

older
6.10-candidate tested

Wolfgang Jeltsch

23 Sep 2008 23 Sep '08

12:07 p.m.

Hello, please consider the following code:

...

{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

data GADT a where

GADT :: GADT ()

class Class a b | a -> b

instance Class () ()

fun :: (Class a b) => GADT a -> b fun GADT = ()

I’d expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message:

...

FDGADT.hs:12:11: Couldn't match expected type `b' against inferred type `()' `b' is a rigid type variable bound by the type signature for `fun' at FDGADT.hs:11:16 In the expression: () In the definition of `fun': fun GADT = ()

What’s the reason for this? Is there a workaround? Does this work in 6.8.3 or 6.10.1? Thank you in advance. Best wishes, Wolfgang

Show replies by date

Alfonso Acosta

23 Sep 23 Sep

12:19 p.m.

On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch wrote:

...

Hello,

please consider the following code:

...
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

data GADT a where

GADT :: GADT ()

class Class a b | a -> b

instance Class () ()

fun :: (Class a b) => GADT a -> b fun GADT = ()

I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message:

bear in mind that the only instance you defined is instance Class () () which doesn't involve your GADT at all. Maybe you meant something like: instance Class (GADT a) () Moreover, your fun cannot typecheck, regardless of using MPTC or GADTs. The unit constructor, (), has type () and not b.

Wolfgang Jeltsch

12:36 p.m.

Am Dienstag, 23. September 2008 18:19 schrieben Sie:

...

On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch

wrote:

...
Hello,

please consider the following code:

...
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

data GADT a where

GADT :: GADT ()

class Class a b | a -> b

instance Class () ()

fun :: (Class a b) => GADT a -> b fun GADT = ()

I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message:

bear in mind that the only instance you defined is

instance Class () ()

which doesn't involve your GADT at all.

This is correct. (It’s only a trimmed-down example, after all.)

...

Maybe you meant something like:

instance Class (GADT a) ()

No, I didn’t.

...

Moreover, your fun cannot typecheck, regardless of using MPTC or GADTs. The unit constructor, (), has type () and not b.

Pattern matching against the data constructor GADT specializes a to (). Since Class uses a functional dependency, it is clear that b has to be (). So it should typecheck. At least, I want it to. ;-) Best wishes, Wolfgang

Alfonso Acosta

12:44 p.m.

On Tue, Sep 23, 2008 at 6:36 PM, Wolfgang Jeltsch wrote:

...

Pattern matching against the data constructor GADT specializes a to (). Since Class uses a functional dependency, it is clear that b has to be ().

True, but it wont work if you provide () as the result and b in the explicit signature. GHC is ranting with reason, the provided type, b, does not match (). On the other hand, this works: fun :: (Class a b) => GADT a -> b fun GADT = undefined And as you stated, b can only be ()

Jason Dagit

1:06 p.m.

On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch wrote:

...

Am Dienstag, 23. September 2008 18:19 schrieben Sie:

...
On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch

wrote:

...
Hello,

please consider the following code:

...
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

data GADT a where

GADT :: GADT ()

class Class a b | a -> b

instance Class () ()

fun :: (Class a b) => GADT a -> b fun GADT = ()

I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message:

bear in mind that the only instance you defined is

instance Class () ()

which doesn't involve your GADT at all.

This is correct. (It's only a trimmed-down example, after all.)

...
Maybe you meant something like:

instance Class (GADT a) ()

No, I didn't.

...
Moreover, your fun cannot typecheck, regardless of using MPTC or GADTs. The unit constructor, (), has type () and not b.

Pattern matching against the data constructor GADT specializes a to (). Since Class uses a functional dependency, it is clear that b has to be (). So it should typecheck. At least, I want it to. ;-)

In the signature: fun :: (Class a b) => GADT a -> b What is there to determine the type a? It's a phantom in the definition of GADT, so it can unify arbitrarily for us, but there is nothing in your program to cause it to unify a certain way. Based on what you're hoping for, I think you would need: class Class a b | b -> a But, then think about how the type checker looks at fun, which returns (). Now we see that b should be (), but () is not the same as b. That is, () does not generalize to b, even though an arbitrary b could specialize to (). Did some other version of ghc accept this code? Jason

Jason Dagit

1:13 p.m.

On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch wrote:

...

Am Dienstag, 23. September 2008 18:19 schrieben Sie:

...
On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch

wrote:

...
Hello,

please consider the following code:

...
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

data GADT a where

GADT :: GADT ()

class Class a b | a -> b

instance Class () ()

fun :: (Class a b) => GADT a -> b fun GADT = ()

I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message:

bear in mind that the only instance you defined is

instance Class () ()

which doesn't involve your GADT at all.

This is correct. (It's only a trimmed-down example, after all.)

...
Maybe you meant something like:

instance Class (GADT a) ()

No, I didn't.

...
Moreover, your fun cannot typecheck, regardless of using MPTC or GADTs. The unit constructor, (), has type () and not b.

Pattern matching against the data constructor GADT specializes a to (). Since Class uses a functional dependency, it is clear that b has to be (). So it should typecheck. At least, I want it to. ;-)

I'm re-reading what you said after my first reply. I'm inserting types in places that may not be valid in Haskell... You're saying that the types should be like this: fun :: (Class a b) => GADT a -> b fun (GADT :: GADT ()) = () So, now I'm more inclined to agree with you than before. And suppose we added this: data GADT a where GADT :: GADT () GADT2 :: GADT String Now I would expect this: fun :: (Class a b) => GADT a -> b fun (GADT :: GADT ()) = () fun (GADT2 :: GADT String) = -- I can't put anything here till I add more instances of Class Now, I'm too confused about how this should work. Jason

Chris Kuklewicz

1:44 p.m.

You cannot create a normal function "fun". You can make a type class function fun :: Class a b => GADT a -> b

...

data GADT a where GADT :: GADT () GADT2 :: GADT String

-- fun1 :: GADT () -> () -- infers type fun1 g = case g of (GADT :: GADT ()) -> ()

-- fun2 :: GADT String -> Bool -- infers type fun2 g = case g of (GADT2 :: GADT String) -> True

-- "fun" cannot type check. The type of 'g' cannot be both "GADT ()" and "GADT String" -- This is because "fun" is not a member of type class. {- fun g = case g of (GADT :: GADT ()) -> () (GADT2 :: GADT String) -> True -}

class Class a b | a -> b where fun :: GADT a -> b

instance Class () () where fun GADT = ()

instance Class String Bool where fun GADT2 = True

main = print $ (fun GADT, fun GADT2) == ( (), True )

David Menendez

2:35 p.m.

On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz wrote:

...

You cannot create a normal function "fun". You can make a type class function

fun :: Class a b => GADT a -> b

...
data GADT a where GADT :: GADT () GADT2 :: GADT String

-- fun1 :: GADT () -> () -- infers type fun1 g = case g of (GADT :: GADT ()) -> ()

-- fun2 :: GADT String -> Bool -- infers type fun2 g = case g of (GADT2 :: GADT String) -> True

-- "fun" cannot type check. The type of 'g' cannot be both "GADT ()" and "GADT String" -- This is because "fun" is not a member of type class. {- fun g = case g of (GADT :: GADT ()) -> () (GADT2 :: GADT String) -> True -}

It may be that fun cannot type check, but surely it isn't for the reason you've given. data Rep a where Unit :: Rep () Int :: Rep Int zero :: Rep a -> a zero r = case r of Unit -> () Int -> 0 The type of r is "both" Rep () and Rep Int. No type class needed. If I had to guess, I'd say the original problem is that any specialization triggered by the functional dependency happens before the specialization triggered by pattern matching on the GADT. If I recall correctly, it is known that GADTs and fundeps don't always work nicely together. The example does seem to work if translated to use type families. type family Fam t :: * type instance Fam () = () data GADT a where GADT :: GADT () fun :: GADT a -> Fam a fun GADT = () -- Dave Menendez http://www.eyrie.org/~zednenem/

Jason Dagit

1:19 p.m.

On Tue, Sep 23, 2008 at 9:07 AM, Wolfgang Jeltsch wrote:

...

Hello,

please consider the following code:

...
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

data GADT a where

GADT :: GADT ()

class Class a b | a -> b

instance Class () ()

fun :: (Class a b) => GADT a -> b fun GADT = ()

I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message:

...
FDGADT.hs:12:11: Couldn't match expected type `b' against inferred type `()' `b' is a rigid type variable bound by the type signature for `fun' at FDGADT.hs:11:16 In the expression: () In the definition of `fun': fun GADT = ()

What's the reason for this? Is there a workaround? Does this work in 6.8.3 or 6.10.1?

There is one workaround that I can think of. Use a data type to get the level of polymorphism you need. You could create a data type to hold b and return that instead of the naked b. data Any where Any :: a -> Any Now you could say, fun :: GADT a -> Any If you go with this existential solution you'll probably want to add type class constraints to the 'a' in Any so that you can recover enough about the type to use the value later. Jason

Simon Peyton-Jones

24 Sep 24 Sep

11:49 a.m.

Wolfgang writes | > data GADT a where | > | > GADT :: GADT () | > | > class Class a b | a -> b | > | > instance Class () () | > | > fun :: (Class a b) => GADT a -> b | > fun GADT = () You're right that this program should typecheck. In the case branch we discover (locally) that a~(), and hence by the fundep, b~(), and away you go. This has never worked with fundeps, because it involves a *local* type equality (one that holds in some places and not others) and my implementation of fundeps is fundamentally based on *global* equality. Prior to GADTs that was fine! By adding local type equalities, GADTs change the game, and associated types/type families change it even more. (One reason that the game is different is that GHC has a typed intermediate language, so we need to maintain evidence of type equality throughout. In contrast, global equalities can be handled by straightforward unification, that makes the two types *identical*.) Our new implementation of type functions does, for the first time, a thorough principled job of handling arbitrary local type equalities. But that still leaves fundeps. Rather than try to fix fudeps directly (which would be a big job -- as I say, the current impl is fundamentally global) the best thing to do is to translate them into type equalities, thus: class (F a ~ b) => C a b type family F a (Note for 6.10 users: type equalities in superclasses is the piece we still have not implemented.) When you write an instance decl you add a type instance decl: instance C () () type F () = () Now everything should be good. Almost all fundep programs can be translated in this way. (Maybe all, I'm not 100% certain.) If you are doing this yourself, you can usually remove C's second parameter; but only if the fundep is unidirectional. So, as of now (6.10), the fundep stuff is still handled exactly as before, using global unification, so your program isn't going to work in 6.10 either. I'm frankly dubious about whether it's worth the effort of automatically performing the above translation from fundeps to type equalities; if you want this level of sophistication, you could just use type functions directly. It's not really a lack of backward compat. I think 6.10 will do all that 6.8 does; but if you want *more* you'll have to switch notation. Does that help clear things up, and explain why things are the way they are? Simon

Claus Reinke

12:48 p.m.

...

This has never worked with fundeps, because it involves a *local* type equality (one that holds in some places and not others) and my implementation of fundeps is fundamentally based on *global* equality. Prior to GADTs that was fine!

Thanks for the explanation, Simon - it clears up some outstanding FD issues.

...

Now everything should be good. Almost all fundep programs can be translated in this way. (Maybe all, I'm not 100% certain.) If you are doing this yourself, you can usually remove C's second parameter; but only if the fundep is unidirectional.

You can be 100% certain that not all FD programs can be translated to TF, if only because of interaction with overlapping instances. This is an area where Ghc differs from Hugs, doing different things for the "same" LANGUAGE extension, and it is difficult territory: Hugs' interpretation is safe, but too restricted in practice, Ghc's is a lot more flexible in practice, at the expense of not knowing whether it is safe in general, leaving those concerns to type class library implementers. I had hoped that Haskell' or Ghc would single out the actual use cases, and work towards principled solutions for these, whether for FD or for TF (eg, guards and closed instances might help).

...

So, as of now (6.10), the fundep stuff is still handled exactly as before, using global unification, so your program isn't going to work in 6.10 either. I'm frankly dubious about whether it's worth the effort of automatically performing the above translation from fundeps to type equalities; if you want this level of sophistication, you could just use type functions directly.

It's not really a lack of backward compat. I think 6.10 will do all that 6.8 does; but if you want *more* you'll have to switch notation. Does that help clear things up, and explain why things are the way they are?

Many of the issues that are going to be fixed for TF have been raised as bugs in the old implementation of FD. If FD are not going to see the same fixes, programs need to switch to TF, which isn't backwards or otherwise compatible (and may well deliver the final blow to the idea of more than one Haskell implementation?). Claus

Claus Reinke

2:26 p.m.

...

...
This has never worked with fundeps, because it involves a *local* type equality (one that holds in some places and not others) and my implementation of fundeps is fundamentally based on *global* equality. Prior to GADTs that was fine!

Actually, how does that relate to reasoning under assumptions? class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => .. f = .. There is no instance of 'FD', so no equalities can be derived from there outside of 'f', and no equalities should be derived globally from instances that are only local hypotheses in 'f' . But inside 'f', we assume that those two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of the implication. Isn't that decidedly local? Claus

Simon Peyton-Jones

26 Sep 26 Sep

12:08 p.m.

By "global" I really meant "throughout the scope of the type variable concerned. Nevertheless, the program you give is rejected, even though the scope is global: class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y Both GHC and Hugs erroneously reject the program, just as they do this one instance FD Int Bool g :: FD Int b => ... The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job. That is what we are fixing with type functions. I do not know how to fix it for FDs (except by way of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to. Simon | -----Original Message----- | From: Claus Reinke [mailto:claus.reinke@talk21.com] | Sent: 24 September 2008 19:27 | To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org | Subject: Re: GADTs and functional dependencies | | >> This has never worked with fundeps, because it involves a *local* type | equality (one that holds | >> in some places and not others) and my implementation of fundeps is | fundamentally based on | >> *global* equality. Prior to GADTs that was fine! | | Actually, how does that relate to reasoning under assumptions? | | class FD a b | a -> b | | f :: (FD t1 t2, FD t1 t3) => .. | f = .. | | There is no instance of 'FD', so no equalities can be derived from there | outside of 'f', and no equalities should be derived globally from instances | that are only local hypotheses in 'f' . But inside 'f', we assume that those | two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of | the implication. | | Isn't that decidedly local? | Claus | |

Claus Reinke

12:58 p.m.

...

By "global" I really meant "throughout the scope of the type variable concerned.

Nevertheless, the program you give is rejected, even though the scope is global:

class FD a b | a -> b

f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y

Both GHC and Hugs erroneously reject the program,

while both GHC and Hugs accept this variation: class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = undefined and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'. So they use the FD globally (when checking use of 'f'), but not locally (when checking the definition of 'f'). Is that interpretation correct, or is there another bug involved?

...

The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job.

Interesting. When the FD-via-CHR discussion started, I toyed with the idea of writing an instance inference engine based on CHR (since CHR happen to be a variant of CPN - Coloured Petri Nets -, I happened to have an implementation at hand;-). But once I noticed the difficulties of managing local constraint stores (and exchanging some, but not all inferred information with the global constraint store), I abandoned the idea. Ever since then I've been wondering how GHC handles that!-)

...

That is what we are fixing with type functions. I do not know how to fix it for FDs (except by way of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to.

Since FDs constrain the set of valid instances, I had been wondering whether one could apply the FD-based refinements/substitutions to the code obtained (just as they are applied to the class constraints) while keeping a typed intermediate language. Claus

Simon Peyton-Jones

29 Sep 29 Sep

7:59 a.m.

| while both GHC and Hugs accept this variation: | | class FD a b | a -> b | f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 | f x y = undefined | | and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'. | | So they use the FD globally (when checking use of 'f'), but not locally | (when checking the definition of 'f'). Is that interpretation correct, or is | there another bug involved? No, by "globally" I meant "throughout the scope of a type variable". I'm surprised GHC accepts the program you give, because it should unify two skolems. With a minor change it fails f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y As I say, GHC's implementation of FDs is flaky and inconsistent; and that is not just because I'm lazy but because it is hard to know just what to do, most especially in situations like this when there is no System F translation. That is why I've been working so hard on FC. Simon

Wolfgang Jeltsch

24 Sep 24 Sep

1 p.m.

Hello Simon, thank you for your extensive answer! I think, I’ll try to work around the fundep deficiencies and if that doesn’t work, switch to type families. But your answer raised further questions/comments:

...

class (F a ~ b) => C a b type family F a

(Note for 6.10 users: type equalities in superclasses is the piece we still have not implemented.)

Do you mean type equalities like the one in the example above? Didn’t this already work in 6.8.2?

...

Almost all fundep programs can be translated in this way. (Maybe all, I'm not 100% certain.)

Not all, I’m afraid. There was a mailing list discussion between us several months ago where we talked about this. The translation from fundeps to type families doesn’t work as soon as overlapping instances are involved. The type equality check from HList is an example for this. You told me that such a check can be implemented with type families as soon as we have closed TFs: type family TypeEq t1 t2 :: * where TypeEq t t = True TypeEq t1 t2 = False Greetings to Victoria! (from Cottbus) Wolfgang

6077

Age (days ago)

6083

Last active (days ago)

List overview

Download

15 comments

7 participants

participants (7)

Alfonso Acosta
Chris Kuklewicz
Claus Reinke
David Menendez
Jason Dagit
Simon Peyton-Jones
Wolfgang Jeltsch

GADTs and functional dependencies

tags

participants (7)