Ponder's type system is unusual. It is more powerful than the
extended by
Haskell. Ponder adds extra recursive 'mu' types
to those of Girard's
System F, allowing more general
["Ponder and its Type System", J. Fairbairn, TR 31, Cambridge
U Computer Lab, Nov 1982].
[J. Fairbairn, "Design and Implementation of a Simple Typed
Language based on the Lambda-Calculus", Technical Report
No. 75, Computer Laboratory, University of Cambridge, May
1985].
[J. Fairbairn, "A New Type-Checker for a Functional Language",
Technical Report No. 53, Computer Laboratory, University of
Cambridge, 1984].
[J. Fairbairn, "Some Types with Inclusion Properties in
forall, rightarrow, mu", Technical Report No. 171, Computer
Laboratory, University of Cambridge, Jun 1989].
[Valeria C. V. de Paiva, "Subtyping in Ponder (Preliminary
Report)", Technical Report No. 203, Computer Laboratory,
University of Cambridge, Aug 1990].