<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:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@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.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
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;}
p.m-6816630248007688217msolistparagraph, li.m-6816630248007688217msolistparagraph, div.m-6816630248007688217msolistparagraph
{mso-style-name:m_-6816630248007688217msolistparagraph;
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;}
/* List Definitions */
@list l0
{mso-list-id:451755832;
mso-list-type:hybrid;
mso-list-template-ids:-183044320 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:974482998;
mso-list-template-ids:-801603622;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2
{mso-list-id:1801415419;
mso-list-template-ids:-75353504;}
@list l2:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l2:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3
{mso-list-id:1917667018;
mso-list-template-ids:-479198444;}
@list l3:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></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">RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared<o:p></o:p></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">I’m not very comfortable with this. The obvious alternative is to make them behave exactly the same. Why did you discard that?<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">In any case this applies solely to H98 data type decls, and class decls. For GADT-style decls we give a complete standalone type sig for the constructor.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">In any case, I’ve lost track of the details here. Might you revise the proposal, incorporating
<o:p></o:p></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo4"><span style="font-size:12.0pt">some of the motivations articulated on this thread (eg by me
</span><span style="font-family:"Segoe UI Emoji",sans-serif">😊</span><span style="font-size:12.0pt">)
<o:p></o:p></span></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo4"><span style="font-size:12.0pt">some of the illustrative examples herein<o:p></o:p></span></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo4"><span style="font-size:12.0pt">what is not covered [I think stuff to do with data type decls?]<o:p></o:p></span></li></ul>
<p class="MsoNormal"><span style="font-size:12.0pt">Then we can take a fresh run at it.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon<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 May 2018 03:06<br>
<b>To:</b> Iavor Diatchki <iavor.diatchki@gmail.com><br>
<b>Cc:</b> Simon Peyton Jones <simonpj@microsoft.com>; ghc-steering-committee@haskell.org<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>
<div>
<div>
<p class="MsoNormal">The proposal, as written, affects only type signatures and class declarations. It does not cover datatype declarations, though perhaps it should. This seems to be an oversight.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">A key problem with this notation in type declarations is that H98-syntax datatype and class declarations do two things: they create a new type and they also inform the types of term-level definitions. In the case of a datatype, the terms
are the constructors; in the case of a class, the terms are the methods.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Suppose we want to make term-level definitions suppress a certain variable but not to suppress this variable in the type definition? For example, perhaps we want data Proxy k (a :: k) = P, where Proxy :: forall k -> k -> Type, but P ::
forall {k} (a :: k). Proxy k a. Note the different visibilities at the different levels.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">We can boil it down to one rule for these situations:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">With this in mind, I'll answer the questions below:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">On May 1, 2018, at 12:56 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>> wrote:<o:p></o:p></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">-- 1) The "normal" case. I've written the types of the introduces names underneath, are they correct?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">data T1 {k} (a :: k) = C1</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">-- T1 :: forall {k::Type}. k -> Type</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">-- C1 :: forall {k::Type} (a :: k). T1 {k} a</span><o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I would say we get<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">T1 :: forall (k :: Type) -> k -> Type -- T1 has *2* visible arguments<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">C1 :: forall {k :: Type} (a :: k). T1 k a -- C1 has one inferred and one specified type argument<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal">-- Am I correct in assuming that while GHC could print the types like that, but users are not allowed to actually write those types (i.e., `T1 {k} (a::k)` is not a valid type).<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">GHC will print braces only around inferred-variable binding sites, not usage sites. If we wanted k not to be visible in the kind of T1, then one comment on the thread proposed<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">data T1' @k (a :: k) = C1'<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">which would yield<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">T1' :: forall (k :: Type). k -> Type<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">C1' :: forall (k :: Type) (a :: k). T1' a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I imagine we could combine the two, so that<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">data T1'' @{k} (a :: k) = C1''<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">would yield<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">T1'' :: forall (k :: Type). k -> Type<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">C1'' :: forall {k :: Type} (a :: k). T1'' a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Under this idea, there would be no way to get k to be *inferred* in the type's kind. A top-level kind signature (#54) would be necessary.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Note that the extensions discussed here, with @, are *not* part of this proposal, but might be a future one.<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) Can GHC add extra inferred parameters? (This examples assumes `PolyKinds`)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">data T2 {k} a = C2</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">-- C2 :: forall {k1::Type} {k::Type} (a :: k1). T2 {k1} {k} a (ambiguous?)</span><o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I get<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">T2 :: forall {x :: Type} {y :: Type}. x -> y -> Type<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">C2 :: forall {x :: Type} {y :: Type} {k :: x} (a :: y). T2 k a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">This is not an ambiguous type, because all the variables are determined by the (injective) result type.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">So, in answer to your question: yes.<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) Can we infer non-kind types?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">data T3 {a} = C3 a</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">-- C3 :: forall {a::Type}. a -> T3 {a}</span><o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I get<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">T3 :: Type -> Type<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">C3 :: forall {a :: Type}. a -> T3 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 question: yes.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<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">-- 4) If `T3` is OK, how does "inferring" work in signatures? To make things concrete, would the following be accepted?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">f :: T3</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">f = C3 True </span><o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal">-- A): not, because the signature is really: `forall {a}. T3 {a}`.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">-- B): yes, because we are going to infer that the missing type is `Bool`, so the signature becomes `T3 {Bool}`.<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">C) not, because T3 still has a visible argument, and therefore T3 has kind `Type -> Type`, which is inappropriate for a type signature.<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">-- 5) The proposal has a class, something like this:<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">class C a {b} where<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> meth1 :: a -> b<o:p></o:p></span></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">-- How do I write an instance for this class?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">-- A)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">instance C Int where</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> meth1 x = x </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">-- B)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">instance C Int {Int} where</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> meth1 x = x</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I imagine the answer is A) is I see nothing about writing types like `{Int}`. If so, here are a couple of follow up questions about instances:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Neither. I would write<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">instance C Int Int where<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> meth1 x = x<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">The braces in the type declaration affect only the term-level definitions therein, not the type definition, according to RULE.<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">-- Valid?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">instance C Int where</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> meth1 x = []</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">-- instance is really `forall {a::Type}. C Int {[a]}` ?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">instance C Int where</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> meth1 x = return x</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">--- error, instance is `C Int {m Int}`, but no `Monad` constraint.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">-- There doesn't seem to be a way to write the instance with the constraint?<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">These are not valid.<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">Sorry for the long e-mail, but I hope that these examples might bring some clarity to users of the proposed feature.<o:p></o:p></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">These questions are really helpful in poking at the squishy spots! Thanks.<o:p></o:p></p>
</div>
<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>
<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">On Tue, May 1, 2018 at 3:55 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.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" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt">[Redirecting to the steering committee]</span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt">I argue for acceptance.</span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
<ul type="disc">
<li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l2 level1 lfo1">
<span style="font-size:12.0pt">For me a compelling motivation is this: at the moment
<i>we can infer types and kinds that we cannot write down with an explicitly-quantified type signature</i>. That seems all wrong to me: we should be able to write down any type you can infer.</span><o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l2 level1 lfo1">
<span style="font-size:12.0pt">The proposal adds <i>notation</i>. It does <i>not</i> add semantics. We already have the distinction between “inferred” and “specified” type variables. You might not like it, but it’s there in GHC.
</span><o:p></o:p></li></ul>
<ul type="disc">
<ul type="circle">
<li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l2 level2 lfo1">
<span style="font-size:12.0pt">If it wasn’t there already, I’d be happy to debate not adding it.
</span><o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l2 level2 lfo1">
<span style="font-size:12.0pt">If you want to argue for removing the distinction, that would certainly render the current proposal moot. But that would take a GHC proposal – and there are good reasons for the status quo!</span><o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l2 level2 lfo1">
<span style="font-size:12.0pt">What is bad is to maintain the semantic distinction, but be unable to express it. That’s what we have right now, and it’s a bad thing.</span><o:p></o:p></li></ul>
</ul>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt">What is the distinction between “specified” and “inferred”?</span><o:p></o:p></p>
<ul type="disc">
<li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l3 level1 lfo2">
<b><span style="font-size:12.0pt">Specified. f :: forall a. blah, or f :: a -> a.</span></b><span style="font-size:12.0pt">
</span><o:p></o:p></li></ul>
<p class="m-6816630248007688217msolistparagraph"><span style="font-size:12.0pt">You may give a visible type argument at a call of f, but you do not have to. Thus (f x) or (f @type x).</span><o:p></o:p></p>
<p class="m-6816630248007688217msolistparagraph"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
<ul type="disc">
<li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo3">
<b><span style="font-size:12.0pt">Inferred</span></b><span style="font-size:12.0pt">.
<b>f :: t a -> t a.</b> The type of f is really</span><o:p></o:p></li></ul>
<p class="m-6816630248007688217msolistparagraph" style="margin-left:72.0pt"><span style="font-size:12.0pt">g :: forall {k} (t :: k -> *) (a :: k). t a -> t a</span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<span style="font-size:12.0pt">Note that k does not appear at all in the signature; that’s why it is “inferred”. In GHC today you cannot supply an explicit kind argument for g, but you can supply explicit argument for t and a.</span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt">So by all means make the case for abolishing the distinction, to render the present proposal moot. But I think it’s unreasonably simply to reject
on the grounds of “please think of something better”.</span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt"> </span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt">Simon</span><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:12.0pt"> </span><o:p></o:p></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" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-devs <<a href="mailto:ghc-devs-bounces@haskell.org" target="_blank">ghc-devs-bounces@haskell.org</a>>
<b>On Behalf Of </b>Iavor Diatchki<br>
<b>Sent:</b> 30 April 2018 17:12<br>
<b>To:</b> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<b>Subject:</b> Discussion on proposal #99: forall {k}</span><o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
<div>
<div>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> <o:p></o:p></p>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">Hello,<o:p></o:p></p>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">As a shepherd for proposal #99, I'd like to kick off the discussion. The full proposal is available here: <a href="https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fexplicit-specificity%2Fproposals%2F0000-explicit-specificity.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C91b5ba6ae508426a711b08d5afd13277%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608235390001323&sdata=2tYpwTwlWtp73a1pkWEIhIOQFnWwLufJWSDKwRkqB8g%3D&reserved=0" target="_blank">https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/proposals/0000-explicit-specificity.rst</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">Summary: allows programmers to write `forall {x}` instead of `forall x` in type signatures. The meaning of the braces is that this parameter cannot be instantiated with an explicit type
application and will always be inferred. The motivation is to shorten explicit type applications by skipping parameters that are known to be inferable, the common example being omitting the kinds in signatures with poly kinds.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">As I understand it, the main motivation for this proposals is to give programmers more flexibility when instantiating type variables, with a less noisy syntax. While the proposed solution
might work in some situations, I am unconvinced that it is the best way to address the issue in general, for the following reasons:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> 1. It requires that programmers commit at declaration time about which arguments will be inferred, and which may be inferred or specified. While in some cases this may be an easy decision
to make, in many cases this really is a decision which should be made at the use site of a function (e.g., I'd like to provide argument X, but would like GHC to infer argument Y).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> 2. It still requires that programmers instantiate arguments in a fixed order, which is sometimes dictated by the structure of the type itslef. Here is, for example, what the proposal
suggests to do if you want to provide type before a kind:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> While technically this is not wrong, it is not exactly elegant.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">I think that we should reject this proposal, and try to come up with a more comprehensive solution to the problem.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">One alternative design is to allow programmers to instantiate type variables by name. This is much more flexible as it allows programmers to instantiate whichever variables they want,
and in whatever order. We've been doing this in Cryptol for a long time, and it seems to work really well.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt">-Iavor<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:6.0pt"> <o:p></o:p></p>
</div>
</div>
</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>
</div>
</body>
</html>