Confusion over the "existential wrapper" of Haskell
From the Haskell file:
import GHC.Exts (Constraint)
-- |Existential wrapper
data Some :: (* -> Constraint) -> * where
Some :: f a => { unSome :: a } -> Some f
I know what Constraint
a different view represents *
, which can be used to categorize the types of contexts that appear to the left of =>
.
But in what sense is the Some
existential wrapper? How can this be used as such?
source to share
The weird GADT / record syntax that doesn't look like it should compile aside, we can figure out what's going on here by setting f ~ Eq
:
Some :: Eq a => a -> Some Eq
So given the Eq
uatable thing, we get the Some Eq
uatable thing out of this. 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 "forgot" the exact type of the value, but we "remembered" that it is Eq
uatable.
The GADT you provide is just a generalization of this from Eq
to anything with the look * -> Constraint
:
(Eq :: * -> Constraint) (Char :: *) :: Constraint
(f :: * -> Constraint) (a :: *) :: Constraint
As for why it is called "existential", GADT hides the implicit one forall
in the constructor declaration:
Some :: forall a. f a => { unSome :: a } -> Some f
After pattern matching, Some f
you will get a value of a type f a => a
where a
it cannot escape its scope for technical reasons. (Which is called skolem ). You can use the CPS combinator to make it 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
one that shows the Some Show
capable thing. It is called "ambiguous" because it is ambiguous in which the actual type is used (i.e. it works for ambiguously show $ Some 'a'
and ambiguously show $ Some "asdf"
)
We cannot do
disambiguate :: f a => Some f -> a
disambiguate (Some a) = a
due to the above skolem limitation.
My (unpublished) library related to this is even more general looking.
source to share