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

Fri Feb 22 08:05:53 UTC 2019

In the end, this proposal does not bring in much over ScopedTypeVariables

So the gain is relatively small.  But the pain is real: more complexity, and that's a long-term cost.

Actually the biggest reason I like this proposal is because it takes another step in the direction of directly expressing System F in Haskell. Not so much because I expect to use it a lot but because it gives a vocabulary in which to express what a lot of the implicit elaboration in GHC is doing.  I use VTA in this way already.

But I'm a bit on the fence overall.  With finite effort cycles, we may have more important fish to fry.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Richard Eisenberg
Sent: 21 February 2019 18:55
To: Iavor Diatchki <iavor.diatchki at gmail.com>
Cc: ghc-steering-committee <ghc-steering-committee at haskell.org>
Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

On Feb 19, 2019, at 2:01 PM, Iavor Diatchki <iavor.diatchki at gmail.com<mailto: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://nam06.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23visible-type-application&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241748539&sdata=YJlqlHlyNlvU7%2FUxxo%2B6E7KhVJik8rGtCGIQGDgj%2FXQ%3D&reserved=0>

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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc%2Fghc%2Fblob%2Fmaster%2Fdocs%2Fusers_guide%2Fglasgow_exts.rst%23L10800&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241748539&sdata=ABm0BqcXoGe5vVfErATx3OehD9LKeojxFM8PxCqOGWI%3D&reserved=0>

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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F155%23issuecomment-459430140&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241758532&sdata=MxZcEwLwkUzM%2B7OgHidINCiC1rNnaYj8nFmnWcpz%2F5E%3D&reserved=0> and https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-460333687<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F155%23issuecomment-460333687&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241758532&sdata=FmRe9%2Ftd7qvXd314pAjNj%2BUX2AVAMvXtP22z57PlxZk%3D&reserved=0> 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Ftype-lambda%2Fproposals%2F0000-type-lambda.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241768529&sdata=azmQaoLX50D7UNWnXdpX4Vu%2Fu7MYwqTXyhu8ikSoP%2B0%3D&reserved=0>).

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<mailto: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/20190222/e96c34d9/attachment-0001.html>