<div dir="ltr"><div dir="ltr"></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Hi Xuanrui and Vanessa,</div><div dir="ltr" class="gmail_attr"><br>Richard's PhD thesis is a big step towards having a specification for GADTs, so if his comment is more than 3 years old (he published his thesis in 2016), then the comment is outdated. I have not read all of his thesis ( <a href="https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf">https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf</a> ), but I think it's the closest thing to a semantics of GADTs there is out there right now.</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">My guess is that what Richard means with 'having a semantics' involves answering two things:</div><div dir="ltr" class="gmail_attr">- which programs are considered 'correct' (i.e. well-typed)</div><div dir="ltr" class="gmail_attr">- what is an execution-step for a correct program. This is a description such that chaining valid execution-steps will cause terminating programs to end up in a value. Here 'value' refers to a correct program with no more possible outgoing execution steps. The description of the execution-step is called 'operational semantics'.</div><div dir="ltr" class="gmail_attr"><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">A problem with Haskell's GADTs is that it has a non-terminating type system. This makes it unclear how to answer the first question. I believe the Pico language avoids this problem by requiring more type annotations. A naive solution could be to state that any program for which the type checker does not terminate is considered incorrect, but then one would need to prove that all execution-steps preserve this property. Another solution could be to ensure there is enough type information, and carry this type information throughout the execution when describing the operational semantics, which is the approach Richard seems to take. The downside is that you are then not describing Haskell itself exactly, but a more type-annotated version of it.</div><div dir="ltr" class="gmail_attr"><br></div>For his own intermediate haskell/GADT-inspired language Pico, Richard gives those semantics in his thesis. He answers the first point by giving syntax (Fig 5.1 and 5.2) and describing typing (up to Section 5.6). For the second point, the execution steps are modeled by the rightward arrow notation (along with some context captured in sigma and gamma) in Section 5.7. If you want to quickly see how similar Pico is to Haskell, I suggest starting with the examples in Section 5.5. It contains some typical GADT examples.</div><div dir="ltr" class="gmail_attr"><br>I hope this helps, did you ask Richard ( <a href="https://richarde.dev/">https://richarde.dev/</a> ) himself yet? I did not, so I may be wrong in all of the above.</div><div dir="ltr" class="gmail_attr"><br>Best, Sebastiaan</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">On Tue, Nov 26, 2019 at 9:54 AM Xuanrui Qi <<a href="mailto:xuanrui@nagoya-u.jp">xuanrui@nagoya-u.jp</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hello all,<br>
<br>
I recently came a cross a comment by Richard Eisenberg that there's<br>
actually no specification for GADTs and creating one would be a major<br>
research project (in a GHC proposal somewhere, I recall, but I don't<br>
remember exactly where).<br>
<br>
I was wondering what exactly does Richard's comment mean. What<br>
constitutes a specification for GADTs in Haskell? I suppose typing<br>
rules and semantics are necessary; what are the major roadblocks<br>
hindering the creation of a formal specification for GADTs in Haskell?<br>
<br>
Thanks!<br>
<br>
Xuanrui<br>
<br>
-- <br>
Xuanrui Qi<br>
Graduate School of Mathematics, Nagoya University<br>
<a href="https://www.xuanruiqi.com" rel="noreferrer" target="_blank">https://www.xuanruiqi.com</a><br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div>