Fwd: [Agda] Parallel or

[Alan Jeffrey]

The problem with or-patterns is that if they still have fall-through 
semantics, then defining:

 >       or True _ || or _ True = True
 >       or False False = False

gives True as the left and right zero for or, but doesn't give False as 
a unit, compared with:

   true  or y     = true
   x     or true  = true
   false or y     = y
   x     or false = x

which would give both zeros and units.

A.

On 11/17/2011 01:21 AM, wren ng thornton wrote:
> On 11/16/11 4:39 PM, Alan Jeffrey wrote:
>> 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.
>
> Alternatively, rather than trying to automatically determine the
> equivalence of the RHS, we could enforce it syntactically / require it
> intensionally by introducing or-patterns a la OCaml. Thus,
>
>       or True _ || or _ True = True
>       or False False = False
>
> (using whatever syntax you'd prefer.)
>
> That's still just a syntactic approximation to semantic properties, but
> at least it's a relatively decent syntactic approximation instead of
> something completely ad hoc.
>
>
>
> Yet a different alternative is that we could take the masking as a
> feature rather than a burden. Thus defining,
>
>       or False False = False
>       or _ _ = True
>
> In theory, given (or x y) if we can prove either x=True or y=True, then
> we should be able to force the whole expression to evaluate to True.
> This approach would also work for addition on naturals. However, it
> doesn't scale as well as the or-pattern option, because it's not clear
> how to get it to cover non-atomic cases like
>
>       mplus Nothing (Just x) || mplus (Just x) Nothing = Just x
>
> and the moral equivalents, where we're binding variables but we don't
> care about exactly where they come from.
>