Re: The GADT debate

On Sun, May 8, 2016 at 11:25 AM, Richard Eisenberg wrote:

On May 7, 2016, at 11:05 PM, Gershom B wrote:

...

an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).

Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:

1. The scrutinee 2. Every case branch 3. The case as a whole

With all of these type signatures in place, GADT type inference is indeed straightforward.

If all three of those signatures are present, doesn't that make "inference" trivial? If I understand you correctly, the only thing to do here would be to check the types, right? I am curious though. Since we don't have true/anonymous type-level functions, why do we need the signatures on every branch (assuming the scrutinee and whole-expression types are given)? I can see why they'd be required in Coq/Agda/etc, but it's less clear why they'd be required in Haskell per se -- Live well, ~wren