RE: The GADT debate

[Augustsson, Lennart]

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:haskell-prime-boun...@haskell.org] On Behalf Of 
Richard Eisenberg
Sent: 08 May 2016 16:25
To: Gershom B
Cc: haskell-prime@haskell.org List
Subject: Re: The GADT debate


On May 7, 2016, at 11:05 PM, Gershom B <gersh...@gmail.com> 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
Haskell-prime@haskell.org
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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: The GADT debate

[wren romano]

On Sun, May 8, 2016 at 1:38 AM, Carter Schonwald
 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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: The GADT debate

[wren romano]

On Sun, May 8, 2016 at 11:25 AM, Richard Eisenberg  wrote:
> On May 7, 2016, at 11:05 PM, Gershom B  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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

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  wrote:

>
>
> On Sunday, May 8, 2016, Richard Eisenberg  wrote:
>
>>
>> On May 7, 2016, at 11:05 PM, Gershom B  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
>> Haskell-prime@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>>
>
> ___
> Haskell-prime mailing list
> Haskell-prime@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
>
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: The GADT debate

[Carter Schonwald]

On Sunday, May 8, 2016, Richard Eisenberg  wrote:

>
> On May 7, 2016, at 11:05 PM, Gershom B >
> 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
> Haskell-prime@haskell.org 
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: The GADT debate

[Richard Eisenberg]

On May 7, 2016, at 11:05 PM, Gershom B  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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: The GADT debate

[Carter Schonwald]

On Saturday, May 7, 2016, Gershom B <gersh...@gmail.com> wrote:

> On May 7, 2016 at 10:30:05 PM, wren romano (w...@community.haskell.org
> <javascript:;>) 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
> Haskell-prime@haskell.org <javascript:;>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: The GADT debate

[Gershom B]

On May 7, 2016 at 10:30:05 PM, wren romano (w...@community.haskell.org) 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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

The GADT debate

[wren romano]

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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime