RE: Repeated variables in type family instances

Interesting points you make here. See my comments below:

-----Original Message----- From: dominique.devriese@gmail.com [mailto:dominique.devriese@gmail.com] On Behalf Of Dominique Devriese [snip] Wouldn't you get the same problem if you try to check a value-level pattern's linearity after including explicit type info. If so, why is that a problem for type instance patterns if it isn't a problem for value-level patterns?

For example, take the following value-level function null :: [a] -> Bool null [] = True null (_:_) = False After including explicit System F-like type arguments, that would become null @a ([] @a) = True null @a ((:) @a _ _) = False So we get the same problem of non-linearity of the expansion even though the original is fine, right?

The nub of the difference is that type families can pattern-match on kinds, whereas term-level functions cannot pattern-match on types. So, while the @a is repeated in the pattern as written above, GHC does not, when matching a pattern, check that these are the same. In fact, they have to be the same if the function argument is well-typed. On the other hand, type family equations *can* branch based solely on kind information, making the repeated variable semantically important. Another salient difference is that pattern-matching on the term level desugars to case statements internally, whereas pattern-matching at the type level does not. It is conceivable that a clever check could fix this problem and disallow "dangerous" non-linearity at the type level while still allowing "benign" non-linearity. But, we seem to have found a consistent approach that doesn't bother with linearity, anyway.

Note: I'm in favor of avoiding non-linear patterns for type families if at all possible, in order to keep the type-level computational model functional and close to the value-leve one. I would hope we could forbid linear patterns for type classes as well at some point in the future, although that could perhaps be more controversial still...

I think this would really lower the expressiveness of type-level computation, and I'm not sure what the gain would be. I, too, like type-level things to mimic term-level things, but in the end, the type world and the term world are very different places with different needs. (Specifically, type-level things need to be reasoned about at compile time to ensure type safety, and term level things need to be able to run in an executable.) I recognize that the difference cause problems with things that want to be share between the worlds (such as singletons), but in my opinion, that's not a good enough reason to disallow non-linearity altogether.

P.S.: I hope you'll be writing a more detailed account of this work (a research paper?) at some point and I look forward to reading it...

Yes, we're busy on it now. It turns out that the proof that all of this is type-safe is... well... interesting. A draft should be online in the next few weeks, and I'll add links from the wiki, etc.

P.S.2: On an unrelated note: will you also do a completeness check on closed type family definitions?

There is no plan for this, no. In the presence of non-linear equations, I'm not sure off the top of my head how I would do this. Richard

2013/5/29 Richard Eisenberg :

...

(Sorry for the re-send - got the wrong subject line last time.)

Hello all,

It's come to my attention that there is a tiny lurking potential hole in GHC's type safety around type families in the presence of UndecidableInstances. Consider the following:

...

type family F a b

...

type instance F x x = Int

...

type instance F [x] x = Bool

...

...

type family G

...

type family G = [G]

This declarations are all valid in GHC 7.6.3. However, depending on the reduction strategy used, it is possible to reduce `F G G` to either Int

...

Bool. I haven't been able to get this problem to cause a seg-fault in practice, but I think that's more due to type families' strictness than anything more fundamental. Thus, we need to do something about it.

I have written a proposal on the GHC wiki at http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/Nonlinearity

It proposes a change to the syntax for branched instances (a new form of type family instance that allows for ordered matching), but as those haven't yet been officially released (only available in HEAD), I'm not too worried about it.

There are two changes, though, that break code that compiles in released versions of GHC:

---

1) Type family instances like the two for F, above, would no longer be accepted. In particular, the overlap check for unbranched (regular standalone instances like we've had for years) would now check for overlap if all variables were distinct. (This freshening of variables is called 'linearization'.) Thus, the check for F would look at `F x y` and `F [x] y`, which clearly overlap and would be conflicting.

2) Coincident overlap between unbranched instances would now be prohibited. In the new version of GHC, these uses of coincident overlap would have to be grouped in a branched instance. This would mean that all equations that participate in coincident overlap would have be defined in the same module. Cross-module uses of coincident overlap may be hard to refactor.

---

Breaking change #1 is quite necessary, as that's the part that closes

or the

...

hole in the type system.

Breaking change #2 is strongly encouraged by the fix to #1, as the right-hand side of an instance is ill-defined after the left-hand side is linearized. It is conceivable that there is some way to recover coincident overlap on unbranched instances, but it's not obvious at the moment. Note that this proposal does not contain a migration path surrounding coincident overlap. In GHC <= 7.6.x, branched instances don't exist and we have coincident overlap among unbranched instances; and in GHC >= 7.8.x, we will prohibit coincident overlap except within branched instances. We (Simon PJ and I) think that this shouldn't be too big of a problem, but please do shout if it would affect you.

Please let me know what you think about this proposal!

Thanks,

Richard

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users