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
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.