RE: New restrictions to open type families
Great answer Richard. (And another yesterday.) I wonder whether it'd be worth updating the wiki to reflect the final situation http://ghc.haskell.org/trac/ghc/wiki/NewAxioms and children: * There is out of date status descriptions. * No pointer to the paper, now that we have gone to all the trouble of writing it. * Pointers to the tickets or email discussions where you have so accurately responded to questions would be useful (or copy/paste into a FAQ) * Retire (explicitly mark as out of date) stuff that we have now rejected, or general ramblings. Eg much of http://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage Might you consider doing that? This might save you some work! Supposedly http://www.haskell.org/haskellwiki/GHC/Type_families is our *programmer-oriented* discussion of type families, so an alternative might be to work on that. I don't feel strongly. Cross links are probably useful. Thanks Simon From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Richard Eisenberg Sent: 23 August 2013 05:24 To: Akio Takano Cc: glasgow-haskell-users@haskell.org Subject: Re: New restrictions to open type families This is a good question. Happily, there are at least two decent answers. 1) We're not sure that this problem cannot cause a segfault... it's just that we've been unable to produce one when trying. Perhaps we haven't tried hard enough. 2) The type soundness of Haskell (as implemented in GHC) rests on the type soundness of System FC (also known as Core), which is the internal language used within GHC. Haskell code is desugared into FC code during compliation. Without this change in behavior of open type families, System FC is not sound. Let's consider the example in #8154: type family BoundsOf x type instance BoundsOf (a - a) = Int type instance BoundsOf (a - a - a) = (Int, Int) Now, add the dangerous looping ingredient: type family Looper a type instance Looper a = Looper a - Looper a System FC includes coercions which witness the equality between two types. A critical part of the proof of FC's type safety rests on the fact that we cannot build a coercion, say, between Int and (Int, Int). Yet, with the definitions above, we can easily make such a coercion, using transitivity: Int ~ (Looper a - Looper a) ~ (Looper a - Looper a - Looper a) ~ (Int, Int) Thus, System FC is not type-safe if we allow the definitions above. Might there be a way to re-specify System FC not to allow coercions such as this one? Possibly, but it would seem to rest on the fact that certain equalities (e.g., those that arise from type families) cannot be run in reverse. This, in turn, would hamper the coercion optimizer and other code transformations. In the end, it would seem to take quite a substantial change to the engineering of FC to fix this problem in this way. Another possibility is to admit that FC is not type-safe, but claim that all FC programs that are produced from Haskell source programs are in a type-safe subset. This approach seems quite dangerous and very brittle; I would say this is quite a weak statement of type safety. So, we chose the route to forbid definitions like BoundsOf. Note that it is easier to prohibit BoundsOf and not Looper, because in the wild, a type family such as Looper may have many more moving parts and it may actually be undecidable to determine whether a given set of type families emulates Looper's behavior. If you have an application where this new restriction in open type families really gets in your way, please email me about it and we'll see what we can do. Thanks, Richard On Aug 22, 2013, at 4:34 AM, Akio Takano wrote: Hi, Looking at the ticket [1] and a draft paper linked there [2] , I learned that in GHC 7.8, two type family instances are considered overlapping if the argument lists unify in the presence of infinite types. My question is, why is this restriction necessary? A footnote in the paper states that it was not possible with GHC 7.6 to actually exploit the inconsistency. Would it be difficult to solve the problem by making this behaviour part of the specification, rather than accepting fewer programs? [1] http://ghc.haskell.org/trac/ghc/ticket/8154 [2] http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf Regards, Takano Akio ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: New restrictions to open type families
Akio Thanks that's amazing! I wonder if it'd be worth adding it, with commentary, (and attaching the files) as a Trac ticket? I know its already fixed, but it's great to be able to say to see an example of why this is vital, see Trac #8324, whereas email archives are more ephemeral somehow. Simon From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Akio Takano Sent: 23 August 2013 11:35 To: glasgow-haskell-users@haskell.org; Richard Eisenberg Subject: Fwd: New restrictions to open type families (I forgot to send to the list, trying again) Thank you very much for your detailed explanation! On Fri, Aug 23, 2013 at 1:24 PM, Richard Eisenberg e...@cis.upenn.edumailto:e...@cis.upenn.edu wrote: This is a good question. Happily, there are at least two decent answers. 1) We're not sure that this problem cannot cause a segfault... it's just that we've been unable to produce one when trying. Perhaps we haven't tried hard enough. I successfully constructed such an example. https://github.com/takano-akio/type-family-overlap - Akio ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: New restrictions to open type families
I created a ticket and attached the files: http://ghc.haskell.org/trac/ghc/ticket/8162 -- Akio On Fri, Aug 23, 2013 at 7:46 PM, Simon Peyton-Jones simo...@microsoft.comwrote: Akio ** ** Thanks that’s amazing! I wonder if it’d be worth adding it, with commentary, (and attaching the files) as a Trac ticket? I know its already fixed, but it’s great to be able to say “to see an example of why this is vital, see Trac #8324”, whereas email archives are more ephemeral somehow. ** ** Simon ** ** *From:* Glasgow-haskell-users [mailto: glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Akio Takano *Sent:* 23 August 2013 11:35 *To:* glasgow-haskell-users@haskell.org; Richard Eisenberg *Subject:* Fwd: New restrictions to open type families ** ** (I forgot to send to the list, trying again) Thank you very much for your detailed explanation! ** ** On Fri, Aug 23, 2013 at 1:24 PM, Richard Eisenberg e...@cis.upenn.edu wrote: This is a good question. Happily, there are at least two decent answers. ** ** 1) We're not sure that this problem cannot cause a segfault… it's just that we've been unable to produce one when trying. Perhaps we haven't tried hard enough. I successfully constructed such an example. https://github.com/takano-akio/type-family-overlap - Akio ** ** ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: New restrictions to open type families
Yes -- wow. I had tried similar techniques, but couldn't get it to go through in the end. I think using the datatype was the key. Cool! I will update the wiki as per Simon's suggestions. On Aug 23, 2013, at 6:34 AM, Akio Takano wrote: (I forgot to send to the list, trying again) Thank you very much for your detailed explanation! On Fri, Aug 23, 2013 at 1:24 PM, Richard Eisenberg e...@cis.upenn.edu wrote: This is a good question. Happily, there are at least two decent answers. 1) We're not sure that this problem cannot cause a segfault… it's just that we've been unable to produce one when trying. Perhaps we haven't tried hard enough. I successfully constructed such an example. https://github.com/takano-akio/type-family-overlap - Akio ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: New restrictions to open type families
This is a good question. Happily, there are at least two decent answers. 1) We're not sure that this problem cannot cause a segfault… it's just that we've been unable to produce one when trying. Perhaps we haven't tried hard enough. 2) The type soundness of Haskell (as implemented in GHC) rests on the type soundness of System FC (also known as Core), which is the internal language used within GHC. Haskell code is desugared into FC code during compliation. Without this change in behavior of open type families, System FC is not sound. Let's consider the example in #8154: type family BoundsOf x type instance BoundsOf (a - a) = Int type instance BoundsOf (a - a - a) = (Int, Int) Now, add the dangerous looping ingredient: type family Looper a type instance Looper a = Looper a - Looper a System FC includes coercions which witness the equality between two types. A critical part of the proof of FC's type safety rests on the fact that we cannot build a coercion, say, between Int and (Int, Int). Yet, with the definitions above, we can easily make such a coercion, using transitivity: Int ~ (Looper a - Looper a) ~ (Looper a - Looper a - Looper a) ~ (Int, Int) Thus, System FC is not type-safe if we allow the definitions above. Might there be a way to re-specify System FC not to allow coercions such as this one? Possibly, but it would seem to rest on the fact that certain equalities (e.g., those that arise from type families) cannot be run in reverse. This, in turn, would hamper the coercion optimizer and other code transformations. In the end, it would seem to take quite a substantial change to the engineering of FC to fix this problem in this way. Another possibility is to admit that FC is not type-safe, but claim that all FC programs that are produced from Haskell source programs are in a type-safe subset. This approach seems quite dangerous and very brittle; I would say this is quite a weak statement of type safety. So, we chose the route to forbid definitions like BoundsOf. Note that it is easier to prohibit BoundsOf and not Looper, because in the wild, a type family such as Looper may have many more moving parts and it may actually be undecidable to determine whether a given set of type families emulates Looper's behavior. If you have an application where this new restriction in open type families really gets in your way, please email me about it and we'll see what we can do. Thanks, Richard On Aug 22, 2013, at 4:34 AM, Akio Takano wrote: Hi, Looking at the ticket [1] and a draft paper linked there [2] , I learned that in GHC 7.8, two type family instances are considered overlapping if the argument lists unify in the presence of infinite types. My question is, why is this restriction necessary? A footnote in the paper states that it was not possible with GHC 7.6 to actually exploit the inconsistency. Would it be difficult to solve the problem by making this behaviour part of the specification, rather than accepting fewer programs? [1] http://ghc.haskell.org/trac/ghc/ticket/8154 [2] http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf Regards, Takano Akio ___ 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
