<div dir="ltr">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><br></div><div>   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>             </div><div>           f1 :: (a,b) -> a                            -- first type param is  `a`?</div><div>           f2 :: Ord b => a -> b -> a           -- first type param is `b`?</div><div>           type T a b = (b,a)</div><div>           f3 :: T a b -> a                           -- first type param is?</div><div>    </div><div>       This approach seems quite fragile.</div><div><br></div><div>    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><br></div><div>    3. There are some things that you can write with the `forall` notation, that you cannot write using this notation.  For example:</div><div><br></div><div>          f3 :: forall a. Bool</div><div>          f3 = null ([] :: [a])</div><div><br></div><div>        Clearly this example is a bit contrived, but still it illustrates a problem.</div><div><br></div><div>As is, I am not sure what we are getting over ScopedTypeVariables.  Am I missing something here?</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div> </div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div>      </div><div><br></div><div><br></div></div><br><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">iavor.diatchki@gmail.com</a>> wrote:<br></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"><div dir="ltr">Hello,<div><br></div><div>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">https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst</a>).</div><div><br></div><div>Summary:</div><div>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><br></div><div>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><br></div><div>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><br></div><div>What does everyone else thing?</div><div><br></div><div>-Iavor </div></div></div>
</blockquote></div>