New restrictions to open type families
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
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
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-bounces@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
participants (3)
-
Akio Takano -
Richard Eisenberg -
Simon Peyton-Jones