Mon Feb 15 09:59:00 CET 2010
If it's a pain to write reduction systems, why not compile them from a
higher level description? Yes, Haskell is not Scheme (convenient
syntactic abstraction), and it's also not MetaOCaml (templates might
be ill-typed) but it's halfway in the middle.
On the practical side: if both the data types and the pattern matching
on these types are generated at the same place, maybe some constraints
of the generated code can be captured in the types of the generator?
Goal: find out how to generate an algebraic rewrite system from a
specification as equalities, i.e. find out if Knuth-Bendix can be used
to build the rules (unary vs. binary?).
EDIT: This seems to be way to far-fetched. Cas.hs turned out to be
quite straightforward. See prev post.