Introduce the obapx.PROC/obapx.DEF Extension

[orcmid]

[updated 2020-06-14T15:42Z to connect related issues.]
[updated 2020-05-25T25:43Z to clarify further and express commitment to having it.]
[updated 2020-05-21T22:20Z to clarify a bit more on the value of .proc.]
[updated 2020-01-15T15:43Z to add the ¶ condition and tidy up a bit.]
[updated 2024-02-01T00:32Z to correct the ¶ condition and also formalize def x

Although it is premature until the implementation and definitions are more-advanced, I have a few extensions in mind. This one is about scripts made into individuals.

proc Extension

There are two new primitives, obapx.PROC and obapx.DEF.

obapx.ap(obapx.PROC, p) determines an individual, standing for the script that p is. Designate that individual by proc(p). The computation model obapx has everything that obap does, along with identified obapx primitives and their computational interpretation. We can similarly define

dev(proc(p)) = p

such that

def(x) ≠ x ⇔ x = proc(def(x))

and, more strongly,

def(x) = x ⇒ ¬∃(y)[ x = proc(y) ]

proc(p) = proc(q) ⇔ p = q

q = proc(p) ⇒ q ¶ p
q = proc(p) ⇒ p ¶ q

obapx.ap(proc(p), x) = ev(p, x, p) = obapx.ap(p, x).

obapx.ap(obapx.DEF, q) yields p for which q = proc(p) and yields q otherwise.

From this, it is the case that when obapx.ap(obapx.DEF, q) ≠ q, q is a proc.

An ob that is not a proc is not equal to any proc.

We have

Since ob p is essentially the unique identifier of proc(p), the canonical form for proc(p) is the expression obapx.PROC(cfp) which can be written proc(cfp) for short with cfp the canonical form of p.

Why?

• proc(p) can be thought of as an encapsulation of the script, p.

• proc(p) is a distinct individual and all conditions on individuals apply to it. In particular, obapx.eval(proc(p)) = proc(p), preserving encapsulation of the script p.

• Although a proc script can be inspected by "reflection," since obapx.(obapx.DEF, proc(p)) = p, the intended confinement of proc semantics to the applicative interpretation, is signaled.

• Accordingly, lambda abstraction does not reach into the p of proc(p). proc(p) could be abstracted out of its occurrences in an ob taken as an applicative script though, just like any other (non-primitive) individual, as a form of refactoring.

• An accelerator (Seeking oMiser Accelerators #26) can be used in implementation of a proc's application, so long as the result (and application of obapx.DEF) are indistinguishable. The sealing of a script in a proc also cues the applicative semantics and restricted semantics with regard to interior applications (e.g., in the Capsule Hack, Make Stateful Constructions: The Capsule Hack #23).

Discussion

I did not originally consider having obapx.DEF, except there needed to be a canonical form, and oFrugal had to have a way to produce it. There is to be a serialized form of obs for retention in files and interchange, and that needs to be able to convey procs also.

Although I am not a fan of reflection in object-oriented programming systems, I see how it is compelled in the case of oMiser once any kind of procedural encapsulation is employed.

I had wondered about an alternative formulation, using

obap.ap(proc(p), x) = ev(proc(p), x, p)

as a way of having some sort of purity around the definition and use of procs. Unfortunately, this breaks the guarantee about equivalence to obap.ap(p, x) and then requires that p require

.def :: .self

to access its own code as data.

The reliance on extensional equality for the proc(p) perpetuates a very strong condition applied in oMiser. It seems appropriate that all obs be "comparable," even at this elementary level. Work on deduction will address how to take this further in appropriate contexts.

It may well be that the proc(x) approach is a solution looking for a problem to solve. I submit that the Capsule Hack (issue #23) is additional evidence that proc is invaluable in the creation of semblances akin to programming-language objects and their interfaces.

[orcmid]

Provision of this feature requires a number of steps.

1. There needs to be a an obapxtheory.txt covering this extension and any related ones, such as potential need for an obapx.tail operator. The Capsule Hack (Make Stateful Constructions: The Capsule Hack #23) and establishment of a specific convention for stateful entities is also important. Of particular interest is handling of "compute expressions" in the F# sense.

2. The grammar must reflect the case of .proc(exp), not because it is needed, but because there must be a kind of meta- approach to producing it in canonical forms.

3. Procedures for output of obs by oFrugal must present case (2) and any pretty-printing needs to treat it.

4. The serialization of obs for persistent storage and reloading must express and accept the form.

This (3-4) follows from the insistence on extensional identity for oMiser. That will not be abandoned lightly. It is a basis for accelerators (#26), with need for higher-order deductions to simulate and expose anything richer. It is a purpose of the oMiser project to reveal such consideration.