<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
p.Code, li.Code, div.Code
{mso-style-name:Code;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:9.0pt;
font-family:"Courier New";}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:Consolas;}
span.pl-en
{mso-style-name:pl-en;}
span.pl-k
{mso-style-name:pl-k;}
span.pl-smi
{mso-style-name:pl-smi;}
span.EmailStyle25
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;
font-weight:normal;
font-style:normal;
text-decoration:none none;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal" style="margin-left:36.0pt">In the end, this proposal does not bring in much over ScopedTypeVariables<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">So the gain is relatively small. But the pain is real: more complexity, and that’s a long-term cost.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Actually the biggest reason I like this proposal is because it takes another step in the direction of directly expressing System F in Haskell. Not so much because I expect to use it a lot but because it gives a vocabulary in which to express
what a lot of the implicit elaboration in GHC is doing. I use VTA in this way already.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">But I’m a bit on the fence overall. With finite effort cycles, we may have more important fish to fry.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Simon<span style="font-size:12.0pt"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-steering-committee <ghc-steering-committee-bounces@haskell.org>
<b>On Behalf Of </b>Richard Eisenberg<br>
<b>Sent:</b> 21 February 2019 18:55<br>
<b>To:</b> Iavor Diatchki <iavor.diatchki@gmail.com><br>
<b>Cc:</b> ghc-steering-committee <ghc-steering-committee@haskell.org><br>
<b>Subject:</b> Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">On Feb 19, 2019, at 2:01 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">After a bit more thought, I am not sure what do we get with this notation over ScopedTypeVariables. In particular, here are some things that came up as I was trying to write a couple of examples:<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> 1. The order in which variables are introduced is not clear---presumably it is some sort of left to write ordering based on the type signature. For example:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> f1 :: (a,b) -> a -- first type param is `a`?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> f2 :: Ord b => a -> b -> a -- first type param is `b`?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> type T a b = (b,a)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> f3 :: T a b -> a -- first type param is?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> This approach seems quite fragile.<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">This problem first came up (in earnest) in the context of type applications. We now specify the answer in the manual; see the first two bullet-points here: <a href="https://nam06.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23visible-type-application&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241748539&sdata=YJlqlHlyNlvU7%2FUxxo%2B6E7KhVJik8rGtCGIQGDgj%2FXQ%3D&reserved=0">https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">These points have actually been refined in HEAD. You can view the documentation source here: <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc%2Fghc%2Fblob%2Fmaster%2Fdocs%2Fusers_guide%2Fglasgow_exts.rst%23L10800&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241748539&sdata=ABm0BqcXoGe5vVfErATx3OehD9LKeojxFM8PxCqOGWI%3D&reserved=0">https://github.com/ghc/ghc/blob/master/docs/users_guide/glasgow_exts.rst#L10800</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">In answer to your examples:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">f1: a, b<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">f2: b, a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">f3: a, b<o:p></o:p></p>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> 2. The proposal says that a problem with the `forall` in ScopedTypeVariables is that the signature can be arbitrarily far away from the implementation. I agree that this is a problem, but it seems to remain a problem with this proposal,
as you have to look at the signature to see in what order you should write the parameters.<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Good point.<o:p></o:p></p>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> 3. There are some things that you can write with the `forall` notation, that you cannot write using this notation. For example:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> f3 :: forall a. Bool<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> f3 = null ([] :: [a])<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> Clearly this example is a bit contrived, but still it illustrates a problem.<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">You can still write `f3 @a = null ([] :: [a])`. <o:p></o:p></p>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">As is, I am not sure what we are getting over ScopedTypeVariables. Am I missing something here?<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">While not highlighted in the proposal, the example named `ex` binds a type variable using the new notation that would be very awkward indeed without this extension. Here is the example:<o:p></o:p></p>
</div>
<div>
<pre><span class="pl-en">higherRank</span> <span class="pl-k">::</span> (<span class="pl-k">forall</span> <span class="pl-smi">a</span><span class="pl-k">.</span> <span class="pl-smi">a</span> <span class="pl-k">-></span> <span class="pl-smi">a</span> <span class="pl-k">-></span> <span class="pl-smi">a</span>) <span class="pl-k">-></span> <span class="pl-k">...</span><o:p></o:p></pre>
<pre>higherRank <span class="pl-k">=</span> <span class="pl-k">...</span><o:p></o:p></pre>
<div>
<pre>ex <span class="pl-k">=</span> higherRank (<span class="pl-k">\</span> <span class="pl-k">@</span>a x _y <span class="pl-k">-></span> (x <span class="pl-k">::</span> <span class="pl-smi">a</span>))<o:p></o:p></pre>
<div>
<p class="MsoNormal">The alternative would be to write<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<pre>ex <span class="pl-k">=</span> higherRank ((<span class="pl-k">\</span> x _y <span class="pl-k">-></span> (x <span class="pl-k">::</span> <span class="pl-smi">a)) :: forall a. a -> a -> a)</span><o:p></o:p></pre>
<div>
<p class="MsoNormal">just to bring the `a` into scope.<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">In the end, this proposal does not bring in much over ScopedTypeVariables -- it just makes the type-variable scoping mechanism more in line with the term-variable scoping mechanism. There's nothing fundamentally new here: just convenience.
You may also want to see <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F155%23issuecomment-459430140&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241758532&sdata=MxZcEwLwkUzM%2B7OgHidINCiC1rNnaYj8nFmnWcpz%2F5E%3D&reserved=0">https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-459430140</a> and <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F155%23issuecomment-460333687&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241758532&sdata=FmRe9%2Ftd7qvXd314pAjNj%2BUX2AVAMvXtP22z57PlxZk%3D&reserved=0">https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-460333687</a> which
outline use-cases that would benefit from this new treatment.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Richard<o:p></o:p></p>
</div>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">-Iavor<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Tue, Feb 19, 2019 at 10:28 AM Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">Hello,<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">let's get the discussion going about proposal #155 (<a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Ftype-lambda%2Fproposals%2F0000-type-lambda.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241768529&sdata=azmQaoLX50D7UNWnXdpX4Vu%2Fu7MYwqTXyhu8ikSoP%2B0%3D&reserved=0" target="_blank">https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst</a>).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Summary:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">the idea is pretty simple: allow functions to name their type arguments explicitly, so that they can be used in type signatures within the function's definition. The notation for a type argument is `@a`, and such type arguments can be
used only when functions have an explicit type signature (technically, when GHC is doing "checking" rather then "inference").<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">This proposal provides an alternative to "ScopedTypeVariables" to refer to type parameters, which I think is a step in the right direction, as using the `forall` to introduce type variables always felt a bit hacky to me (now, there's a
technical argument :)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I am a bit concerned with the notation though: in other places where we use `@a`, (e.g., #126 type application in patterns, and TypeApplications) the `a` is a type, while in this use it must be a variable. I wonder if this punning might
be confusing. I don't really have an alternative suggestion though.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">What does everyone else thing?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">-Iavor <o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal">_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><o:p></o:p></p>
</div>
</blockquote>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</body>
</html>