「継承はサブタイピングではない」[Cook90]

…のメモ。再帰的な型 T を、

T = µt.F[t]

と書くとき、

T  = µt.{a:int, c:t, b:t→t}
T1 =    {a:int, c:T, b:T→T, d:bool}
T2 = µt.{a:int, c:t, b:T→t, d:bool}
T3 = µt.{a:int, c:t, b:t→t, d:bool}

で、
T1, T2 は T のサブタイプだが、T3 はそうではない（型 T3→T3 は、型 T→T のサブタイプではないから）。

また、再帰的な型 T = µt.F[t] と同様の再帰的構造を持つ t ならば、

t ≤ F[t] (t は F[t] のサブタイプ)

を満たす、らしい。ｗ　上の例では、T = µt.F[t] において、

F[t] = {a:int, c:t, b:t→t}