Hello, what is the state with the semantic specification of GADTs? I am wondering if they fit in the usual CPO-style semantics for Haskell, or do we need some more exotic mathematical structure to give semantics to the language.
-Iavor On Sun, May 8, 2016 at 8:36 AM, Carter Schonwald <carter.schonw...@gmail.com > wrote: > > > On Sunday, May 8, 2016, 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. As a strawman, I would be open to standardizing GADTs with >> these requirements in place and the caveat that implementations are welcome >> to require fewer signatures. Even better would be to do this research and >> come up with a good answer. I may very well be open to doing such a >> research project, but not for at least a year. (My research agenda for the >> next year seems fairly solid at this point.) If someone else wants to >> spearhead and wants advice / a sounding board / a less active co-author, I >> may be willing to join. >> >> Richard > > > > This sounds awesome. One question I'm wondering about is what parts of > the type inference problem aren't part of the same challenge in equivalent > dependent data types? I've been doing some Intersting stuff on the latter > front recently. > > It seems that those two are closely related, but I guess there might be > some complications in Haskell semantics for thst? And or is this alluded to > in existing work on gadts? > > > >> _______________________________________________ >> Haskell-prime mailing list >> Haskell-prime@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime >> > > _______________________________________________ > Haskell-prime mailing list > Haskell-prime@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime > >
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime