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

[Simon Peyton Jones]

1. Should we allow binding type variables that are not explicitly quantified with a forall? I'm concerned about the potential for breaking code should GHC's rules for ordering quantifiers change. Does GHC already guarantee a particular ordering?



See my comments<https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-469241834> on GitHub.





2. I wonder if supporting type binders in inference mode is as hard as the proposal fears.



I think it’s hard.

              f @a x = x

we could infer any of.

              f :: forall a b. b -> b

              f :: forall a. a -> a

              f :: forall b a. b -> b



Roughly, it’s as hard as figuring out impredicative polymorphism I think.  Let’s not go there 😊.



Simon



-----Original Message-----
From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Eric Seidel
Sent: 04 March 2019 01:44
To: ghc-steering-committee at haskell.org
Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas



One argument in favor of the proposal that I don't believe I've seen mentioned is that, now that we can explicitly apply types with the @ syntax, it feels very intuitive to also bind them with the same syntax. So even if this proposal does not add much technically over ScopedTypeVariables, I think it's still a good idea.



I do have a couple of questions/comments though:



1. Should we allow binding type variables that are not explicitly quantified with a forall? I'm concerned about the potential for breaking code should GHC's rules for ordering quantifiers change. Does GHC already guarantee a particular ordering? Would we want to?



2. I wonder if supporting type binders in inference mode is as hard as the proposal fears. The alternatives section mentions the possibility of extracting a partial type signature from the LHS, but I had a simpler thought. Why not say that `\ @a -> body` infers the type `forall a. ty` where `body :: ty`, and let unification handle the rest? It seems like that would handle all of the variants of `null` in section 7, though not the example in section 3 with the equality constraint. But to be honest, I'd be ok with rejecting that program. It would be much clearer with a single type binder.



I don't think the lack of a solution for type binders in inference mode should block this proposal, but it would be much nicer if we had one! I don't want Haskell programmers to have to learn the intricacies of bidirectional type checking to use what is otherwise a very intuitive feature.



Eric





On Tue, Feb 19, 2019, at 14:01, Iavor Diatchki 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.

>

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

> >

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

> ee

>

_______________________________________________

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/20190304/36e0c4dd/attachment-0001.html>