<div dir="ltr">Hello,<div><br></div><div>I just re-read the proposal and I am a bit unclear: are we proposing that we make this change only in type signatures or in all places where we bind type variables? At first I thought we are talking only about type signatures, but I noticed that the proposal seems to mention type classes, but not `data` declarations or type families. I find the "implicit" hidden parameters in those to be one of the most confusing features of GHC, so having a way to write those would certainly be useful. I do have some clarifying questions illustrated by the examples below (assuming that this extension should work on `data`):</div><div><br></div><div>-- 1) The "normal" case. I've written the types of the introduces names underneath, are they correct?</div><div><font face="monospace">data T1 {k} (a :: k) = C1</font></div><div><font face="monospace">-- T1 :: forall {k::Type}. k -> Type</font></div><div><span style="font-family:monospace">-- C1 :: forall {k::Type} (a :: k). T1 {k} a</span><br></div><div>-- 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).</div><div><br></div><div>-- 2) Can GHC add extra inferred parameters? (This examples assumes `PolyKinds`)</div><div><font face="monospace">data T2 {k} a = C2</font></div><div><font face="monospace">-- C2 :: forall {k1::Type} {k::Type} (a :: k1). T2 {k1} {k} a (ambiguous?)</font></div><div><br></div><div>-- 3) Can we infer non-kind types?</div><div><font face="monospace">data T3 {a} = C3 a</font></div><div><font face="monospace">-- C3 :: forall {a::Type}. a -> T3 {a}</font></div><div><br></div><div>-- 4) If `T3` is OK, how does "inferring" work in signatures? To make things concrete, would the following be accepted?</div><div><font face="monospace">f :: T3</font></div><div><font face="monospace">f = C3 True </font></div><div><div>-- A): not, because the signature is really: `forall {a}. T3 {a}`.</div><div>-- B): yes, because we are going to infer that the missing type is `Bool`, so the signature becomes `T3 {Bool}`.</div></div><div><br></div><div>-- 5) The proposal has a class, something like this:</div><div><font face="monospace"><div>class C a {b} where</div><div> meth1 :: a -> b</div></font></div><div><br></div><div>-- How do I write an instance for this class?</div><div>-- A)</div><div><font face="monospace">instance C Int where</font></div><div><font face="monospace"> meth1 x = x </font></div><div><font face="monospace"><br></font></div><div>-- B)</div><div><font face="monospace">instance C Int {Int} where</font></div><div><font face="monospace"> meth1 x = x</font></div><div><br></div><div>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:</div><div><br></div><div>-- Valid?</div><div><font face="monospace">instance C Int where</font></div><div><font face="monospace"> meth1 x = []</font></div><div>-- instance is really `forall {a::Type}. C Int {[a]}` ?</div><div><br></div><div><font face="monospace">instance C Int where</font></div><div><font face="monospace"> meth1 x = return x</font></div><div>--- error, instance is `C Int {m Int}`, but no `Monad` constraint.</div><div>-- There doesn't seem to be a way to write the instance with the constraint?</div><div><br></div><div>Sorry for the long e-mail, but I hope that these examples might bring some clarity to users of the proposed feature.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, May 1, 2018 at 3:55 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple">
<div class="m_-6816630248007688217WordSection1">
<p class="MsoNormal"><span style="font-size:12.0pt">[Redirecting to the steering committee]<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">I argue for acceptance.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><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.<u></u><u></u></span></li><li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><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.
<u></u><u></u></span>
<ul style="margin-top:0cm" type="circle">
<li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><span style="font-size:12.0pt">If it wasn’t there already, I’d be happy to debate not adding it.
<u></u><u></u></span></li><li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><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!<u></u><u></u></span></li><li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><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.<u></u><u></u></span></li></ul>
</li></ul>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">What is the distinction between “specified” and “inferred”?<u></u><u></u></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><b><span style="font-size:12.0pt">Specified. f :: forall a. blah, or f :: a -> a.</span></b><span style="font-size:12.0pt">
<u></u><u></u></span></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).<u></u><u></u></span></p>
<p class="m_-6816630248007688217MsoListParagraph"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="m_-6816630248007688217MsoListParagraph" style="margin-left:0cm"><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<u></u><u></u></span></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<u></u><u></u></span></p>
<p class="MsoNormal" style="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.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><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”.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></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-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}<u></u><u></u></span></p>
</div>
</div></div></div></div><div lang="EN-GB" link="blue" vlink="purple"><div class="m_-6816630248007688217WordSection1"><div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Hello,<u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
As a shepherd for proposal #99, I'd like to kick off the discussion. The full proposal is available here: <a href="https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/proposals/0000-explicit-specificity.rst" target="_blank">https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/proposals/0000-explicit-specificity.rst</a><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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).<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
While technically this is not wrong, it is not exactly elegant.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
I think that we should reject this proposal, and try to come up with a more comprehensive solution to the problem.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
-Iavor<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
</div></div></div></blockquote></div>