Fwd: [Agda] Parallel or

[Dan Doel]

On Wed, Nov 16, 2011 at 4:39 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> I went off to the epigram mailing list archives, were you meaning the
> discussion around Berry's majority function, e.g.
> http://article.gmane.org/gmane.comp.lang.epigram/183 ?

Yes, that's the one.

> I think I'm (er kind of) proposing something less radical, which is a static
> check to ensure that overlapping definitions unify. This would rule out your
> example:
>
>> foo true y = 1
>> foo x false = 2
>
> since there's a critical pair given by (foo true false) which don't unify.

You want to rule that out entirely? Or just rule out the extra
definitional rewrites if the check fails?

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.

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