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

[Simon Peyton Jones]

Note we aren't binding any type variables here, we're just selecting a specific instantiation of the constructor via type application

Interesting. (I did misunderstand you!)   So in your example, Int and only Int would do at that spot.   To you it seems like a “natural meaning” but not to me.   In a pattern I expect to enumerate the bound variables, and that is just what is proposed here,

  *   using @ to distinguish type binders from term binders
just as visible type application

  *   uses @ to distinguish type argument from term arguments

Also, you can readily do what you want with an ordinary type signature in a pattern


h (C n :: C Int) = n      -- infers h :: C Int -> Int

Moreover you don’t explain what it would mean to supply the existential argument with @ applications in a pattern match.  Do those bind type variables?

I think we should be cautious about rejecting one proposal because it precludes another, unless the other is actually made and worked out so we can see it.  I say cautious, not that it’s an invalid argument – we don’t want to accept proposals that everyone agrees will preclude future flexibility.  But here it is controversial (at least between you and me 😊).
Would you like to make an alternative proposal?

Simon

From: Roman Leshchinskiy <rleshchinskiy at gmail.com>
Sent: 26 March 2018 09:54
To: Simon Peyton Jones <simonpj at microsoft.com>
Subject: Re: [ghc-steering-committee] Proposal: Binding existential type variables (#96)

On Mon, Mar 26, 2018 at 8:59 AM, Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> wrote:
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.

Simon, I think you might have misunderstood me. I'm not proposing to be able to *bind* universally quantified variables via @ in patterns. My argument is much simpler. To revisit my example:

data C a = C a

This gives us the constructor C :: forall a. a -> a and in expressions, C @Int is the Int -> Int instance of the constructor. Personally, I would expect C @Int to have the exact same meaning in patterns since it makes total sense there (to me, at least), like in my example:

h (C @Int n) = n      -- infers h :: C Int -> Int

Note we aren't binding any type variables here, we're just selecting a specific instantiation of the constructor via type application, just like we would do in expressions. Under the proposal, the meaning of @ in patterns would be different and to me, surprising. In fact, I naively assumed that the above is already possible with visible type application.

Now, perhaps type application in patterns isn't and will never be useful and repurposing the syntax is ok? After all, patterns already reuse function application syntax in much the same way. I'll certainly reconsider my opinion if that's the case but I don't think this has been discussed at all so far. Hence, I'm very wary of taking away syntax that already has a natural meaning.

Roman


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