Albert Graef Interview Continuation - Constructor Symbols and Constructors with Equations

This is a continuation of the Interview With Albert Gräf - Author of the Pure Programming Language, going more in depth about rewrite rules for data structures and functions.

It is recommended to read the Data Structures section of the Pure Primer before reading this interview as it covers basics of user-defined data structures in Pure and is referred to in this interview.

Keeping with the spirit of term rewriting, Pure eliminates the segregation of "defined functions" and "data constructors". Any function symbol can occur in a normal form term, so a (pure) constructor symbol is nothing but a function symbol which happens to not have any equations. This might first seem like an arcane feature, but it makes it possible to deal with symbolic terms and "constructors with equations" in a direct fashion. For instance, if you want you can write constructor equations for the "list cons" (denoted ':', like in Haskell) which keep your lists sorted and duplicate free:

> x:y:xs = y:x:xs if x>y; x:y:xs = x:xs if x==y;
> [13,7,9,7,1]+[1,9,7,5];
[1,5,7,9,13]

In this example is ':' the constructor symbol?

Yes.

I was wondering if you could give another example or two of the use of constructor symbols and constructors with equations.

You can find a useful example in the prelude, namely the "poor man's tuples":

> show ","
infixr 1200 ,;
x,() = x;
(),y = y;
(x,y),z = x,y,z;

Those are the equations for the tuple constructor ','. (Note that parentheses aren't part of the tuple syntax in Pure, so (x,y) means just x,y; the parentheses are used for grouping only. And ',' is a right-associative infix operator declared in the prelude just like any other. Thus the right-hand side x,y,z of the 3rd equation should in fact be read as x,(y,z).)

Tuples in Pure are somewhat unusual in that they are always "flat". The above equations take care of that. In fact, they just say that the empty tuple () is left- and right-neutral with respect to ',' and that the ',' operator is associative.

For instance:

> (a,b,c),(d,e);
a,b,c,d,e
> (a,b,c),();
a,b,c
> (),(a,b,c);
a,b,c

So tuples are in effect a flat variation of the list data structure in Pure. (I decided to define them that way in the prelude since it reflects common mathematical usage, and there already are the list and matrix data structures if you need a nestable aggregate.)

Note that this is all just normal business in Pure. In fact, any function symbol effectively becomes a constructor symbol if you apply it to some arguments for which there is no corresponding rewriting rule. Thus you could in fact say that (+) is a "constructor with equations", too. For instance, we have:

> 5+(a,b);
5+(a,b)

Of course, you might decide at any time that you want to be able to add a value and a tuple, so that 5+(a,b) isn't a normal form any more. Easy, just add a rule which does that:

> x+(y,z) = x+y,x+z;
> 5+(a,b);
5+a,5+b

You see, the point here is that there's really no distinction between "functions" and "constructors" in term rewriting, that's all just in your head. ;-)

Can you comment on the example given in the Data Structures section of the Pure Primer?.

If you look at my examples again you will notice that the special thing about "constructor equations" is that a symbol is used both as the head symbol (or function symbol) and in the argument patterns of the left-hand side of a rewriting rule. That's not the case in Sergei Winitzki's example, you just have a pure constructor named 'Point' with two arguments there, and some equations for (+) on terms formed with this constructor. That's all very conventional, you'd do it exactly like this with Haskell's algebraic types, too. In contrast, the self-sorting list and flat tuples examples will never work in Haskell, since Haskell doesn't allow the use of non-constructor symbols in argument patterns.

I am not sure what you mean by head symbol. Are you saying that function symbols can be used in the left-hand side of rewrite rules, and this is not the case in Haskell?

Exactly. What I meant by "head symbol" is the function symbol which comes "first" on the left-hand side of a rule (considering operators to be denoted in prefix notation). So, in the rule

(Point x1 y1) + (Point x2 y2) = Point (x1+x2) (y1+y2);

the infix operator (+) is the head symbol (not Point), and in

get_x (Point x1 y1) = x1;

get_x is the head symbol. In traditional FP parlance, the head symbol is the function being defined, and 'Point' just plays the role of a "dumb" constructor symbol here, it doesn't have any equations of its own. In Haskell, this would be impossible anyway, because 'Point' would always be a constructor there, end of story. But in Pure you might well add another equation like

Point x y = Point (x-y) y if x>y;

if you want (this is pretty useless in this specific example, but just to illustrate the idea). Considering 'Point' as a constructor, you'd then call this a "constructor equation".

The rule

(x,y),z = x,(y,z);

is even more illuminating since ',' is used both as the head symbol and inside an argument pattern there. Thus, in traditional terms it's the "function" being defined and a "constructor symbol" at the same time. This is possible because in Pure there's in fact no distinction between these.

(As a Lisp programmer, another way you can look at this is that an
unquoted term like (foo x y) becomes "self-quoting" if it is in normal form, i.e., if there's no rule which allows it to be rewritten.)