Repeated variables in type family instances

[Richard Eisenberg]

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