New restrictions to open type families

[Richard Eisenberg]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130823/77b317f3/attachment.htm>