RE: 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.html#type-instance-declarations Simon From: Richard Eisenberg [mailto:e...@cis.upenn.edu] Sent: 11 January 2013 03:03 To: Carter Schonwald Cc: Martin Sulzmann; glasgow-haskell-b...@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 carter.schonw...@gmail.commailto:carter.schonw...@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 e...@cis.upenn.edumailto:e...@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 martin.sulzmann.hask...@googlemail.commailto:martin.sulzmann.hask...@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 simo...@microsoft.commailto:simo...@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-boun...@haskell.orgmailto:glasgow-haskell-bugs-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@haskell.orgmailto:glasgow-haskell-bugs-boun...@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-b...@haskell.orgmailto:glasgow-haskell-b...@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
Re: 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 simo...@microsoft.com wrote: The manual for HEAD is always online here http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-families.html#type-instance-declarations Simon From: Richard Eisenberg [mailto:e...@cis.upenn.edu] Sent: 11 January 2013 03:03 To: Carter Schonwald Cc: Martin Sulzmann; glasgow-haskell-b...@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 carter.schonw...@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 e...@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 martin.sulzmann.hask...@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 simo...@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 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-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-b...@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
RE: 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: 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 e...@cis.upenn.eduwrote: 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 carter.schonw...@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 e...@cis.upenn.eduwrote: 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.hask...@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 simo...@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-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@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
Re: 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 e...@cis.upenn.edu 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 carter.schonw...@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 e...@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 martin.sulzmann.hask...@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 simo...@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-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-b...@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
Re: 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: 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 e...@cis.upenn.eduwrote: 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 e...@cis.upenn.eduwrote: 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 carter.schonw...@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 e...@cis.upenn.eduwrote: 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.hask...@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 simo...@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-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality ** ** Hello Conal, ** ** GHC implementation of functional
Re: 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 martin.sulzmann.hask...@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 simo...@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-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-b...@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 co...@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
Re: 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 e...@cis.upenn.eduwrote: 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.hask...@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 simo...@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-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@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 co...@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
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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Class instance specificity order (was Re: Fundeps and type equality)
Is http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap insufficiently clear? If so, let's clarify it. Simon | -Original Message- | From: Tyson Whitehead [mailto:twhiteh...@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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Class instance specificity order (was Re: Fundeps and type equality)
On Thu, 2013-01-10 at 22:17 +, Simon Peyton-Jones wrote: Is http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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 carter.schonw...@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 e...@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 martin.sulzmann.hask...@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 simo...@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-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-b...@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
Re: 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 e...@cis.upenn.eduwrote: 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.hask...@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 simo...@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-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@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
RE: 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-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@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 co...@conal.netmailto:co...@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-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
RE: 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-boun...@haskell.org [mailto:glasgow-haskell-bugs-boun...@haskell.org] On Behalf Of Iavor Diatchki Sent: 26 December 2012 02:48 To: Conal Elliott Cc: glasgow-haskell-b...@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 co...@conal.netmailto:co...@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-b...@haskell.orgmailto:glasgow-haskell-b...@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
Re: 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 simo...@microsoft.comwrote: 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-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@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 co...@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
Re: 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 iavor.diatc...@gmail.comwrote: 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 co...@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.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: 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 iavor.diatc...@gmail.comwrote: 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 co...@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-b...@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
Re: Fundeps and type equality
I presume that injectivity of type families is the sole reason why data families exist. Roman * Conal Elliott co...@conal.net [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 iavor.diatc...@gmail.comwrote: 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 co...@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-b...@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
Re: 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 co...@conal.net [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 iavor.diatc...@gmail.comwrote: 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 co...@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-b...@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
Re: Fundeps and type equality
* Brent Yorgey byor...@seas.upenn.edu [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 co...@conal.net [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 iavor.diatc...@gmail.comwrote: 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 co...@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-b...@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
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 co...@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.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
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 co...@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-b...@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
RE: fundeps help
| And here we know that y=Bool; yet since we don't write the type sig | directly we can't say it. So GHC's implementation of fundeps rejects | this program; again it can't be translated into System F. | | Conveniently, this is a good example of my other problem with fundeps :-) | I can work around the problem from my first email with an unsafeCoerce, | but is there any way I can get around the issue above at the moment in | either 6.8 or the HEAD? I actually plan to recast the code in question | using associated type synomyms once they're working properly, but would | like to be able to make some progress now. I think that if you use the HEAD, much of this will work, if you use the type-equality notation. But you will probably encounter bugs too. And in so doing, and reporting them, you'll be doing us a service. Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: fundeps help
I think that if you use the HEAD, much of this will work, if you use the type-equality notation. But you will probably encounter bugs too. And in so doing, and reporting them, you'll be doing us a service. I did originally intend to try all this with the HEAD, but one obstacle to this is the lack of recent linux binaries in http://www.haskell.org/ghc/dist/current/dist/ I tried building it myself, but something or another failed, and in general I think keeping up by that route would be a rather high overhead process. Cheers, Ganesh == Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html == ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: fundeps help
| I did originally intend to try all this with the | HEAD, but one obstacle to this is the lack of recent linux | binaries in http://www.haskell.org/ghc/dist/current/dist/ Ian is fixing that. We'd missed the fact that the bindists weren't being built. Hold on a day or two. Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: fundeps help
| I'm trying to understand what fundeps do and don't let me do. One
| particular source of confusion is why the following program doesn't
| typecheck:
|
| {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
| module Fundeps where
|
| class Dep a b | a - b, b - a
|
| conv :: (Dep a b1,Dep a b2) = b1 - b2
| conv = id
| {- end of program -}
GHC implements improvement by *identifying* the two equal types. Here they
cannot be identified because they are separate type variables. A good way to
think of this is to imagine translating the program into System F: you can't do
it. Functional dependencies guide type inference by adding extra unifications,
resolving types that would otherwise be under-constrained and ambiguous -- but
fundeps (or at least GHC's implementation thereof) does not deal with the case
where the types become *over*-constrained.
GHC's new intermediate language, System FC, is specifically designed to do
this. Currently we're in transition: equality constraints are starting to
work, but fundeps are implemented as they always were. I hope we can
eventually switch over to implementing fundeps using equality constraints, and
then the above program will work.
Meanwhile, in the HEAD you can write
conv :: (a~b) = a - b
conv = id
Which, IHMO, is a much clearer way to say it!
You may also like to try the paper that Martin and I and others wrote about
fundeps:
http://research.microsoft.com/%7Esimonpj/papers/fd-chr
Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: fundeps help
On Dec 3, 2007, at 4:02 AM, Simon Peyton-Jones wrote: GHC's new intermediate language, System FC, is specifically designed to do this. Currently we're in transition: equality constraints are starting to work, but fundeps are implemented as they always were. I hope we can eventually switch over to implementing fundeps using equality constraints, and then the above program will work. Meanwhile, in the HEAD you can write conv :: (a~b) = a - b conv = id Which, IHMO, is a much clearer way to say it! Is it really a good idea to permit a type signature to include equality constraints among unifiable types? Does the above type signature mean something different from a -a? Does the type signature: foo :: (a~Bar b) = a - Bar b mean something different from: foo :: Bar b - Bar b ? I know that System FC is designed to let us write stuff like: foo :: (Bar a ~ Baz b) = Bar a - Baz b Which is of course what we need for relating type functions. But I'm wondering if there's a subtlety of using an equality constraint vs just substitution that I've missed---and if not why there are so many ways of writing the same type, many of them arguably unreadable! Hoping this will give me a bit of insight into SystemFC, -Jan-Willem Maessen You may also like to try the paper that Martin and I and others wrote about fundeps: http://research.microsoft.com/%7Esimonpj/papers/fd-chr Simon ___ 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
RE: fundeps help
| Is it really a good idea to permit a type signature to include | equality constraints among unifiable types? Does the above type | signature mean something different from a -a? Does the type signature: | foo :: (a~Bar b) = a - Bar b | mean something different from: | foo :: Bar b - Bar b | ? I know that System FC is designed to let us write stuff like: | foo :: (Bar a ~ Baz b) = Bar a - Baz b | Which is of course what we need for relating type functions. But I'm | wondering if there's a subtlety of using an equality constraint vs | just substitution that I've missed No, you didn't miss anything. I wouldn't expect anyone to write these types directly. But it can happen: class C a b | a-b instance C Int Bool class D x where op :: forall y. C x y = x - y instance D Int where op = ... In the (D Int) instance, what's the type of op? Well, it must be op :: forall y. C Int y = Int - y And here we know that y=Bool; yet since we don't write the type sig directly we can't say it. So GHC's implementation of fundeps rejects this program; again it can't be translated into System F. Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: fundeps help
On Mon, 3 Dec 2007, Simon Peyton-Jones wrote: No, you didn't miss anything. I wouldn't expect anyone to write these types directly. But it can happen: class C a b | a-b instance C Int Bool class D x where op :: forall y. C x y = x - y instance D Int where op = ... In the (D Int) instance, what's the type of op? Well, it must be op :: forall y. C Int y = Int - y And here we know that y=Bool; yet since we don't write the type sig directly we can't say it. So GHC's implementation of fundeps rejects this program; again it can't be translated into System F. Conveniently, this is a good example of my other problem with fundeps :-) I can work around the problem from my first email with an unsafeCoerce, but is there any way I can get around the issue above at the moment in either 6.8 or the HEAD? I actually plan to recast the code in question using associated type synomyms once they're working properly, but would like to be able to make some progress now. Cheers, Ganesh ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: fundeps help
Jan-Willem Maessen: Is it really a good idea to permit a type signature to include equality constraints among unifiable types? Does the above type signature mean something different from a -a? Does the type signature: foo :: (a~Bar b) = a - Bar b mean something different from: foo :: Bar b - Bar b ? I know that System FC is designed to let us write stuff like: foo :: (Bar a ~ Baz b) = Bar a - Baz b Which is of course what we need for relating type functions. But I'm wondering if there's a subtlety of using an equality constraint vs just substitution that I've missed---and if not why there are so many ways of writing the same type, many of them arguably unreadable! Simon answered most of your question, but let me make a remark regarding why there are so many ways of writing the same type, many of them arguably unreadable! Equalities of the form a ~ someType are essentially a form of let-bindings for types - you can give a type a name and then use the name in place of the type. Just like with value-level let bindings, you can abuse the notation and write unreadable terms. However, this is no reason to remove let-bindings from the value level, so why should it be different at the type level? Manuel ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] Re: Fundeps: I feel dumb
On 13 Apr 2006 03:27:03 -, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: Creighton Hogg wrote: No instance for (MatrixProduct a (Vec b) c) arising from use of `*' at interactive:1:3-5 Probable fix: add an instance declaration for (MatrixProduct a (Vec b) c) In the definition of `it': it = 10 * (vector 10 ([0 .. 9])) Let us look at the instance class MatrixProduct a b c | a b - c where (*) :: a - b - c instance (Num a) = MatrixProduct a (Vec a) (Vec a) where it defines what happens when multiplying a vector of some numeric type 'a' by a value _of the same_ type. Let us now look at the error message: (MatrixProduct a (Vec b) c) That is, when trying to compile your expression 10 * (vector 10 ([0 .. 9])) the typechecker went looking for (MatrixProduct a (Vec b) c) where the value and the vector have different numeric types. There is no instance for such a general case, hence the error. It is important to remember that the typechecker first infers the most general type for an expression, and then tries to resolve the constraints. In your expression, 10 * (vector 10 ([0 .. 9])) we see constants 10, 10, 0, 9. Each constant has the type Num a = a. Within the expression 0 .. 9, both 0 and 9 must be of the same type (because [n .. m] is an abbreviation for enumFromThen n m, and according to the type of the latter enumFromThen :: a - a - [a] both arguments must be of the same type). But there is nothing that says that the first occurrence of 10 must be of the same numeric type as the occurrence of 9. So, the most general type assignment will be (Num a = a) for 10, and (Num b = b) for 9. Thank you very much for the explanation: it makes alot of sense. So, if one does not want to for alot of type declarations into the code, which would be fairly awkward, is there a way to do this with fundeps or other type extensions that will be alot prettier or is any way of defining type classes going to run into the same problems? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Fundeps: I feel dumb
Creighton Hogg wrote: No instance for (MatrixProduct a (Vec b) c) arising from use of `*' at interactive:1:3-5 Probable fix: add an instance declaration for (MatrixProduct a (Vec b) c) In the definition of `it': it = 10 * (vector 10 ([0 .. 9])) Let us look at the instance class MatrixProduct a b c | a b - c where (*) :: a - b - c instance (Num a) = MatrixProduct a (Vec a) (Vec a) where it defines what happens when multiplying a vector of some numeric type 'a' by a value _of the same_ type. Let us now look at the error message: (MatrixProduct a (Vec b) c) That is, when trying to compile your expression 10 * (vector 10 ([0 .. 9])) the typechecker went looking for (MatrixProduct a (Vec b) c) where the value and the vector have different numeric types. There is no instance for such a general case, hence the error. It is important to remember that the typechecker first infers the most general type for an expression, and then tries to resolve the constraints. In your expression, 10 * (vector 10 ([0 .. 9])) we see constants 10, 10, 0, 9. Each constant has the type Num a = a. Within the expression 0 .. 9, both 0 and 9 must be of the same type (because [n .. m] is an abbreviation for enumFromThen n m, and according to the type of the latter enumFromThen :: a - a - [a] both arguments must be of the same type). But there is nothing that says that the first occurrence of 10 must be of the same numeric type as the occurrence of 9. So, the most general type assignment will be (Num a = a) for 10, and (Num b = b) for 9. Solution: either choose a specific (non-polymorphic type) test1 = (10::Int) * (vector 10 [0..9::Int]) Or tell the typechecker that those constants must be of the same type: test2 = let n = 10 in n * (vector 10 [0..(9 `asTypeOf` n)]) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: fundeps syntax is ugly
Hello Johannes, Thursday, February 02, 2006, 2:17:42 PM, you wrote: JW When I first learned functional dependencies JW I remember I was really confused by their syntax. JW First, it is hard to find it defined: i should wrote this earlier, but nevertheless: Hugs documentation contains excellent introduction into the fundeps. i learned on it and never read any other papers. moreover, i recommended it to other ghc users, who was unhappy with current ghc docs Simon, may be it's the time to just steal this document section? i will don't say to anyone :) -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: fundeps for extended Monad definition
In article
[EMAIL PROTECTED]
ft.com,
Simon Peyton-Jones [EMAIL PROTECTED] wrote:
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
Is the defn of f legal? Both GHC and Hugs reject it because the
inferred type of f is more like
C Int Int = Int - Int
If this were allowed, it would effectively allow type-lambda. For
instance, I have a type function T that maps Int to Bool and Bool to
Char:
class C a b | a - b
instance C Int Bool
instance C Bool Char
newtype T a = MkT (forall b.(C a b) = b)
helperIn :: (forall b.(C a b) = b) - T a
helperIn b = MkT b; -- currently won't work
helperOut :: T a - (forall b.(C a b) = b)
helperOut (MkT b) = b;
Here T is a type-constructor that does that. If I like, I can represent
Char as T (T Int), though of course I need to use the helper functions
to actually use it as a Char.
--
Ashley Yakeley, Seattle WA
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps for extended Monad definition
Ashley Yakeley wrote: If this were allowed, it would effectively allow type-lambda class C a b | a - b instance C Int Bool instance C Bool Char newtype T a = MkT (forall b.(C a b) = b) helperIn :: (forall b.(C a b) = b) - T a helperIn b = MkT b; -- currently won't work helperOut :: T a - (forall b.(C a b) = b) helperOut (MkT b) = b And it does work (based on the code shown here previously): class C a b | a - b instance C Int Bool instance C Bool Char instance C Char Float instance C Float (Int-()) instance (C a b) = C (a-()) (b-()) newtype T a = T (forall b.(C a b) = b) data T1 a = T1 a (T a) xx b = case (T1 b (T undefined)) of T1 _ (T x) - x Ok, modules loaded: Main. *Main :type xx$(1::Int) Bool *Main :type xx$ xx$ (1::Int) Char *Main :type xx$ xx$ xx$ (1::Int) Float *Main :type xx$ xx$ xx$ xx$ (1::Int) Int - () *Main :type xx$ xx$ xx$ xx$ xx$ (1::Int) Bool - () *Main :type xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) Char - () *Main :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) Float - () *Main :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) (Int - ()) - () *Main :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) (Bool - ()) - () *Main :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) (Char - ()) - () It seems it does compute The principle was to use constraints to force the evaluation of the type lambda. Obtaining the type lambda was the thrust behind the exercise with existential and useless types. Perhaps I neglected to mention that point. We can use the Coerce type function (aka class) mentioned in the thread on first-class types to convert from the types computed by 'xx' to values. Incidentally, the class D was already a type function: the function 'meet'. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
| I believe something along the lines of the following would work:
|
| class C a b | a - b where { foo :: b - String }
| instance C Int Int where { foo x = show (x+1) }
| x :: forall b. C Int b = b
| x = 5
|
| (Supposing that the above definition were valid; i.e., we didn't get
the
| type signature error, this reads that x has type b for all types
| b such that C Int b -- the fact that there is only one such type
(due to
| the fun dep) is for us to know.)
|
| Then, we should be able to say:
|
| foo x
|
| and get 6.
I understand that is what you would like, but I do not know how to
achieve it in a reasonable way. (By reasonable I mean both in terms
of a reasonably simple type inference algorithm, and in terms of a
reasonable translation into a typed intermediate language. The latter
is, in a sense, just an implementation matter, but I have found it to be
an excellent sanity check.)
Simon
|
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
| The reason, which is thoroughly explained in Simon Peyton-Jones' | message, is that the given type signature is wrong: it should read | f1 :: (exists b. (C Int b) = Int - b) | | Right. Simon pointed out that this is a pretty useless function, but not | entirely so, since the result of it is not of type 'forall b. b', but | rather of 'forall b. C Int b = b'. Thus, if the C class has a function | which takes a 'b' as an argument, then this value does have use. I disagree. Can you give an example of its use? Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
| entirely so, since the result of it is not of type 'forall b. b', but
| rather of 'forall b. C Int b = b'. Thus, if the C class has a
function
| which takes a 'b' as an argument, then this value does have use.
I disagree. Can you give an example of its use?
I believe something along the lines of the following would work:
class C a b | a - b where { foo :: b - String }
instance C Int Int where { foo x = show (x+1) }
x :: forall b. C Int b = b
x = 5
(Supposing that the above definition were valid; i.e., we didn't get the
type signature error, this reads that x has type b for all types
b such that C Int b -- the fact that there is only one such type (due to
the fun dep) is for us to know.)
Then, we should be able to say:
foo x
and get 6.
From a translation to untyped core perpective (*grin*), we essentially
replace class constraints with dictionaries. The definition of C
introduces a dictionary like the following (I'm not 100% familiar with
MPTC dictionaries, but I assume they're just like normal dictionaries):
data CDict a b = CDict (b - String)
Then the instance will give us:
cIntIntDict :: CDict Int Int
cIntIntDict = CDict (\x - show (x+1))
foo will become:
foo (CDict foo_f) x = foo_f x
and if we apply this properly, we get:
| foo cIntIntDict x
| == (\ (CDict foo_f) x - foo_f x) cIntIntDict x
| == (\ (CDict foo_f) - foo_f x) cIntIntDict
| == (\x - show (x+1)) x
| == show (5+1)
| == 6
or something like that?
In fact, except for the type definition on x, this is actually a valid
translation into typed core, I believe. The weird type on x is the only
stumbling block, afaics.
...it is well known that I could be wrong though...
- Hal
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
| The reason, which is thoroughly explained in Simon Peyton-Jones' | message, is that the given type signature is wrong: it should read | f1 :: (exists b. (C Int b) = Int - b) Can you give an example of its use? Yes, I can. class (Show a, Show b) = C a b | a - b where doit:: a - b - String instance C Int Int where doit a b = (show a) instance C Bool Bool where doit a b = if a then everything else nothing newtype M a = M (forall b.(C a b) = b) f :: Int - M Int f x = M undefined g :: Bool - M Bool g x = M undefined test1 a = case (f a) of M b - doit a b test2 a = case (g a) of M b - doit a b I wonder if the Obfuscated Haskell contest has an entry for the most useless type (with no uses). However, if a type can be used for the contest, it is no longer the most useless. This makes one wonder if the rules of the contest implicitly contain the Russel paradox. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps known beforehand (was RE: fundeps for extended Monad definition)
| since this claims that it will take a Bool and produce a value of type b | for all types b. However, would it be all right to say (in | pseudo-Haskell): | | f :: exists b . Bool - b | f x = x But this is a singularly useless function, because it produces a result of utterly unknown type, so you can't actually use it. For example you could not say f x + 4 Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
The reason, which is thoroughly explained in Simon Peyton-Jones' message, is that the given type signature is wrong: it should read f1 :: (exists b. (C Int b) = Int - b) Right. Simon pointed out that this is a pretty useless function, but not entirely so, since the result of it is not of type 'forall b. b', but rather of 'forall b. C Int b = b'. Thus, if the C class has a function which takes a 'b' as an argument, then this value does have use. Hal Daume's original example works as well: newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) = mb) class Monad2 m a ma | m a - ma, ma - m a where return2 :: a - ma bind2 :: ma - (a - (MM2 m a)) - (MM2 m a) unused :: m a - () unused = \_ - () This wasn't quite my original example. The type of bind2 needs to be: bind2 :: ma - (a - (MM2 m b)) - (MM2 m b) Which does typecheck. However, you cannot seem to write instances of it: instance Monad2 [] a [a] where return2 x = [x] bind2 l f = MM2 (concatMap (unmm2 . f) l) where unmm2 (MM2 mb) = mb yields our friend cannot unify mb with [b], both in hugs and ghc. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
Hello! It seems we can truly implement Monad2 without pushing the envelope too far. The solution and a few tests are given below. In contrast to the previous approach, here we lift the type variables rather than bury them. The principle is to bring the type logic programming at the level of classes and instances but avoid putting them at the level of their members. class TwoMonadific m a ma | m a - ma, ma - m a where unused :: m a - () unused = undefined instance TwoMonadific [] a [a] instance TwoMonadific Maybe a (Maybe a) class (TwoMonadific m a ma, TwoMonadific m b mb) = Monad2 m a b ma mb where return2 :: a - ma bind2 :: ma - (a - mb) - mb instance Monad2 [] a b [a] [b] where return2 x = [x] bind2 l f = concatMap f l instance Monad2 Maybe a b (Maybe a) (Maybe b) where return2 x = Just x bind2 Nothing f = Nothing bind2 (Just x) f = f x test1 = (return2 5) `bind2` (\n - [1..n]) `bind2` (\n - [1..n]) test2 = (return2 5) `bind2` Just `bind2` Just *Main test1 [1,1,2,1,2,3,1,2,3,4,1,2,3,4,5] *Main test2 Just 5 It all works in GHC. Hugs complaints about return2: ERROR /tmp/b.hs:11 - Ambiguous type signature in class declaration *** ambiguous type : Monad2 a b c d e = b - d *** assigned to: return2 My version of Hugs isn't up-to-date though. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
Interesting example
| class Monad2 m a ma | m a - ma, ma - m a where
| return2 :: a - ma
| bind2 :: Monad2 m b mb = ma - (a - mb) - mb
| _unused :: m a - ()
| _unused = \_ - ()
| instance Monad2 [] a [a] where
| bind2 = error urk
The functional dependencies say
m a - ma
Instantiating this with the instance declaration
instance Monad2 [] a [a]
we can deduce that
given any constraint (Monad2 t1 t2 t3),
if t1 = [], then t3 must be [t2]
In the instance declaration, we instantiate the type of bind2 to get
the type of bind2 needed for this particular instance declaration:
bind2 :: forall b mb. Monad2 [] b mb = ma - (a - mb) - mb
Now the rule above says that means mb must be [b] and that gives rise
to the error.
GHC is consistent about this --- if you don't supply an defn for bind2,
it makes one up, and complains in more or less the same way.
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
Is the defn of f legal? Both GHC and Hugs reject it because the
inferred type of f is more like
C Int Int = Int - Int
Functional dependencies tell us that 'b' must be Int, so in fact the two
types are equivalent. In this example the programmer could write the
'correct' type, but in your case you can't because the type signature
arises by instantiating the one in the class declaration.
I'm really not sure what to do about this. GHC has an excellent way of
keeping me honest in type-checking: the type checker has to produce a
translation of the program into the (typed) core language. What could
f's translation look like. It must presumably be
f (d::C Int Int) (x::Int) = x
giving f the type
f :: C Int Int - Int - Int
Another translation could be
f b (d::C Int b) (x::Int) = x
(the 'b' is a type variable, a big-lambda binding) giving f the type
f :: forall b. C Int b - Int - Int
But what I *cannot* get is the type
f : forall b. C Int b - Int - b
how could I write the term?
f b (d:: C Int b) (x::Int) = ?
I suppose I could use (unsafeCoerce x) as the RHS, which amounts to
saying in every call to f, b will be Int, so we know that the coercion
is safe. But that is a scarily global property. For example, if a
call site of f does not see the instance declaration, it might call f
with an argument of type (C Int Bool) or something. Nor can I see an
easy way to insert the 'right' coercions in general.
Bottom line: excellent point, but I can't see how to fix it. Maybe
there are some fundep experts out there who can guide us through the
swamp?
Simon
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
fundeps known beforehand (was RE: fundeps for extended Monad definition)
Hi Simon, all,
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
This is interesting, but I'm not entirely sure what the problem is (from a
theoretical, not practical, standpoint). Obviously there is no problem in
a one module program, so let's assume we have the following modules:
module C where
class C a b | a - b where {}
module I1 where
import C
instance C Int Int where {}
module I2 where
import C
instance C Int Bool where {}
module U where
import C
import ?
f :: C Int b = Int - b
f x = x
Now, there are four cases:
1) U (transitively) imports I1
2) U (transitively) imports I2
3) U (transitively) imports both I1 and I2
4) U (transitively) imports neither I1 nor I2
Suppose we are in case 1. Then the programmer has written a too-general
type signature on f. The programmer *must* know that b=Int in this case
otherwise his function definition makes no sense. However, I don't really
see a reason why this should be an error rather than just a warning. If
some other module K imports both U and (for instance) I2, then we'll get a
fundep clash and the whole program will be invalid.
Suppose we are in case 2. Then the programmer has clearly screwed up
because we know b=Bool and x::Int and x::Bool are incompatible. This
should clearly be a type error.
Case 3 is impossible, as this will be a fundep clash.
Case 4 should produce an error (IMO). Of course, there could be a module
K which imports this U and also I1 in which case you might argue that this
should be allowed, but I don't think that makes much sense.
I suppose I could use (unsafeCoerce x) as the RHS, which amounts to
saying in every call to f, b will be Int, so we know that the coercion
is safe. But that is a scarily global property. For example, if a
call site of f does not see the instance declaration, it might call f
with an argument of type (C Int Bool) or something. Nor can I see an
easy way to insert the 'right' coercions in general.
Is this possible? In order for this to happen, this evil module M must
import U. This means that it has transitively imported I1 and thus has
the instance declaration. Or am I missing something. I think the
unsafeCoerce x is safe in these cases.
Bottom line: excellent point, but I can't see how to fix it. Maybe
there are some fundep experts out there who can guide us through the
swamp?
Yes, please!
- Hal
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
Hello!
Simon Peyton-Jones wrote:
class C a b | a - b where {}
instance C Int Int where {}
f1 :: (forall b. (C Int b) = Int - b)
f1 x = undefined
Indeed, this gives an error message
Cannot unify the type-signature variable `b' with the type `Int'
Expected type: Int
Inferred type: b
The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) = Int - b)
Alas, 'exists' is not an allowed type quantifier. Not explicitly that
is. We can get 'exists' if we use the permitted 'forall' in a negative
position (aka in an existential type).
The following code
class C a b | a - b where {}
instance C Int Int where {}
newtype M a = M (forall b.(C a b) = b)
f :: Int - M Int
f x = M undefined
typechecks in both Haskell compilers.
Hal Daume's original example works as well:
newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) = mb)
class Monad2 m a ma | m a - ma, ma - m a where
return2 :: a - ma
bind2 :: ma - (a - (MM2 m a)) - (MM2 m a)
unused :: m a - ()
unused = \_ - ()
instance Monad2 [] a [a] where
bind2 = error urk
Again, it typechecks both in Hugs and GHC.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps known beforehand (was RE: fundeps for extended Monad definition)
Suppose we are in case 1. Then the programmer has written a too-general
type signature on f. The programmer *must* know that b=Int in this case
otherwise his function definition makes no sense. However, I don't really
see a reason why this should be an error rather than just a warning. If
some other module K imports both U and (for instance) I2, then we'll get a
fundep clash and the whole program will be invalid.
I now retract this comment :). Clearly this is just as bad as saying:
f :: Bool - b
f x = x
since this claims that it will take a Bool and produce a value of type b
for all types b. However, would it be all right to say (in
pseudo-Haskell):
f :: exists b . Bool - b
f x = x
?
Here, we're simply claiming that there is *some* type b for which f takes
a Bool and produces a b?
I believe this same analysis extends to something like:
class C a b | a - b where {}
instance C Int Int where {}
f :: exists b . C Int b = Int - b
f i = i
It seems that this would be legal in a language like haskell but which
allowed existensial quantification.
Am I correct?
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
The reason, which is thoroughly explained in Simon Peyton-Jones' message, is that the given type signature is wrong: it should read f1 :: (exists b. (C Int b) = Int - b) Sigh, read this after posting :) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps question
On Monday 16 December 2002 18:18, Ashley Yakeley wrote: In article [EMAIL PROTECTED], Hal Daume III [EMAIL PROTECTED] wrote: I spent about a half hour toying around with this and came up with the following, which seems to work (in ghci, but not hugs -- question for smart people: which is correct, if either?)... Both are correct. Hugs fails (correctly) because it doesn't have anything like -fallow-overlapping-instances. Urr... I think hugs invented overlapping instances - or at least Mark Jones did... ;-) Try `+o'. --Jeff ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps question
Hi, I spent about a half hour toying around with this and came up with the following, which seems to work (in ghci, but not hugs -- question for smart people: which is correct, if either?)... class Mul a b c | a b - c where mul :: a - b - c-- our standard multiplication, with fundeps data Commute a b = Commute a b -- just pair them -- now, our helper class class Mul2 x a b c | a b - c where mul2 :: x a b - c -- given a helper instance with Commute, we have an instance of the -- original Mul class instance Mul2 Commute a b c = Mul a b c where mul a b = mul2 (Commute a b) -- now, we make Mul2 commutative over Commute: instance Mul2 Commute a b c = Mul2 Commute b a c where mul2 (Commute i j) = mul2 (Commute j i) -- helper function: i2d :: Int - Double i2d = fromInteger . toInteger -- finally we can make our definition: instance Mul2 Commute Int Int Int where mul2 (Commute i j) = i * j instance Mul2 Commute Int Double Double where mul2 (Commute i j) = i2d i * j -- note that we don't have to define Mul2 Commute Double Int Double instance Mul Commute Double Double Double where mul2 (Commute i j) = i * j -- we can now test these i :: Int i = 3 d :: Double d = 5 -- now, in ghci: *TryCommute mul i i 9 *TryCommute mul i d 15.0 *TryCommute mul d d 25.0 *TryCommute mul d i 15.0 Woohoo, even the last one worked. Of course, like so many things, this requires -fallow-overlapping-instances as well as -fallow-undecidable-instances. Interestingly, with -98, Hugs doesn't allow this program, saying: ERROR TryCommute.hs:23 - Instances are not consistent with dependencies *** This instance: Mul2 Commute a b c *** Conflicts with : Mul2 Commute Int Int Int *** For class: Mul2 a b c d *** Under dependency : b c - d I'm not entirely sure why -- Hal Daume III Computer science is no more about computers| [EMAIL PROTECTED] than astronomy is about telescopes. -Dijkstra | www.isi.edu/~hdaume On Sat, 14 Dec 2002 [EMAIL PROTECTED] wrote: I want to use functional dependencies in a way I've not yet seen: to enforce commutativity. I define class Mul a b c | a b - c, b a - c where mul :: a - b - c I want instance (Mul a b c) = Mul b a c where mul x y = mul y x do what I expect: if I can multiply a and b, then I can multiply b and a _and always have the same type_. In a sense, this makes multiplication commute (in the land of types). For a whole variety of reasons, the many (4 or 5 now) ways I've tried to make this work have failed, both using Hugs and GHC. I mentioned I wanted typed multiplication to commute. Let me explain more thoroughly: suppose I had data Unit u v = Unit u v I want (Unit u1 value1) `mul` (Unit u2 value2) to have the same type as (Unit u2 value2) `mul` (Unit u1 value1). So say u1 :: Int, u2 :: Float, then (Unit u1 value1) `mul` (Unit u2 value2) :: (Unit Int (Unit Float blah)) and (Unit u2 value2) `mul` (Unit u1 value1) :: (Unit Int (Unit Float blah)) I don't care if the result type is Unit Int ... or Unit Float ..., as long as it is a) consistent and b) inferred and c) enforced. So far, no luck. A few other questions: What happenned to +m in Hugs? In general, if I wanted a fundep to specify that a pair (a, b) determined c _regardless of the order of a and b_, how could it be done? Why doesn't a b - c, b a - c do this? What I mean is that if I have one of a, b and Int (say) and c a Float, then I could infer the other of a, b once I have a single instance. And a 'bug' report: in the overlapping instance one-liner above, the Mul a b c = Mul b a c, I can have this in place and write contradictory instances that violate the fundeps that are not caught in GHC. (Hugs does not allow the overlapping instances to begin with, even worse.) Well, that became a clearinghouse for the frustrations of the last several days. Sorry. Thanks, Nick ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps question
In article [EMAIL PROTECTED], Hal Daume III [EMAIL PROTECTED] wrote: I spent about a half hour toying around with this and came up with the following, which seems to work (in ghci, but not hugs -- question for smart people: which is correct, if either?)... Both are correct. Hugs fails (correctly) because it doesn't have anything like -fallow-overlapping-instances. -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps question
At 2002-12-14 15:27, [EMAIL PROTECTED] wrote: I define class Mul a b c | a b - c, b a - c where mul :: a - b - c The two constraints are identical. Each one says given a and b, you have c. What you want is essentially this: class (Mul b a c) = Mul a b c where mul :: a - b - c mul a b = mul b a ...but that's not allowed as superclass contexts cannot be circular. I want instance (Mul a b c) = Mul b a c where mul x y = mul y x This will overlap with any other Mul instance. Instance declarations cannot be made overridable the way functions in OOP languages can be: each instance declaration must have an entirely separate domain. -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
--- Tom Pledger [EMAIL PROTECTED] wrote: anatoli writes: : | The same error message is given for | | data Foo a = (Eq b) = MkFoo b Since the type variable a is orphaned, how about reducing it to this? data Foo = forall b . Eq b = MkFoo b This is possible (the semantics is different of course). What I want to do is, given a multi-parameter context, orphan one type variable leaving the other intact, and that's not possible now. I can only orphan all or preserve all. so that MkFoo :: Eq b = b - Foo | I don't know whether this is intended behaviour; IMHO | it should be treated identically to | | data Foo a = MkFoo (Eq a = a) Isn't the Foo-ed a hidden by the Eq-ed a in this example too? i.e. data Foo = MkFoo (forall a . Eq a = a) It appears that both examples are wrong, or at least Hugs thinks so. The first MkFoo happily accepts any type, not just of class Eq: Main :t MkFoo head MkFoo head :: Foo ([a] - a) The second accepts nothing of interest: Main :t MkFoo 'a' ERROR: Inferred type is not general enough *** Expression: 'a' *** Expected type : Eq a = a *** Inferred type : Eq Char = Char Hm... The more I experiment with this, the less I understand. It seems that the only correct place to put the quantifier is before the data constructor, and the context may go either before the type constructor or after the quantifier. This is very unfortunate. How can I correctly write something to this effect: data Quick a = Eq a = Unsorted [a] | Ord a = Sorted (Tree a) ??? Regards -- anatoli __ Do You Yahoo!? Get personalized email addresses from Yahoo! Mail - only $35 a year! http://personal.mail.yahoo.com/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
Hi everybody:
I think I've found what's the problem. Still no solution in sight :(
The problem has nothing to do with fundeps. Consider an example:
data Foo a = (Eq a) = MkFoo a
This gives the same error message: type variable a is not locally
bound. Apparently, 'a' in 'Eq a' hides 'a' in 'Foo a' instead of
using it. The same error message is given for
data Foo a = (Eq b) = MkFoo b
I don't know whether this is intended behaviour; IMHO
it should be treated identically to
data Foo a = MkFoo (Eq a = a)
Hugs accepts either
data Eq a = Foo a = MkFoo a
or
data Eq a = MkFoo (Eq a = a)
with no problem, but neither syntax works with Collection:
the first one would look like
data forall c. Collection c e = AnyColl e = MkColl c
which is a syntax error, and the second one
data AnyColl e = forall c . MkCall (Collection c e = c)
or alternatively
data AnyColl e = MkCall (forall c . Collection c e = c)
gives me 'Ambiguous type signature in type component' error.
{
Apparently Hugs is still buggy in the fundep/multiparameter
classes area; I have an example where Hugs assigns garbage types
to things when fundeps are involved. This is probably a
hugs-bugs issue.
}
Now to the question:
--- Tom Pledger [EMAIL PROTECTED] wrote:
Does it introduce any new implementation issues? When a constructor
like MakeSomeCollection is applied, some implementations gather a
dictionary of methods appropriate for use with the existentially
quantified type, right?
I believe that in the general case all implementation must do so, in one
form or another.
Is that more difficult when it involves a
non-locally bound type variable? Even when that type variable is
constrained by a fundep?
I believe there should be no implementation problems. In order to gather the
dictionary, an implementation must know the type of the argument to
MakeSomeCollection. When this type (say T) is known, the compiler just finds
'instance Collection T whatever' declaration. There can be only one such
instance (because of the fundep). All needed methods are specified there.
Regards
--
anatoli
__
Do You Yahoo!?
Yahoo! Auctions - Buy the things you want at great prices.
http://auctions.yahoo.com/
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: Fundeps
Hi Marcin, | module M where | | class Seq s a | s - a where | m :: Seq s b = (a - b) - s a - s b This combination of constructor classes and functional dependencies looks very odd! The dependency says that, if you pick a particular implementation s of sequences, then there will be at most one choice for the element type a. I can have lists of Char or lists of Int, but not both together! Perhaps you wanted something more like the following: class Seq s a | s - a where m :: Seq t b = (a - b) - s - t Note that the kinds have changed here; s and t are both of kind *, not * - * as before. The trouble with this version is that it doesn't require/ensure that you've used the same form of sequence for both s and t. The parametric type classes folks had an answer for this in the form of a constraint s ~ t requiring that the two types had "the same outermost constructor", but I don't think it was really a good solution either. | instance Seq PS Char where | m f (PS s) = PS (map f s) | | This is not accepted by Hugs: Rightly so. With this definition, you've promised that the element type corresponding to PS will be Char, which means that you can't have a different element type in the returned collection! Hope this helps! All the best, Mark
