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

[Iavor Diatchki]

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.

    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.

    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.

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

-Iavor












On Tue, Feb 19, 2019 at 10:28 AM Iavor Diatchki <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
> ).
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20190219/900d4b91/attachment.html>