The type system is generalized to permit regular types, which are possibly infinite types that are unrollings of finite trees. For example, this makes possible a definition of Curry's Y combinator:
dec Ycurry : (alpha -> alpha) -> alpha; --- Ycurry f <= Z Z where Z == lambda z => f(z z);This fails in the usual type system because Z must have a function type with argument type the same as the whole type.
Type synonyms are now allowed to be recursive, so they can be used to describe infinite types, like the type of infinite sequences:
type seq alpha == alpha # seq alpha;Recursive uses of the type constructor being defined must have exactly the same arguments as the left-hand side. However, these arguments may be permuted, as in
type alternate alpha beta == alpha # alternate beta alpha;The syntax of types is also extended to express regular types. For example, the above two types could be defined as
type seq alpha == mu s => alpha # s; type alternate alpha beta == mu a => alpha # (beta # a);This notation is also used by the system to print regular types.