Guards? Or what? about mary HOT 8 CLOSED

Merged!

from mary.

Re Booleans, we must not use [] as false if we're sticking with explicit environments, because [] is the empty environment, i.e., trivial success. I'm minded to go with 0 and 1.

I'm also toying with the idea that 0(-) aborts without evaluating its argument and 1(x) is x.

That's to say, guarding is also contextualization.

from mary.

The key question here is at what point we commit to a match. Too early, and we lose the ability to recover from failure. Too late, and we leak space like bastards, remembering all the alternative things we might do that we're just not going to do.

How do we signal that commitment? Is that what -> does? Perhaps.

from mary.

One thing I've done on the explicit-environments branch is to rename the match-failure effect to 'abort (either for running out of clauses or in a matching expression). I do wonder whether the operator

catch('abort,):
catch({'abort() -> _}, k) = k()
catch(x,_) = x

as used in

catch(e1,{e2})

deserves to be

e1 <something> e2

Pro tem, I'll use ?>. Binds weakly, so p1 = e1 ; a1 ?> p2 = e2 ; a2 has a go at the 2s if e1 aborts or fails to match p1 or a1 aborts.

from mary.

Might we write

{ p1.1,..p1.n | g1.1 -> e1.1 | g1.2 -> e1.2 |.. g1.k1 -> e1.k1
  p2.1,..p2.n | g2.1 -> e2.1 | g2.2 -> e2.2 |.. g2.k2 -> e2.k2
  ...
  pm.1,..pm.n | g2m1 -> em.1 | gm.2 -> em.2 |.. gm.km -> em.km
}

?

We find a row of ps which match the inputs, then each g contextualizes its e, but if g(-) aborts, we try the next guard in the same clause, or the next clause, if we've run out of guards. However, once we cross the ->, we commit: if an e aborts, the whole function application aborts.

Does that make sense? (Of course, the same notation works for function definition as well, except there we have f(p1.1,..p1.n) | g1.1 -> e1.1 ....)

from mary.

At some point we will also need notation for suppressing effects. The simplest form of this is something like

'foo ^ e

which means that if e does a 'foo, it is handled by the second-most local 'foo handler, instead of the most local. That is, when we're looking in the context for a handler, as well as holding the name that we're looking for, we also hold a counter, initially 0. Each 'foo ^ puts a frame in the context, and when handling 'foo, that frame causes the counter to increment. When we find 'foo handler, we run it if the counter is 0, but if the counter is more than 0, we decrement it and keep on outward.

So,

{ p1 | g1 -> e1
  p2 | g2 -> e2
}

means the same as

{ x -> p1 = x ; g1 ; 'abort ^ e1 ?> p2 = x ; g2 ; 'abort ^ e2 ?> 'abort() }

where ?> associates rightward. That is, once we commit to e1, we also suppress the power of ?> to handle 'abort. However, a match failure in p1 or a guard failure in g1 cause an 'abort which is handled by the first ?>, and so on.

from mary.

On the explicit-environments branch, I've now made '0 and '1 the Boolean constants. Booleans guard; numbers don't.

from mary.

Bikeshedding has thus far confirmed ?> and ^, despite flirtation with other options.

Meanwhile, on the right, you have either one -> e, or at least one guarded form, those being | g -> e or | -> e.

The translation via prioritization and masking makes guarding very easy to implement.

from mary.