Lincoln is developed to be a new programming environment, including a simple IR, an simple interpreter, and later some layers of hight level languages.
The IR is also designed for a form that is suitable as a target of many other programming languages, although those languages generally have quite different sementics.
In computing, Lincoln lies in between two other simple models: the Turing machine and the lambda calculus. The Turing machine have simple operational sementic, but lacks of denotational semantics, which means you need to formally describe what a "state" and a piece of symbols in the tap means, the definition of the machine cannot tell you anything about it. The lambda calculus on the other hand, has full of denotational semantics, but hard to define operational sementic - a single substitution can be arbitary complicated, and the order of reduction is unspeified.
Lincoln has simple operational sementic: the state transition is deterministic, and is always O(1). However it is also have native denotation semantics. In Lincoln, values are not simple symbols like in the Turing machine. They are black boxes that can carry meaning and internal states.
Jmp,Ret,Call), minimal build-in types (closure types).In additional, unlike other programming platforms, Lincoln does not look for a big "std" library. Instead, every Lincoln program is supposed to be isolated, abstracted building blocks that rely on the outside world to supply basic operations. It only garantee that, as long as the external provided did their part, a Lincoln program will do what it supposed to do.
A context is a set of values. The basic operation over a context includes: split a context into two, or merge two context into one, or take a value out from a context, or use a permutation to reorder the values. Both should be O(1) operation.
How to represent a context is up to the intepretor. In this demostrate intepretor we represent it as a vector, but it can be the set of registries of a CPU, or a piece of memory, or cookies from a website, or anything.
The values in a context can be categoried into two:
Closures. This is the only "build-in" type of Lincoln. They can be created and executed (used) within Lincoln. It is suprisingly rich and is able to represent types that are familier to other languages, includeing
External types. Lincoln does not understand those types and so any attempt to drop or execute them will result in error. They can only be produced and consumed by external code.
When a continuation is going to be executed, we use permutations to reorder the values. We use the Fisher and Yate's algorithm (but instead of generate the number randomly, specify the number) to map a permutation into a set of numbers, then map these numbers into a single number.
Implementations of intepretor will need to support at least 6 variables, as this is what a 8-bit integer can represent for a permutation.
A program contains a set of code entries, or instructions. There are 3 different kind of code entries:
Every code entries are refered by a name.
When talking about "another entry or an external function" in code entries, I am talking about code references. A code reference is pointing to one of the following:
Run the following in a console:
sh
git clone https://github.com/earthengine/lincoln
cargo run
The program will show a prompt
sh
Lincoln>
Now you can run some commands like
text
entry: call entry1 1 from
entry1: jmp count #!ba
set export entry
You can use save command to save your work to a json file:
text
save myprogram.json
Or load it back
text
load myprogram.json
You can then compile the prog by
text
compile bint
where "bint" is a set of external functions for converting from and to a number data type defined in pure Lincoln.
There are also another set of external functions provided, which is "fact" that use the executer's native data type.
To run the program, use
run entry 0 10
and get something like:
text
Result(1/1): 10
Two example programs are given
This is a demostration of how to define copiable native data type. To run, use the following commands:
text
load bint.json
compile bint
run test_copy 0 "10usize"
Right now only "usize" type are supported, it is usually a 64 bit unsigned integer according to your system.
By running this you are expected to get
text
Result(1/2): 10
Result(2/2): 10
This is a demostration of how to define algorithm completely rely on the outside world to provide the functions we need.
To run, use the following commands:
text
load fact.json
compile fact
run fact 0 "10usize"
You are expected to get
text
Result(1/1): 3628800
The minimalism design of Lincoln means that the current IR will be likely be freezed like it is right now. Some thoughts
If we represent the fact example above in a high level language that is Haskell-like, it would looks like
```haskell extern zero extern one extern copyint extern eq extern dropint extern minus extern mul
fact c n := -- a definition of fact, takes variable c and n
f = -- an assignment, which is always lazy
call c n := fact c n -- a definition of a variant "call"
drop c := c -- another variant "drop"
zero -> z -- an invocation, result are in z
one -> o -- zero and one are external
copyint n -> n1 n2 -- copy_int is external
eq n1 z -- Without the arrow, the group of variants simple values only
equals :=
dropint n2 -> -- drop_int is external
f.drop -> -- call the drop variant of f
c o -- the final statement
notequal :=
copyint n2 -> n1 n2
minus n1 o -> n -- minus is external
c = _ n := -- Assign a closure to c
mul n n2 -> n -- mul is external
c n
f.call c n -- call the call variant of f (recursion)
```
The above example demostrates the basic idea:
The language in the above is not statically typed, but we should be able to have a type system for it.
If talking about the future statically typed language, yes they will be considered. Otherwise, it is not hard to image a dynamically typed language like the above that checking it at runtime.
Needless to say again Lincoln is something in between Turing machine and Lambda calculus.
There is also another similar idea like B Geron's continuation calculus. My system is different because it is linear: B Geron's system allows to copy and drop terms freely, but my system do not.
If you are interested in this project, please feel free to contact me through
Or just raise an issue if you don't care it to be public.