Existential types

Existential quantification
Existential types
Module abstraction
Dependent pairs
Encoding in universal types
ExistentialQuantification in Haskell

Haskell

{-# LANGUAGE RankNTypes #-}


{-
data ToString = forall a. ToString (a -> String, a)
-}

{-
data ToString where
  ToString :: (a -> String) -> a -> ToString
-}

newtype ToString = ToString (forall z . (forall a. (a -> String) -> a -> z) -> z)

toString :: (a -> String) -> a -> ToString
toString s a = ToString $ \f -> f s a


foo :: [ToString]
foo = [toString id "he", toString show 11, toString show ()]

main :: IO ()
main = putStrLn $ foldr (\(ToString t) acc -> t (\s a -> s a) ++ acc) "!" foo