Non-uniform Recursion: The solution (minimal sorting for fold)

  Martin Wehr

submitted to MFCS200 (Mathematical Foundations of Computer Science)

A central data structure in functional programming languages like
ML or Haskell are algebraic data types. I argue in this paper that 
the natural program structure to deal with algebraic data types is 
not yet provided either in Haskell or in ML. One might think that 
that pattern matching together with general recursion is the natural 
program structure to deal with algebraic data types. But the use of 
general recursion runs into trouble when faced to deal with non-uniform 
recursive data through fundamental problems of type inference 
(the non-decidability of minimal typing for polymorphic recursion).

What we provide for algebraic data types is a structural recursion 
mechanism that derives generalised fold functions from algebraic 
data specification. Especially non-uniform folds are an byproduct 
of these more general folds. The structural recursion mechanism is 
presented together with a typing method which relies on a method of 
minimal sorting for algebraic data specifications.