[xsl] The Holy Trinity of Functional Programming ... Is there a way to define recursive data types in XSLT 2.0?

["Costello, Roger L." <costello@xxxxxxxxx>]

Hi Folks,

Professor Richard Bird has written extensively on functional programming. In
one of his books he has a fascinating discussion on three key aspects of
functional programming, which he calls the holy trinity of functional
programming.

The first key aspect is:

	User-defined recursive data types

He gives an example (Haskell notation):

	data Nat = Zero | Succ Nat

The elements of this data type include:

	Zero,  Succ Zero,  Succ (Succ Zero),  Succ (Succ (Succ Zero)),  ...

Is there a way in XSLT 2.0 to define recursive data types? If yes, how would
the Nat data type be defined in XSLT 2.0?

/Roger

P.S. For those interested, below is my summary of Bird's discussion on the
holy trinity of functional programming.

---------------------------------------------------------
The Holy Trinity of Functional Programming
---------------------------------------------------------
These three ideas constitute the holy trinity of functional programming:

1.  User-defined recursive data types.
2.  Recursively defined functions over recursive data types.
3.  Proof by induction: show that some property P(n) holds for each element of
a recursive data type.

Here is an example of a user-defined recursive data type. It is a declaration
for the natural numbers 0, 1, 2, ...:

	data Nat = Zero | Succ Nat

The elements of this data type include:

	Zero,  Succ Zero,  Succ (Succ Zero),  Succ (Succ (Succ Zero)),  ...

To understand this, when creating a Nat value we have a choice of either Zero
or Succ Nat. Suppose we choose Succ Nat. Well, now we must choose a value for
the Nat in Succ Nat. Again, we have a choice of either Zero or Succ Nat.
Suppose this time we choose Zero, to obtain Succ Zero.

The ordering of the elements in the Nat data type can be specified by defining
Nat to be a member of the Ord class:

	instance Ord Nat where
         	      Zero < Zero 		=  False
        	      Zero < Succ n	=  True
        	      Succ m < Zero	=  False
        	      Succ m < Succ n 	=  (m < n)

Here is how the Nat version of the expression 2 < 3 is evaluated:

	   Succ (Succ Zero) < Succ (Succ (Succ Zero))	-- Nat version of 2 < 3

	= Succ Zero < Succ (Succ Zero)			-- by the 4th equation defining order

	= Zero < Succ Zero				-- by the 4th equation defining order

	= True						-- by the 2nd equation defining order

Here is a recursively defined function over the data type; it adds two Nat
elements:

	(+) :: Nat -> Nat -> Nat
	m + Zero = m
	m + Succ n = Succ(m + n)

Here is how the Nat version of 0 + 1 is evaluated:

	   Zero + Succ Zero				-- Nat version of 0 + 1

	= Succ (Zero + Zero)				-- by the 2nd equation defining +

	= Succ Zero					-- by the 1st equation defining +

Here is another recursively defined function over the data type; it subtracts
two Nat elements:

	(-) :: Nat -> Nat -> Nat
	m - Zero = m
	Succ m - Succ n = m - n

If the Nat version of 0 - 1 is executed, then the result is undefined:

	Zero - Succ Zero

The "undefined value" is denoted by this symbol: _|_ (also known as "bottom")

Important: _|_ is an element of *every* data type.

So we must expand the list of elements in Nat:

	_|_,  Zero,  Succ Zero,  Succ (Succ Zero),  Succ (Succ (Succ Zero)),  ...

There are still more elements of Nat. Suppose we define a function that
returns a Nat. Let's call the function undefined:

	undefined :: Nat
	undefined = undefined

It is an infinitely recursive function: when invoked it never stops until the
program is interrupted.

This function undefined is denoted by the symbol _|_

Recall how we defined the ordering of values in Nat:

	instance Ord Nat where
  	      Zero < Zero 		=  False
  	      Zero < Succ n	=  True
  	      Succ m < Zero	=  False
  	      Succ m < Succ n 	=  (m < n)