What's the REPL/Ob input/output notation?

[orcmid]

Here breaking down topics raised in #1 for separate threads.

@rnd0101: I want to see ... if I can make REPL from Coq representation.

The Miser REPL Idea

MAJOR UPDATE 2018-02-01 reflecting the latest thinking for the oFrugal REPL

MODEST UPDATE 2018-02-09 with adjustment to use of back-tick, not apostrophe

The basic idea for an oFrugal REPL is to have a written (i.e., text) form for reading obs as expressions, ob-exp. So the R-Read part is to accept the text, parse it, and provide any diagnostics in case the input is not well-formed, The E-Eval part consists of the evaluation of the parsed text, to arrive at the ob that the expression determines. The P-Print part is to then present that result in the same ob-exp text form used for input. This particular Read-Eval-Print-Loop notion stems back to the original implementation of LISP.

A common idea is to present the result in a form that, if itself read (via R-Read), the E-eval would produced the same result. There are other ways for the result to be retained, and the REPL may need command variations. That is, the REPL can accept statements, not just expressions for obs, and have more flexibility. That is all for oFrugal to handle, since, in the Miser project, it is oFrugal that provides a human interface for exercising oMiser operation.

Key Point 1 In the oFrugal formulation of a REPL, the ob-exp that is read is a formula for an ob. The Eval stage evaluates the ob-exp to compute the ob that is expressed. From this perspective, it is appropriate for the default P-Print to produce the result in the R-read notation that could be read back in to reconstruct the same ob without any applicative operations required.

Key Point 2 In the oFrugal notation, the :: and ‵ operators instruct the construction of the ob being read. In this notation, ( ... ) is for grouping, white space is for separation, and the symbols are all for individuals. By convention, primitive individuals all have names begun by "." and lindies all have names begun with a letter.

In the typography, the ‵-character has Unicode code point U+2035 (reversed prime). (Ed.Note: The Reader will allow ` (grave accent, the back-tick) for that, but output should always be the reverse-prime when Unicode is supported. The use of ` should not be used in code snippets because of conflicts raised if pasted into Markdown notation.

Key Point 3 there are "sugared" forms that the reader also accepts as expressions for obs. These can be chosen as more-expressive of an intended use of an ob for data or to include applicative-expressions to be used as part of the derivation of the resulting ob. The Eval process always produces a canonical ob, if it produces anything. So the output (Print) is always for a canonical ob.

The written text for oFrugal ob expressions is sketched in the file omiser/ob.txt. This file may also help in the explanation of the separation of obtheory from obaptheory, with the second an application atop the first, with supplemental additions in Ot, the theory language.

The ob-exp grammar and its interpretation are specified in the file ob-exp.txt. All future examples employ that notation.

WITH THE AVAILABILITY OF A PRECISE GRAMMAR AND EVALUATION, THIS TOPIC IS NOW CLOSED

[rnd0101]

FYI, I've produced quick-n-dirty Python version (I have not checked it yet though)

PS. Code not quite good, lindy handling most likely buggy. I will probably rewrite that in more object oriented fashion instead of doing it half-way. (now that I looked into SML more closely)

[orcmid]

FYI, I've produced quick-n-dirty Python version (I have not checked it yet though)

I have remarked on this at Question #6, and we can do more if you enable issues on your fork.

Thank you for expanding the mockups of oMiser. This is great as demonstration and for confirmation of understanding how oMiser and oFrugal are being approached.

[rnd0101]

I guess that my understanding is still lacking, but I am determined to have it working so I can evaluate how oMiser can be useful to the Eternal Programming. Even if evaluation will be negative, both projects will hopefully benefit. At least, I get hands-on experience, which will help me form design goals for the Eternal Programming language.

What I am sure of, is that it should be applicative (like LISP, ML), good to be concatenative (like Forth and a bit stretching definition of PL - RDF), definitely based on a "miserly" small foundation, be utterly extendable using only that fixed core. Developer ergonomics is also one of the goals. For example, EP language should be easily embeddable into Jupyter, so it can be part of learning management systems, running on the Web, etc, etc.

If I can get at least from 'miser' assembler to C language - there is enormous amount of software, which can be preserved "for eternity". (I do not know if my goal is achievable, but all crazy ideas had this property)

[orcmid]

What I am sure of, is that it should be applicative (like LISP, ML), good to be concatenative (like Forth and a bit stretching definition of PL - RDF), definitely based on a "miserly" small foundation, be utterly extendable using only that fixed core.

• oMiser is certainly applicative at its level.
• I've forgotten what about Forth that makes it concatenative. I think for the applicative nature of oMiser, functional composition must be the equivalent. I hesitate to call it catenative. Also, because application associates to the right in oMiser, concatenating ‵(g) to‵(f) :: '(x) to form exp = ‵(g) :: ‵(f) :: ‵(x) has eval(exp) provide essentially g( f( x ) ).
• I'm uncertain over use of RDF or OWL. I think that makes me neutral on the matter. I'm content with the ‹ob› structure, for now. Revisiting the use of RDF might be a consideration for the future.

Speaking of other representations,, I do have in mind an XML schema for the export of obs in digital signature/hash-taggedverified (and optionally compressed) XML documents that make for (1) fast loading (working bottom-up like reverse-Polish for obs) and (2) provide a way to load only once those subtrees that are re-used in differentmultiple parts of the ob. I think the oFrugal REPL is needed first, though.

update 2018-01-09: improve the sketch of the intended XML dump/reload form.

[orcmid]

There has been more refinement of REPL input for oFrugal in a comment at Question #7.

It is time to dig out something like an oFrugal grammar, as requested in Question #8.

[orcmid]

@orcmid The basic idea for a REPL is to have a written (i.e., text) form for reading obs as expressions, exp. So the R-Read part is to accept the text and, if well-formed, obtain the ob that is described as exp. The E-Eval part is to then to perform obap.eval(exp). The P-Print part is to then present that result in the same text form used for input. This particular Read-Eval-Print-Loop notion stems back to the original implementation of LISP.

I must recant this observation. It is the case that the REPL will Read, Eval, and Print, but it is not by Read delivering an Ob, exp, that is evaluated by obap.eval(exp) to produce the ob that is then reported (Print) in text form. That's a very clumsy way of handling the ob-exp form that is read for evaluation to an ob result.

There is an Eval stage, but it doesn't work that way. A REPL need not treat Read and Eval as separate stages. As @rnd0101 has pointed out, it is valuable that the input be checked as well-formed before Eval occurs, but the semantics don't require it and mock-up REPLs will likely Eval in the course of Read, because it is simpler to get right.

There is now a complete grammar for REPL-input ob-exp text and the rules for evaluation of those expressions to arrive at a computer ob are rigorous and straightforward. The summary version is supplied at Question #8 and Question #14.

I believe this question can now be closed, since there is a precise definition for the expressions that the oFrugal REPL will evaluate to yield obs.