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

[Simon Peyton Jones]

The reason is that the proposal "steals" the syntax for explicit type application in patterns but it seems to me that type application in patterns makes perfect sense!

I disagree with Roman here.   I don’t think type application makes sense in patterns.  Suppose we have


data T a where

  MkT :: [a] -> [b] -> T a



f :: T c -> c -> [c]

f t x = x : (case t of

                 T ys zs -> if length zs > 1 then ys else [])


Then

  *   ‘c’ is really bound at f’s definition site; not in the pattern match
  *   You might want to mention ‘c’ in lots of places, not just inside the pattern match, so you might want to make ‘c’ lexically scope over its entire actual scope.  Providing a convenient way to make it scope over just part of its actual scope seems entirely ad-hoc.  We might want to do that at any sub-expression.  And we can do so with an ordinary type signature with an explicit forall.
  *   In contrast the type of ‘zs’ really is bound at the pattern match.
  *   Imagine that we had a type-passing implementation that really did pass data structures representing types for every big lambda and type application. Then we really would store the data structure representing the existential inside the data constructor, and match it in a pattern; but it would be a waste of space to store and match the universal too.
  *   In Core, we have MkT :: forall a b . [a] -> [b] -> T a, so a use of MkT as a constructor is applied to two types.  But in a pattern match we just match one type, namely the existential one.

I think the proposal is a fine one!  Let’s accept it.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Roman Leshchinskiy
Sent: 25 March 2018 23:24
To: ghc-steering-committee at haskell.org
Subject: [ghc-steering-committee] Proposal: Binding existential type variables (#96)

Hi everyone,

The proposal is to add a way to name existential type variables in pattern matches: https://github.com/ghc-proposals/ghc-proposals/pull/96<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F96&data=02%7C01%7Csimonpj%40microsoft.com%7Cd6086d1899084366a94208d5929f1b8b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636576134424867601&sdata=rabZEgeT8DzDp6fhA2sKQLzavwy2T1SqhYPs5XRgVG4%3D&reserved=0>.

Suppose we have a constructor with an existential:

data T where
  MkT :: forall a. Show a => a -> T

Under the proposal, we could then bind that existential in a match against MkT:

f :: T -> String
f (MkT @a x) = show (x :: a)

Note that this reuses the syntax for visible type application. Only the forms @a (where 'a' is a variable) and @_ are permitted.

In the discussion the following major questions have been raised.

1. What about universally quantified type variables, such as 'a' in the following definition:

data U a where
  MkU :: forall a b. Show a => b -> T a

Do we need to mention 'a' in a pattern match against MkU? The answer (now reflected in the proposal) is no - universally quantified type variables can't be bound in this way. The pattern would look like this:

g :: U a -> String
g (MkU @b x) = show (x :: b)

The bulk of the discussion was about this question.

2. What exactly is an existential? The above examples are clear but what about:

type family Id a where Id a = a
data T a where
  MkT :: forall a. a -> T (Id a)

This is an existential under the current rules but given this, the distinction between existentials and universals might be not entirely intuitive.

3. What about pattern synonyms? The proposal now clarifies that they are treated exactly the same as data constructors.


My recommendation is to reject the proposal as is but to encourage the authors to come up with a different syntax. The reason is that the proposal "steals" the syntax for explicit type application in patterns but it seems to me that type application in patterns makes perfect sense! I don't see why I shouldn't be eventually able to write something like:

data C a = C a
h (C @Int n) = n

and have the compiler infer h :: C Int -> Int. Having @type mean something other than type application in pattern seems highly confusing to me and kills a possibly useful future feature. I believe a lot of the confusion with respect to point 1 above happened precisely because the proposal blurs the difference between type application and binding in patterns.

As to syntax, perhaps using 'type' or 'forall' as type binders instead of '@' would work.

Thanks,

Roman

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180326/6cd3ca5b/attachment-0001.html>