The GADT debate

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

The GADT debate

wren romano-2
Hi all,

There's been some discussion about whether to consider including GADTs
in the new report, but it's been mixed up with other stuff in the
thread on incorporating extensions wholesale, which has unfortunately
preempted/preceded the discussion about how to go about having such
discussions(!).

My position on the debate is that we should avoid having the debate,
just yet. (Which I intended but failed to get across in the email
which unintentionally started this all off.) I think we have many much
lower-hanging fruit and it'd be a better use of our time to try and
get those squared away first. Doing so will help us figure out and
debug the process for having such debates, which should help the GADT
debate itself actually be fruitful. As well as making progress on
other fronts, so we don't get mired down first thing.

Whenever the debate occurs, here's a summary of the relevant emails so
that they are not lost, buried in the emails of time:


* Andres Löh puts forth criteria on how to judge whether extensions
should be included. Mentions GADTs as an example of something that, if
we decide they're a good idea in principle (criterion #1), then we
should work towards things which will help them be easier to
feasibly/sensibly specify (criterion #2)

    https://mail.haskell.org/pipermail/haskell-prime/2016-May/004104.html

* wren agrees with the criteria, loves GADTs, thinks they do not fully
satisfy criterion #2

    https://mail.haskell.org/pipermail/haskell-prime/2016-May/004115.html

* Simon Peyton Jones says type inference for GADTs has, in fact,
stabilized. Albeit, not entirely satisfactory because it's "a bit
operational"

    https://mail.haskell.org/pipermail/haskell-prime/2016-May/004119.html

* Henrik Nilsson thinks GADTs are one of the most important extensions
to Haskell (fwiw, wren agrees). Also worries about being able to
specify type inference declaratively.

    https://mail.haskell.org/pipermail/haskell-prime/2016-May/004120.html

* Dominique Devriese suggests including MonoLocalBinds, finds "let
should not be generalized" convincing

    https://mail.haskell.org/pipermail/haskell-prime/2016-May/004117.html

* wren finds "let should not be generalized" unconvincing

    https://mail.haskell.org/pipermail/haskell-prime/2016-May/004145.html

--
Live well,
~wren
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

Gershom Bazerman
On May 7, 2016 at 10:30:05 PM, wren romano ([hidden email]) wrote:

> Hi all,
>  
> There's been some discussion about whether to consider including GADTs
> in the new report, but it's been mixed up with other stuff in the
> thread on incorporating extensions wholesale, which has unfortunately
> preempted/preceded the discussion about how to go about having such
> discussions(!).
>  
> My position on the debate is that we should avoid having the debate,
> just yet. (Which I intended but failed to get across in the email
> which unintentionally started this all off.) I think we have many much
> lower-hanging fruit and it'd be a better use of our time to try and
> get those squared away first. Doing so will help us figure out and
> debug the process for having such debates, which should help the GADT
> debate itself actually be fruitful. As well as making progress on
> other fronts, so we don't get mired down first thing.

Thanks for this summary Wren. Let me add something I would be interested in seeing happen in the “meantime” — an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report). A compliant compiler could then be required to have inference “at least” that good, but also be allowed to go “above and beyond”. Thus fully portable H2020 code might require more specified signatures than we need in GHC proper, but all such code would also typecheck in GHC. It seems to me that the creation of such an algorithm might be an interesting bit of research in itself.

—Gershom
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

Carter Schonwald


On Saturday, May 7, 2016, Gershom B <[hidden email]> wrote:
On May 7, 2016 at 10:30:05 PM, wren romano (<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;wren@community.haskell.org&#39;)">wren@...) wrote:
> Hi all,
>
> There's been some discussion about whether to consider including GADTs
> in the new report, but it's been mixed up with other stuff in the
> thread on incorporating extensions wholesale, which has unfortunately
> preempted/preceded the discussion about how to go about having such
> discussions(!).
>
> My position on the debate is that we should avoid having the debate,
> just yet. (Which I intended but failed to get across in the email
> which unintentionally started this all off.) I think we have many much
> lower-hanging fruit and it'd be a better use of our time to try and
> get those squared away first. Doing so will help us figure out and
> debug the process for having such debates, which should help the GADT
> debate itself actually be fruitful. As well as making progress on
> other fronts, so we don't get mired down first thing.

Thanks for this summary Wren. Let me add something I would be interested in seeing happen in the “meantime” — an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report). A compliant compiler could then be required to have inference “at least” that good, but also be allowed to go “above and beyond”. Thus fully portable H2020 code might require more specified signatures than we need in GHC proper, but all such code would also typecheck in GHC. It seems to me that the creation of such an algorithm might be an interesting bit of research in itself.

—Gershom

I agree, there's definitely value in some research / engineering work that articulates a clear simple checker and a simple and slightly conservative inference alg , and that could pave a nice path towards gadts inclusion or at least a concrete starting point. Thanks for articulating this, I've been thinking much the same thing.  Of course the proof is in the pudding for how it works out :)


Peripherally, this also brings up the notion of type equality, and I'm a bit fuzzy about how big a chasm there is between what that means in Haskell 2010 vs more bleeding edge styles, or am I pointing at a shadows?

 
_______________________________________________
Haskell-prime mailing list
<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;Haskell-prime@haskell.org&#39;)">Haskell-prime@...
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

Richard Eisenberg-2
In reply to this post by Gershom Bazerman

On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> wrote:
>
> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).

Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:

1. The scrutinee
2. Every case branch
3. The case as a whole

With all of these type signatures in place, GADT type inference is indeed straightforward. As a strawman, I would be open to standardizing GADTs with these requirements in place and the caveat that implementations are welcome to require fewer signatures. Even better would be to do this research and come up with a good answer. I may very well be open to doing such a research project, but not for at least a year. (My research agenda for the next year seems fairly solid at this point.) If someone else wants to spearhead and wants advice / a sounding board / a less active co-author, I may be willing to join.

Richard
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

Carter Schonwald


On Sunday, May 8, 2016, Richard Eisenberg <[hidden email]> wrote:

On May 7, 2016, at 11:05 PM, Gershom B <<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;gershomb@gmail.com&#39;)">gershomb@...> wrote:
>
> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).

Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:

1. The scrutinee
2. Every case branch
3. The case as a whole

With all of these type signatures in place, GADT type inference is indeed straightforward. As a strawman, I would be open to standardizing GADTs with these requirements in place and the caveat that implementations are welcome to require fewer signatures. Even better would be to do this research and come up with a good answer. I may very well be open to doing such a research project, but not for at least a year. (My research agenda for the next year seems fairly solid at this point.) If someone else wants to spearhead and wants advice / a sounding board / a less active co-author, I may be willing to join.

Richard


This sounds awesome.  One question I'm wondering about is what parts of the type inference problem aren't part of the same challenge in equivalent dependent data types? I've been doing some Intersting stuff on the latter front recently. 

It seems that those two are closely related, but I guess there might be some complications in Haskell semantics for thst? And or is this alluded to in existing work on gadts?

 
_______________________________________________
Haskell-prime mailing list
<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;Haskell-prime@haskell.org&#39;)">Haskell-prime@...
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

Iavor Diatchki
Hello,

what is the state with the semantic specification of GADTs?  I am wondering if they fit in the usual CPO-style semantics for Haskell, or do we need some more exotic mathematical structure to give semantics to the language.

-Iavor




On Sun, May 8, 2016 at 8:36 AM, Carter Schonwald <[hidden email]> wrote:


On Sunday, May 8, 2016, Richard Eisenberg <[hidden email]> wrote:

On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> wrote:
>
> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).

Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:

1. The scrutinee
2. Every case branch
3. The case as a whole

With all of these type signatures in place, GADT type inference is indeed straightforward. As a strawman, I would be open to standardizing GADTs with these requirements in place and the caveat that implementations are welcome to require fewer signatures. Even better would be to do this research and come up with a good answer. I may very well be open to doing such a research project, but not for at least a year. (My research agenda for the next year seems fairly solid at this point.) If someone else wants to spearhead and wants advice / a sounding board / a less active co-author, I may be willing to join.

Richard


This sounds awesome.  One question I'm wondering about is what parts of the type inference problem aren't part of the same challenge in equivalent dependent data types? I've been doing some Intersting stuff on the latter front recently. 

It seems that those two are closely related, but I guess there might be some complications in Haskell semantics for thst? And or is this alluded to in existing work on gadts?

 
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

wren romano-2
In reply to this post by Richard Eisenberg-2
On Sun, May 8, 2016 at 11:25 AM, Richard Eisenberg <[hidden email]> wrote:

> On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> wrote:
>>
>> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).
>
> Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:
>
> 1. The scrutinee
> 2. Every case branch
> 3. The case as a whole
>
> With all of these type signatures in place, GADT type inference is indeed straightforward.

If all three of those signatures are present, doesn't that make
"inference" trivial? If I understand you correctly, the only thing to
do here would be to check the types, right?

I am curious though. Since we don't have true/anonymous type-level
functions, why do we need the signatures on every branch (assuming the
scrutinee and whole-expression types are given)? I can see why they'd
be required in Coq/Agda/etc, but it's less clear why they'd be
required in Haskell per se

--
Live well,
~wren
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: The GADT debate

wren romano-2
In reply to this post by Carter Schonwald
On Sun, May 8, 2016 at 1:38 AM, Carter Schonwald
<[hidden email]> wrote:
> Peripherally, this also brings up the notion of type equality, and I'm a bit
> fuzzy about how big a chasm there is between what that means in Haskell 2010
> vs more bleeding edge styles, or am I pointing at a shadows?

Generally speaking, notions of "equality" are a major source of
complication in any dependently typed theory. The issue isn't coming
up with a story that works, but rather choosing between a number of
different stories each of which works in slightly different ways. This
problem of "equality" is the bulk of why I think it'd be good to
postpone the GADT (and TypeFamily) debate.

One Haskell-specific example of why defining equality is hard is when
we try to handle both the "equalities" induced by dependent
case-analysis as well as the "equalities" induced by newtype
definitions. Though we use the same word for them, they're two
entirely different notions of "equality". However, since they both
exist, we must have some story for how these two notions interact with
one another (including possibly "not at all"). The new role-typing
stuff is one approach to handling this, but many people feel it's
overly complicated or otherwise not quite the right way forward. If we
add GADTs to the report, then we also need to define how to type check
dependent case-analysis, which seems to require introducing type
equality, which in turn requires specifying how the semantic notion of
type equality interacts with the operational notion of representation
equality introduced by newtypes, which is still imo an open area of
research.

If we can come up with some story that lets us make progress towards
eventually including GADTs (and TypeFamilies) while avoiding the
equality tarpit, I'm all for it. I'd just really rather avoid the
tarpit until we have other easier things squared away.

...

One possible way forward may be to introduce the syntax for (~)
constraints and defining them merely as "delayed unification
constraints". This would require including unification in the report,
but may be doable in a way that allows non-unification-based
implementations as well.

The reason I bring this possibility up now is that it helps handle
some other situations where we don't even have GADTs or TypeFamilies.
In particular, when FlexibleInstances is enabled it allows for
non-linear use of type variables in the instance head. However, this
is often not what we mean since "instance Foo (Bar i i)" means that
the two parameters to Bar must be unified *prior* to selecting that
instance; which often leads to type inference issues since we can't
resolve the instance eagerly enough. Whereas, often times what is
actually desired is "instance (i ~ j) => Foo (Bar i j)" which causes
us to select the instance immediately if the type constructor is Bar,
and then *after* committing to the instance we then try to unify the
two parameters. Thus, adding delayed unification constraints would be
helpful for adding (something like) FlexibleInstances to the report.
Of course, "delayed unification constraints" don't have any sort of
evidence associated with them like the dependent case-analysis
equalities do; so, again, we'd want to make sure to phrase things in
such a way that we don't prematurely commit to more than we intend.

--
Live well,
~wren
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

RE: The GADT debate

Augustsson, Lennart
In reply to this post by Richard Eisenberg-2
Do you really need that many type signatures?  I remember trying to work out what extra information is needed when type checking case with dependent types.  If memory serves, you can get by with just specifying the single (type) function that is instantiated in each arm and in the conclusion.  Maybe something similar is possible here.

       

-----Original Message-----
From: Haskell-prime [mailto:[hidden email]] On Behalf Of Richard Eisenberg
Sent: 08 May 2016 16:25
To: Gershom B
Cc: [hidden email] List
Subject: Re: The GADT debate


On May 7, 2016, at 11:05 PM, Gershom B <[hidden email]> wrote:
>
> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).

Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:

1. The scrutinee
2. Every case branch
3. The case as a whole

With all of these type signatures in place, GADT type inference is indeed straightforward. As a strawman, I would be open to standardizing GADTs with these requirements in place and the caveat that implementations are welcome to require fewer signatures. Even better would be to do this research and come up with a good answer. I may very well be open to doing such a research project, but not for at least a year. (My research agenda for the next year seems fairly solid at this point.) If someone else wants to spearhead and wants advice / a sounding board / a less active co-author, I may be willing to join.

Richard
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

This email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please delete all copies and notify the sender immediately. You may wish to refer to the incorporation details of Standard Chartered PLC, Standard Chartered Bank and their subsidiaries at http://www.standardchartered.com/en/incorporation-details.html

Insofar as this communication contains any market commentary, the market commentary has been prepared by sales and/or trading desk of Standard Chartered Bank or its affiliate. It is not and does not constitute research material, independent research, recommendation or financial advice. Any market commentary is for information purpose only and shall not be relied for any other purpose, and is subject to the relevant disclaimers available at http://wholesalebanking.standardchartered.com/en/utility/Pages/d-mkt.aspx

Insofar as this e-mail contains the term sheet for a proposed transaction, by responding affirmatively to this e-mail, you agree that you have understood the terms and conditions in the attached term sheet and evaluated the merits and risks of the transaction. We may at times also request you to sign on the term sheet to acknowledge in respect of the same.

Please visit http://wholesalebanking.standardchartered.com/en/capabilities/financialmarkets/Pages/doddfrankdisclosures.aspx for important information with respect to derivative products.
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime