Object semantics
-- fixed point $ %s = F[%s] $
\Y ( %l( self ).F( self ) ) : %s
Unrolling
-- unraveling a type
%m %a.F[%a] = F[ %m %a.F[%a] ]
Example
T =
\
%m
\
%a
.{ a:int, c:
\
%a
, b:
\
%a
->
\
%a
}
T_1 = { a:int, c:T, b:T->T, d:bool }
T_2 =
\
%m
\
%a
.{ a:int, c:
\
%a
, b:T->T, d:bool }
T_3 =
\
%m
\
%a
.{ a:int, c:
\
%a
, b:
\
%a
->
\
%a
, d:bool }
T_1, T_2 <= T
,
T_3 \not<= T
\zline{(contravariance)}
slide
:
Recursive types -- examples
