On Sun, May 8, 2016 at 11:25 AM, Richard Eisenberg <e...@cis.upenn.edu> wrote: > On May 7, 2016, at 11:05 PM, Gershom B <gersh...@gmail.com> 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 _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
