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

On Mar 26, 2018, at 2:43 PM, Joachim Breitner 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@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