[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

[Richard Eisenberg]

> On Feb 19, 2019, at 2:01 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> 
> 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:
> 
>    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:
>              
>            f1 :: (a,b) -> a                            -- first type param is  `a`?
>            f2 :: Ord b => a -> b -> a           -- first type param is `b`?
>            type T a b = (b,a)
>            f3 :: T a b -> a                           -- first type param is?
>     
>        This approach seems quite fragile.

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: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application>

These points have actually been refined in HEAD. You can view the documentation source here: https://github.com/ghc/ghc/blob/master/docs/users_guide/glasgow_exts.rst#L10800 <https://github.com/ghc/ghc/blob/master/docs/users_guide/glasgow_exts.rst#L10800>

In answer to your examples:

f1: a, b
f2: b, a
f3: a, b

> 
>     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.

Good point.

> 
>     3. There are some things that you can write with the `forall` notation, that you cannot write using this notation.  For example:
> 
>           f3 :: forall a. Bool
>           f3 = null ([] :: [a])
> 
>         Clearly this example is a bit contrived, but still it illustrates a problem.

You can still write `f3 @a = null ([] :: [a])`. 

> 
> As is, I am not sure what we are getting over ScopedTypeVariables.  Am I missing something here?

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:
higherRank :: (forall a. a -> a -> a) -> ...
higherRank = ...
ex = higherRank (\ @a x _y -> (x :: a))
The alternative would be to write

ex = higherRank ((\ x _y -> (x :: a)) :: forall a. a -> a -> a)
just to bring the `a` into scope.

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 https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-459430140 <https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-459430140> and https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-460333687 <https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-460333687> which outline use-cases that would benefit from this new treatment.

Thanks,
Richard

> 
> -Iavor
> 
> 
>  
> 
> 
> 
> 
> 
>       
> 
> 
> 
> On Tue, Feb 19, 2019 at 10:28 AM Iavor Diatchki <iavor.diatchki at gmail.com <mailto:iavor.diatchki at gmail.com>> wrote:
> Hello,
> 
> let's get the discussion going about proposal #155 (https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst <https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst>).
> 
> Summary:
> 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").
> 
> 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 :)
> 
> 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.
> 
> What does everyone else thing?
> 
> -Iavor 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20190221/34141b5f/attachment.html>