Dynamic Existentials

Uncategorized
1

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
       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
  • Transit Existentials
       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

Int < exists a. a < forall b. b

The full proposal you could find here Proposal: DynamicExistentials
You could react, like or comment there or here.

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

2 Likes
2

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
1 Like
3

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?

4

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.

5

Consider

 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)

 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:

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

 lengthE = L.length . unE
6

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.

1 Like
7

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:

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.

8

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.

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).

6 Likes
9

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.

10

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?

12

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

What is in my proposal wrong or incorrect?