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

I'm of several minds on this issue. 1. Like Joachim, I really like expressions and patterns to have a similar structure. The lack of this feature in this proposal irks me. 2. Like Roman, I see the value in being able to specialize universal variables in patterns. This is not an overwhelming desire, but I see the point here. 3. Like Simon, I see the value in being able to say that everything that occurs in a pattern is a pattern -- that is, an output of the match. On balance, I think (3) outweighs (2). A programmer should be able to tell, just based on concrete syntax alone, whether a variable mention in a program is a *binding site* or *occurrence*. Currently, variables that appear after a constructor in a pattern are binding sites. That suggests that type variables appearing after @ in patterns should also be binding sites. (This agrees with the proposal.) As for (1), perhaps we simply accept that patterns and expressions really are different. It's quite like how a pattern synonym type has to have two separate sets of constraints (one is required and one is provided) when being used as a pattern, but these constraints get smooshed together when the pattern synonym is used in an expression. And I agree with Simon that the programmer needs to know what the existentials are to have any hope of writing type-correct code. I am thus in favor of the proposal, but acknowledging these soft spots. Richard

On Mar 26, 2018, at 10:31 AM, Joachim Breitner wrote:

Hi,

without adding much to the discussion, I agree with Roman’s sentiment here. And maybe that is an indication that more people out there, who are not as deep into the theory and implementation of this feature, will be similarly surprised.

Am Montag, den 26.03.2018, 09:24 +0000 schrieb Simon Peyton Jones:

...

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

Isn’t that true for most uses of TypeApplications in expressions as well, that they could readily be replaced by type signatures? And yet we offer the TypeApplications extension?

Here is another example where the current proposal superficially breaks the nice equational nature of Haskell:

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

idU :: forall a. U a -> U a idU (MkU @b x) = MkU @a @b x

or even

idU :: forall a. U a -> U a idU (MkU @b x) = MkU @a x

It is the identity! Why don’t I write the same things on both sides?

I think all reserverations would disappear if we can find a good syntax for existential type variable that does not clash with TypeApplication.

Maybe @? instead of @ (given that ? is commonly used to refer to ∃)?

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee