<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Feb 19, 2019, at 2:01 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">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:<div class=""><br class=""></div><div class=""> 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:</div><div class=""> </div><div class=""> f1 :: (a,b) -> a -- first type param is `a`?</div><div class=""> f2 :: Ord b => a -> b -> a -- first type param is `b`?</div><div class=""> type T a b = (b,a)</div><div class=""> f3 :: T a b -> a -- first type param is?</div><div class=""> </div><div class=""> This approach seems quite fragile.</div></div></div></blockquote><div><br class=""></div><div>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://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application" class="">https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application</a></div><div><br class=""></div><div>These points have actually been refined in HEAD. You can view the documentation source here: <a href="https://github.com/ghc/ghc/blob/master/docs/users_guide/glasgow_exts.rst#L10800" class="">https://github.com/ghc/ghc/blob/master/docs/users_guide/glasgow_exts.rst#L10800</a></div><div><br class=""></div><div>In answer to your examples:</div><div><br class=""></div><div>f1: a, b</div><div>f2: b, a</div><div>f3: a, b</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class=""> 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.</div></div></div></blockquote><div><br class=""></div><div>Good point.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class=""> 3. There are some things that you can write with the `forall` notation, that you cannot write using this notation. For example:</div><div class=""><br class=""></div><div class=""> f3 :: forall a. Bool</div><div class=""> f3 = null ([] :: [a])</div><div class=""><br class=""></div><div class=""> Clearly this example is a bit contrived, but still it illustrates a problem.</div></div></div></blockquote><div><br class=""></div><div>You can still write `f3 @a = null ([] :: [a])`. </div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">As is, I am not sure what we are getting over ScopedTypeVariables. Am I missing something here?</div></div></div></blockquote><div><br class=""></div><div>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:</div><div><pre class=""><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>
higherRank <span class="pl-k">=</span> <span class="pl-k">...</span>
</pre><div class=""><pre class="">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>))</pre><div class="">The alternative would be to write</div></div><div class=""><br class=""></div><div class=""><pre class="">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></pre><div class="">just to bring the `a` into scope.</div></div><div class=""><br class=""></div><div class="">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://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-459430140" class="">https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-459430140</a> and <a href="https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-460333687" class="">https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-460333687</a> which outline use-cases that would benefit from this new treatment.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Richard</div></div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">-Iavor</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""> </div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""> </div><div class=""><br class=""></div><div class=""><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Feb 19, 2019 at 10:28 AM Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" class="">iavor.diatchki@gmail.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr" class=""><div dir="ltr" class="">Hello,<div class=""><br class=""></div><div class="">let's get the discussion going about proposal #155 (<a href="https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst" target="_blank" class="">https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst</a>).</div><div class=""><br class=""></div><div class="">Summary:</div><div class="">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").</div><div class=""><br class=""></div><div class="">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 :)</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">What does everyone else thing?</div><div class=""><br class=""></div><div class="">-Iavor </div></div></div>
</blockquote></div>
_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<br class=""></div></blockquote></div><br class=""></body></html>