Effects and Proofs

Running procedures backwards is nice at times, particularly for matching in case statements. However it is only going to work when there is no information loss (procedure is 1-1), and most complex procedures aren't. I think I know how to run more complex things, like factorial, backwards (to stop arms of a case going into infinite loops you run the cases in coroutines, and when one succeeds kill the others and restart them with the improved parameter). However that will very rarely be useful. The current scheme probably hits the sweet spot in usefulness.

So I should move onto more important things: Effects and Proofs.

My simple-minded idea of effects is that they arise in types where the semantics includes the time. For example an Assignable(X) has a stream of assignments with associated times, and a stream of accesses with associated times, and the semantics specify that the result of an access is equal to the value of the most recent assignment. Similarly IO operations typically need to be done in some order (not necessarily linear: some can be done in parallel). The plan is to provide a framework for this, but leave any specific cleverness to the types themselves (and their related operational properties).

First we introduce a new (special) type TimeOrder. This always starts as a future time, then turns into an actual time when passed. Time related operations use the ! operator. There is also !< and any other time related operators should include an !.

• `t ! expression means that the expression should happen at TimeOrder t. This is infix !.
• ! expression allocates a nameless time. This time specifies that the expression is executed in lexical order relative to other ! expressions in the current closure. This is prefix !.
• t1 !< t2 means that t1 must happen before t2.

So consider:

`t1 ! expr1; `t2 ! expr2; `t3 ! expr3; t1 !< t3; t2 !< t3

This says that t1 is before t3, and so is t2, but t1 and t2 can be in either order (or concurrent). TimeOrder entities can be passed around like any other. If a call to a procedure is not done with a bang (!), then, even if it has IO or other effects internally, it will be treated like any other expression and may be executed in any order or not at all.

It is not yet clear whether this simple treatment can be used by libraries to achieve the control of effects that we are coming to expect.

The next issue is proofs. I need proofs, and it seems that the language should be well designed to allow them, but I can't seem to figure it out.

Propositions are dependent types which are proved by constructing an inhabitant. Wombat supports dependent types and uninhabited types. Proofs are programs, i.e. procedures. That shouldn't be a problem.

Let's suppose that a % sign indicates a proposition as a type. Let's consider 1 <% 2 (natural numbers). This type is inhabited. Maybe it is useful to think about what the inhabitants are like and what relation they have to each other. Proofs are programs, meaning a closure in Wombat. So I guess it takes no input and generates an object of the type. Suppose we have some builtin stuff (axioms):

• zeroLessThanNonZero takes n:Nat and returns an element of the dependent type 0<%n.
• moveLessUp takes an n<%m and return an element of type succ(n)<%succ(m).

Now our proof of 1<%2 is { 1 |> zeroLessThanNonZero |> moveLessUp } where x|>f means f(x).

Now suppose we have a proposition "for all abc there exists xyz such that prop(abc,xyz)". This also has a (different) procedural view where forall corresponds to input and there exists corresponds to output. That should suit Wombat where we access to both in the body of the closure. So first of all we have something like: { $=`abc; `$=`xyz; code-generating prop(abc,xyz) }. Then we have to turn that into a proof. We must be pretty close.