Lambda the Ultimate

It seems to me that the way even constructors can be captured by pattern variables makes it hard to keep things well-encapsulated. For example, if one implements lists with binary trees, one cannot expose multiple binary constructor/destructor pairs (e.g. cons and splitting in halves). To a certain extent, that can be alleviated by overloading on arity. I suppose that it can also be "solved" by first expliciting which constructors to expose by default via a ~casting operation.

EDIT: I was also wondering how the definition of generic equality works in the presence of a wildcard constant. It's defined as a constant, not as a variable, so its behaviour can't be fixed by making the set of bindings variables empty.

On another more pragmatic note, it seems to me that making the behaviour of patterns dependent on data that can only be known at runtime (the binding variables of patterns, when the latter are passed around) will make it hard to compile the language well, not to mention the way every datum must be a pattern. At least, binding variables must be used linearly. Being able to receive arbitrary patterns means that one either compiles datum to patterns as needed, or makes every datum a pattern, so that constructors build both datum and patterns in parallel. I don't think that sounds too bad, except if you want to support multiple constructors.

Hi everyone, I'm new to this forum and have just the read the post.

1) The pattern calculus (PC) is good for handling multiple representations of data structures. For example, if the list cons x xs is given by the binary tree node (leaf x) xs then one can write a pattern-matching function of the form

next ==
leaf \x --> x
| cons \x \y --> x
| node \x \y --> next x

(where \z indicates that z is bound). The pattern for the cons case reduces to

| node (leaf \x) \y -> x

2) Generic equality on wildcards is no different from any other value

equal _ reduces to

_ --> true
| \y --> false

so that the wildcard _ is equal to anything. Again, equal (leaf _) reduces to

leaf _ --> true
| \y --> false

which will match with any leaf.

3) compilation model. Implementation work is not sufficiently developed to give complete answers on this point, but if the reduction rules are simple then there should be a good implementation.