Guards? Or what?

[pigworker]

Before we can even think about guards, we should ask how Boolean values are to be represented. Is it [] and 'true? Is it 0 and 1? Is it altogether more wibbly-wobbly?

Nothing is stopping us doing p | g -> e or the like.

I guess my question is whether p -> (1=g)(e) should mean the same thing.

When should IncompletePattern requests be handled by offers of alternative matches? Fun design space.

[pigworker]

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.

[pigworker]

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.

[pigworker]

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.

[pigworker]

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

[pigworker]

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.

[pigworker]

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

[pigworker]

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.

[pigworker]

Merged!