# Dynamic Existentials

**URL:** <https://discourse.haskell.org/t/dynamic-existentials/14903>\
**Category:** Uncategorized\
**Created:** [October 26, 2026, 11:07pm UTC](https://discourse.haskell.org/t/dynamic-existentials/14903 "2026-10-26T23:07:11Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [October 26, 2026, 11:07pm UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/1 "2026-10-26T23:07:11Z")

</div>

I spent over a year trying to improve my proposal how to easyly implement Existential types into the Haskell.

And I have a brilliant idea!  
In Haskel `forall` quantifier is stands for … input type!  
So we add `exists` quantifer for … output type! That means thatwe new the exact type in dynamic runtime only.

ForallType during Typecheck is checked and become Monomorhic by substitutional law.  
But ExistentialType during Typecheck is checked but remains Polymorphic. And … during runtime it could be substituted to Monomorphic type.

Dynamic Existentials do NOT cover all Existentials, but it covers 4 main cases

- Quasi Existentials

```haskell
   qex :: exists a.a
   qex = therefore @String in "Some small text"

```

- Extractable Existentials

```haskell
   data E = forall a. MkE [a]

   unE :: E -> exists a. [a]
   unE (MkE @e xs) = therefore @e in xs

```

- Branched Existentials

```hasell
   data T a where
       MkInt :: T Int
       MkBool :: T Bool

   serialize :: forall a. T a -> String
   serialize MkInt = "int"
   serialize MkBool = "bool"

   deserialize :: String -> exists a. T a
   deserialize "int" = therefore @Int in MkInt
   deserialize "bool" = therefore @Bool in MkBool

```

- Transit Existentials

```haskell
   someT :: exists a. T a
   someT = id $ deserialize "bool"

```

Here we see that we guarantee that during Runtime construction `therefore @ty in expr` allows to supstitute existential variable to monomorhic one.

We also change how to find a type from `case` expression: if any sub-type of type application is NOT the same, but still have same kind, then we replace this column type to existential variable.

And the last change: substitutional hierarchy to

```haskell
Int < exists a. a < forall b. b

```

The full proposal you could find here [Proposal: DynamicExistentials](https://github.com/ghc-proposals/ghc-proposals/pull/773)  
You could react, like or comment there or here.

But here I have a question: what did I wrote **WRONG**?  
Any suggestion are welcomed!

---

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [October 27, 2026, 10:57pm UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/2 "2026-10-27T22:57:18Z")

</div>

With Output Existentials it is possible to write Nat-Vectors:

```haskell
data Nat = Zero | Succ Nat

type Vec :: Nat -> Type -> Type
data Vec n a where
  VNil :: Vec Zero a
  (:>) :: a -> Vec n a -> Vec (Succ n) a
infixr 5 :>

toVec :: forall a. [a] -> exists (n::Nat). Vec n a
toVec [] = therefore @Zero in VNil
toVec (x:xs) = therefore @(Succ m) in x :> tvxs
   where
     tvxs :: exists m. Vec m a
     tvxs = toVec xs

filterVec :: forall a (n::Nat). (a -> Bool) -> Vec n a -> exists (m::Nat). Vec m a
filterVec p VNil = therefore @Zero in VNil
filterVec p (x :> xs) = if
      | p x -> therefore @(Succ r) in x :> fpxs
      | otherwise -> therefore @r in fpxs
   where
     fpxs :: exists r. Vec r a
     fpxs = filterVec p xs

```

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 28, 2026, 2:45am UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/3 "2026-10-28T02:45:17Z")

</div>

> [@VitWW](#):
>
> In Haskel `forall` quantifier is stands for … input type!

I think this is not true. (Or I don’t understand what you’re claiming.) Consider

- read :: forall a. Read a =\> String → a

The forall’d type is the output type. And it must be Universally quantified, so that whatever calls `read` can type-safely consume that type.

> [@VitWW](#):
>
> during runtime it could be substituted to Monomorphic type.

Haskell is a statically-typed language. Inference can’t wait ‘til runtime to find out what some return type is. Because whatever consumes that result then has no guarantees for type safety.

A GADT wraps a unknown/constrained type inside a Constructor. Its type only gets exposed within code that explicitly `case`-matches on that constructor. The type can’t escape that scope, because that would destroy type safety.

Perhaps those who’ve hearted the post could explain what merit they see?

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 28, 2026, 6:57am UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/4 "2026-10-28T06:57:55Z")

</div>

> Richly typed programming invariably uses its share of existential types, [quoting from the Motivation]

I think that’s not true. There’s a style of Haskell (“Finally tagless”) that deliberately avoids existentials and GADTs. Rust programming doesn’t support GADTs (and I understand has no plans to); you can achieve the effect via overloading and traits — something akin to Haskell type classes and Associated Types.

Rust considers type inference for GADTs to be too complex. I wish you would just not make claims like “vastly easier” when you are in no position to know. If there were an easier way, I’m sure the discussion around #473 would have considered it.

I believe existentials are in the long-term plan for Dependent Haskell. Again if there were a straightforward approach, it would be more prominent.

---

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [October 28, 2026, 8:37am UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/5 "2026-10-28T08:37:49Z")

</div>

> Consider
> 
> ```haskell
> read :: forall a. Read a => String → a
> 
> ```
> 
> The forall’d type is the output type.

Even if it looks like a return type, but first BEFORE the computation during compile time (except 1 case) it was used as INPUT type.

> Haskell is a statically-typed language. Inference can’t wait ‘til runtime to find out what some return type is.

Hopefully, Haskell ALREADY support Runtime for types (this 1 exception)

```haskell
 data E = forall a. MkE [a]

 lengthE :: E -> Int
 lengthE (MkE @e xs) = L.length @e xs

```

What I try - split this function in 2:

```haskell
 unE :: E -> exists a. [a]
 unE (Mk @e xs) = therefore @e in xs

 lengthE = L.length . unE

```

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 29, 2026, 6:23am UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/6 "2026-10-29T06:23:38Z")

</div>

> [@VitWW](#):
>
> `lengthE (MkE @e xs) = L.length @e xs`

`length` nowadays has two type params, so that code is wrong. How are you going to express the needed typing for `therefore`?

In any case, `length` is a poor example because it doesn’t care about the element type. Instead, consider:

- `maximum :: (Foldable t, Ord e) => t e -> e`

So with `maximum . unE`, `unE`’s output existential is to be `maximum`’s input _and_ its output. Does this mean `maximum` must output an existential? How does that work? Or must I create a different version of `maximum`? And presumably of every other function/method that wants to consume an existential.

Furthermore, `maximum` needs `Ord`. How to push that inside `MkE`? Or might `maximumE` just fail at runtime?

The proposal is silent about use-cases.

Talking about function outputs only is too much dumbing-down: every output becomes an input to the next function. Rather than making anything “vastly easier”, this has arrived at vastly unworkable.

---

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [October 29, 2026, 7:54am UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/7 "2026-10-29T07:54:11Z")

</div>

Wow! So many good questions!

> Furthermore, `maximum` needs `Ord`. How to push that inside `MkE`? Or might `maximumE` just fail at runtime?

You are right - we cannot guarantee, that `MkE` has a type which is bounded by `Ord`!  
That’s why such code `maximum . unE` fails during a compile time!  
Yes, we need to push boundaries inside the `data` first and transitively preserve them:

```haskell
data E' = forall a. Ord a => MkE' [a]

unE' :: E' -> exists a. Ord a => [a]
unE' (MkE' @e xs) = therefore @e in xs

```

> Or must I create a different version of `maximum`? And presumably of every other function/method that wants to consume an existential.

No-no, `maximum` and other functions works perfecly fine with existentials.  
Code `maximum . unE'` is right!

> So with `maximum . unE`, `unE`’s output existential is to be `maximum`’s input _and_ its output. Does this mean `maximum` must output an existential? How does that work?

As I wrote, existential type FITS INTO forall type by substitutional hirarchy.  
Like `[Int]` is a valid input type for `forall a. Ord a => [a]`, with same substitutional logic `exists b. Ord b => [b]` is also valid for input (but not vice versa).  
Yes, total return type of such expression is also existential and it is typechecked so. But we must remember, that during Runtime type would become monomorphic and instance would be chosen correctly.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [October 29, 2026, 1:03pm UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/8 "2026-10-29T13:03:57Z")

</div>

It seems to me that if you work out all the details (like the desugaring to Core) you’ll find that your proposal basically needs many of the same things that [#473](https://github.com/ghc-proposals/ghc-proposals/pull/473) has.

In particular, as you note, universal quantification is a kind of dependent function and existentials are a kind of dependent tuple (which you call “output type”). You need to construct them, which you propose to do with this `therefore @a in x` syntax, #473 calls this `Pack a x` (the `a` is a required type argument). One thing that I’m missing from your proposal is that you also need to be able to access the components of the existential. In #473 it is just a constructor, you can also just pattern match to get out the type and the value.

Another problem is that you cannot simply use `exists a. Ord a => [a]` to represent a list of existential but orderable values, because `=>` is a function-like thing whereas you need a tuple like thing for constraints too. That’s why #473 introduces the `/\` type former to represent constraint tupling and you’d write `exists a. Ord a /\ [a]` which desugars to a 3-tuple in Core containing the type, the class dictionary, and the value (of course the type is erased at run-time).

---

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [October 29, 2026, 8:26pm UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/9 "2026-10-29T20:26:06Z")

</div>

> It seems to me that if you work out all the details (like the desugaring to Core) you’ll find that your proposal basically needs many of the same things that #473 has.

These 2 cases are a bit different. 473 tries to add existentials in more general form than my proposal.  
He has Witnesses, Packing and Unpacking, rising expressionts to types and store them.  
But in my proposal a lot of things are done automatically, we have a math guarantee, that type variables satisfies existential laws.

> In particular, as you note, universal quantification is a kind of dependent function and existentials are a kind of dependent tuple (which you call “output type”).

From the math perspective? Maybe. But from the architectural perspective - `forall` just means input type (it appears in LHS part of equation only) and I suggest that `exists` means output type (it appears in RHS part of equation after some evaluation) and in signatures existentials are always a return type.

> Another problem is that you cannot simply use `exists a. Ord a => [a]` to represent a list of existential but orderable values, because `=>` is a function-like thing whereas you need a tuple like thing for constraints too. That’s why #473 introduces the `/\` type former to represent constraint tupling and you’d write `exists a. Ord a /\ [a]` which desugars to a 3-tuple in Core containing the type, the class dictionary, and the value (of course the type is erased at run-time).

This is what I don’t fully understand. But `ExistentialQuantifier` extension does not require any `/\`. That’s why I think `=>` is good enough.

> You need to construct them, which you propose to do with this `therefore @a in x` syntax, #473 calls this `Pack a x` (the `a` is a required type argument).

No, we do not need any Constructor, because during copile time we **don’t know** which type is used, so nothig could be preserved inside the Constructor. Hopefully we have a guarantee, that during Runtime the specific type would be known due `therefore` construction.

> One thing that I’m missing from your proposal is that you also need to be able to access the components of the existential. In #473 it is just a constructor, you can also just pattern match to get out the type and the value.

Typececk works in compile time **only** , but in compiling time we don’t know specific type, so nothing we could access to.

---

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [October 29, 2026, 9:20pm UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/10 "2026-10-29T21:20:24Z")

</div>

I just think, that maybe “iutput” word confuse people a bit.  
Maybe it is more right to call them “Evaluated Existentials”. Has this new name more clear meaning?

---

<div class="post-metadata">

**Author:** ![VitWW](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vitww/32/4184_2.png) [@VitWW](https://discourse.haskell.org/u/VitWW)\
**Post date:** [November 9, 2026, 10:31am UTC](https://discourse.haskell.org/t/dynamic-existentials/14903/12 "2026-11-09T10:31:52Z")

</div>

I’ve update the name of topic and the name of proposal.  
Any feedback is welcomed!

What is in my proposal wrong or incorrect?