I'm really looking forward to it, thank you. Just this week I wrote some code where I believe I could have made use of something like [exists a . Parseable a /\ Proxy a].

If we, at some point, have forall and foreach, will we also have exists and _____ (not sure what name it would have)?

exists n. KnownNat n /\ Vec n a in the example looks a lot like a counterpart to forall a n . KnownNat n => Vec n a -> ..., which could become forall a . foreach n . Vec n a -> ... instead, so I imagine the answer is yes, and we might eventually be able to replace exists n. KnownNat n /\ Vec n a with ______ n . Vec n a?

(I'm not suggesting that this works for /\ in general, but for KnownNat in particular, since it's a singleton.)

Sounds great!

I have a question: How does this compare with the "traditional" encoding of sigma types via pi types, that is very often found in e.g. Agda and Idris:

record Sigma (A : Set) (P : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : P fst

From a quick skim, it seems like the main benefits of making these "first class" are

• we don't have to do additional manual (un)wrapping with a constructor for a sigma pair (the _,_ constructor from above)
• we get more type erasure without doing additional work (e.g. having to make fst from above be erased)

Is there anything else I'm missing?

I don't like the /\ name. I see https://hackage.haskell.org/package/lattices-2.0.3/docs/Algebra-Lattice.html#v:-47--92- and I don't feel nice about this. AFAIU it's a new kind of pair, so I'd rather see some syntax based on comma , (which also wouldn't steal any names as , is special already).

EDIT: In fact, In Core, GHC already makes Constraint, Type pairs. (In weird cases of Arrows syntax desugaring).

Just a few quick responses (I will return to @int-index's points later):

@JakobBruenker Yes, very good point. The new keyword (I propose: forone. Or maybe for_one.) would essentially allow Witness to be used in terms. Other than perhaps reserving the keyword now, I don't think I want to expand this proposal in that direction yet, but please argue against me if you think it would be very easy.

@googleson78 I agree with your two bullet points, both of which are significant (in my opinion) -- and undersold in the proposal, as @int-index rightly points out. The "first class" nature also gives us custom syntax.

@phadej I'm open to a new name instead of /\, but I'm not so worried about a name clash here. The /\ symbol is imported just as any other and can be used qualified. One could even make a synonym for it if renaming were important. (Witness, on the other hand, would not support a synonym. It's more of a keyword, but discovered to be a keyword by the renamer, so it can be imported and qualified if necessary.) I'm not sanguine about the possibility of using , here, but do try to make your case. :)

@goldfirere alternative keyword suggestion for forone: forsome, since it's already used for existential quantification, and I think is a bit easier to read (personally, I'm not a fan of the _ to solve readability).

I agree with not doing much about that in this proposal, though.

It shouldn't have for in its name, because then it sounds like a universal. I like given.

On a different note, I want to be able to do "open"/witness -like projecting fields from GADTs too, and also "nominal existentials" directly without coercing to a newly underlying existential type first. If the witnesses are forced to leak the contents in the latter case, we can't use such projection with abstract newtypes, and that sounds bad.

Finally, while this is very exciting and would be great to have, I'm a bit concerned we're starting a big core language and type theory project when we already have one in flight — Dependent Haskell. If this delays that further, I rather just wait and do it after.

To fill out the quantifier matrix further - we have erasable exists and non-erasable <keyword tbd>, what about visible exists ->, would that make sense? I imagine you'd end up with a more conventional dependent pair.

@Ericson2314 funnily enough given sounds more like a universal to me than the other options we have so far, e.g. I might read

f :: forall a . Show a => String

as "given some type a with a Show instance, f will produce a String."

@JakobBruenker Yeah I thought it about some more and I agree given is no good. I think the problem is if classical/erased is "there exists ...", constructive/unerased is "here exists ..." -- they both have "exists" in common! "given" to me on further thought seems used for stuff before the turnstyle / external implication.

Another potential issue I noticed is that it seems trying to recursively open an existential to eliminate each bound variable will result in types that grow super-linearly?

Assuming

expr : exists (a :: k) (b :: k1). inner_ty

we have

Open expr : inner_ty[Witness @k (exists (a :: k) (b :: k1). inner_ty) expr / a]

Open (Open expr) : inner_ty[Witness @k (exists (a :: k) (b :: k1). inner_ty) expr / a]
                           [Witness @k1 (exists (b :: k1). inner_ty[Witness @k (exists (a :: k) (b :: k1). inner_ty) expr / a]) expr / b]

Perhaps we better get type-level let first?

Open (Open expr) : let
    a_witness = Witness @k (exists (a :: k) (b :: k1). inner_ty) expr
    a_elim = inner_ty[a_witness/ a]
    b_witness = Witness @k1  (b :: k1) (c :: k2). a_elim) expr
    b_elim = a_elim[b_witness / b]
  in b_elim

and further with a 3 variable existential:

expr : exists (a :: k) (b :: k1) (c :: k2). inner_ty

Open (Open expr) : let
    a_witness = Witness @k (exists (a :: k) (b :: k1) (c :: k2). inner_ty) expr
    a_elim = inner_ty[a_witness / a]
    b_witness = Witness @k1  (b :: k1) (c :: k2) (c :: k2). a_elim) expr
    b_elim = a_elim[b_witness / b]
    c_witness = Witness @k2  (c :: k2). b_elim) expr
    c_elim = b_elim[c_witness / c]
  in c_elim

Relatedly, we've long had a principle in Haskell that if you can do it, you can abstract over it. (This is different than, say, Rust, where there is sorts of borrow-checker magic within functions that cannot be expressed formally at function boundaries.)

However, with this feature we run into these issues:

1. Cannot abstract over opens without foreach since we need to use an (open) expression at the type level for Witness.
2. Cannot abstract over the substitution of witnesses without some sort of nonmatchable type-level function like Unsaturated type families #242.
   • I will concede the mere instantiation of foralls also hits this, so this isn't a new violation. Still, rather not make it worse by adding another case where it happens.

This makes me further suspect we should wait on implementing this proposal until these "dependencies" are implemented. I both think that principle of abstracting over anything is very important to instill in beginners about what Haskell is all about, and it is also simply darn useful for more advanced users using extensions in anger, where it's very frustrating to fight the type checker for an hour and then end finding the would-be solution is something that cannot be expressed.

@Ericson2314

Good point about datatype-based existentials. I've added a comment in the proposal (an "interaction").

Also good point about dependent types. I've added a comment in the proposal (an "unresolved question").

About big substitutions: What's the type of expr in your initial example? Remember that users (or GHC) can let-bind expressions if it helps.

About lack of ability to abstract: Could you illustrate with examples? I don't catch what you're describing here.

@JakobBruenker

I think a visible existential is really just a user-written sigma type. Maybe a visible existential has some magical type syntax? Because it wouldn't impact type inference, etc., I'd like to leave this as a future extension.

What's the type of expr in your initial example?

I edited my comment to provide. I think the source of confusion was I had a different expr.

Remember that users (or GHC) can let-bind expressions if it helps.

The problem just seems to be in the types, and I am not exactly sure when in Core the type is mandatory so I am not sure how bad the problem is.

Still, if there is indeed a big blow up in the Core wrt the user-written original, we would need to introduce type-level lets as part of the the desugaring to do the common expression elimination, which seems rather tricky.

About lack of ability to abstract: Could you illustrate with examples? I don't catch what you're describing here.

Sure:

etaOpen
  :: forall (rep :: RuntimeRep) 
  .  forall k
  .  forall (f :: k %U -> TYPE rep)
  .  foreach (expr :: exists (a :: k). f a)
  -> f (Witness @k (exists (a :: k). f a) expr)
etaOpen expr = expr

I think is the "principle" eta-expansion of existential opening, but we are very far away from it being legal Haskell.

Finally, while this is very exciting and would be great to have, I'm a bit concerned we're starting a big core language and type theory project when we already have one in flight — Dependent Haskell.

Darn it! Are you saying this proposal is apart from Dependent Haskell? Because I was excited to see something that I thought used dependent types, and I could see a use for, and I couldn't see how to do any other way (I tried). Getting a type-safe head from a value-filtered data structure seems a big win. In

   filter :: (a -> Bool) -> Vec n a -> Vec ???? a

isn't the index type ???? dependent on the value resulting from filter, in a Dependent-Haskelly way?

| The return type of a dependent function may depend on the value (not just type) of one of its arguments. [wikipedia]

(Or does this not deliver a safe head? I suppose I don't know if I'm applying head to a xs :: Vec (Succ ...) a until I've pattern-matched on the GADT constructor. So head will still throw an exception at run-time?)

@Ericson2314 You say your expr has type Witness blah. But Open works only on an argument whose type is headed by exists. So I think this still isn't quite right.

@AntC2 This proposal is definitely in sympathy with dependent types, in that a language with both dependent types and existentials is more than the sum of its parts. But this proposal is distinct from dependent types. In particular, the features in this proposal are new -- they are not already in Idris or Agda, for example. So we could have dependent types, or first-class existentials, or both.

I agree with the definition for dependent types you quoted from Wikipedia. But the type for filter I'm proposing is (a -> Bool) -> Vec n a -> exists m. Vec m a, where the type of the result (exists m. Vec m a) does not depend on any argument. We might imagine dependentFilter :: foreach (predicate :: a -> Bool) (input :: Vec n a) -> Vec (count predicate input) a, where count :: (a -> Bool) -> Vec n a -> Nat counts the number of elements in a vector that satisfy a predicate. My dependentFilter does have a dependent type, because the type of the result depends on both predicate and input. The existential sidesteps the dependency. In a dependently typed language, you would likely sometimes want filter and sometimes want dependentFilter, just like you would sometimes still prefer lists over Vec.

As for head: I'm assuming you're thinking of a head with type Vec (Succ n) a -> a. Indeed, head (filter predicate v) won't type-check, because we can't be sure that any element in v satisfies the predicate.

I also don't like the /\ operator name. It looks symmetrical, so a reader might (should even) expect it to be commutative. But the arguments don't even have the same kind!

I do think it should be an operator and not a name, since Haskellers are used to using operators when dealing with constraints. To match up with => I think having a double stroke somewhere would be nice. # would do except hash already means something completely different in Haskell. The only other option I can think of is //\, with de double stroke being on the Constraint side. (It looks better in variable-width: //\ )

@goldfirere oops. That was just a cut and paste error, the open paren was also not balanced! I deleted the Witness..( part; it should be correct now.

@AntC2's "darn it" is useful to me. To me, the idea that this feature can be properly done before dependent types is a bit of a siren's call.

I understand the appeal: get something done which seems less fancy and broadly popular across skill levels, and builds a bridge with Liquid Haskell.

But it will require what to me feels like a very nearly ad-hoc subset of Dependent Types to make opening work, and to provide expression coercions. In line with what @nomeata said, it feels like we are opening a can of worms trying to rush that stuff in to do this, and that is in addition to my point above about sacrificing the ability to eta-expand.

As far as the research goes, it is great that we can have papers and proposals for each occurring independently --- in particular I am not saying the formalization in the paper has gaps or any slander like that. But for development the order for implementation to me is very important, and we must constantly fight the urge to rush to popular new features without first doing the behind the scenes infrastructure/ tech debt work to have a good. (I am not even sure Dependent Haskell is even less exciting in vaccum, but rather this is the new kid on the block, and DH isn't, and that has an effect.)

Bottom line is, it is very clear to me how we can do DH without this, and add this later, and is very sketchy to me that we can do this without much of DH, without running the risk of opening and Witness acting super weird the harder one pushes GHC.

@Ericson2314 Getting closer, but still not quite there. Yet I think I can now fill it out myself:

Assuming

expr : exists (a :: k) (b :: k1). inner_ty

we have

let subst1 = [Witness @k (exists (a :: k) (b :: k1). inner_ty) expr / a] in   -- this is meta-syntax
-- important: `b` is not free in `Witness @k (exists (a :: k) (b :: k1). inner_ty) expr`, because `b` is not in scope.
Open expr : (exists (b :: k1). inner_ty)[subst1]
Open expr : exists (b :: k1[subst1]). (inner_ty[subst1])

Open (Open expr) : (inner_ty[subst1])[Witness @(k1[subst1]) (exists (b :: k1[subst1]). (inner_ty[subst1])) (Open expr) / b]
Open (Open expr) : (inner_ty[subst1])[(Witness @k1 (exists (b :: k1). inner_ty) (Open expr))[subst1] / b]
Open (Open expr) : inner_ty[Witness @k1 (exists (b :: k1). inner_ty) (Open expr) / b][subst1]

That's not really so bad, but I do see how a nested dependent existential might grow. I think this can be fixed. I will take another pass through the proposal, as I think that second argument of Witness isn't necessary in Core. (It is necessary in Haskell.)

OK thanks for working through that and simplifying.

Per what @nomeata and you were talking about, if Witness is not actually a type constructor but a dedicated syntactic form, can it just differ between HsType and Type, or need we also need the with-2nd-arg non-Core form during type checking and so much shave the https://gitlab.haskell.org/ghc/ghc/-/issues/18758 yak finally?

Because we cannot know the behavior of the filtering function on every element in the input, we cannot know the length of the output of filter.

Emm (apologies if this is a dumb question/I'll delete it) isn't it more general than that? We could unload the Vec to a (un-indexed) List and filter that. But we can't load the resulting List back to a Vec, again because we cannot know its length.

listtoVec :: [a] -> Vec ???? a

And in general we cannot load to a type-length-indexed Vec by IO (say) reading it from a stream external to the program. "nasty error"/infinite type, dating back to the introduction of GADTs. Then are these indexed lists so beloved of type theoreticians currently usable for anything real-life?

@AntC2 I think it's a good question, and the answer is somewhat counterintuitive at first. This is exactly what we need existential types for, but we can already encode existential types in Haskell. However, it does get a bit unwieldy (as well as having some other disadvantages) without the first-class existential types introduced in this proposal. For example, right now, we can write

data SomeVec a = forall n . MkSomeVec (Vec n a)
filter :: (a -> Bool) -> Vec n a -> SomeVec a
filter p VNil = MkSomeVec VNil
filter p (x :> xs) = case filter p xs of
  MkSomeVec v | p x       -> MkSomeVec (x :> v)
              | otherwise -> MkSomeVec v
fromList :: [a] -> SomeVec a
fromList [] = MkSomeVec VNil
fromList (x:xs) = case fromList xs of
  MkSomeVec v -> MkSomeVec (x :> v)

So if we can produce a list from IO, we can also produce a Vec n a from IO - we just don't know statically what that n is, so we have to produce a SomeVec a. We can use this with any function expecting a Vec n a by pattern matching on the MkSomeVec data constructor. You can use the same kind of encoding of existential types for the SK example from the wiki you linked to.

But with this proposal, we could instead write

filter :: (a -> Bool) -> Vec n a -> exists m. Vec m a
filter p VNil = VNil
filter p (x :> xs)
  | p x       = x :> filter p xs
  | otherwise = filter p xs
fromList :: [a] -> exists n. Vec n a
fromList [] = VNil
fromList (x:xs) = x :> fromList xs

Thanks @JakobBruenker, you're right about "counterintuitive".

   filter p (x :> xs) = case filter p xs of
     MkSomeVec v | p x       -> MkSomeVec (x :> v)
                 | otherwise -> MkSomeVec v

So the guard is applying to something outside the scrutinee of the case. (There's other ways to code that; they're just as convoluted.)

There's other ways to code that; they're just as convoluted.

The one with the proposed exists n. quantifier seems straightforward to me.

My 2 lovelace:

• How about (=/\) for packed class constraints? I like (//\) as well or (=,) if it were valid.

  • edit: I tried out (=&), it looks rather pleasing.
  • (/\) alternative pronunciation from SuchThat: With, Granting, Bearing, Holding, Witnessed ..
  • thereis :) as an alternative to the dependent version of exists

• Are these types interchangable apart from type applications, where forall. playing an existential role is replaced with exists.:

  length :: forall a. [a] -> Int
         :: (exists a. [a]) -> Int
  length :: forall f a. Foldable f => f a -> Int
         :: (exists f a. Foldable f =/\ f a) -> Int
  const :: forall a b. a -> b -> a
        :: forall a. a -> (exists b. b) -> a

• One thing that bothers me is the need to write uncurried definitions. It seems a function cannot be written with exists. if an existential type appears in more than one argument. Not without changing the implementation (uncurrying).

  • We cannot give liftA2 (where a and b are both existential) an exists. type signature. A new definition must be introduced which packs them in a triple.

    liftA2 :: forall f a b c. Applicative f => (a -> b -> c) -> (f a -> f b -> f c)
    liftA2' :: forall f c. Applicative f => (exists a b. (a -> b -> c, f a, f b)) -> f c
    liftA2' ((·), as, bs) = liftA2 (·) as bs

  • I don't know the theory but I want a principle: "any universally quantified function where the quantifiee does not appear in the return type can be typed with exists. without change to the implementation."
  • This may seem like an inevitable consequence of exists. but I claim it can be special-cased. Unparenthesised commas , within an exists. signal that the following functions thus take 3 arguments, not a triple:

    liftA2 :: forall f a b c. Applicative f => (a -> b -> c) -> (f a -> f b -> f c)
           :: forall f c. Applicative f => (exists a b. a -> b -> c, f a, f b) -> f c
           
    foo :: a -> a -> a -> Bool
        :: (exists a. a, a, a) -> Bool

    but foo' does take a single argument showing the difference between exists a. a, a, a and exists a. (a, a, a)

    foo' :: (a, a, a) -> Bool
         :: (exists a. (a, a, a)) -> Bool
    foo' (a1, a2, a3) = foo a1 a2 a3

    this would only be permitted in negative positions, so Int -> (exists a. a, a) doesn't make sense.
  • edit: Or phrased as a question, how would you rewrite this particular definition of Ran with an existential Functor z with a first-class existential while preserving the type of Ran?

    type Ran :: Constructor k -> Constructor k -> Constructor Type
    data Ran g h a where
      Ran :: Functor z => (forall x. z (g x) -> h x) -> z a -> Ran g h a

    Unless I am mistaken this is not possible because there is no way to talk about "two curried arguments" but that is what z scopes over:

      Ran :: (exists z. Functor z =/\ (forall x. z (g x) -> h x), z a) -> Ran g h a

@VitWW I'm looking forward to your ICFP paper :P

More seriously, I don't think that pseudo-type approach generalizes to other situations where existential types are used. For example if we want to convert a list into a length-indexed vector: toVec :: [a] -> exists n. Vec n a, then the pseudo-type would need to be infinitely large n = 0 | 1 | 2 | .... And the pseudo-type itself also seems complicated or at least needs more explanation.

@noughtmare Good point.
More precise, I expect for function toVec :: [a] -> exists n. Vec n a
that pseudo-type would be something like exists m. n = Nil | m | Succ m

But yes, I agree, this also requires some additional calculations

#473 (comment)
An existential quantifier is "just" an existential quantifier, it doesn't necessarily have anything to do with branching.

data Box = forall a . Box a
unbox (Box a) = a
-- unbox :: Box -> exists a. a

With dependent types you wouldn't need existentials for branching either. You can do this with type families and singletons in Haskell. If you don't want to use singletons, then you would start bringing in existentials (losing the information that the existential is simply the parameter). If anything, the existentials are here because you don't have dependent types and aren't using singletons, so you are forced to combine two different types by losing information where they differ.

I think (though am not certain) having the existential before the bool is unsound in your first example.

let f = fn @Int @Char :: exists c . Bool -> Int -> Char -> c

I could at this point unpack f to get c - the fixed, specific return type - and then apply the function with both False and True, which should give the same type (but really they won't - in one case c = Int in the other c = Char).
In this case you could argue that you can't make use of the result anyway so maybe it doesn't matter, but I don't know if that is true in all cases.

I think what you are imagining is a type nearly isomorphic to the existential that does not make use of existentials.
In the case of the Vec it would just be a list.
There is always (forall r . (forall a . F a -> r) -> r).

My update @Jashweii @noughtmare :

1. every n-ranked forall quantifier is a (n-1)-ranked exists quantifier
   that's mean (on pseudo-Haskell):

data exists a. Box = forall a. Box a
unbox :: exists a. Box -> a
unbox (Box a) = a
box :: a -> exists a. Box
box a = Box a
-- more flexible working with existential types
doublebox :: exists a. Box -> (exists a. Box, exists a. Box)
doublebox a = (a, a)
constbox :: exists a. Box -> exists b. Box -> exists a. Box
constbox = const
-- append :: [exists a. Box] -> exists a. Box -> [exists a. Box]
append    :: [exists a. Box] -> exists b. Box -> [exists c. Box]
append list b = b : list

2. More flexible branching exists quantifier

-- F(default, auto) c = Id c
-- c ~ a | b
fn ::  forall a b. Bool -> a -> b -> exists c. F c
fn c t f = if c then t else f

3. Surprisingly, functional-depended classes become classes with existential parameters:

-- class (Monad m) => MonadState s m | m -> s where ...
   class (Monad m) => MonadState (exists s. s) m where ...
-- class Foo a b c | a b -> c where ...
   class Foo a b (exists c. c)  where ...

how does this relate to rank N types and current existentially quantified types? are the representation equal or would we need to explicitly or implicitly convert between them?

@eldritch-cookie My posts were unrelated to current existentially quantified types. Which are de facto UpRankedExistentials .

So I've just create an alternative proposal #642
My proposal suggest to add DownRankedExistentials, the opposite to UpRankedExistentials.

@VitWW my question was about the proposal in general not your comment but i see how it could be misunderstood.
does this proposal permit Generic for GADTS? there was this 2018 blog post that mentions that some GADTS can't have an instance of Generic due to their representation needing existential types. Would this proposal help this specific usecase?

I see )))

tomjaguarpaw commented on Sep 8, 2023:

How important to this proposal is it that /\ is a special "magic" form? Put another way, if I had a version of GHC with the exists part of this proposal but not the /\, what would I lose?
[...]
Am I missing something, or does this proposal naturally split into two fairly orthogonal pieces?

Exactly how I felt when reading the proposal.

Note, I am far from understanding most of the technical details here. My position is that of a user of existentially quantified types as they are available now i.e. with GADTs; and suffering from the limitations that this proposal seems to be addressing, including but not limited to https://gitlab.haskell.org/ghc/ghc/-/issues/17130.

I find it sad that this proposal seems to have been abandoned.

I find it sad that this proposal seems to have been abandoned.

Me too. I'm currently heavily using singleton style and returning existentials from functions is a very common pattern. It's sad to have to either CPS or wrap everything in SomeThis/SomeThat.

How important to this proposal is it that /\ is a special "magic" form? Put another way, if I had a version of GHC with the exists part of this proposal but not the /\, what would I lose?

The very purpose of this proposal is to repair the discrepancy that, in the following table, four of the cells are first-class while two of them have to be expressed as encodings.

Adding exists but not (/\) would be half-baking the cake.

That's interesting, because that's not my understanding of the intention of the proposal. I would say that the intention, as with most of the proposals I've read recently, is to create something of use to Haskellers. Indeed the motivation section does not mention anything like your table. Furthermore, as far as I can tell, half baking this cake would be useful to Haskellers.

(It's possible that I've missed something, of course. Perhaps abstract consistency is more important than practical utility, or perhaps half baking the cake wouldn't be practically useful, for reasons not yet clear to me.)

You are creating a false dichotomy between "abstract consistency" and "practical utility". Abstract concepts are useful in practice, and Haskell has historically been one of the main languages to embrace this viewpoint.

Anyway, this discussion is pointless. As the proposal says:

We could imagine just adding exists without /\ (using e.g. Dict to accomplish the goal of /\). However, I think these features go nicely together: would we want forall without =>?

I'm not trying to create a dichotomy. I agree that many (not all) abstract concepts are useful in practice, and I would say that Haskell is the language that benefits most from this viewpoint. That's a major reason why I love Haskell.

What I am trying to suggest is that if this proposal naturally splits into two then it would be useful to make the split, because the first part provides incremental practical benefit even if it is lacking in some other regard.

I'm grateful that you pointed out to me that the proposal already touches on my suggestion. I didn't notice that! However, I disagree that further discussion is pointless. I think the proposal is mistaken in that regard. I would really, really, really love exists. It would make my day to day singleton style Haskelling much less unpleasant. In fact I can't overstate how important exists is for ergonomic use of data kinds. On the other hand, I don't think I strongly care about /\. (I may be mistaken of course. Maybe someone can see something I can't. If so then please try to convince me!)

Ideally I would love both, but if adding just exists is significantly easier than adding both exists and /\ then I think we should start with just that. (It doesn't preclude adding /\ later.) That's the issue I have least insight into however: is it significantly easier? Perhaps not!

Ideally I would love both, but if adding just exists is significantly easier than adding both exists and /\ then I think we should start with just that. (It doesn't preclude adding /\ later.) That's the issue I have least insight into however: is it significantly easier? Perhaps not!

My understanding is that the blockers have more to do with existentials than with implicit constraint packing (the former, as currently formulating, requiring significant changes to Core). That being said, my reading is that the design of /\ is also still more open than the one for the existential quantifier, and it may become an issue in the future. If that happens, I agree that splitting the proposal would be desirable. Right now, though, it doesn't seem to be really help move things forward.

Great to know, thanks @aspiwack! So it looks like my suggestion is moot, at least for the time being.

For what it's worth, I still have quite a bit of love for this proposal / direction of travel. What I don't have is time to really push this through. If someone else wants to become a champion here, I would happily support that person with e.g. weekly meetings, code review, etc.

For what it's worth, I still have quite a bit of love for this proposal / direction of travel. What I don't have is time to really push this through. If someone else wants to become a champion here, I would happily support that person with e.g. weekly meetings, code review, etc.

Let me add that the proposal involves a very significant change to Core, with lots of follow-on consequences. I'd not just a matter of implementation. We have not changed Core in such a significant way for over two decades.

Implementing it would give a clearer sense of what the costs would be. But it'd take quite a bit of effort, and then we might end up rejecting the proposal anyway. Yet, deciding whether to accept the proposal depends quite a bit on how hard it is to adjust Core.

I would love to have first class existentials too, but the price is fairly high, and I'm genuinely not sure if the pain justifies the gain. Not against, but rather cautious.

I just want to say that I agree with Simon here -- it's one of the reasons I haven't really pushed this forward. I think it would be great to have existentials. But it's a lot of work! And I agree that it's not clear the gain will be worth the implementation and specification effort.

I don't want to dissuade folks from volunteering here. But instead I would want people to come in eyes wide open about the potential challenges here.

Alternative algorithm of existential quantifier (without /\) to this proposal is "Extractable Existentials" with 642#issuecomment quite minimal changing the Core.

I was thinking about this recently and user datatypes, and got to re-thinking about @VitWW's idea, which I think I now get (but I might be wrong). I am curious if it is a real alternative to this, or if it plays well with type inference. Essentially instead of a witness type, you would infer refinement types of existential data types (for a variant you would need to know which constructor as well) that lift the existential type variable(s) to additional parameters of the refined type, thus also acting as Witness by naming the first part of the existential pair. Using this example datatype:

type Exists :: (Type -> Type) -> Type
data Exists f = forall a . MkExists (f a)
-- I am going to use MkExists @a but it is probably MkExists @f @a or MkExists @_ @a.
-- This would all work with (k -> Type) -> Type but would be yet another @ parameter.

In Haskell today MkExists @a :: f a -> Exists f (ignoring that f should probably come first). If Witness applied to Exists (I'm not saying it should) it would give you a. The refined version (represented here with ^ for additional refinement arguments) would have type f a -> Exists f ^a, thus not inherently losing the information. The unrefined version Exists f we see in Haskell today would be equivalent to exists a. Exists f ^a. You can imagine Exists f ^a as { x : Exists f | MkExists @b _ <- x, a = b }. This gives you a way of naming the first part of the existential pair via a refinement syntax, e.g. forall a. Exists f ^a -> f a or type instance Witness (Exists f ^a) = a. This would still want first class existential types and given/returned constraints i.e. exists and /\ ala forall and =>. There's no need for refined versions of the first class exists ... types since you can just use the body of the exists without the qualifier.

Edit:
The refinement type is just my understanding of the idea from that proposal, where I think it has confusing syntax where what is really a parameter is described using a quantifier. There's not really any inherent benefit (at least not justifying the cost) of supporting the refined version over never putting the existential in the datatype to begin with:

data Exists' f a = MkExists' (f a)
-- Exists f ^a = Exists' f a
-- Exists f = exists a . Exists' f a

Which incidentally is what I imagine people will do more often were first class existentials (strong or weak) supported.
Since this is ultimately just weak existentials, I suppose the question boils down to the benefits of strong existentials and it would be useful to see more examples in the proposal - e.g. does forall a . Outputtable a => a -> SDoc not subsume (exists a. Outputtable a /\ a) -> SDoc in the pprs example? The only thing immediately coming to mind is using record dot syntax instead of matching an existentially quantified record.

The main thing that has been dragging this proposal is the needs for changes to core.

I've been spending a bit of time thinking about Andreas Rossberg's 1ML line of work.

My understanding is that one component of 1ML is that you can elaborate of a language with open into a language with unpack. Namely, in 1ML, a module { type a; body = u[a] } behaves like exists a. u[a] in this proposal, with x.body corresponding to open x (see in particular Fig. 8, p26). 1ML then manages to encode provenance as a type gadget with no injection of terms in types. (I won't explain how, because if does feel like dark magic to me still). The elaboration targets a version of Fω with existential quantifier, which are eliminated with unpack (Fig. 4 p19). This master thesis targets a variant of system Fc instead.

So it seems to me that we can probably get away with a minimal modification to Core (as exists with unpack is basically a magic GADT). Could it help unblock this PR?

I don't think the insights from 1ML really apply here. 1ML contains a phase separation, where all module expressions can be resolved to values at compile time. This indeed avoids the troublesome need to inject terms into types, but it is not expressive enough to handle the cases, like filter over length-indexed vectors, that motivate some of the need for these existentials in Haskell.

1ML contains a phase separation, where all module expressions can be resolved to values at compile time

I don't think that's quite right. 1ML's modules are ordinary values. They can be function arguments, and they can be computed dynamically. The differences with ordinary records is that: 1ML modules can contain types, and 1ML module types' fields can depend on a type defined by another field.

The (critical!) phase distinction story is that, despite appearances static types cannot actually depend on dynamic values (you can have dynamic type values, but for a type to be able to branch on a such a value, the value must be known statically). This is the secret sauce. And I think it applies to your existentials. Probably. I hope?

Maybe there's a subtlety in your filter example, but if so I'm missing it.

The length in the filter example depends on a dynamic choice. Is that not dynamic enough?

I don't think it's too dynamic for 1ML, at least. Let's try. We give ourselves (I'm modelling the integers at sort type for simplicity, but I don't think it's necessary either)

type o
type s a
val vec : {
  type t n a;
  nil : t o a;
  cons : a -> t n a -> t (s n) a;
}

Now, I think the following will typecheck in 1ML:

let list = {
  type t a = {
    type ln; (* a nat really *) 
    b :  vec.t ln a
  };
  nil  : t a = {
    type ln = o;
    b = vec.nil;
  };
  cons : a -> t a -> t a = fun x xs -> {
     type ln = s (xs.ln);
     b = vec.cons x xs.b
  };
}

And from there, building filter : (a -> bool) -> vec.t n a -> list.t a is straightforward.

That looks reasonable... but I also think that the mini slice of dependent types as needed here is pretty fundamental (sadly). (Exception: we might plausibly be able to store just variables in types, not whole expressions.) Something has to give in 1ML -- maybe we can't achieve laziness the right way? I'm afraid I don't have the time to do an exploration of this.

I don't claim to understand the magic in 1ML's elaboration. But somehow, this is translated to just Fω + unpacking-existentials.

The catch seems to be that translating types to such a Core requires peppering them generously with existential quantifications. Which may not be such a good trade-off in that it may go against the grain of GHC's implementation. But I'm honestly not sure either way.

@aspiwack @goldfirere I working right now on try to add Existentials into system F and Core language with explicit types at Discourse:
Existential quantifier forany
You are welcomed to discussion!