A Specification for GADTs in Haskell?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

A Specification for GADTs in Haskell?

Xuanrui Qi-2
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.
Reply | Threaded
Open this post in threaded view
|

Re: A Specification for GADTs in Haskell?

Vanessa McHale-2
A spec would be something in the spirit of the Haskell2010 perhaps? Typing rules written up, plus the syntax, plus specification for pattern matching.

Cheers,
Vanessa McHale

> On Nov 26, 2019, at 8:54 AM, Xuanrui Qi <[hidden email]> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A Specification for GADTs in Haskell?

Sebastiaan Joosten-2
In reply to this post by Xuanrui Qi-2
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 <[hidden email]> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A Specification for GADTs in Haskell?

Richard Eisenberg-5
In reply to this post by Xuanrui Qi-2
Hi Xuanrui,

Glad you're interested in pursuing this topic!

By specification, I mean that it should be possible to write down a set of (simple... or simple-ish) rules describing A) what programs are accepted by the compiler, and B) what will happen when these programs are run. (A) is called either typing rules or static semantics; (B) is called operational or dynamic semantics (or sometimes just semantics).

The problem with GADTs is that we don't have that set of rules, at least not for Haskell's realization of GADTs. There is some work on this area:

* GHC's type system and inference algorithm are well documented in https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf  This paper lays out an overly-permissive set of rules for when GADTs should be accepted, but some programs are rejected that the rules suggest would be accepted.

* These two papers describe type inference with GADTs: https://dl.acm.org/citation.cfm?id=2837665 and https://dl.acm.org/citation.cfm?id=3290322. Neither is applicable to Haskell out-of-the-box.

While I'm grateful to anyone who braves my thesis, it does not really address this problem, focusing much more on the internal language than on type inference. I suppose you could extract something from Chapter 6 (on type inference), but there are key bits missing there -- notably, any specification of a solver.

I hope this is helpful -- happy to expand on this if you like!

Richard

On Nov 26, 2019, at 2:54 PM, Xuanrui Qi <[hidden email]> 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.


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