Interesting points you make here. See my comments below: > -----Original Message----- > From: dominique.devri...@gmail.com > [mailto:dominique.devri...@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 <e...@cis.upenn.edu>: > > (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 or > > 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 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 > > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
