Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow ScopedTypeVariables to refer to types #128

Merged
merged 7 commits into from Aug 4, 2018

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented Apr 25, 2018

The proposal has been accepted; the following discussion is mostly of historic interest.


Rendered

@simonpj
Copy link
Contributor

simonpj commented Apr 25, 2018

I basically support this proposal, but starting with an intricate GADT example conceals the point. Please can we offer a series of examples, starting simple. For example (all assuming -XScopedTypeVariables):

f :: Maybe a -> Int
f (Just (x :: b)) = <body>

This is clearly fine. b scopes over <body>. The variable a is not in scope at all (no explicit forall).

f :: forall a. Maybe a -> Int
f (Just (x :: b)) = <body>

Both a and b are in scope in <body>, as aliases.

Now the kicker:

f :: Maybe Int -> Int
f (Just (x :: a)) = <body>

If this was allowed a would have to be an alias for Int. Currently that is not allowed: a lexically scoped type variable can only be bound to a type variable. The whole point of the proposal is to lift that restriction.

One reason for making the change is that it's not really clear what being "bound to a type variable" means in the presence of type equalities. For example:

f1 :: (a ~ Int) => Maybe a -> Int
f1 (Just (x :: b)) = <body>

f2 :: (a ~ Int) => Maybe Int -> Int
f2 (Just (x :: a)) = <body>

Which of these should be accepted under the current rules? (SPJ says: I don't even know; I'd have to try it.) An advantage of the proposal is that such questions become irrelevant.

....You can add some more examples. Be sure to talk about repeated variables too!

@RyanGlScott
Copy link
Contributor

I also support this proposal.

Another motivation that might be worth mentioning is the ability to bind large types to shorter variable names, such as in:

f :: ReallyReallyReallyReallyLongTypeName -> T
f (x :: a) = ...
-- Instead of f (x :: ReallyReallyReallyReallyLongTypeName)

@goldfirere
Copy link
Contributor

What about this:

foo (Just (x :: a)) = not x

Note: no type signature. This is rejected today, because a is not Bool. Under your proposal, it sounds like you would want to accept this. However, the proposal states "GHC insists that the type variable is bound to a rigid, or fully-known, type". In this case, a is not rigid or fully-known at the time it's bound. To be honest, I don't know exactly what "fully-known" means here.

@nomeata
Copy link
Contributor Author

nomeata commented Apr 25, 2018

Indeed, my branch accepts that code:

Prelude> :set -XScopedTypeVariables 
Prelude> foo (Just (x :: a)) = not x
Prelude> :t foo
foo :: Maybe Bool -> Bool

However, the proposal states "GHC insists that the type variable is bound to a rigid, or fully-known, type". In this case, a is not rigid or fully-known at the time it's bound. To be honest, I don't know exactly what "fully-known" means here.

The proposal states that only because it is the smallest delta to the status quo. I am too typechecker ignorant to get this right on my own, so I will need your help. (Where “you” refers to the numerous hoards of type-checker hacker out there, not necessarily just Richard. There are legions of those, are there?)

Shall we simply drop that sentence?

@goldfirere
Copy link
Contributor

I vote to drop that sentence, or for someone to explain what it means.

and also mention that the current behavior about repeated type variables is unchanged.
@simonpj
Copy link
Contributor

simonpj commented Apr 25, 2018

"GHC insists that the type variable is bound to a rigid, or fully-known, type".

Yes I think that sentence is probably nonsense

@simonpj
Copy link
Contributor

simonpj commented Apr 25, 2018

Could you take advantage of the opportunity, and write as tight a spec for the new system as you can? Things specified by deltas from an ill-specified baseline are never satsifying. Just specify pattern type signatures ab-initio. In the light of this discussion doing so may not be hard.

@yav
Copy link
Contributor

yav commented Jun 15, 2018

I also think this is a good idea. Oddly, I am pretty sure that type variables in patterns used to work as in the proposal some time ago, but I guess at some point they got switched to being universal??

We've had this feature for a long time in Cryptol, and I think it works pretty well.

@simonpj
Copy link
Contributor

simonpj commented Jun 15, 2018

My request for a spec is answered by this paper: https://www.microsoft.com/en-us/research/publication/type-variables-patterns/. Have a look!

@adamgundry
Copy link
Contributor

Lovely. Is there a plan to implement appendix B? I for one would be happy to give up ScopedTypeVariables for the ability to bind type variables in function definitions.

@simonpj
Copy link
Contributor

simonpj commented Jun 15, 2018

One step at a time. Let's do type applications in patterns first.

@goldfirere
Copy link
Contributor

Is this ready to submit to the committee now?

@nomeata
Copy link
Contributor Author

nomeata commented Jul 14, 2018

Is there merit in bundling this with #126 and have just one proposal for the paper? But probably not, they are nicely orthogonal… Are you happy with the text?

@goldfirere
Copy link
Contributor

In the "specification" part, there is a reference to "the above sentence" which is unclear to me. The best referent seems to have two sentences.

@nomeata nomeata added the Pending committee review The committee needs to evaluate the proposal and make a decision label Jul 14, 2018
@Ericson2314
Copy link
Contributor

Ericson2314 commented Jul 16, 2018

The paper mentions type lambdas as an alternative. But isn't there no conflict? Isn't this forward compatible with:

singleton @b (x :: b) = x -- good
singleton :: a -> [a]
singleton @b (x :: b) = x -- good
singleton :: Show a => a -> [a]
singleton @b (x :: b) = x -- good
singleton :: forall b. b ~ Int => Int -> [Int]
singleton @b (x :: b) = x -- good
singleton :: Int -> [Int]
singleton @b (x :: b) = x -- bad, because there's explicitly no ∀ type
singleton :: a -> [a]
singleton @b (x :: c) = x 
-- ^ bad, because cannot mix implicit (for `c`) and explicit (for `b`) Λ

@nomeata
Copy link
Contributor Author

nomeata commented Jul 16, 2018

Interesting example. At the moment, I think the way forward will be that type lambdas (#155) will not and never refer to types, and only ever to forall’ed type variables. But maybe that discussion should happen in #155 :-)

@goldfirere
Copy link
Contributor

I've responded to #128 (comment) in #155.

@Ericson2314
Copy link
Contributor

Haha, what timing!

@nomeata nomeata merged commit 90bda91 into master Aug 4, 2018
@nomeata nomeata added Accepted The committee has decided to accept the proposal and removed Pending committee review The committee needs to evaluate the proposal and make a decision labels Aug 4, 2018
@nomeata nomeata added the Implemented The proposal has been implemented and has hit GHC master label Dec 3, 2018
@Ericson2314
Copy link
Contributor

Ericson2314 commented Jul 23, 2019

All the examples are pattern signatures within function binds. What about pattern binds? It is not clear to me.

x :: a = 1 :: Int -- OK ?

f :: a -> a -- fresh or captured a?
f = id

The options I think make sense to me are

  • accepted, captured a below.
  • disallowed, only patterns within function binds, case patterns, and do notation patterns are allowed. Fresh a below.

What worries me would be taking a turn from #228 and trying to allow a but limit its scope.

x :: a = 1 :: Int
x' :: forall a. Num a => a = \ @c => 1 :: c
Just (y :: b) = Just (1 :: Int)
Just (y :: forall b. Num b => b) = Just $ \ @c => 1 :: c

In deference to future work on impredicative types, I only want the two a bindings to work the same if the two b bindings work the same.

@int-index
Copy link
Contributor

int-index commented Jul 23, 2019

What about pattern binds?

Both before & after this proposal, pattern binds don't support scoped type variables.

x :: a = 1 :: Int -- OK ?

Not OK as pattern binds don't support -XScopedTypeVariables at all:

ghci> x :: a = 1 :: Int
<interactive>:3:1: error:
    • You cannot bind scoped type variable ‘a’
        in a pattern binding signature
    • In the pattern: x :: a
      In a pattern binding: x :: a = 1 :: Int

However, #228 reclassifies this as a nullary function bind, so it should be OK in the future.

@Ericson2314
Copy link
Contributor

Ericson2314 commented Jul 23, 2019

@int-index sorry lost internet so tardily edited the post above.

Both before & after this proposal, pattern binds don't support scoped type variables.

I believe you but the error messages make this rather confusing

Prelude> (1 :: Int) = 1

<interactive>:8:2: error:
    Illegal type signature: Int
      Type signatures are only allowed in patterns with ScopedTypeVariables

If we still had PatternSignatures the situation might make more sense!

@Ericson2314
Copy link
Contributor

Ericson2314 commented Jul 23, 2019

@int-index I'll take the second part back to a #228 modification. Thanks for clarifying exactly what this does.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Accepted The committee has decided to accept the proposal Implemented The proposal has been implemented and has hit GHC master
Development

Successfully merging this pull request may close these issues.

None yet

9 participants