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:[email protected]] On Behalf Of
Richard Eisenberg
Sent: 08 May 2016 16:25
To: Gershom B
Cc: [email protected] List
Subject: Re: The GADT debate
On May 7, 2016, at 11:05 PM, Gershom B <[email protected]> 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
[email protected]
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
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
