[Haskell-beginners] The Holy Trinity of Functional Programming

[Jay Sulzberger]

On Wed, 22 Aug 2012, Costello, Roger L. <costello at mitre.org> wrote:

> Hello Christopher,
>
>> But do you think you could provide a
>> more "real world" example of an application
>> of the "Holy Trinity" ideas?
>
> A commonly cited real-world example that illustrates the first key idea (recursive data type) is a binary tree:
>
> data Tree = Node String Tree Tree | Leaf
>
> The elements of this data type include:
>
> 	Leaf
>
>        	Node "Root" Leaf Leaf
>
> 	Node "Root" 	(Node "Left" Leaf Leaf)
> 			(Node "Right" Leaf Leaf)
>
> 	And so forth.
>
> Common functions on this data type include insertions, deletions, traversal.
>
> I am not sure if there is a use for the infinite value of this data type.
>
> /Roger

Let us leave aside two kind of things:

1. _|_

2. "infinite" things

Let us define a signature Sig to be a structure like so:

1. We have a finite set Names.

2. For each name a in Names we have a finite non-negative
    integer, called the "arity" of a.

Note that we allow a name, say a, to have an arity of zero.  Such
names are called "constants" in some formalisms and distinguished
from names with an arity greater than zero.

We define a structure, sometimes called a "model" or an "algebra
with signature Sig", to be:

1. A nonempty set S.

2. For each name a of arity n we have a function f: S^n -> S,
    where
    a. S^n is the Cartesian product of S
    b. f is everywhere defined on S^n and f is single-valued

If we call our model M then we may use this notation:

1. The ground set of M is S, which we write as Ground(M).

2. The f associated to the name a is M(a).

We now define the set of terms, which set we call "Terms", over our signature:

1. Given a name a and list of terms of length n, where n is the
arity of a, t0, t1, .. t(n-1) the list a, t0, t1, ... t(n-1) is a
term.

2. Terms is the minimal set which satisfies 1.

Now, given a signature Sig, we may translate this setup into Haskell.
We do an example.  Let Sig be given as follows:

   Names is the set {a, b, c, d, e, f}.

   The arities are
    a has arity 0
    b has arity 0
    c has arity 0
    d has arity 1
    e has arity 2
    f has arity 5

   the set Terms over Sig is in one to one correspondence with
   those values of this type in Haskell:

   Data T = Ta | Tb | Tc | Td T | Te T T | Tf T T T T T

(If I have made an error in the translation please tell me.)

So, for the special case of "term algebras", or absolutely free
algebras, or "magmas", over a finite set of generators (here
taken to be the names with zero arity) and a finite set of
operations we get a natural, ah mystic word of power, isomorphism
with a certain simple kind of type in Haskell.

This special case is one of the paradigm cases in Type Theory.

One of the standard texts on Universal Algebra, Birkhoff style:

    A Course in Universal Algebra
     ** The Millennium Edition **
    by
    Stanley N. Burris and H.P. Sankappanavar

is at

    http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html

The discussion of signatures begins on page 25, and the
discussion of term algebras on page 68.  (The treatment is less
good for people studying programming than I remembered it as
being.)

New Types workers have undertaken the large task of extending the
theory of ordinary algebras to "algebras" with such things as _|_
and (+ a (+ b (+ c ... .  But new phenomena appear, and, when
starting the study of type theory, even in the practical case of
learning Haskell, it is good to take one concept at a time.

Note that in this special case, clearly to every term of type T
corresponds a (labeled) tree.  In our example the leaves, that
is, nodes with zero children, are labelled with Ta, Tb, and Tc,
and the interior nodes with one child are labelled by Td, with
two by Te, and with five by Tf.

So for this paradigm case, "definition by pattern matching" has a
natural first cartoon: we watch a dot race down the tree of the
given term, and at each node, ah, I now restrain myself from the
rest of the standard rant.

And I now notice that I have not made use of the concept "Model over a Sig".
Heaven forwarding, I will rant^Wpost more.

oo--JS.


PS. ad use of one infinitely downward branching tree: Often paths
in this particular binary tree, which is often called "The
Infinite Binary Tree", are taken, modulo a subtle equivalence
relation, to be the reals between 0 and 1.