Go backward to Variant Types and Recursion Go up to Top Go forward to Polymorphic Functions

Universal Quantification

• Typed lambda-calculus describes monomorphic functions.
  • Unsufficient to describe functions that behave the same way for argumentes of different types.
• Introduce types as parameters:
  • value id = all[a] fun(x:a) x
    id[Int](3)
• May omit type information:
  • value id = fun(x:a) x
    id(3)
  • Type-checker reintroduces all[a] and [Int]
• Polymorphic types:
  • type GenericId = forall a. a -> a
    id: GenericId
  • value inst = fun(f: forall a. a -> a)(f[Int], f[Bool])
  • value intid: Int -> Int = fst(inst(id))
    value boolid: Bool -> Bool = snd(inst(id))