Re: [ghc-steering-committee] Proposal: Binding existential type variables (#96)

I can’t say that I am sure of the details, but Joachim’s proposal seems appealing to me. Manuel

Am 27.03.2018 um 16:24 schrieb Joachim Breitner :

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://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...) 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@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee