[Agda] Parallel or

[Alan Jeffrey]

A niave question about dependent pattern-matching...

One of the problems I keep hitting in writing Agda programs is having to 
choose an order for pattern matches, because of the fall-through 
semantics. The prototypical example is boolean or:

   _or_ : Bool -> Bool -> Bool
   true  or y     = true
   x     or true  = true
   false or false = false

This definition of or gives true as a left unit up to beta-reduction, 
but true as a right unit only up to propositional equality. (Ditto the 
units for natural addition, list concatenation, etc. etc.)

I have a half-baked idea that the semantics of pattern-matching could 
instead be nondeterministic, so any pattern that matches does so and 
causes beta-reduction, without worrying about if it is masked by an 
earlier case. In the case above, (M or true) would reduce to true, even 
if M is a (meta-)variable.

Of course to get normalization, the compiler would have to check 
critical pairs and ensure syntactic identity of the rhs, and I can 
imagine that this might be painful.

Has anyone already baked (or burned) this idea?

A.