Go backward to Recursive Definitions Go up to Top Go forward to Information Hiding

Existential Quantification

• Existential type quantification:
  • p: exists a. t(a)
  • For some type a, p has type t(a)
• Examples:
  • (3, 4): exists a. a x a
  • (3, 4): exists a. a
  • Constant can satisfy different existential types!
• Sample existential types:
  • type Top = exists a. a (type of any value)
  • exists a. exists b. a x b (type of any pair)
• Particularly useful:
  • x: exists a. a x (a -> Int)
  • (snd(x))(fst(x))