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

Tue Mar 27 05:24:51 UTC 2018

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.html#pattern-type-signatures)
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
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180327/18aa307a/attachment.sig>