From a Haskell file:
import GHC.Exts (Constraint)
-- |Existential wrapper
data Some :: (* -> Constraint) -> * where
Some :: f a => { unSome :: a } -> Some f
I know that Constraint represents a kind distinct from * that can be used to categorize context types that appear to the left of a =>.
But in what sense is Some an existential wrapper? How could it be used as such?
The strange GADT/record syntax that doesn't look like it should compile aside, we can understand what is going on here by setting f ~ Eq:
Some :: Eq a => a -> Some Eq
So, given an Equatable thing, we get Some Equatable thing out of it. Let's apply this to 'a' :: Char and see what happens:
(Some :: Eq Char => Char -> Some Eq) ('a' :: Char) :: Some Eq
As you can see, we have "forgotten" the exact type of the value, but "remembered" that it is Equatable.
The GADT you provide is simply a generalization of this from Eq to anything with kind * -> Constraint:
(Eq :: * -> Constraint) (Char :: *) :: Constraint
(f :: * -> Constraint) (a :: *) :: Constraint
As for why it is called "existential", the GADT hides an implicit forall in the constructor declaration:
Some :: forall a. f a => { unSome :: a } -> Some f
Once you pattern match on Some f, you get a value of type f a => a, where a can't escape its scope for technical reasons. (Which is called skolem) You can use a CPS combinator like this to work with it:
ambiguously :: (forall s. f s => s -> r) -> Some f -> r
ambiguously f (Some s) = f s
Now you have ambiguously show :: Some Show -> String, which shows Some Showable thing. It is called "ambiguously" because it is ambiguous in which actual type it is using (ie it works for ambiguously show $ Some 'a' and ambiguously show $ Some "asdf")
We can't do
disambiguate :: f a => Some f -> a
disambiguate (Some a) = a
because of the aforementioned skolem restriction.
My (unpublished) library related to this, with an even more general kind.
