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

[Manuel M T Chakravarty]

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 <mail at joachim-breitner.de>:
> 
> 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/
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 874 bytes
Desc: Message signed with OpenPGP
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180328/0e93a21f/attachment-0001.sig>