Fwd: [Agda] Parallel or

[Alan Jeffrey]

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 ?

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.

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.

A.

On 11/16/2011 02:14 PM, Dan Doel wrote:
> Bah, copying the list with this. Sorry for the duplication.
>
> ---------- Forwarded message ----------
> From: Dan Doel<dan.doel at gmail.com>
> Date: Wed, Nov 16, 2011 at 3:13 PM
> Subject: Re: [Agda] Parallel or
> To: Alan Jeffrey<ajeffrey at bell-labs.com>
>
>
> There was a discussion about this sort of thing back in the day on the
> old Epigram mailing list. I don't recall much coming of it (although
> now thinking back, I almost want to say someone had a system that did
> better that I never got around to looking at).
>
> For one, I think it was agreed that the runtime semantics wouldn't be
> expected to change. However, it might be possible to extend the static
> evaluation machinery to do more intelligent rewriting (epigram 2 does
> (in theory) a lot of rewriting that doesn't happen during runtime
> evaluation, like 'map id' to 'id'). However, you do have to be
> careful, as you can have a series of clauses such that the first
> clause invalidates the second's admissibility as a rewrite. For
> instance:
>
> foo true y = 1
> foo x false = 2
> ...
>
> You obviously can't just rewrite 'foo x false' to 2 for neutral x. I
> don't know how hard it is to decide these conditions in general,
> though.
>
> Anyhow, you might want to go check the old epigram logs for this past
> discussion and see what all went on there (there's also an amusing
> flame war of sorts in that section).
>
> -- Dan
>
> On Wed, Nov 16, 2011 at 2:39 PM, Alan Jeffrey<ajeffrey at bell-labs.com>  wrote:
>> 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.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda