Fwd: [Agda] Parallel or

[Alan Jeffrey]

On 11/16/2011 03:56 PM, Dan Doel wrote:
> On Wed, Nov 16, 2011 at 4:39 PM, Alan Jeffrey<ajeffrey at bell-labs.com>  wrote:
> You want to rule that out entirely? Or just rule out the extra
> definitional rewrites if the check fails?

I'd be tempted to go for the brutal (oh and not exactly 
backward-compatible) approach and rule it out entirely. I am cruel and 
heartless.

> I'm not sure I'm behind the former, but the latter is what I'd expect.
> I don't know how hard it is to check either, though.
>
> As for why the former is bad, I want to write definitions like:
>
>      foo T y = true
>      foo x T = true
>      foo x y = false
>
> Or, replace x and y with _ if you wish. And imagine that the data type
> that has T as a constructor also has 7 other nullary constructors, and
> I don't want to write out all the permutations that the last case
> covers.

This is true for defining functions, but breaks down a bit when you come 
to prove properties about foo, at which point you discover yourself 
having to write all the cases out anyway. And I find myself proving 
properties about programs more than I do writing them :-) For example:

   foo1 : forall x y -> foo x y == true -> (x == T \uplus y == T)
   foo1 T y z = inj1 refl
   foo1 x T z = inj2 refl
   ... oh dear lots of cases needed here ...

Mind you, since we're discussing vaporware programming languages at this 
point, you could say that the fix would be for the pattern-matcher to 
keep track of previously matched patterns, to allow that last line to be 
"foo1 x y ()".

A.

> -- Dan
>
>> Of course this would come with its own problems, e.g. checking critical
>> pairs may be expensive, throws up algorithmic issues (e.g. checking
>> unification of critical pairs may include recursive calls to the function
>> being checked, eeks) and it's yet another syntactic approximation to a
>> semantic property. So I can well believe there is a tar-pit there.