<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=utf-8">
<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;}
/* 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;}
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.apple-converted-space
{mso-style-name:apple-converted-space;}
p.m1767376915746529235code, li.m1767376915746529235code, div.m1767376915746529235code
{mso-style-name:m1767376915746529235code;
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.EmailStyle21
{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"><span style="font-size:12.0pt">It’s already present in the implementation, but it’s not already present in any explicitly-stated language proposal. So this proposal might be a good opportunity to fix that deficiency.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><br>
S<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"> Richard Eisenberg <rae@cs.brynmawr.edu>
<br>
<b>Sent:</b> 02 July 2018 13:23<br>
<b>To:</b> Simon Peyton Jones <simonpj@microsoft.com><br>
<b>Cc:</b> Iavor Diatchki <iavor.diatchki@gmail.com>; ghc-steering-committee@haskell.org; Joachim Breitner <mail@joachim-breitner.de><br>
<b>Subject:</b> Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Yes -- it's a property of the type. This aspect wasn't highlighted in the original proposal because it's not a change. Types *already* have this inferred/specified distinction (and have since GHC 8.0), but users can't directly access the
feature. This proposal is all about -- and only about -- concrete syntax.<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Richard<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 Jul 2, 2018, at 4:49 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
It really is not quite clear if the specificity is a property of the type itself, or the thing that has that type.<o:p></o:p></p>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">I think Richard has clarified now, right? It’s a property of a<span class="apple-converted-space"> </span><i>type</i>.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<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">
<div>
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span class="apple-converted-space"><span lang="EN-US"> </span></span><span lang="EN-US">Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>><span class="apple-converted-space"> </span><br>
<b>Sent:</b><span class="apple-converted-space"> </span>29 June 2018 19:26<br>
<b>To:</b><span class="apple-converted-space"> </span>Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>><br>
<b>Cc:</b><span class="apple-converted-space"> </span>Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>>;
<a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a>; Joachim Breitner <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>><br>
<b>Subject:</b><span class="apple-converted-space"> </span>Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}</span><o:p></o:p></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">I am supportive of accepting the proposal, but I think that we should address the point raised by Joachim on the the git-hub thread first (<a href="https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F99%23issuecomment-401060976&data=02%7C01%7Csimonpj%40microsoft.com%7C895db05b58cc4765bd7808d5ddedc70f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636658935675847308&sdata=FqRb6%2F0hnMfQ8Bx%2BRtJdlR9VTe5Dk%2Bx6wjlin5x9x5s%3D&reserved=0"><span style="color:purple">https://github.com/ghc-proposals/ghc-proposals/pull/99#issuecomment-401060976</span></a>).
It really is not quite clear if the specificity is a property of the type itself, or the thing that has that type.<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <o:p></o:p></p>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <o:p></o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">On Thu, Jun 28, 2018 at 1:07 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com"><span style="color:purple">simonpj@microsoft.com</span></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-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">I’m keen on this proposal. I am very keen to be able to express in a type or kind signature everything needful to use the value (or type constructor). The proposal gives an example at the term level. It’d
be strengthened by an example at the type level. Eg</span><o:p></o:p></p>
</div>
<p class="m1767376915746529235code">type T1 :: forall {k}. (k->Type) -> k -> Type<o:p></o:p></p>
<p class="m1767376915746529235code">data T1 f a = MkT (f a)<o:p></o:p></p>
<p class="m1767376915746529235code"> <o:p></o:p></p>
<p class="m1767376915746529235code">type T2 :: forall k. (k->Type) -> k -> Type<o:p></o:p></p>
<p class="m1767376915746529235code">data T2 f (a::k) = MkT2 (f a)<o:p></o:p></p>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Here T1 has an inferred kind variable, mentioned nowhere in the declaration. The kind signature (which I have written as if it were code, which is the subject of a separate proposal) is inferred as shown.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">T2 mentions k, so its kind signature looks a bit different.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">What’s the difference? It’s exactly in explicit kind application. You can write (T1 @Type Maybe Int), but T2 can’t have that explicit kind argument.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">The whole business of Required/Specified/Inferred is more complicated than I like, but if we have it (which we do right now) we should allow the programmer to specify exactly what they mean.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">(An alternative is to abolish the Specified/Inferred distinction, but that carries significant costs of its own and no one is proposing it.)</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Let’s accept!</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<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">
<div>
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span class="apple-converted-space"><span lang="EN-US"> </span></span><span lang="EN-US">Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank"><span style="color:purple">rae@cs.brynmawr.edu</span></a>><span class="apple-converted-space"> </span><br>
<b>Sent:</b><span class="apple-converted-space"> </span>28 June 2018 05:45<br>
<b>To:</b><span class="apple-converted-space"> </span>Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank"><span style="color:purple">iavor.diatchki@gmail.com</span></a>><br>
<b>Cc:</b><span class="apple-converted-space"> </span>Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank"><span style="color:purple">simonpj@microsoft.com</span></a>>;<span class="apple-converted-space"> </span><a href="mailto:ghc-steering-committee@haskell.org" target="_blank"><span style="color:purple">ghc-steering-committee@haskell.org</span></a>;
Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank"><span style="color:purple">mail@joachim-breitner.de</span></a>></span><o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<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">
<div>
<p class="MsoNormal"><span lang="EN-US"><br>
<b>Subject:</b><span class="apple-converted-space"> </span>Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}</span><o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">But we morally *do* have explicit kind application. See accepted proposal <a href="https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0015-type-level-type-applications.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=%2B7wS%2F75AielivG1KfFAzGPXKSS5aHOtEVwy9Q6WyYLU%3D&reserved=0" target="_blank"><span style="color:purple">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-type-level-type-applications.rst</span></a>
So the only reason that we don't have it is that GHC hasn't caught up to its specification. (I have a student working on this now.)<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">The reason that T2 and T3 are different here is that T2 mentions the k in the type declaration, while T3 mentions it only in the constructor declaration.<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Richard<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal">On Jun 26, 2018, at 6:52 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank"><span style="color:purple">iavor.diatchki@gmail.com</span></a>> wrote:<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal">Hello,<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal">thanks for the revisions---I read through the new version, and I think I almost understand the plan. I would say that for this proposal it makes more sense to just deal with explicit specificities at the value level, and never have the
curly braces in type constructors. Since we don't have an explicit kind application at the type level (e.g., we can't write `Proxy @Type`), I don't think it really makes sense to add the braces to type constructors. If we ever implemented THAT feature,
then we can discuss which declarations should have explicit and which should have implicit parameters. In the current set of examples, I find it odd that `T2` does not have braces, but `T3` does.<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">-Iavor<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal">On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank"><span style="color:purple">rae@cs.brynmawr.edu</span></a>> wrote:<o:p></o:p></p>
</div>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal">I have posted the new proposal, at <a href="https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F148&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=RQ4V%2FWdRz009o6sieAUpx7wQ6RCqWydsQGbENvHFZfM%3D&reserved=0" target="_blank"><span style="color:purple">https://github.com/ghc-proposals/ghc-proposals/pull/148</span></a><o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">I've also updated #99 to clarify where the new syntax is allowed.<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">For Iavor's examples: <o:p></o:p></p>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<p class="MsoNormal">data T1 a = C1 a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">type T1 :: Type -> Type<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">C1 :: forall a. a -> T1 a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<p class="MsoNormal">data T2 (a :: k) = C2 { f2 :: Proxy a }<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">type T2 :: forall k. k -> Type<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">C2 :: forall k (a :: k). Proxy a -> T2 a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">f2 :: forall k (a :: k). T2 a -> Proxy a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<p class="MsoNormal">data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">type T3 :: forall {k}. k -> Type<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">C3 :: forall k (a :: k). Proxy a -> T3 a<o:p></o:p></p>
</div>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<p class="MsoNormal">data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">type T4 :: forall {k}. k -> Type<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">C4 :: forall {k} (a :: k). Proxy a -> T3 a<o:p></o:p></p>
</div>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<p class="MsoNormal">data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">> data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">we would get<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">type T5 :: forall k -> k -> Type<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">C5 :: forall k (a :: k). Proxy a -> T5 k a<o:p></o:p></p>
</div>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<p class="MsoNormal">data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Rejected, like T6. If we revise to:<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">> data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">we get<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">type T6 :: forall k -> k -> Type<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">C6 :: forall {k} (a::k). Proxy a -> T6 k a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">I've updated the proposal itself to include these examples.<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Does this help to clarify?<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Richard<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal">On May 25, 2018, at 1:56 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank"><span style="color:purple">iavor.diatchki@gmail.com</span></a>> wrote:<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal">Hello,<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes
are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all
names introduced.<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal">data T1 a = C1 a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">data T2 (a :: k) = C2 { f2 :: Proxy a }<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a<o:p></o:p></p>
</div>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">-Iavor<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal">On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank"><span style="color:purple">simonpj@microsoft.com</span></a>> wrote:<o:p></o:p></p>
</div>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">I’m keen to get #99 into GHC in some form. </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t.
For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down.</span><o:p></o:p></p>
</div>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal">based on the discussion so far, it seems that #99 in its current form might not be exactly what we want<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
</div>
</div>
<div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Can you summarise the reasons it might not be exactly what we want?</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
</div>
<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">
<div>
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span class="apple-converted-space"><span lang="EN-US"> </span></span><span lang="EN-US">ghc-steering-committee <<a href="mailto:ghc-steering-committee-bounces@haskell.org" target="_blank"><span style="color:purple">ghc-steering-committee-bounces@haskell.org</span></a>><span class="apple-converted-space"> </span><b>On
Behalf Of<span class="apple-converted-space"> </span></b>Richard Eisenberg<br>
<b>Sent:</b><span class="apple-converted-space"> </span>24 May 2018 21:17<br>
<b>To:</b><span class="apple-converted-space"> </span>Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank"><span style="color:purple">iavor.diatchki@gmail.com</span></a>><br>
<b>Cc:</b><span class="apple-converted-space"> </span><a href="mailto:ghc-steering-committee@haskell.org" target="_blank"><span style="color:purple">ghc-steering-committee@haskell.org</span></a>; Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank"><span style="color:purple">mail@joachim-breitner.de</span></a>><br>
<b>Subject:</b><span class="apple-converted-space"> </span>Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}</span><o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do
next week.<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Richard<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal">On May 24, 2018, at 1:54 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank"><span style="color:purple">iavor.diatchki@gmail.com</span></a>> wrote:<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal">Hello,<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation
for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time?<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">-Iavor<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal">On Sat, May 5, 2018 at 8:48 PM Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank"><span style="color:purple">mail@joachim-breitner.de</span></a>> wrote:<o:p></o:p></p>
</div>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">Hi,<br>
<br>
Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:<br>
> Joachim, you are always a fount of interesting ideas.<br>
><span class="apple-converted-space"> </span><br>
> > On May 2, 2018, at 2:51 PM, Joachim Breitner <mail@joachim-breitner<br>
> > .de> wrote:<br>
> ><span class="apple-converted-space"> </span><br>
> > class C k (a : k) where meth :: a<br>
> > meth :: forall {k} a. C k a -> k -> Constraint<br>
><span class="apple-converted-space"> </span><br>
> I think this is brilliant. But not only for this proposal! Imagine<br>
> this:<br>
><span class="apple-converted-space"> </span><br>
> class Num a where<br>
> fromInteger :: Integer -> a<br>
><span class="apple-converted-space"> </span><br>
> fromInteger :: Integer -> forall a. Num a => a<br>
><span class="apple-converted-space"> </span><br>
> If we do that, then #129 is essentially solved, at no further cost to<br>
> anyone. (Note that in all Haskell98-style code, no one will ever be<br>
> able to notice the changed type of fromInteger.)<br>
><span class="apple-converted-space"> </span><br>
> This approach also allows for the possibility of reordering<br>
> quantified type variables for Haskell98-style constructors, if anyone<br>
> should want to do it.<br>
><span class="apple-converted-space"> </span><br>
> And it allows for updated types (including quantified variable<br>
> ordering, etc.) for record selectors.<br>
><span class="apple-converted-space"> </span><br>
> And it allows (maybe?) for giving good types to GADT record<br>
> selectors:<br>
><span class="apple-converted-space"> </span><br>
> data X a where<br>
> Foo :: { bar :: Int } -> X Int<br>
> Quux :: { bar :: Bool } -> X Bool<br>
> bar :: X a -> a<br>
><span class="apple-converted-space"> </span><br>
> GHC currently rejects the declaration for X, but it could be accepted<br>
> if only we could specify the correct type of bar. And now we can. I<br>
> don't particularly want to cook up the typing rules here, but I don't<br>
> think I'm totally crazy.<br>
><span class="apple-converted-space"> </span><br>
> GADT record selectors aside, the rule for these could be that the<br>
> top-level type signature must be equivalent w.r.t. the subtype<br>
> relation with the original type signature. That is, if the new<br>
> signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy<br>
> enough to check for. The implementation would probably do a little<br>
> worker/wrapper stunt.<br>
<br>
I smell a new proposal… what does this mean for #99? Will you want to<br>
revise it?<br>
<br>
Cheers,<br>
Joachim<br>
--<span class="apple-converted-space"> </span><br>
Joachim Breitner<br>
<span class="apple-converted-space"> </span><a href="mailto:mail@joachim-breitner.de" target="_blank"><span style="color:purple">mail@joachim-breitner.de</span></a><br>
<span class="apple-converted-space"> </span><a href="https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0" target="_blank"><span style="color:purple">http://www.joachim-breitner.de/</span></a><br>
_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank"><span style="color:purple">ghc-steering-committee@haskell.org</span></a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" target="_blank"><span style="color:purple">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</span></a><o:p></o:p></p>
</div>
</blockquote>
</div>
<div>
<p class="MsoNormal">_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank"><span style="color:purple">ghc-steering-committee@haskell.org</span></a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" target="_blank"><span style="color:purple">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</span></a><o:p></o:p></p>
</div>
</div>
</blockquote>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</blockquote>
</div>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
</body>
</html>