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 to
Building on android - compiled program segfaults
Hi, I was succesfull in building ghc (pulled from git) to compile for arm-linux-androideabi! Now using inplace/bin/ghc-stage1 -dcore-lint -debug I compiler this Main.hs: main = putStrLn Hello, World I get an executable, which I can run on my android device. Unfortantly it segfaults. Running it with ./Main +RTS -DS gives: cap 0: initialised Now I am trying to debug this in gdb. When I try to display the stack (which should be in r13 on arm of I understand correctly, I get); (gdb) p8 $r13 0xbef00a74: 0x0 0xbef00a70: 0x0 0xbef00a6c: 0x3c2e74 0xbef00a68: 0x530350 0xbef00a64: 0x0 0xbef00a60: 0x0 0xbef00a5c: 0x0 0xbef00a58: 0x0 And now I am clueless. So I tried the good old printf debugging in the rts. Using this, I see that it gets before the call to scheduleWaitThread in the function rts_evalLazyIO (in RtsAPI.c). But when I put a printf in the beginning of scheduleWaitThread (in Schedule.c) it is not shown. What else can I do to find out more? Thanks! Nathan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: (mips64el) Cross-building GHC
What do you mean by barely-just-works? Anything besides: * no GHCi support and * bad performance due to the lack of a native code generator is probably a bug that we (the GHC maintainers in Debian) would like to know about. Could you help me to find a workaround for the mentioned error? ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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: Error building ghc on raspberry pi.
On Thu, 10 Jan 2013, Karel Gardas wrote: Hmm, are you using Raspbian? I.e. hard-float abi caught my eye in case of ARMv6/ARM11 chip here... I'm afraid LLVM is not well guided in your case so could you be so kind and test if adding -optlc=-mattr=+vfp2 helps? You need to add it to your build.mk probably and you will need to rebuild everything again... Add it to the GhcLibHcOpts? Cheers, Karel -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Error building ghc on raspberry pi.
On 01/11/13 09:25 PM, rocon...@theorem.ca wrote: On Thu, 10 Jan 2013, Karel Gardas wrote: Hmm, are you using Raspbian? I.e. hard-float abi caught my eye in case of ARMv6/ARM11 chip here... I'm afraid LLVM is not well guided in your case so could you be so kind and test if adding -optlc=-mattr=+vfp2 helps? You need to add it to your build.mk probably and you will need to rebuild everything again... Add it to the GhcLibHcOpts? Probably too, I'm not the expert here, just make sure you use this option for any ghc invocation which invokes llc to get consistent vfp usage in your object files... Once you test it and if succeed we can hack ghc to support it. Karel ___ 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. ** ** In the
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
