Conor McBride wrote:
Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway)
But unification is what you get by adding non-linearity. Sure, all terms are ground; would you prefer I said "testing for membership in an element of the RATEG class"?
For more ickiness about RATEG, it's not closed under compliment and the emptiness problem is undecidable (so dead code elimination can't always work). Even restricting to the closed subset (aka "tree-automata with (dis-)equality constraints") leaves emptiness undecidable, though there are a couple still more restricted classes that are decidable.
cf ch.4 of TATA <http://tata.gforge.inria.fr/> -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
