[Haskell-cafe] Partial type family application

[mniip]

On Wed, Apr 26, 2017 at 09:20:34PM -0400, Richard Eisenberg wrote:
> But what *is* the (->) arrow? In a type describing a term, (->) describes an unmatchable function. In a kind describing a type, it describes a matchable function. And this is the tension. -XTypeInType means that types and kinds are the same, so this discrepancy is even stranger. It doesn't really bite, quite, but I very much think that any work in this direction should aim to have (->) be unequivocally unmatchable (because unmatchable functions are the vastly common case, taking both terms and types into account).

After some more reading, I think I understand what you mean here.

> As far as I can tell, a matchable -> occurs in Haskell today in kind signatures and the type signature of a GADT-style data constructor.

Why is a GADT constructor's arrow matchable? A GADT constructor is
indistinguishable from a term function in that you can't pattern-match
partially applied constructors.

> These spots are easy to discern syntactically, so it's not hard to keep this legacy behavior in a brave new world with first-class matchable and unmatchable arrows. I would see phasing these out at some point -- it also wouldn't be hard to write a tool to automatically change current usage of arrows to the new one. But perhaps the community wouldn't want this (that is, phase out current usage), and that's fine too.

I could see that very easily being an issue, yes. Perhaps, if we
consider unmatchable arrows as a supertype of matchable arrows, then we
could secretly assign matchable arrows in the appropriate places even if
an unmatchable arrow was written (why would anyone want an explicitly
unmatchable arrow?) and not display them in type signatures until
appropriate extensions are enabled. That would be backwards compatible
with all current code, and the only place you'd need to use the new
arrow would be a higher order type family.


> Also: I have no strong opinions at all about the spelling of the new arrow. Using '-> had some nice similarity with other uses of ', but ~> is a notation I've also long considered.

I don't either, and I came up with ~> in a few seconds. Honestly I don't
know what a good candidate for it would be. '-> throws me off because it
looks more like \hookrightarrow.

> and would happily debate this on a ghc-proposal.

On Wed, Apr 26, 2017 at 10:58:10AM -0400, Richard Eisenberg wrote:
> The good news here is that this idea should be realizable independent from Dependent Haskell. It just needs someone to work out the details, propose, get community acceptance, and implement. But, from a theory point of view, I’m confident you’re describing the right direction to take all this in.

Are you suggesting that this idea is worthy of a GHC proposal?