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

[Richard Eisenberg]

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 <mail at joachim-breitner.de> 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 at joachim-breitner.de
>  http://www.joachim-breitner.de/
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee