- Let F[α] = {m1:σ1,…,mj:σj}
- P:\A α\leqslant F[α].t → F[α]
- P = Λ α\leqslant F[α].λ( self:α).{m1:e1,…,mj:ej}
F-bounded constraint α\leqslant F[α]
Object instantiation:
\Y(P[σ]) for σ = μt.F[t]
We have P[σ]:σ→ F[σ] because F[σ] = σ
slide: Bounded type constraints