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!
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.
Output Existentials do NOT cover all Existentials, but it covers 3 main cases
Quasi Existentials
qex :: exists a.a
qex = therefore @String in "Some small text"
Extractable Existentials
data E = forall a. MkE [a]
unE :: E -> exists a. [a]
unE (MkE @e xs) = therefore @e in xs
Branched Existentials
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
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.
With Output Existentials it is possible to write Nat-Vectors:
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
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.
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?
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.