We already have a proposal Packed Existentials , but it has very limited use.
I propose an ALTERNATIVE: to add Polymorphic existentials (and Monomorphic existentials)
Quantifiers:
∀a : forall a. a is a monomorphic Set
∃b : exists b. b is a polymorphic Set
☥c : forunique c. c is a monomorphic element of Set
Constraint operations of Sets
a ≡ b : a =~ b Sets a and b are equal
a ⊆ b : a <~ b Set a is a subset of b
a ∈ b : a !~ b a is an element of b
a | b : a | b Union of Sets a and b
a \ b : a \ b Remove set b from a set
Some axioms and rules
For forunique:
1) let forunique a. then a ~ a
For forall and exists:
1) let exists a. then a =~ a
2) let exists a b. if a =~ b then b =~ a
3) let exists a. then a <~ a
4) let exists a b c. if a <~ b, b <~ c then a <~ c
5) let exists a b. then a | b =~ b | a
6) let exists a b. then a <~ a | b
7) let exists a b. then a | b \ b <~ a
Narrow Type < Wide Type
1) (forunique a: a) < (exists b. forunique a. a !~ b. b)
2) (forunique a: a) < (forall b. forunique a. a !~ b. b)
3) (forall a: a) < (exists b. forall a. a <~ b => b)
4) (forall a: a) >! (forall a. forunique b. b !~ a. a)
5) (exists a: a) < (exists b. exists a. a <~ b => b)
6) (exists a: a) >! (exists a. forunique b. b !~ a => b)
All real data, which consists forall a is simplified to some specific Int, String, ....
Same with real data exists a: a is simplified to some specific exists a. forunique b. b !~ a => b.
But not all existential data is reducible.
- Irreducible Compound-valued (self-recursive type), like
exists a. [a] - Irreducible Compound-argument types, like
exists a. (a, a)
Some examples:
fromEither :: forall a b. exists c. c =~ a | b => Either a b -> c
fromEither (Left a) = a
fromEither (Right b) = b
2-ranked forall
data exist a. Box a = forall b. b =~ a => MkBox b
fromBox :: exists a. Box a -> a
fromBox (MkBox a) = a
multitypedList :: exists a. [Box a]
multitypedList :: exists a. a =~ String | Int | Maybe Int => [Box a]
multitypedList = [MkBox "a", MkBox 1, MkBox (Just 5)]
multitypedList :: forall c. [Box c]
multitypedList :: forunique b. [Box b]
multitypedList :: [Box String]
multitypedList2 = [MkBox "a", MkBox "bb", MkBox "ccc"]
Class as named existential function (it is not part of proposal), just for clarification:
class Eq a where
(==) :: Eq a => a -> a -> Bool
instance Eq Int where
instance Eq String where
-- pseudo-haskell
type exists Eq
(==) :: forall a. a =~ Eq => a -> a -> Bool
override type exists Eq = Eq | Int
(==) :: Int !~ Eq => Int -> Int -> Bool
override type exists Eq = Eq | String
(==) :: String !~ Eq => String -> String -> Bool
and depended classes:
class C a b | a -> b where
-- pseudo-haskell
class C a (foruniuqe b. b) where
Promoted Sum-Type
Promoted Sum-Type is … existential!
data Nat = Zero | Succ Nat
-- promoted, pseudo-haskell
data exists 'Nat = 'Zero | 'Succ 'Nat
About Vectors:
type Vec :: Nat -> Type -> Type
data Vec n a where
VNil :: Vec Zero a
(:>) :: forall a n. a -> Vec n a -> Vec (Succ n) a
vecUnique :: forall a. forunique m. exists n. n =~ Nat, m !~ Nat => Vec n a -> Vec m a
vecUnique x = x
filter :: exists m. forall a n. n =~ Nat, m =~ Nat => (a -> Bool) -> Vec n a -> Vec m a
filter p VNil = VNil
filter p (x :> xs)
| p x = x :> (vecUnique (filter p xs))
| otherwise = filter p xs
fromList :: forall a. exists n. n ~ Nat => [a] -> Vec n a
fromList [] = VNil
fromList (x:xs) = x :> (vecUnique (fromList xs))