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

[Simon Peyton Jones]

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

I really don't agree.   If we wrote

	f (?x : ?xs) = ...

to signal that x and xs were binding sites, then I'd be fine with writing

	f (MkT @?a ?xs) = ...

But we don’t.  In patterns, a plain variable is a binding site.  And it should be the same for types -- save that we need a way to distinguish terms from types, just as we do in terms.


You should think of 

* the universal type args and required dictionaries, as INPUTs to
  the match

* the existential args and value args, as OUTPUTS of the match

Consider
	data T p where
   	  MkT :: p -> [q] -> T p

	f :: forall a. (Num a, Eq a) => T a -> Int
	f (T 3 y) = length y

Here, the type 'a' and the dictionaries for (Eq a, Num a) are inputs to the match. If successful, the match binds the existential type 'q', and value argument (y :: [q]).

A matcher for the pattern (T 3 y) would have a type like

	forall a r. (Num a, Eq a) => (forall q. [q] -> r) -> T a -> r

Now, the things matched by the pattern are the arguments (both type and term arguments) to that continuation.  These are what I expect to see bound.

As a programmer you really do need to know which variables are existential.  Without that you can't possibly know what programs are well typed.

It seems so simple to me to say

"we use the @ to distinguish between term and type arguments in applications; and between term and type binders in patterns".

Simon

|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-
|  bounces at haskell.org> On Behalf Of Joachim Breitner
|  Sent: 26 March 2018 15:32
|  To: ghc-steering-committee at haskell.org
|  Subject: Re: [ghc-steering-committee] Proposal: Binding existential
|  type variables (#96)
|  
|  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
|  
|  https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.jo
|  achim-
|  breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Cecf2cfd38b0947
|  25e09d08d593265bd5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636576
|  715317265122&sdata=H5kvHXEYy9L7Pnp3CyajY9BFbhkuzHhqrxxR5xykx0M%3D&rese
|  rved=0