[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas
Richard Eisenberg
rae at cs.brynmawr.edu
Thu Feb 21 18:55:05 UTC 2019
> 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>
More information about the ghc-steering-committee
mailing list