Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for existentials #3492

Open
garyb opened this issue Dec 20, 2018 · 8 comments

Comments

Projects
None yet
6 participants
@garyb
Copy link
Member

commented Dec 20, 2018

@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 garyb added this to the Ideas milestone Dec 20, 2018

@garyb

This comment has been minimized.

Copy link
Member Author

commented Dec 20, 2018

I think something like

data Box = exists a. Box a

might also be worth bikeshedding about.

@yuxuanchiadm

This comment has been minimized.

Copy link

commented Dec 27, 2018

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

This comment has been minimized.

Copy link
Member

commented Dec 27, 2018

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

This comment has been minimized.

Copy link
Contributor

commented Dec 27, 2018

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

This comment has been minimized.

Copy link
Contributor

commented Dec 27, 2018

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

@rightfold

This comment has been minimized.

Copy link
Contributor

commented Jan 4, 2019

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

This comment has been minimized.

Copy link
Contributor

commented Jan 4, 2019

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 comment has been minimized.

Copy link

commented Jan 4, 2019

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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.