[Haskell-cafe] Partial type family application

[Richard Eisenberg]

> On Apr 26, 2017, at 8:39 PM, mniip <14 at mniip.com> wrote:
> 
> I'm reading your thesis, and in it you propose to make all -> arrows
> unmatchable, and all constructors automagically get '-> arrows.

Yes, that's what it says.

> 
> Naturally, if we implement just this type extension, then it'd make
> sense to leave the -> arrow as is and introduce an ~> unmatchable arrow.
> However this makes transition to fully dependent arrows even more
> awkward.

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). 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. 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.

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.

> 
> On the other hand we would have to pull the implicit '-> constructor
> arrows into this proposal, which makes it not so independent from
> dependent types, so still awkward.

Yes, if we say that -> is always unmatchable, then the implicit treatment of -> in certain syntactic situations would have to become part of this proposal, making it a little harder to implement. And if we consider this proposal in the absence of dependent types, your choice of notation might make more sense. (To be clear, "your choice" is, as I understand: -> describes an unmatchable function in terms, -> describes a matchable function in types, and ~> describes an unmatchable function in types.) So I see how the possibility of dependent types colors this proposal.

> 
> What do you think should be done?

I still maintain the opinion I present in my thesis, that -> should always be unmatchable and some new symbol (I propose '->, but have no strong opinion) should always be matchable. We would have support for legacy uses of -> in kinds, perhaps disabled with -XCurriedTypeFamilies (just because -XUnsaturatedTypeFamilies isn't quite as tasty).

That said, I can see the virtue of the opposing viewpoint and would happily debate this on a ghc-proposal.

Richard