A more idiomatic approach to code lowering. λ symbolizes a process for defining the ways to do something. ☶ symbolizes a process for selecting the natural way to do something.
λ☶ is a programming language written in the passive voice.
eval-soft and eval-hard are the exposed entry points into your program.
A λ☶ program is then defined as capabilities gifted to anyone with access to your entry points.
Each program defines a policy and implementation of capabilities.
Any attempt to subvert these policies should result in an error instead of actual evaluation.
Syntactically, capabilities are exposed to the user as globally bound variables.
User-land programs can then be thought of as simple lambda-calculus expressions.
Below is an example of a user-land program containing one policy bound to the variable print.
User programs can be any unicode text. Anything. Really. "Free Grammar!"
λ-calculus
print "hello world"
The "string" syntax from the above program needs to be rewritten into a lambda-calculus expression. Grammatical Rewriting is accomplished in the policy definition as follows.
λ☶
::pre := λ["] (literal s) ["]. s
::pre := λc (::pre cs). c cs
literal := λc (literal cs). c cs
Each bound variable gets its own line in the policy definition.
λ☶
print := λmsg. org 0x100 \n (splat msg) mov ah, 0x4c \n int 0x21 \n
splat := λc cs. mov dl, c \n mov ah, 2 \n int 0x21 \n (splat cs)
The x86 assembler output here needs to be compiled and run. This is accomplished in the policy definition as follows.
λ☶
::post := λeval-result. ... side effects go here ...
soft reductions are not guaranteed to reach normal form.
though, up until they halt they will always be equivalent.
soft reductions will not diverge and are strongly normalizing.
note: "strongly normalizing" does not mean the term is "normalized".
hard reductions are evaluations until normal form and may diverge.
TBD.
A definition of a minimal language kernel will also be developed in L1. L1 itself is not stable yet, so development of this project is delayed pending.