[Haskell-cafe] A Specification for GADTs in Haskell?

[Sebastiaan Joosten]

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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191126/6b1ef806/attachment.html>