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

[Roman Leshchinskiy]

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.

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/20180325/918c3b41/attachment.html>