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.
I'm reading your thesis, and in it you propose to make all -> arrows unmatchable, and all constructors automagically get '-> arrows. 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. 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. What do you think should be done? --mniip