Repeated variables in type family instances
eir at cis.upenn.edu
Mon Jun 24 16:06:48 CEST 2013
Interesting points you make here. See my comments below:
> -----Original Message-----
> From: dominique.devriese at gmail.com
> [mailto:dominique.devriese at gmail.com] On Behalf Of Dominique Devriese
> 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.
> 2013/5/29 Richard Eisenberg <eir at 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
> > 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
> > yet been officially released (only available in HEAD), I'm not too
> > 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
> > 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]
> > which clearly overlap and would be conflicting.
> > 2) Coincident overlap between unbranched instances would now be
> > In the new version of GHC, these uses of coincident overlap would have
> > grouped in a branched instance. This would mean that all equations that
> > participate in coincident overlap would have be defined in the same
> > Cross-module uses of coincident overlap may be hard to refactor.
> > ---
> > Breaking change #1 is quite necessary, as that's the part that closes
> > 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
> > linearized. It is conceivable that there is some way to recover
> > overlap on unbranched instances, but it's not obvious at the moment.
> > that this proposal does not contain a migration path surrounding
> > 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
> > prohibit coincident overlap except within branched instances. We (Simon
> > 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 at haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
More information about the Glasgow-haskell-users