[ghc-steering-committee] Proposal: Binding existential type variables (#96)
Simon Peyton Jones
simonpj at microsoft.com
Tue Mar 27 21:53:28 UTC 2018
Interesting idea from Joachim. But it's quite complicated.
Here is a much simpler version.
Consider
data T a where
MkT :: forall a b. a -> b -> T a
Suppose we said that
- In pattern you must list a type binder for every forall,
whether universal or existential. Thus a pattern with
explicit type binders would look like
MkT @x @y p q
f :: T Int -> Int
f (MkT @x @y (p::x) (q::y)) = x
- In a pattern (MkT @x @y p q)
x and y are both brought into scope by the pattern,
and must be variables (not types).
(In contrast, p and q can be patterns.)
- For universals, you implicitly get an equality that connects
the binder to the type of the scrutinee. So in the above
example
f :: T Int -> Int
f (MkT @x @y (p::x) (q::y)) = x
we would have an implicit equality x~Int, which is why the
RHS (which must return an Int) is well typed. It's much as if
we had declared MkT with two existentials
MkT :: forall a b c. (a~c) => a -> b -> T c
This is a bit simpler than what Joachim suggests, but I think it
meets his key goal: that a MkT pattern has the same number of type
args as a MkT term.
I had not previously thought of this, but it removes most of
my objections: here 'x' really is brought into scope, just with
an accompanying equality. And it is fairly simple to explain.
Hmm. Do others like this? If so we could go back to the
proposer with this as a suggestion.
Simon
| -----Original Message-----
| From: ghc-steering-committee <ghc-steering-committee-
| bounces at haskell.org> On Behalf Of Joachim Breitner
| Sent: 27 March 2018 06:25
| To: ghc-steering-committee at haskell.org
| Subject: Re: [ghc-steering-committee] Proposal: Binding existential type
| variables (#96)
|
| Hi,
|
| I was close to writing “I am not convinced, but if I am the only one
| who is unhappy with the current proposal, then I will not stand in the
| way”. But I was away from the computer, so I could not write that, and
| so I pondered the issue some more, and the more I ponder it, the more
| dissatisfied with that outcome I am (and it kept me awake tonight…).
|
| But I want to be constructive, so I am offering an alternative
| proposal. Still half-baked, of course, but hopefully already
| understandable and useful.
|
| ### What are the issues?
|
| But first allow me to summarize the points of contention, collecting
| the examples that I brought up before, and adding some new ones.
|
| 1. It breaks equational reasoning.
|
| data T a where MkT :: forall a b. b -> T a
| foo (MkT @a y) = E[a :: y]
| bar = C[foo (MkT @Int True)]
|
| is different from
|
| bar = C[E[True :: Int]]
|
| While we can certainly teach people the difference between @ in
| expression and @ in patterns, I find this a high price to pay.
|
| 2. The distinction between existentials and universals is oddly abrupt.
|
| data A a where MkA :: forall a. A a
|
| has a universal, but
|
| data A' a where MkA' :: forall a. A (Id a)
|
| has an extensional.
|
| Also, every universal can be turned into an existential, by
| introducing a new universal. a is universal in A, but existential in
|
|
| data A'' a where MkA'' :: forall a b. a ~ b -> A b
|
| although it behaves pretty similar.
|
| 3. The intuition “existential = Output” and “universal = Input” is
| not as straight-forward as it first seems. I see how
|
| data B where MkB :: forall a. B
|
| has an existential that is unquestionably an output of the pattern
| match. But what about
|
| data B2 where MkB2 :: forall a b. a ~ b -> B
|
| now if I pattern match (MkB2 @x @y), then yes, “x” is an output,
| but “y” somehow less so. Relatedly, if I write
|
| data B3 where MkB3 :: forall a. a ~ Int -> B
|
| then it’s hardly fair to say that (MkB3 @x) outputs a type “x”. And
| when we have
|
| data B4 a where MkB4 :: forall a b. B (a,b)
|
| then writing (MkB4 @x @y) also does not really give us a new types
| stored in the constructor, but simply deconstructs the type argument
| of B4.
|
| ### Goals of the alternative proposal
|
| So is there a way to have our cake and eat it too? A syntax that
| A. allows us to bind existential variables,
| B. has consistent syntax in patterns and expressions and
| C. has the desired property that every variable in a pattern is bound
| there?
|
| Maybe there is. The bullet point 3. above showed that thinking in terms
| of Input and Output – while very suitable when we talk about the term
| level – is not quite suitable on the Haskell type level, where
| information flows in many ways and direction.
|
| A better way of working with types is to think of type equalities,
| unification and matching. And this leads me to
|
| ### The alternative proposal (half-baked)
|
| Syntax:
| Constructors in pattern may have type arguments, using the @ syntax
| from TypeApplication. The type argument correspond to _all_ the
| universally quantified variables in their type signature.
|
| Scoping:
| Any type variable that occurs in a pattern is brought into scope by
| this pattern. If a type variable occurs multiple times in the same
| pattern, then it is the still same variable (no shadowing within a
| pattern).
|
| Semantics:
| (This part is still a bit vague, if it does not make sense to you, then
| better skip to the examples.)
| Consider a constructor
|
| C :: forall a b. Ctx[a,b] => T (t2[a,b])
|
| If we use use this in a pattern like so
|
| (C @s1 @s2) (used at some type T t)
|
| where s1 and s2 are types mentioning the type variables x and y, then
| this brings x and y into scope. The compiler checks if the constraints
| from the constructor C', namely
| (t ~ t2[a,b], Ctx[a,b])
| imply that a and b have a shape that can be matched by s1 and s2.
| If not, then a type error is reported.
| If yes, then this matching yields instantiations for x and y.
|
| Note that this description is completely independent of whether a or b
| actually occur in t2[a,b]. This means that we can really treat all type
| arguments of C in a consistent way, without having to put them into two
| distinct categories.
|
| One could summarize this idea as making these two changes to the
| original proposal:
| + Every variable is an existential (in that proposal’s lingo)
| + We allow type patterns in the type applications in patterns, not
| just single variables.
|
|
| ### Examples
|
| Let's see how this variant addresses the dubious examples above.
|
| * We now write
|
| data T a where MkT :: forall a b. b -> T a
| foo (MkT @_ @a y) = E[a :: y]
| bar = C[foo (MkT @Int True)]
|
| which makes it clear that @a does not match the @Int, but rather an
| implicit parameter. If the users chooses to be explicit and writes
| it as
| bar = C[foo (MkT @Int @Bool True)]
| then equational reasoning worksand gives us
| bar = C[E[True :: Bool]]
|
| * The difference between
|
| data A a where MkA :: forall a. A a
| data A' a where MkA' :: forall a. A (Id a)
| data A'' a where MkA'' :: forall a b. a ~ b -> A b
|
| disappears, as all behave identical in pattern matches:
|
| foo, foo', foo'' :: A Integer -> ()
| foo (MkA @x) = … here x ~ Integer …
| foo' (MkA' @x) = … here x ~ Integer …
| foo'' (MkA'' @x) = … here x ~ Integer …
|
| * Looking at
|
| data B where MkB :: forall a. B
| data B2 where MkB2 :: forall a b. a ~ b -> B
| data B3 where MkB3 :: forall a. a ~ Int -> B
| data B4 a where MkB4 :: forall a b. B (a,b)
|
| we can write
|
| foo (MkB @x) = … x is bound …
|
| to match the existential, as before, and
|
| foo (MkB @(Maybe x)) =
|
| would fail, as expected. We can write
|
| bar (MkB2 @x @y) = … x and y are in scope, and x~z …
|
| just as in the existing proposal, but it would also be legal to
| write, should one desire to do so,
|
| bar (MkB2 @x @x) =
|
| With B3 we can match this (fixed) existential, if we want. Or we
| can
| assert it’s value:
|
| baz (MkB3 @x) = … x in scope, x ~ Int …
| baz (MkB3 @Int) = …
|
| With B4, this everything works just as expected:
|
| quux :: B4 ([Bool],())
| quux (MkB4 @x @y) = … x and y in scope, x ~ [Bool], y ~ ()
|
| which, incidentially, is equivalent to the existing
|
| quux (MkB4 :: (x, y)) = … x and y in scope, x ~ [Bool], y ~ ()
|
| and the new syntax also allows
|
| quux' (MkB4 @[x]) = … x in scope, x ~ Bool
|
|
| ### A note on scoping
|
| Above I wrote “every type variable in a pattern is bound there”. I fear
| that this will be insufficient when people want to mention a type
| variable bound further out. So, as a refinement of my proposal, maybe
| the existing rules for Pattern type signatures
| (https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownload
| s.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts
| .html%23pattern-type-
| signatures&data=02%7C01%7Csimonpj%40microsoft.com%7C1b42c7e570c94b8d26e1
| 08d593a31aad%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63657725109818
| 1218&sdata=G3twWyxN9UkQ%2Bs3vBOiNxj4NfZCOty24nk3lbXV5WNI%3D&reserved=0)
| should apply: “a pattern type signature may mention a type variable
| that is not in scope; in this case, the signature brings that type
| variable into scope”
|
| In this variant, all my babbling above can be understood as merely the
| natural combination of the rules of ScopedTypeVariables (which brought
| signatures to patterns) and TypeApplications (which can be understood
| as an alternative syntax for type signatures).
|
| What if I really want to introduce a new type variable x, even if x
| might be in scope? Well, I could imagine syntax for that, where we can
| list explicitly bound type variables for each function equation.
|
| data C a where MkC1 :: forall a, a -> C a
| MkC2 :: forall b, b -> C Int
|
| foo :: forall a. a -> C a -> ()
| foo x c = bar c
| where
| bar (MkC1 @a) = …
| -- matches the a bound by foo with the argument to MkC1
| -- which succeeds
| forall a. bar (MkC2 @a) = x
| -- introduces a fresh a, bound to MkC2’s existential argument
| -- and shadowing foo’s type variable a
|
|
|
| Ok, that ended up quite long. I guess there is a strong risk that I am
| describing something that Emmanuel, Simon and Richard have already
| thought through and discarded… if so: why was it discarded? And if not:
| does this proposal have merits?
|
| Cheers and good night,
| Joachim
|
| PS: Happy 3rd anniversary to GHC-7.10 :-)
|
|
| --
| Joachim Breitner
| mail at joachim-breitner.de
|
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joac
| him-
| breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C1b42c7e570c94b8d
| 26e108d593a31aad%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6365772510
| 98181218&sdata=bl1ob%2FZWifjoMkgXXMRVjnTbn0RS1588ZCf4Cw7Juw0%3D&reserved
| =0
More information about the ghc-steering-committee
mailing list