Hi Xuanrui and Vanessa, 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 ( https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf ), but I think it's the closest thing to a semantics of GADTs there is out there right now. My guess is that what Richard means with 'having a semantics' involves answering two things: - which programs are considered 'correct' (i.e. well-typed) - 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'. 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. 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. I hope this helps, did you ask Richard ( https://richarde.dev/ ) himself yet? I did not, so I may be wrong in all of the above. Best, Sebastiaan On Tue, Nov 26, 2019 at 9:54 AM Xuanrui Qi <xuanrui@nagoya-u.jp> wrote:
Hello all,
I recently came a cross a comment by Richard Eisenberg that there's actually no specification for GADTs and creating one would be a major research project (in a GHC proposal somewhere, I recall, but I don't remember exactly where).
I was wondering what exactly does Richard's comment mean. What constitutes a specification for GADTs in Haskell? I suppose typing rules and semantics are necessary; what are the major roadblocks hindering the creation of a formal specification for GADTs in Haskell?
Thanks!
Xuanrui
-- Xuanrui Qi Graduate School of Mathematics, Nagoya University https://www.xuanruiqi.com
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.