On Wed, 22 Aug 2012, Costello, Roger L.
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.