[Haskell-cafe] conflicting variable definitions in pattern

[Conor McBride]

On 16 May 2009, at 03:54, wren ng thornton wrote:

> 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.

Hang on a minute: we're solving for sb in sb(p)=v not
in sb(s)=sb(t)...

> Sure, all terms are ground;

...which makes it a rather special and degenerate and
unawesome case of unification: the kind of unification
you don't need a unification algorithm to solve.

> would you prefer I said "testing for membership in an element of the  
> RATEG class"?

I'm not familiar with that terminology, but I'll
check out the link.

> 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/>

Let's be clear. The suggestion is only that a slightly
more compact notation be permitted for functionality
already available via guards or view patterns. It
cannot introduce any dead code elimination problems
which are not already present.

I'm sorry, but I just don't see the bogeyman here.

All the best

Conor