Abstract:
We present an 
time type inference algorithm for a type
system with a largest type 
, a smallest type 
, and the usual
ordering between function types. The algorithm infers type annotations of
minimal size, and it works equally well for recursive types. For the problem
of typability, our algorithm is simpler than the one of Kozen, Palsberg, and
Schwartzbach for type inference without . This may be
surprising, especially because the system with is strictly more
powerful.
Available as PostScript, PDF, DVI.