Existential types

Created: 2023-01-12 16:42

Existential type, Haskell Wiki

Existential types are a feature in some programming languages, such as Haskell, that allow type variables to appear on the left side of a type signature but not on the right side. This can be useful when the specific type of a value is not important, as long as it can be used in a certain way.

An example with GADTs

data Stepper :: * -> * where
  Stepper :: s -> (s -> (a, s)) -> Stepper a
 
step :: Steper a -> Stepper a
step (Stepper x f) = Seppter (snd $ f x) f
 
look :: Stepper a -> a
look (Stepper x f) = fst $ f x

In the example of Stepper Int, the specific type of s is not revealed. However, this is not a concern, as the primary focus is on how Stepper interacts with that particular s to obtain the subsequent value of type a. This demonstrates the utility of existential types, as they allow for abstraction and flexibility when the exact type is not crucial to the functionality of the code.