Go backward to Record Types and Inheritance Go up to Top Go forward to Object Oriented Programming

Bounded Quantification 'n Subtyping

• Mix subtyping and polymorphism.
  • value f₀ = fun(x: {one: Int}) x.one
    f₀({one = 3, two = true})
  • value f = all[a] fun(x: {one: a}) x.one
    f[Int]({one = 3, two = true})
• Constraint all[a <=T] e
  • value g₀ = all[a <= {one: Int}] fun(x: a) x.one
    g₀[{one:Int, two:Bool}]({one=3, two=true})
• Two forms of inclusion constraints:
  • In f₀, implicit by function parameters.
  • In g₀, explicit by bounded quantification.
• Type expressions:
  • g₀: forall a <= {one: Int}. a -> Int
• Type abstraction:
  • value g = all[b] all[a<={one: b}] fun(x:a)x:one
    g[Int][({one:Int,two:Bool})]({one=3,...})