GADTs and functional dependencies

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
19 messages Options
Reply | Threaded
Open this post in threaded view
|

GADTs and functional dependencies

Wolfgang Jeltsch-2
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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Bugzilla from alfonso.acosta@gmail.com
On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
<[hidden email]> 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.
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Wolfgang Jeltsch-2
Am Dienstag, 23. September 2008 18:19 schrieben Sie:

> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
>
> <[hidden email]> 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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Bugzilla from alfonso.acosta@gmail.com
On Tue, Sep 23, 2008 at 6:36 PM, Wolfgang Jeltsch
<[hidden email]> 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 ()
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Jason Dagit-2
In reply to this post by Wolfgang Jeltsch-2
On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch
<[hidden email]> wrote:

> Am Dienstag, 23. September 2008 18:19 schrieben Sie:
>> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
>>
>> <[hidden email]> 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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Jason Dagit-2
In reply to this post by Wolfgang Jeltsch-2
On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch
<[hidden email]> wrote:

> Am Dienstag, 23. September 2008 18:19 schrieben Sie:
>> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
>>
>> <[hidden email]> 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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Jason Dagit-2
In reply to this post by Wolfgang Jeltsch-2
On Tue, Sep 23, 2008 at 9:07 AM, Wolfgang Jeltsch
<[hidden email]> 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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

haskell-2
In reply to this post by Jason Dagit-2
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 )
>


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

David Menendez-2
On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz
<[hidden email]> 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 <[hidden email]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Wolfgang Jeltsch-2
In reply to this post by Wolfgang Jeltsch-2
Am Dienstag, 23. September 2008 19:07 schrieben Sie:

> >> {-# 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?
>
> This similar code using type families compiles in 6.8.3 and 6.9:
>
> data GADT a where
>    GADT :: GADT ()
>
> type family F a
> type instance F () = ()
>
> fun :: GADT a -> F a
> fun GADT = ()

Exactly.  But this makes my code incompatible with GHC 6.6. :-(

I thought, someone said that with the new typing machinery in GHC 6.10, more
functional dependency programs are accepted because functional dependencies
are handled similarly to type families (or something like that).  Is this
true?  Since the type family version is okay, why shouldn’t the functional
dependency version be okay?

Best wishes,
Wolfgang
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Ian Lynagh
On Wed, Sep 24, 2008 at 12:55:29PM +0200, Wolfgang Jeltsch wrote:
>
> I thought, someone said that with the new typing machinery in GHC 6.10, more
> functional dependency programs are accepted because functional dependencies
> are handled similarly to type families (or something like that).  Is this
> true?  Since the type family version is okay, why shouldn’t the functional
> dependency version be okay?

In
    http://hackage.haskell.org/trac/ghc/ticket/345
Simon says:
    Ultimately, I think we can implement fundeps using type families,
    and then the fundep version will work too. Until then, it'll only
    work in type-family form.


Thanks
Ian

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Wolfgang Jeltsch-2
Am Mittwoch, 24. September 2008 15:11 schrieb Ian Lynagh:

> On Wed, Sep 24, 2008 at 12:55:29PM +0200, Wolfgang Jeltsch wrote:
> > I thought, someone said that with the new typing machinery in GHC 6.10,
> > more functional dependency programs are accepted because functional
> > dependencies are handled similarly to type families (or something like
> > that).  Is this true?  Since the type family version is okay, why
> > shouldn’t the functional dependency version be okay?
>
> In
>     http://hackage.haskell.org/trac/ghc/ticket/345
> Simon says:
>     Ultimately, I think we can implement fundeps using type families,
>     and then the fundep version will work too. Until then, it'll only
>     work in type-family form.
>
>
> Thanks
> Ian

And further:

> So, since we now have a good workaround (well, actually, a better way to
> write the program rather than a workaround), I'll leave it open, but at low
> priority and with milestone bottom.  

So for now the answer is: Use type families and thereby drop 6.6
compatibility?

Best wishes,
Wolfgang
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: GADTs and functional dependencies

Simon Peyton Jones
In reply to this post by Wolfgang Jeltsch-2
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


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Claus Reinke
> 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

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Wolfgang Jeltsch-2
In reply to this post by Simon Peyton Jones
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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Claus Reinke
In reply to this post by Claus Reinke
>> 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


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: GADTs and functional dependencies

Simon Peyton Jones
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:[hidden email]]
| Sent: 24 September 2008 19:27
| To: Simon Peyton-Jones; [hidden email]
| 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
|
|


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: GADTs and functional dependencies

Claus Reinke
> 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

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: GADTs and functional dependencies

Simon Peyton Jones
| 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

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users