Fwd: [Agda] Parallel or

[Dan Doel]

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