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

[Simon Peyton Jones]

Yes I like the "\" too.  (Or some syntax separating inputs from outputs.)

More specifically, I really like the possibility of specifying input values to a pattern.  You can do that with view patterns - but you can't abstract over those view patterns with a pattern synonym (currently).  It'd be great to be able to say


       pattern P n \ x   <-   ((\y -> if y>2*n+1 then Just y else Nothing)

                              -> Just x)


This looks pretty impenetrable, but it's using a view pattern to test if the argument is > 2n+1, and match if so.  So 'n' is an input, and x is an output.

I think we have to group all the inputs together and have a separator.   No inter-mingling.  Remember, we want the distinction to be syntactically obvious; and outputs must be variables while inputs can be arbitrary terms or types.

As discussed earlier, for inputs, @ distinguishes types from terms; for outputs, @ distinguishes type binder from term binders.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Richard Eisenberg
Sent: 27 March 2018 03:47
To: Roman Leshchinskiy <rleshchinskiy at gmail.com>
Cc: ghc-steering-committee at haskell.org; Joachim Breitner <mail at joachim-breitner.de>
Subject: Re: [ghc-steering-committee] Proposal: Binding existential type variables (#96)




On Mar 26, 2018, at 5:54 PM, Roman Leshchinskiy <rleshchinskiy at gmail.com<mailto:rleshchinskiy at gmail.com>> wrote:

  C <inputs> \ <outputs>

I had been trying to figure out how to get \ involved, and this is the way. Thanks! It does require that all inputs come before all outputs, which might not be true for constructors:

data T a where
  MkT :: forall b a. b -> T a

Here, `b` is an output while `a` would be an input. And in many cases constructors designed with visible type application in mind will want to put existentials ("outputs") before universals ("inputs"). If we ever did the C <inputs> \ <outputs> in the future, I suppose we could just say that such constructors will have their type variables reordered, perhaps issuing a warning if someone writes a mis-ordered constructor.

In any case, I'm glad that this discussion has changed your mind about accepting this proposal.

Thanks,
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180327/9c560297/attachment-0001.html>