The GADT debate

[Iavor Diatchki]

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.schonwald at gmail.com
> wrote:

>
>
> On Sunday, May 8, 2016, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>
>>
>> On May 7, 2016, at 11:05 PM, Gershom B <gershomb at 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>>
>
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-prime/attachments/20160508/cb500ee0/attachment.html>