[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas
Simon Peyton Jones
simonpj at microsoft.com
Mon Mar 4 12:56:59 UTC 2019
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>
More information about the ghc-steering-committee
mailing list