Rewrite Combinators in Haskell [pdf]

dev.stephendiehl.com

20 points·tenslisi··2 comments

I’m always torn with term rewriting: it seems a nice way to express many ideas but also brittle to changes, potentially hard to follow, and often requiring difficult and various proofs of termination.

There are easier cases (typically imposing either some ordering and requiring rules be strictly monotonic) but these are difficult to make useful. Searching for matches is also difficult to do efficiently.

I tried to implement a term-rewriting system for computer algebra once and it ended in disaster.

On the other hand I feel like a (possibly more real time) datalog would be a great tool in many cases.

Advice I received from a logic programming researcher concerning my own attempts to make a C++ logic programming library: "I think that a good model [...] is rewriting not lambda calculus."

Yet I still struggle to find a good way to integrate that as a DSL. The problem is that it is natural to use functions and lambdas of the host language to package usage of the DSL expressions, but that is a leaky abstraction: you need variables of the logic DSL to act nonlocally, yet you would like to be able to reason locally about branches of the full expression tree. These are mutually exclusive. For functional programming we want to treat the terms as values, but for non-local connections (same variable in two different subexpressions) we need variables to have semantics of pointers. And what of memory management...

Reply on news.ycombinator.com