$NAME language specification

$NAME is a dynamic reflective language. It aims to run on as many platforms as possible.

To us acceptable performance is when using $NAME does not have to incur overhead compared to not using $NAME. For example it is acceptable to have to write assembly or javascript in $NAME to get "native" performance. By platform we mean the combination of some software and hardware, such as Javascript in a browser or a process running on an operating system and x86_64 hardware. We do this by late binding and partial evaluation.

Initial environment

The prelude definitions.

($define! $quote ($vau (x) () x))
($define! $quote* ($vau x () x))
($define! id (wrap $quote))
($define! list (wrap $quote*))
($define! $lambda ($vau (p b) e (wrap (eval (list $vau p nil b) e))))
($define! $true ($vau (x y) e (eval x e)))
($define! $false ($vau (x y) e (eval y e)))
($define! $or ($vau (x y) e ((eval x e) $true ((eval y e) $true $false))))
($define! or ($lambda (x y) (x $true (y $true $false))))
($define! $and ($vau (x y) e ((eval x e) ((eval y e) $true $false) $false)))
($define! and ($lambda (x y) (x (y $true $false) $false)))
($define! $if ($vau (c t f) e ((eval c e) (eval t e) (eval f e))))
($define! $let/1 ($vau (s a b) e (eval b (bind s (eval a e) e))))
($define! apply
  (wrap ($vau (applicative arguments) env
    (eval (cons (unwrap applicative) arguments) env))))
($define! Ycombinator
  ($lambda (f)
           (($lambda (x) (x x))
            ($lambda (g)
                     (f ($lambda a (apply (g g) a)))))))
($define! $fold-right
  (Ycombinator
    ($lambda (r)
    ($lambda (binary-combiner initial elements)
      ($if (empty? elements)
        initial
        (binary-combiner
          (first elements)
          (r binary-combiner initial (rest elements))))))))

The ground environment containing the primitive combiners and constants.

first
rest
cons
nil
bind
$true
$false
cons?
same?
environment?
error?
operative?
applicative?
wrap
unwrap
lift
run

Specification of language combiners

How to read the reduction rules

The following rules describe the reduction rules for the language kernel. Briefly explained the rules should be read as follows:

[ ] represents reduction to be performed.
... is used for values where the inner content of the value is not important to the reduction rule. Typically when matching only on the kind of value.
\name is the value of a operative combiner. This is in contrast with the symbol which is usually bound to the value. For example the symbol $first is typically bound to operative combiner \first. Note that the literal syntax for operative combiners is only used in the reduction rules, it is not a valid in $NAME expressions.
x@{KIND ...} is used to match a value by kind on the left hand side and bind it to a variable for use in the right hand side. This may only be used on the left hand side with values.
{ } represents a value. If it is on the left hand side of ~ it is a pattern match. If it is on the right is a construction.
[OPERATION ...] ~ {RESULT ...} is a form of reduction rule where [OPERATION ...] reduces to the value {RESULT ...}

Kinds of values

{sym _} a symbol.
{cons _} a cons pair.
{nil _} an end of list marker value.
{env _} an environment value.
{clo _} an operative closure.
{wrp _} a wrapped combiner.
{err _} an error value.
{code _ _} a later stage expression.
\_ a primitive operative combiner.

Change \_ syntax to use the {FOO ...} syntax, for consistency with the rest.

Add the {tag _ _} value kind and the relevant combiners.

Reduction rule for closure combination

RCC01: [combine {clo p s b e0} o e1] ~ [eval b [bind s env1 [bind p o env0]]]

Reduction rule for `\bind`

BND001: [combine \bind {cons S@{sym _} {cons V {cons E {nil}}}} _] ~ TODO
BND002: [combine \bind _  _] ~ {err}

Reduction rule for `\eval`

REV01: [combine \eval {cons a {cons b {nil}}} e] ~ [eval a b]
REV02: [combine \eval _ _]                         ~ {error}

Describe how to differentiate between errors during evaluation of a and errors in the combination of \eval.

Explicit check that b is an environment! The [eval ...] rules do not currently handle the case of non-environments in the second component.

Reduction rules for applicative (wrapped) combiners

Old approach to wrapped reduction and code (before introducing `\run`)

We introduce code. What is the effect on combine? Is there an affect on operatives? No, because operatives do not evaluate their operands. When combining applicatives we may need to do things. Because we are evaluating arguments. When the operator evaluates to a code value we cannot do anything with the operands, because we do not know if the operator will be an operative or applicative, so we just preserve the operands in the returned code value. When the operator evaluates to an combiner we can proceed with further work. If it is an operative we can perform the combination as in Kernel. If it is an applicative we will proceed with evaluating the operand expressions to argument values. If the argument values are code values we shall once again emit a code value. If we wish to preserve evaluation ordering whe have to do let insertion here (by placing them in the returned code, as a separate part from the expression). If we do not care, we do not have to?

We add the reduction rule combine-app to perform let insertion if the operands evaluate to arguments that are code values. The combine-app is only used with operative that where wrapped. So combine-app is always given arguments, not operands. The combine-app does not perform the actual combination of the combiner and arguments. It delegates that back to combine once combine-app has performed let insertion if it was necessary.

If the argument tree given to combine-app contains a code element we are in the process of generating code for a future stage. So we should not actually run the computation now, in this stage. Rather we should return a code value, which may need to include suspended let-insertions. A suspended let-insertion is a binding to be done before evaluating the expression wrapped in the code value. This is done to preserve the order of side effects.

If the argument tree has mixed code and other values things get interesting. In Lambda-Up-Down the only cases allowed are either current stage values or future stage code, the arguments must all belong to one group. No mixing. What does it mean to mix?

Actually delecate combination to combine. Right now combination is partially and incorrectly duplicate it into combine-app to make it easier to experiment.

Attempt two, flat `combine` list for applicatives and applicatives.

RW01: [combine {wrap comb} operands env] ~ [combine-app comb [eval-list operands env] env]

The combine reduction rule contains the Kernel-based entries for every operative combiner. It also contains the unwrapping case from Kernel. Finally it adds cases for code values. Unlike previous attempts that handled code values in the unwrap and operand evaluation step this attempt does it in the individual rules for combiners. The reason is that not all combiners actually handle code values in the same way. Cruically the \run combiner accepts either two code values or one non-code value and one code-value. Previous attempts always expected the operands of wrapped combiners to either all be non-code values or all be code values and let insertion was done in one place, during unwrapping and operand evaluation. The current approach will lead to a lot of duplication of let-insertions. Perhaps it will be possible to eliminate the duplication later and finish with a simpler rule system.

????: [combine \first {cons {code Expr0 Lets0} {nil}} Env]
    ~ {code [list {wrap \first} Var0]
            [let-ins Var0 Expr0 Lets0]}
????: [combine \first {cons {cons A _} {nil} Env} Env] ~ A

Reduction rule for `\run`

The \run combiner either takes a code value and runs it now or it suspends itself and returns a new code value, to be executed at a later stage. Which behaviour is is controlled by the first argument.

The \run combiner is tricky, because it is going to be wrapped yet needs to receive mixed code and non-code values. The initial approach was to handle all code values passed to wrapped combiners in a dedicated rule named combine-app. However \run does not appear to fit into that design, since it will receive both code and non-code values.

Specify rule for other values in the first operand to \run. Everything but the code value kind should cause evaluation of the second argument in this stage.

How do we do let insertion? Lifting and reflection inserts lets-of-expressions that will be applied later during \run. Do we also need the environment from where we did the lifting?

[combine \run {cons {symbol _} {cons {code Expr Lets} {nil}}} Env] ~

[combine \run {cons {code _ _} {cons {code Expr Lets} {nil} }} Env] ~ TODO

Reduction rule for `\lift`

[combine \lift {cons Sym@{sym _} {nil}} Env] ~ {code Sym {nil}}
[combine \lift {cons {cons {code E1 L1} {code E2 L2}} {nil}} Env] ~

Reduction rule for list evaluation

????: [eval-list {cons a l} env] ~ {cons [eval a env] [eval-list l env]}
????: [eval-list {nil} env] ~ {nil}

Reduction rule for variable lookup

RV01: [eval s0@{sym _} {env s1 v0 e}] ~ if s0 == s1 then v0 else [eval s0 e]
RV02: [eval s0@{sym _} {env}]         ~ {error}

Reduction rule for combination expressions

RC01: [eval {cons opr ops} env] ~ [combine [eval opr env] ops env]

Reduction rules of `\first`

RF001 [combine \first {cons {cons x _} {nil}} env] ~ x
RF002 [combine \first {cons {code A B} {nil}} env] ~
  {code 
RF003 [combine \first _ env]                           ~ {error}

Reduction rules of `\rest`

RR001 [combine \rest {cons {cons _ x} {nil}} env]     ~ x
RR002 [combine \rest {cons {code A B} {nil}} env]     ~ TODO
RR003 [combine \rest _ env]                           ~ {error}

Reduction rules for `\wrap`

RWR01 [combine \wrap {cons c@{clo ...} {nil}} env]     ~ {wrap c}
RWR03 [combine \wrap _ env]                            ~ {error}

Reduction rules for `\unwrap`

RUR01 [combine \unwrap {cons {wrap c} {nil}} env]     ~ c
RUR03 [combine \unwrap _ env]                         ~ {error}

Add rules for primitive operative combiners, \vau and friends. Because {clo ...} is currently only for compound combiners, or closures.

Reduction rules for `\symbol?`

RP001: [combine \symbol? {cons {sym _} {nil}} env]        ~ \true
RP002: [combine \symbol? {cons {cons _} {nil}} env]       ~ \false
RP003: [combine \symbol? {cons {nil} {nil}} env]          ~ \false
RP004: [combine \symbol? {cons {env _} {nil}} env]        ~ \false
RP005: [combine \symbol? {cons {clo _} {nil}} env]        ~ \false
RP006: [combine \symbol? {cons {wrp _} {nil}} env]        ~ \false
RP008: [combine \symbol? {cons {err _} {nil}} env]        ~ \false
RP008: [combine \symbol? {cons {code _ _} {nil}} env]       ~ \false
RP007: [combine \symbol? {cons \_ {nil}} env]             ~ \false
RP009: [combine \symbol? _ env]                           ~ {error}

Reduction rules for `\cons?`

RP011: [combine \cons? {cons {sym _} {nil}} env]        ~ \false
RP012: [combine \cons? {cons {cons _} {nil}} env]       ~ \true
RP013: [combine \cons? {cons {nil} {nil}} env]          ~ \false
RP014: [combine \cons? {cons {env _} {nil}} env]        ~ \false
RP015: [combine \cons? {cons {clo _} {nil}} env]        ~ \false
RP016: [combine \cons? {cons {wrp _} {nil}} env]        ~ \false
RP017: [combine \cons? {cons {err _} {nil}} env]        ~ \false
RP017: [combine \cons? {cons {code _ _} {nil}} env]       ~ \false
RP017: [combine \cons? {cons \_ {nil}} env]             ~ \false
RP018: [combine \cons? _ env]                           ~ {error}

Reduction rules for `\null?`

RP021: [combine \null? {cons {sym _} {nil}} env]        ~ \false
RP022: [combine \null? {cons {cons _} {nil}} env]       ~ \false
RP023: [combine \null? {cons {nil} {nil}} env]          ~ \true
RP024: [combine \null? {cons {env _} {nil}} env]        ~ \false
RP025: [combine \null? {cons {clo _} {nil}} env]        ~ \false
RP026: [combine \null? {cons {wrp _} {nil}} env]        ~ \false
RP027: [combine \null? {cons {err _} {nil}} env]        ~ \false
RP027: [combine \null? {cons {code _ _} {nil}} env]       ~ \false
RP027: [combine \null? {cons \_ {nil}} env]             ~ \false
RP028: [combine \null? _ env]                           ~ {error}

Reduction rules for `\env?`

RP031: [combine \env? {cons {sym _} {nil}} env]        ~ \false
RP032: [combine \env? {cons {cons _} {nil}} env]       ~ \false
RP033: [combine \env? {cons {nil} {nil}} env]          ~ \false
RP034: [combine \env? {cons {env _} {nil}} env]        ~ \true
RP035: [combine \env? {cons {clo _} {nil}} env]        ~ \false
RP036: [combine \env? {cons {wrp _} {nil}} env]        ~ \false
RP037: [combine \env? {cons {err _} {nil}} env]        ~ \false
RP037: [combine \env? {cons {code _ _} {nil}} env]       ~ \false
RP037: [combine \env? {cons \_ {nil}} env]             ~ \false
RP038: [combine \env? _ env]                           ~ {error}

Reduction rules for `\op?`

RP041: [combine \op? {cons {sym _} {nil}} env]        ~ \false
RP042: [combine \op? {cons {cons _} {nil}} env]       ~ \false
RP043: [combine \op? {cons {nil} {nil}} env]          ~ \false
RP044: [combine \op? {cons {env _} {nil}} env]        ~ \false
RP045: [combine \op? {cons {clo _} {nil}} env]        ~ \true
RP046: [combine \op? {cons {wrp _} {nil}} env]        ~ \false
RP047: [combine \op? {cons {err _} {nil}} env]        ~ \false
RP047: [combine \op? {cons {code _ _} {nil}} env]       ~ \false
RP047: [combine \op? {cons \_ {nil}} env]             ~ \true
RP048: [combine \op? _ env]                           ~ {error}

Reduction rules for `\ap?`

RP051: [combine \ap? {cons {sym _} {nil}} env]        ~ \false
RP052: [combine \ap? {cons {cons _} {nil}} env]       ~ \false
RP053: [combine \ap? {cons {nil} {nil}} env]          ~ \false
RP054: [combine \ap? {cons {env _} {nil}} env]        ~ \false
RP055: [combine \ap? {cons {clo _} {nil}} env]        ~ \false
RP056: [combine \ap? {cons {wrp _} {nil}} env]        ~ \true
RP057: [combine \ap? {cons {err _} {nil}} env]        ~ \false
RP057: [combine \ap? {cons {code _} {nil}} env]       ~ \false
RP057: [combine \ap? {cons \_ {nil}} env]             ~ \false
RP058: [combine \ap? _ env]                           ~ {error}

Reduction rules for `\err?`

RP061: [combine \err? {cons {sym _} {nil}} env]        ~ \false
RP062: [combine \err? {cons {cons _} {nil}} env]       ~ \false
RP063: [combine \err? {cons {nil} {nil}} env]          ~ \false
RP064: [combine \err? {cons {env _} {nil}} env]        ~ \false
RP065: [combine \err? {cons {clo _} {nil}} env]        ~ \false
RP066: [combine \err? {cons {wrp _} {nil}} env]        ~ \false
RP067: [combine \err? {cons {err _} {nil}} env]        ~ \true
RP068: [combine \err? _ env]                           ~ {error}

TODO: Add \eq?

Example reductions

Example reduction of `(first (lift nil))` reducing to an error value

   [eval (first (lift nil)) StdEnv]

Reduction of `symbol?` in empty environment

We start with the expression symbol?, which is just a symbol, in the reduction symbol we write literal symbols as {sym symbol?}. So our starting state is [eval {sym symbol?} {env}]

       [eval {sym symbol?} {env}]
RV02 ~ {error}

Reduction of `(symbol? $vau)` in standard environment

        [eval (symbol? $vau) stdenv]
      = [eval {cons {symbol symbol?} {cons {symbol $vau} {nil}}} stdenv]
RC01  ~ [combine [\eval symbol? stdenv] {cons {symbol $vau} {nil}} stdenv]
RV01  ~ [combine {wrp \symbol?} {cons {symbol $vau} {nil}} stdenv]
RW01  ~ [combine \symbol? [eval-list {cons {symbol $vau} {nil}} stdenv] stdenv]
     ...  ; TODO eval-list 
RP007 ~ [combine \symbol? {cons \vau {nil}} stdenv]

Specification of language syntax

EXPRESSION ::= LIST | SYMBOL | NUMBER | TEXT
LIST ::= '(' OWSPACE ')' | '(' OWSPACE ELEMENTS OWSPACE ')'
ELEMENTS ::= EXPRESSION WSPACE ELEMENTS | EXPRESSION
SYMBOL ::= SCHAR SCHARS
NUMBER ::= DIGIT SCHARS
TEXT ::= '"' CHARS '"' | '#' SCHARS '"' CHARS '"' SCHARS

SCHAR ::= LOWERCASE | UPPERCASE | SPUNCTUATION

CHARS ::= CHAR | CHAR CHARS

CHAR ::= UPPERCASE LOWERCASE SPUNCTUATION

SPUNCTUATION ::= '!' | '"' | '$' | '%' | '&' | "'" | '*' | ',' | '-' | '.'
              | '/' | ':' | ';' | '<' | '=' | '>' | '?' | '@' | '[' | '\' | ']' | '^'
              | '_' | '{' | '|' | '}' | '~'

UPPERCASE ::= 'A' | 'B' | 'C' | 'D' | 'E' | 'F' | 'G' | 'H' | 'I' | 'J' | 'K' | 'L'
            | 'M' | 'N' | 'O' | 'P' | 'Q' | 'R' | 'S' | 'T' | 'U' | 'V' | 'W' | 'X'
            | 'Y' | 'Z'
LOWERCASE ::= 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'g' | 'h' | 'i' | 'j' | 'k' | 'l'
            | 'm' | 'n' | 'o' | 'p' | 'q' | 'r' | 's' | 't' | 'u' | 'v' | 'w' | 'x'
            | 'y' | 'z'

The TEXT grammar is required to accurately represent data that does not conform to the syntax of $NAME. Such as data that contains unbalanced parenthesises, uses separators other than parenthesis and whitespace, etc.

In the future full Unicode will be supported. The changes to the grammar is expected to be minimal. Unicode specifies additional whitespace and those will be added as separators. Other Unicode graphme clusters will be added to the SYMBOL and TEXT rules.

Scratch

Example Pink session using the Scheme implementation and augmented with a simple repl.

   (lift 42)
(code 42)

   (quote a)
a

   (lift (quote a))
(code a)

   (lift (quote 42))
(code 42)

   (lift (quote (a)))
*exception*

   (lift (lambda f x x))
(code (var 0))
stBlock: ((lambda (var 1)))
stFresh: 1
stFun: ((0 () (var 1)))

   (lift ((lambda f x x) 42))
(code 42)
stBlock: ()
stFresh: 0
stFun: ()

   (run 0 (lift 42))
42
stblock: ()
stFresh: 0
stFun: ()

   (run (lift 1) (lift 42))
(code (var 0))
stBlock: ((run 1 42))
stFresh: 1
stFun: ()

   (lift (lift 1))
(code (var 0))
stBlock: ((lift 1))
stFresh: 1
stFun: ()

   (lift (cons (lift 1) (lift 2)))
(code (var 0))
stBlock: ((cons 1 2))
stFresh: 1
stFun: ()

   (lift (lambda f x (car x)))
(code (var 0))
stBlock: ((lambda (let (car (var 1)) (var 2))))
stFresh: 1
stFun: ((0 () (car (var 1))))

   (lift (lambda f x (car f)))
(code (var 0))
stBlock: ((lambda (let (car (var 0)) (var 2))))
stFresh: 1
stFun: ((0 () (car (var 0))))

$NAME language specification

Initial environment

Specification of language combiners

How to read the reduction rules

Kinds of values

Reduction rule for closure combination

Reduction rule for \bind

Reduction rule for \eval

Reduction rules for applicative (wrapped) combiners

Old approach to wrapped reduction and code (before introducing \run)

Attempt two, flat combine list for applicatives and applicatives.

Reduction rule for \run

Reduction rule for \lift

Reduction rule for list evaluation

Reduction rule for variable lookup

Reduction rule for combination expressions

Reduction rules of \first

Reduction rules of \rest

Reduction rules for \wrap

Reduction rules for \unwrap

Reduction rules for \symbol?

Reduction rules for \cons?

Reduction rules for \null?

Reduction rules for \env?

Reduction rules for \op?

Reduction rules for \ap?

Reduction rules for \err?