Type inference with non-structural subtyping

Jens Palsberg, Mitchell Wand, Patrick O'Keefe · Formal Aspects of Computing · 1997

Abstract We present an O(n 3 ) 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 least shape, 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.

Read the paper · More papers on PaperTik