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

[Richard Eisenberg]

> On Mar 26, 2018, at 2:43 PM, Joachim Breitner <mail at joachim-breitner.de> wrote:

> And once we have syntax to instantiate universals and bind
> existentials, there is the question, which of these two deserves @ and
> which has to get the yet-to-be-found other one. (Personally, I’d say
> that @ should instantiate universals, for consistency with
> TypeApplications, but will not insist on this point.)

And I'd say that @ should bind existentials, for consistency with the usual default for patterns, which is the "output" mode. Besides, I think binding existentials will be much more common than instantiating universals.

> 
> 
> 
> Somewhat tangentially, how much should it worry us that according to
> the current proposal, in
> 
>  type Id a = a
>  data Foo  a where MkFoo  :: forall a,  a -> Foo a
>  data Foo' a where MkFoo' :: forall a,  a -> Foo (Id a)
> 
> the constructors MkFoo and MkFoo' behave totally different wrt
> universals and existentials? I see the technical justification for it,
> but it still feels odd and unsmooth.

The rule in the proposal is dumb-and-predictable, far better than clever-and-abstruse. GHC is clever-and-abstruse enough as it is -- we should claim dumb-and-predictable where we can find it. :)

Richard

> 
> 
> 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