P = Λ α \leqslant F[α].λ( self: α).{…}
C = Λ α \leqslant G[α].λ( self:α).P[α]( self ) \with {…}
with recursive types
F[α] = {i:int, id:α→ bool}
G[α] = {i:int, id:α→ bool, b : bool}
Valid, because G[α] \leqslant F[α]
However \Y(C[σ]) \not\leqslant
subtype
\Y(P[τ])
slide
:
Inheritance and constraints