Support for existentials

[garyb]

@natefaubion is talking a good game on Slack, so I'll open an issue for it.

Proposal is:

1. to introduce forall-before-the-constructor: data Box = forall a. Box a
2. to allow binding of existential variables in case expressions: case b of forall a. Box v -> ... where a is introduced as a usable type in ..., to annotate v, etc.
3. maybe support packaging of dictionaries

A somewhat relevant paper about type annotations in patterns: https://arxiv.org/pdf/1806.03476.pdf

Old discussion: #82.

[garyb]

I think something like

data Box = exists a. Box a

might also be worth bikeshedding about.

[yuxuanchiadm]

I think something like

data Box = exists a. Box a

might also be worth bikeshedding about.

No imo. Instead if "exists" is introduced. It should be something like:

data Box = Box (exists a. a)

Keep using "forall" is better choice.

[hdgarrood]

Can someone summarize the arguments in favour of adding this as opposed to polykinds and using the purescript-exists library? Obviously it's easier with dedicated syntax, as you don't need to do extra work in the case where the type variable you want to use as an existential is not the last type argument; is there more to it than that?

[natefaubion]

Downsides to existential encodings:

• You need a variation for every kind and number of variables, as long as you always keep the existentials at the end of the variable list. This is tedious enough that I think most often users just define ad-hoc unsafe existential coercions rather than use Exists.
• It only really works with product types, so if you want existentials in a sum-type it requires extra boxing.
• Using CPS eliminators breaks tail-call optimization, so most libraries that want to preserve stack safety (like Free) use an internal unsafe value where the type system can't help you.

[natefaubion]

I think forall is appropriate in the data declaration. I know it seems wrong, but it corresponds to the CPS encoding of a datatype.

[no-longer-on-githu-b]

Will this work with newtypes? In Haskell you can't do that for some reason I don't quite understand.

Re forall syntax, if we allow GADT syntax then it is a lot more natural because the constructors are written as type signatures.

[natefaubion]

You can't have existential constraints with newtypes because they have to be bundled in the constructor. Constraints on functions are just arguments, and constraints on constructors are just values. You could have existential type variables with a newtype.

[timjs]

This would be a great feature to have! I'm encountering it more and more when working with (deeply) embedded DSLs. Being able to package dictionaries would be the next great step forward.

The combination of existentially quantified variables + (multi-parameter) type classes + functional dependencies would give us the means to do a lot of things GADTs are used for. In literature this is called an EADT (Extended Algebraic Data Type), which is in turn a generalisation of a GRDT (General Recursive Data Type). Sulzmann, Wazny, and Stucky give an example of a length indexed vector using EADTs:

data Zero
data Succ m

data Vect n a
  = (n = Zero) => Nil
  | forall m. (n = Succ m) => Cons a (Vect m a)

Everything before the => is an equality constraint, like PureScripts TypeEquals. forall is used to introduce existential variables. Although they use Zero and Succ m data declarations, we could also use (built in) constraints on a kind of natural numbers. More examples, like type safe expressions, can be found in Chapter 8 of Wazny's dissertation. (It's a good read! We could learn a lot about generating great error messages too!)

Regarding @garyb's comment, I think that exists reads better then forall. I think it is better to use the correct logical meaning of "exists" than the meaning that derives from the encoding that is used under the hood. Clean too makes this distinction.

Also, I have to say that the syntax used by Sulzmann et al. takes me a bit off guard. My mind tends to think that => is associated to type annotations. Therefore, when I'm reading =>, I tend to think everything that follows it is a type, not a constructor... To have some comparison, Clean puts it's packed constraints behind the data constructors like this (unfortunately this is not described in the language report, which is a bit behind):

:: Vect n a
  = Nil & Equals n Zero
  | E.m: Cons a (Vect m a) & Equals n (Succ m)

[JordanMartinez]

A more recent paper was mentioned in Haskell's proposals repo: An Existential Crisis Resolved: Type inference for first-class existential types