• id = Λ α. λx:α.x id : \A α. α→ α
  • twice1 = Λ α.λf: Λ β. β→ β. λx:α. f[α](f[α](x)) twice1 : \A α. \A β. (β→ β) → α→ β
  • twice2 = Λ α.λf: α→ α. λx:α. f(f(x)) twice2 : \A α. (α→ α) → α→ α
  
  • id [ Int ] ( 3 ) = 3

  • twice1 [ Int ] ( id )( 3 ) = 3

  • twice1 [ Int ] ( S ) = illegal

  • twice2 [ Int ] ( S )( 3 ) = 5

slide: Parametrized types -- examples