Standard ML with polymorphic recursion: Examples

Example 1

A disadvantage of monomorphic recursion is that although datatypes with increasing type parameters can be defined in SML, recursion along the structure of their data is impossible: Suppose we store data of type 'a, indexed by structured keys, in a tree-like datastructure called 'a trie.

datatype key = 
     Atom of int | Pair of key * key
datatype 'a trie =
     Empty | Branch of ((int * 'a) list) * (('a trie) trie)

For atomic keys, the data are stored in the first component, a list, while for compound keys, the data for all keys with the same first component are grouped into a trie structured according to the second component of keys. The search by recursion on key structure,

exception NoEntry
fun find (Branch((c,a)::l,_), Atom(d)) = 
         if d=c then a else find (Branch(l, Empty), Atom(d))
  | find (Branch(_,t), Pair(p,q)) = find (find (t,p), q)
  | find (_, _) = raise NoEntry

is untypable in SML: since 'a tries contain ('a trie) tries, functions recurring along the structure of 'a tries need more complex types at recursive calls than at top level. However, the principal Milner-Mycroft type

val find = fn : 'a trie * key -> 'a

is returned by SML/NJ [Poly Rec].

Example 2

In mutual recursive definitions, one sometimes uses a residual function with different types at different occurrences, which may lead to untypability when using monomorphic recursion. For example,

fun map f [] = [] 
  | map f (x::xs) = (f x) :: (map f xs) 
and mapTwice l = map (fn n => 2 * n) l 
and mapNot l = map not l

is untypable in SML, while SML/NJ [Poly Rec] returns

val map = fn : ('a -> 'b) -> 'a list -> 'b list
val mapTwice = fn : int list -> int list
val mapNot = fn : bool list -> bool list

More examples are given in the distribution package.

Further applications of polymorphic recursion

Polymorphic recursion should also be useful in typing object-oriented programs, where the type of a recursive functions depends on the classes which implement sections of the function (so each section is likely to have different type).
M.Tofte uses a restricted version of polymorphic recursion for region inference in his KIT compliler for SML.
M.Rittri showed that type inference for dimension-polymorphic recursion, which is useful on datatypes for polynomials and power series where the coefficients have dimensions, is a computable extension of ML-type inference. (Proc. 7th Conf. on Functional Programming Languages and Computer Architecture, 1995).

Back to main page for SML [Poly Rec]

Created: Mon Mar 16 18:30:06 MET 1998
Last modified: Thu Mar 9 13:31:37 MET 2000