Haskell GADT Existentials
An existential is a value whose inner type is hidden inside a wrapper. A ShowBox value keeps only the Show constraint of its hidden value.
ShowBox hides one value behind Show
ShowBox 42 hides an integer. showBox prints it through Show.
{-# LANGUAGE GADTs #-}
data ShowBox where
ShowBox :: Show a => a -> ShowBox
showBox :: ShowBox -> String
showBox (ShowBox x) = show x
main :: IO ()
main = do
putStrLn (showBox (ShowBox 42))
putStrLn (showBox (ShowBox 3.5))
One list holds different hidden types
Each list item hides a different type. showBox shows every item.
{-# LANGUAGE GADTs #-}
data ShowBox where
ShowBox :: Show a => a -> ShowBox
showBox :: ShowBox -> String
showBox (ShowBox x) = show x
boxes :: [ShowBox]
boxes = [ShowBox 7, ShowBox True, ShowBox "cat"]
main :: IO ()
main = mapM_ (putStrLn . showBox) boxes
Only Show operations work on the hidden value
showAll turns every box into text. The count of boxes is three.
{-# LANGUAGE GADTs #-}
data ShowBox where
ShowBox :: Show a => a -> ShowBox
showBox :: ShowBox -> String
showBox (ShowBox x) = show x
boxes :: [ShowBox]
boxes = [ShowBox 7, ShowBox True, ShowBox "cat"]
showAll :: [ShowBox] -> [String]
showAll = map showBox
main :: IO ()
main = do
print (length boxes)
putStrLn (unwords (showAll boxes))
Example
{-# LANGUAGE GADTs #-}
data ShowBox where
ShowBox :: Show a => a -> ShowBox
showBox :: ShowBox -> String
showBox (ShowBox x) = show x
boxes :: [ShowBox]
boxes = [ShowBox 7, ShowBox True, ShowBox "cat"]
main :: IO ()
main = do
print (length boxes)
mapM_ (putStrLn . showBox) boxes
Key points
- Existential: a wrapper that hides the inner type of its value.
- ShowBox: ShowBox wraps any Show value and hides its type.
- Constraint: only the Show constraint survives the hiding.
- Shown list: a list of ShowBox values can hold integers, booleans and text together.
- Recovery limit: the hidden type cannot be recovered from a ShowBox value.
In this example, boxes is a list of three ShowBox values with different hidden types. The main action prints the count first and then shows each hidden value on its own line.
Note
an existential needs the GADTs form with a constraint on its constructor.
Try it Yourself
Edit the code, then press Run.
Running is simulated · Haskell Playground
Exercise
What survives when a value is hidden inside a ShowBox?