Re: Fundeps and type equality

Iavor Diatchki

25 Dec 2012 25 Dec '12

9:47 p.m.

Hello Conal, GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class). As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC. Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet. On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

...

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Attachments:

attachment.html (text/html — 3.8 KB)

Show replies by date

Conal Elliott

26 Dec 26 Dec

1:23 p.m.

New subject: Fundeps and type equality

Hi Iavor, Thanks much for the explanation. Before this experiment with FDs, I was using a type family. I tried switching to FDs, because I wanted the compiler to know that the family is injective in order to assist type-checking. Can we declare type families to be injective? Now I see that I ran into a similar problem almost two years ago: http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html. I guess the answer is still "no", judging by this ticket: http://hackage.haskell.org/trac/ghc/ticket/6018 . -- Conal On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki wrote:

...

Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

...
I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Roman Cheplyaka

2:19 p.m.

New subject: Fundeps and type equality

I presume that injectivity of type families is the sole reason why data families exist. Roman * Conal Elliott [2012-12-26 10:23:46-0800]

...

Hi Iavor,

Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried switching to FDs, because I wanted the compiler to know that the family is injective in order to assist type-checking. Can we declare type families to be injective? Now I see that I ran into a similar problem almost two years ago: http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html. I guess the answer is still "no", judging by this ticket: http://hackage.haskell.org/trac/ghc/ticket/6018 .

-- Conal

On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki wrote:

...
Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

...
I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

...

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Brent Yorgey

2:49 p.m.

New subject: Fundeps and type equality

I don't think that's true (though a few minutes of searching has not yet turned up anything describing the original motivation for data families). Sometimes you really do want to construct a family of new data types, instead of just mapping to existing ones. I think everyone agrees that using data families as a stand-in for injective type families is a kludgy hack. -Brent On Wed, Dec 26, 2012 at 09:19:56PM +0200, Roman Cheplyaka wrote:

...

I presume that injectivity of type families is the sole reason why data families exist.

Roman

* Conal Elliott [2012-12-26 10:23:46-0800]

...
Hi Iavor,

Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried switching to FDs, because I wanted the compiler to know that the family is injective in order to assist type-checking. Can we declare type families to be injective? Now I see that I ran into a similar problem almost two years ago: http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html. I guess the answer is still "no", judging by this ticket: http://hackage.haskell.org/trac/ghc/ticket/6018 .

-- Conal

On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki wrote:

...
Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

...
I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

...
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Roman Cheplyaka

3:13 p.m.

New subject: Fundeps and type equality

* Brent Yorgey [2012-12-26 14:49:16-0500]

...

I don't think that's true (though a few minutes of searching has not yet turned up anything describing the original motivation for data families). Sometimes you really do want to construct a family of new data types, instead of just mapping to existing ones.

Right, sorry. Now that you made me think about it, I realised that they are also needed for partial application.

...

I think everyone agrees that using data families as a stand-in for injective type families is a kludgy hack.

Sure. Roman

...

On Wed, Dec 26, 2012 at 09:19:56PM +0200, Roman Cheplyaka wrote:

...
I presume that injectivity of type families is the sole reason why data families exist.

Roman

* Conal Elliott [2012-12-26 10:23:46-0800]

...
Hi Iavor,

Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried switching to FDs, because I wanted the compiler to know that the family is injective in order to assist type-checking. Can we declare type families to be injective? Now I see that I ran into a similar problem almost two years ago: http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html. I guess the answer is still "no", judging by this ticket: http://hackage.haskell.org/trac/ghc/ticket/6018 .

-- Conal

On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki wrote:

...
Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

...
I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

...
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Simon Peyton-Jones

2 Jan 2 Jan

4:04 a.m.

New subject: Fundeps and type equality

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). Iavor is quite right It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions The main issues are, I think: · How to express functional dependencies like “fixing the result type and the first argument will fix the second argument” · How to express that idea in the proof language Simon From: glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-bugs@haskell.org; GHC Users Mailing List Subject: Re: Fundeps and type equality Hello Conal, GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class). As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC. Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet. On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott mailto:conal@conal.net> wrote: I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...

class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

Martin Sulzmann

4:01 p.m.

New subject: Fundeps and type equality

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end) Similar to FC, coercions (proof terms) are used to represent type equations (improvement). Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small). It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ... -Martin On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones wrote:

...

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ****

** **

Iavor is quite right****

** **

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ****

** **

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions****

** **

The main issues are, I think:****

**· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”****

**· **How to express that idea in the proof language****

** **

Simon****

** **

*From:* glasgow-haskell-bugs-bounces@haskell.org [mailto: glasgow-haskell-bugs-bounces@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-bugs@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality****

** **

Hello Conal,****

** **

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).****

** **

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.****

** **

Cheers,****

-Iavor****

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.****

** **

** **

** **

** **

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:*** *

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.****

Any insights about what's going wrong here?****

-- Conal****

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs****

** **

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Richard Eisenberg

10 Jan 10 Jan

1:56 p.m.

New subject: Fundeps and type equality

For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.) So, as yet, we can't fully encode functional dependencies with type families, I don't think. Richard On Jan 2, 2013, at 4:01 PM, Martin Sulzmann wrote:

...

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones wrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC).

Iavor is quite right

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is.

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

The main issues are, I think:

· How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”

· How to express that idea in the proof language

Simon

From: glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-bugs@haskell.org; GHC Users Mailing List Subject: Re: Fundeps and type equality

Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers,

-Iavor

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Carter Schonwald

3:14 p.m.

New subject: Fundeps and type equality

so the overlapping type families are in HEAD? Awesome! I look forward to finding some time to try them out :) On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg wrote:

...

For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann < martin.sulzmann.haskell@googlemail.com> wrote:

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones
...
wrote:

...
As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ****

** **

Iavor is quite right****

** **

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ****

** **

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions****

** **

The main issues are, I think:****

**· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”****

**· **How to express that idea in the proof language****

** **

Simon****

** **

*From:* glasgow-haskell-bugs-bounces@haskell.org [mailto: glasgow-haskell-bugs-bounces@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-bugs@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality****

** **

Hello Conal,****

** **

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).****

** **

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.****

** **

Cheers,****

-Iavor****

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.****

** **

** **

** **

** **

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:** **

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.****

Any insights about what's going wrong here?****

-- Conal****

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs****

** **

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Richard Eisenberg

10:03 p.m.

New subject: Fundeps and type equality

Yes, I finished and pushed in December. A description of the design and how to use the feature is here: http://hackage.haskell.org/trac/ghc/wiki/NewAxioms There's also a section (7.7.2.2 to be exact) in the manual, but building the manual from source is not for the faint of heart. Richard On Jan 10, 2013, at 3:14 PM, Carter Schonwald wrote:

...

so the overlapping type families are in HEAD?

Awesome! I look forward to finding some time to try them out :)

On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg wrote: For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann wrote:

...
I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones wrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC).

Iavor is quite right

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is.

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

The main issues are, I think:

· How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”

· How to express that idea in the proof language

Simon

From: glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-bugs@haskell.org; GHC Users Mailing List Subject: Re: Fundeps and type equality

Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers,

-Iavor

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Simon Peyton-Jones

11 Jan 11 Jan

4:56 a.m.

New subject: Fundeps and type equality

The manual for HEAD is always online here http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-families.... Simon From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 11 January 2013 03:03 To: Carter Schonwald Cc: Martin Sulzmann; glasgow-haskell-bugs@haskell.org; Simon Peyton-Jones; GHC Users Mailing List Subject: Re: Fundeps and type equality Yes, I finished and pushed in December. A description of the design and how to use the feature is here: http://hackage.haskell.org/trac/ghc/wiki/NewAxioms There's also a section (7.7.2.2 to be exact) in the manual, but building the manual from source is not for the faint of heart. Richard On Jan 10, 2013, at 3:14 PM, Carter Schonwald mailto:carter.schonwald@gmail.com> wrote: so the overlapping type families are in HEAD? Awesome! I look forward to finding some time to try them out :) On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg mailto:eir@cis.upenn.edu> wrote: For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.) So, as yet, we can't fully encode functional dependencies with type families, I don't think. Richard On Jan 2, 2013, at 4:01 PM, Martin Sulzmann mailto:martin.sulzmann.haskell@googlemail.com> wrote: I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end) Similar to FC, coercions (proof terms) are used to represent type equations (improvement). Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small). It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ... -Martin On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones mailto:simonpj@microsoft.com> wrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). Iavor is quite right It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. Iavor: I don't think it's straightforward, but I'm willing to be educated. By all means start a wiki page to explain how, if you think it is. I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions The main issues are, I think: * How to express functional dependencies like "fixing the result type and the first argument will fix the second argument" * How to express that idea in the proof language Simon From: glasgow-haskell-bugs-bounces@haskell.orgmailto:glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.orgmailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-bugs@haskell.orgmailto:glasgow-haskell-bugs@haskell.org; GHC Users Mailing List Subject: Re: Fundeps and type equality Hello Conal, GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class). As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC. Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet. On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott mailto:conal@conal.net> wrote: I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...

class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none. Any insights about what's going wrong here? -- Conal _______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.orgmailto:Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Richard Eisenberg

9:42 a.m.

New subject: Fundeps and type equality

That link looks like it points to the manual for the most recent distribution, not HEAD. The edits I put into the manual for the new family instances are not there, for example. Richard On Jan 11, 2013, at 4:56 AM, Simon Peyton-Jones wrote:

...

The manual for HEAD is always online here http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-families....

Simon

From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 11 January 2013 03:03 To: Carter Schonwald Cc: Martin Sulzmann; glasgow-haskell-bugs@haskell.org; Simon Peyton-Jones; GHC Users Mailing List Subject: Re: Fundeps and type equality

Yes, I finished and pushed in December. A description of the design and how to use the feature is here: http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

There's also a section (7.7.2.2 to be exact) in the manual, but building the manual from source is not for the faint of heart.

Richard

On Jan 10, 2013, at 3:14 PM, Carter Schonwald wrote:

so the overlapping type families are in HEAD?

Awesome! I look forward to finding some time to try them out :)

On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg wrote: For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann wrote:

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones wrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC).

Iavor is quite right

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is.

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked fromhttp://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

The main issues are, I think: · How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”

· How to express that idea in the proof language

Simon

From: glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-bugs@haskell.org; GHC Users Mailing List Subject: Re: Fundeps and type equality

Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote: I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Carter Schonwald

3:52 p.m.

New subject: Fundeps and type equality

One thing thats unclear (or at least implicit) about the overlapping type families from the docs is this: does it let me write recursive type level functions? (I really really really want that :) ) thanks -Carter On Thu, Jan 10, 2013 at 10:03 PM, Richard Eisenberg wrote:

...

Yes, I finished and pushed in December. A description of the design and how to use the feature is here: http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

There's also a section (7.7.2.2 to be exact) in the manual, but building the manual from source is not for the faint of heart.

Richard

On Jan 10, 2013, at 3:14 PM, Carter Schonwald wrote:

so the overlapping type families are in HEAD?

Awesome! I look forward to finding some time to try them out :)

On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg wrote:

...
For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann < martin.sulzmann.haskell@googlemail.com> wrote:

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones < simonpj@microsoft.com> wrote:

...
As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ****

** **

Iavor is quite right****

** **

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ****

** **

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions****

** **

The main issues are, I think:****

**· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”****

**· **How to express that idea in the proof language****

** **

Simon****

** **

*From:* glasgow-haskell-bugs-bounces@haskell.org [mailto: glasgow-haskell-bugs-bounces@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-bugs@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality****

** **

Hello Conal,****

** **

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).****

** **

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.****

** **

Cheers,****

-Iavor****

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.****

** **

** **

** **

** **

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:* ***

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.****

Any insights about what's going wrong here?****

-- Conal****

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs****

** **

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Richard Eisenberg

4:04 p.m.

New subject: Fundeps and type equality

Recursive type level functions are actually not new -- type families as they have existed for some time can be recursive. The new overlap mechanism doesn't really interact with the recursion feature in any interesting way. For anything moderately interesting and recursive, though, you will have to enable UndecidableInstances, but the only potential harm that extension can cause is for GHC to hang; your program will still be guaranteed not to crash if it compiles. Enjoy hacking with types! Richard On Jan 11, 2013, at 3:52 PM, Carter Schonwald wrote:

...

One thing thats unclear (or at least implicit) about the overlapping type families from the docs is this: does it let me write recursive type level functions? (I really really really want that :) )

thanks -Carter

On Thu, Jan 10, 2013 at 10:03 PM, Richard Eisenberg wrote: Yes, I finished and pushed in December. A description of the design and how to use the feature is here: http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

There's also a section (7.7.2.2 to be exact) in the manual, but building the manual from source is not for the faint of heart.

Richard

On Jan 10, 2013, at 3:14 PM, Carter Schonwald wrote:

...
so the overlapping type families are in HEAD?

Awesome! I look forward to finding some time to try them out :)

On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg wrote: For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann wrote:

...
I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones wrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC).

Iavor is quite right

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is.

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

The main issues are, I think:

· How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”

· How to express that idea in the proof language

Simon

From: glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-bugs@haskell.org; GHC Users Mailing List Subject: Re: Fundeps and type equality

Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers,

-Iavor

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Carter Schonwald

4:36 p.m.

New subject: Fundeps and type equality

Cool! For some reason I had thought that wasn't previously allowed, thanks for clarifying! That said, the new overlapping type families should make things a bit easier to write. awesome -Carter On Fri, Jan 11, 2013 at 4:04 PM, Richard Eisenberg wrote:

...

Recursive type level functions are actually not new -- type families as they have existed for some time can be recursive. The new overlap mechanism doesn't really interact with the recursion feature in any interesting way. For anything moderately interesting and recursive, though, you will have to enable UndecidableInstances, but the only potential harm that extension can cause is for GHC to hang; your program will still be guaranteed not to crash if it compiles.

Enjoy hacking with types! Richard

On Jan 11, 2013, at 3:52 PM, Carter Schonwald wrote:

One thing thats unclear (or at least implicit) about the overlapping type families from the docs is this: does it let me write recursive type level functions? (I really really really want that :) )

thanks -Carter

On Thu, Jan 10, 2013 at 10:03 PM, Richard Eisenberg wrote:

...
Yes, I finished and pushed in December. A description of the design and how to use the feature is here: http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

There's also a section (7.7.2.2 to be exact) in the manual, but building the manual from source is not for the faint of heart.

Richard

On Jan 10, 2013, at 3:14 PM, Carter Schonwald wrote:

so the overlapping type families are in HEAD?

Awesome! I look forward to finding some time to try them out :)

On Thu, Jan 10, 2013 at 1:56 PM, Richard Eisenberg wrote:

...
For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann < martin.sulzmann.haskell@googlemail.com> wrote:

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones < simonpj@microsoft.com> wrote:

...
As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ****

** **

Iavor is quite right****

** **

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ****

** **

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions****

** **

The main issues are, I think:****

**· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”****

**· **How to express that idea in the proof language****

** **

Simon****

** **

*From:* glasgow-haskell-bugs-bounces@haskell.org [mailto: glasgow-haskell-bugs-bounces@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-bugs@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality****

** **

Hello Conal,****

** **

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).****

** **

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.****

** **

Cheers,****

-Iavor****

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.****

** **

** **

** **

** **

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote: ****

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.****

Any insights about what's going wrong here?****

-- Conal****

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs****

** **

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Tyson Whitehead

10 Jan 10 Jan

5:12 p.m.

New subject: Class instance specificity order (was Re: Fundeps and type equality)

On January 10, 2013 13:56:02 Richard Eisenberg wrote:

...

Class instances that overlap are chosen among by order of specificity;

Sorry to jump in the middle here, but this caught my attention as this sort of specificity determination is exactly what I had in mind when I was working on my "The shape of things: a reason for type preference" paper. I would love to know what approach GHC is currently taking to determine this. The document gives the example of matching C Int [Int] against C Int a C a Bool C Int [a] C Int [Int] This is easy though. Obviously the last match is best because it is exact. What if we have something like C Int [[Int]] against C Int b C a [[b]] though. How is the best match determined in this case? Thanks! -Tyson

Simon Peyton-Jones

5:17 p.m.

New subject: Class instance specificity order (was Re: Fundeps and type equality)

Is http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension... insufficiently clear? If so, let's clarify it. Simon | -----Original Message----- | From: Tyson Whitehead [mailto:twhitehead@gmail.com] | Sent: 10 January 2013 22:12 | To: glasgow-haskell-users@haskell.org | Cc: Richard Eisenberg; Martin Sulzmann; Simon Peyton-Jones | Subject: Class instance specificity order (was Re: Fundeps and type equality) | | On January 10, 2013 13:56:02 Richard Eisenberg wrote: | > Class instances that overlap are chosen among by order of specificity; | | Sorry to jump in the middle here, but this caught my attention as this sort of | specificity determination is exactly what I had in mind when I was working on | my "The shape of things: a reason for type preference" paper. | | I would love to know what approach GHC is currently taking to determine this. | The document gives the example of matching C Int [Int] against | | C Int a | C a Bool | C Int [a] | C Int [Int] | | This is easy though. Obviously the last match is best because it is exact. | What if we have something like C Int [[Int]] against | | C Int b | C a [[b]] | | though. How is the best match determined in this case? | | Thanks! -Tyson

Tyson Whitehead

8:51 p.m.

New subject: Class instance specificity order (was Re: Fundeps and type equality)

On Thu, 2013-01-10 at 22:17 +0000, Simon Peyton-Jones wrote:

...

Is http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension... insufficiently clear? If so, let's clarify it.

Thanks for getting back to me Simon. The document says "For example, consider these declarations: instance context1 => C Int a where ... -- (A) instance context2 => C a Bool where ... -- (B) instance context3 => C Int [a] where ... -- (C) instance context4 => C Int [Int] where ... -- (D) ... The -XOverlappingInstances flag instructs GHC to allow more than one instance to match, provided there is a most specific one. For example, the constraint C Int [Int] matches instances (A), (C) and (D), but the last is more specific, and hence is chosen. If there is no most-specific match, the program is rejected." What it doesn't says is how "most-specific match" is computed. While it is pretty clear in the given example (one matches exactly), not all cases are so clear. For example, which of instance context1 => C Int b instance context2 => C a [[b]] does C Int [[Int]] match best against? If there isn't currently a good way to resolve this, I would like to suggest the type-shape measure I proposed in that paper I wrote up awhile back could be used. Thanks! -Tyson

Simon Peyton-Jones

11 Jan 11 Jan

1:55 p.m.

New subject: Class instance specificity order (was Re: Fundeps and type equality)

| The -XOverlappingInstances flag instructs GHC to allow more than one | instance to match, provided there is a most specific one. For example, | the constraint C Int [Int] matches instances (A), (C) and (D), but the | last is more specific, and hence is chosen. If there is no most-specific | match, the program is rejected." | What it doesn't says is how "most-specific match" is computed. An instance declaration (A) is "more specific" than another (B) iff the head of (A) is a substitution instance of (B). For example (A) instance context1 => C [Maybe a] (B) instance context2 => C [b] Here (A) is more specific than (B) because we can get (A) from (B) by substituting b:=Maybe a. Does that make it clear? If so I will add it to the manual. | not cases are so clear. For example, which of | | instance context1 => C Int b | instance context2 => C a [[b]] | | does C Int [[Int]] match best against? Neither is instance is more specific than the other, so C Int [[Int]] is rejected. | If there isn't currently a good | way to resolve this, I would like to suggest the type-shape measure I | proposed in that paper I wrote up awhile back could be used. I think the current design is reasonable, and I don't want to complicate it unless there is a very compelling reason to do so. Simon

Tyson Whitehead

4:07 p.m.

New subject: Class instance specificity order (was Re: Fundeps and type equality)

On January 11, 2013 13:55:58 Simon Peyton-Jones wrote:

...

| The -XOverlappingInstances flag instructs GHC to allow more than one | instance to match, provided there is a most specific one. For example, | the constraint C Int [Int] matches instances (A), (C) and (D), but the | last is more specific, and hence is chosen. If there is no most-specific | match, the program is rejected." | | What it doesn't says is how "most-specific match" is computed.

An instance declaration (A) is "more specific" than another (B) iff the head of (A) is a substitution instance of (B). For example

(A) instance context1 => C [Maybe a] (B) instance context2 => C [b]

Here (A) is more specific than (B) because we can get (A) from (B) by substituting b:=Maybe a.

Does that make it clear? If so I will add it to the manual.

Thanks Simon. That is exactly what I was looking for. It is clear now.

...

| not cases are so clear. For example, which of | | instance context1 => C Int b | instance context2 => C a [[b]] | | does C Int [[Int]] match best against?

Neither is instance is more specific than the other, so C Int [[Int]] is rejected.

This was what I was wondering.

...

| If there isn't currently a good | way to resolve this, I would like to suggest the type-shape measure I | proposed in that paper I wrote up awhile back could be used.

I think the current design is reasonable, and I don't want to complicate it unless there is a very compelling reason to do so.

Applying the type-shape measure to resolve this boils the problem down to what unification requires C Int b --(b = [[Int]])--> C Int [[Int]] C a [[b]] --(a = Int, b = Int)--> C Int [[Int]] The assignments required for the first (b = [] ([] Int)) involve three terms. The assignments required for the second (a = Int and b = Int) involve two terms. This means the second wins out as being the simplest. It's easy to compute, and I believe it completely subsumes GHCs current definition of more specific. The fact that we can get (A) from (B) by doing substitutions on (B) implies that something that unifies against both (A) and (B) will involve more terms in the substitutions done in unifying against (B). The complexity of the paper was in the derivation of the measure. The implication of the results is really really simple. Just count terms. Cheers! -Tyson

Martin Sulzmann

2:24 a.m.

New subject: Fundeps and type equality

Thanks, indeed you're right. For better or worse, so let's extend FC to include FD-style improvement :) Aren't we running then into the same 'type soundness' issues (connected to ordering of overlapping instances) you mention below? There's currently no issue for FDs because FD-style improvement is not manifested in GHC's internal language FC. So, if FD-style improvement will be treated similarly compared to type families, then we might have to rethink the entire case of overlapping type class instances? -Martin On Thu, Jan 10, 2013 at 7:56 PM, Richard Eisenberg wrote:

...

For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.)

So, as yet, we can't fully encode functional dependencies with type families, I don't think.

Richard

On Jan 2, 2013, at 4:01 PM, Martin Sulzmann < martin.sulzmann.haskell@googlemail.com> wrote:

I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: "Extracting programs from type class proofs" (type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations (improvement).

Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small).

It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones
...
wrote:

...
As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ****

** **

Iavor is quite right****

** **

It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ****

** **

I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions****

** **

The main issues are, I think:****

**· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”****

**· **How to express that idea in the proof language****

** **

Simon****

** **

*From:* glasgow-haskell-bugs-bounces@haskell.org [mailto: glasgow-haskell-bugs-bounces@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-bugs@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality****

** **

Hello Conal,****

** **

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).****

** **

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.****

** **

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.****

** **

Cheers,****

-Iavor****

PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.****

** **

** **

** **

** **

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:** **

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...
class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.****

Any insights about what's going wrong here?****

-- Conal****

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs****

** **

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

4512

Age (days ago)

4528

Last active (days ago)

List overview

Download

20 comments

9 participants

participants (9)

Brent Yorgey
Carter Schonwald
Conal Elliott
Iavor Diatchki
Martin Sulzmann
Richard Eisenberg
Roman Cheplyaka
Simon Peyton-Jones
Tyson Whitehead