git @ Cat's Eye Technologies Argyle / master doc / Definition-of-Argyle.md
master

Tree @master (Download .tar.gz)

Definition-of-Argyle.md @masterview markup · raw · history · blame

Definition of Argyle

This document aims to serve as the definion of the Argyle programming language.

-> Functionality "Parse Argyle program" is implemented by
-> shell command "bin/argyle parse %(test-body-file)"

-> Functionality "Evaluate Argyle program" is implemented by
-> shell command "bin/argyle eval %(test-body-file)"

These tests are written in Falderal format. Each indented code block (generally preceded by a description) represents a test. All the lines of the code block up until the ===> line give the input to be tested; the text after ===> gives the expected output. ???> gives an expected error message, which is permitted to be a partial (substring) match.

Parsing

-> Tests for functionality "Parse Argyle program"

A well-formed S-expression does not have anything except whitespace following it.

(add) mul
???> Unexpected characters

A well-formed S-expression must have an opening parenthesis.

add)
???> Incomplete expression

A well-formed S-expression must have an closing parenthesis.

(add
???> Incomplete expression

A well-formed S-expression does parse to an AST and thence to an ABT.

(add mul)
===> (add mul)
===> Apply [Atom "add",Atom "mul"]
===> (quote (add mul))
===> Operator "apply" [Var "add",Var "mul"]

An S-expression may include comments, which begin at ; and extend until the end of the line.

(add ;what does this say!!)
mul)
===> (add mul)
===> Apply [Atom "add",Atom "mul"]
===> (quote (add mul))
===> Operator "apply" [Var "add",Var "mul"]

Identifiers used in S-expressions do have to be bound, unless they're in a special form which is a binder.

(hi there)
???> Unbound variable

The let special form does have a syntax that you do need to follow.

(let me go)
???> Invalid

This is what a valid let looks like and parses to.

(let ((x 4) (y 9)) (add x y))
===> (let ((x 4) (y 9)) (add x y))
===> Let "x" (Number 4) (Let "y" (Number 9) (Apply [Atom "add",Atom "x",Atom "y"]))
===> (quote (let ((x 4) (y 9)) (add x y)))
===> Operator "let" [Binder "x" (Operator "let" [Binder "y" (Operator "apply" [Var "add",Var "x",Var "y"]),Operator "values" [Literal 9]]),Operator "values" [Literal 4]]

If a variable is not bound at the point it appears in a var node in an abt value construct, that's a syntax error.

(let ((x 1)) (quote y))
???> Unbound variable

Simple Operation

-> Tests for functionality "Evaluate Argyle program"

Numeric literals and basic arithmetic

Simple number literals work:

42
===> 42

Negative numbers can be created with neg:

(neg 5)
===> -5

Multiple arithmetic operations can be composed:

(add (mul 2 3) (neg 4))
===> 2

String Literals

Basic string literals work:

"hello"
===> "hello"

Strings can be quoted:

(quote "hello")
===> (quote "hello")

Strings can be bound to names:

(let ((s "hello")) s)
===> "hello"

if-apply Function

(if-apply 1 (lambda (x) 123) (lambda (x) "no"))
===> 123

(if-apply 0 (lambda (x) 123) (lambda (x) "no"))
===> "no"

equal? Function

(equal? 123 123)
===> 1

(equal? 123 456)
===> 0

(equal? "word" "word")
===> 1

(equal? "word" "world")
===> 0

Lambda expressions and function application

Simple lambda with immediate application:

((lambda (x) (add x 1)) 41)
===> 42

Lambda that uses a free variable:

(let ((y 1))
  ((lambda (x) (add x y)) 5))
===> 6

Higher-order functions - passing a function as argument:

(let ((f (lambda (x) (add x 1))))
  (let ((g (lambda (h n) (h (h n)))))
    (g f 5)))
===> 7

Multiple parameters in lambda (testing currying):

((lambda (x y) (add x y)) 2 3)
===> 5

Name binding with let

let binds names to values.

(let ((x 4)) (add x 1))
===> 5

let can be nested inside another let.

(let ((x 4))
  (let ((y 2))
    (add x y)))
===> 6

let can have more than one binding in its list of bindings.

(let ((x 4) (y 9)) (add x y))
===> 13

A binding established in a let shadows previous bindings of that name.

(let ((x 9))
  (let ((x 2))
    (add x x)))
===> 4

Scoping rules

Let bindings are evaluated in order:

(let ((x 1)
      (y (add x 1)))
  y)
===> 2

Closure captures environment properly:

(let ((x 1))
  (let ((f (lambda (y) (add x y))))
    (let ((x 10))
      (f 1))))
===> 2

Multiple nested functions maintain proper scope:

(let ((x 1))
  (let ((f (lambda (y)
             (let ((g (lambda (z) (add x (add y z)))))
               (g 3)))))
    (f 2)))
===> 6

Let binding shadows lambda parameter:

((lambda (x)
   (let ((x 5))
     x))
 1)
===> 5

Homoiconic Operation

quote

quote is a special form that evaluates to an ABT value derived from its argument, similar to quote in Scheme. However, it differs in two key ways:

  1. It honors lexical scope - variables must be bound either in the current scope or within a lambda binding in the quoted expression
  2. The result is always an ABT value that can be manipulated by transformers

Here are examples of valid and invalid quoted expressions:

If a variable is not bound at the point it appears in a quoted expression, that's a syntax error:

(let ((x 1)) (quote y))
???> Unbound variable

However, variables bound in the current scope can be referenced. Note that we bring the machinery that causes it to be bound, into the ABT itself.

(let ((x 1)) (quote x))
===> (quote (let ((x 1)) x))

Basic Operations in Quoted Expressions

Numbers in quoted expressions become literal ABT nodes:

(quote 5)
===> (quote 5)

Quoted expressions can be evaluated:

(eval (quote 5))
===> 5

Quoted values can be bound to names:

(let ((x (quote 1))
      (y (quote 2)))
  (eval x))
===> 1

Function application is represented naturally.

(quote (add 1 2))
===> (quote (let ((add <builtin:add>)) (add 1 2)))

And can be evaluated:

(eval (quote (add 2 3)))
===> 5

Variables and Binding

Lambda expressions in quotes create binders:

(quote (lambda (x) x))
===> (quote (lambda (x) x))

Let expressions work similarly:

(quote (let ((x 1)) x))
===> (quote (let ((x 1)) x))

Functions bound in the outer scope can be referenced in quoted expressions:

(let ((foo (let ((double (lambda (x) (mul x 2))))
             (quote (double 5)))
      ))
  (eval foo))
===> 10

This applies to functions that have closed over values in outer scopes too:

(let (
  (factor 2)
  (foo (let ((double (lambda (x) (mul x factor))))
    (quote (double 5))))
  )
  (eval foo))
===> 10

All outer scopes, that is.

(let (
  (factor 2)
  (foo (let ((double (let ((biggify (lambda (x) (mul x 2)))) (lambda (x) (biggify x)))))
    (quote (double 5))))
  )
  (eval foo))
===> 10

And just some big ol' monster binder things to test this with.

(let (
  (base 2)
  (foo (let ((make-adder (lambda (x)
                         (lambda (y)
                           (let ((inner (lambda (z) (add (add x y) (mul base z)))))
                             (quote (inner 3)))))))
         (quote ((make-adder 5) 7))))
  )
  (eval (eval foo)))
===> 18

(let ((base 10))
  (let ((make-counter
          (lambda (start)
            (let ((count start)
                  (increment (lambda (n)
                             (let ((next (add count n)))
                               (lambda ()
                                 (quote (mul next base))))))
                  (decrement (lambda (n)
                             (let ((prev (add count (neg n))))
                               (lambda ()
                                 (quote (mul prev base)))))))
              (quote ((increment 5)))))))
    (eval (eval (make-counter 7)))))
===> 120

Complex Expressions

Nested expressions maintain proper structure.

(quote (let ((double (lambda (x) (mul x 2))))
        (double 5)))
===> (quote (let ((mul <builtin:mul>) (double (lambda (x) (mul x 2)))) (double 5)))

Evaluation of complex quoted expressions works as expected:

(eval (quote (let ((x 3))
              (let ((y 4))
                (add x y)))))
===> 7

Quote can be nested:

(quote (quote 5))
===> (quote (quote 5))

Variables from different scopes interact properly:

(let ((x 1))
  (eval (quote (let ((y 2))
                (add x y)))))
===> 3

abt

The abt function behaves like quote with the exception that it evaluates its argument.

abt is to quote in Argyle as list is to quote in Scheme. (Sorta.)

(abt (add 1 2))
===> (quote 3)

Since the argument expression is evaluated, unlike quote, the resulting ABT value will not contain any variable bindings.

(let ((x 1)) (abt (add x 2)))
===> (quote 3)

Since the argument expression is evaluated, it may not contain any free variables.

(abt (add x 2))
???> Unbound variable

stencil

Quoted literal ABTs are allowed to have free variables. The stencil form take a list of variables that are to be considered free in the ABT expression. We call these variables "declared free" to distinguish them from when we use the term "free variables" to describe variables that we have discovered to have no bindings (a perhaps more traditional usage of "free").

quote is actually a special case of stencil where the set of variables declared free is empty.

(stencil (x) x)
===> (stencil (x) x)

ABTs with variables declared free can't be eval'ed.

(eval (stencil (x) x))
???> Cannot eval

The variables that we declare to have been declared free, don't actually have to appear in the expression.

(stencil (x) 1)
===> (stencil (x) 1)

But an ABT with variables declared free still can't be eval'ed, even if those variables don't actually appear in it.

(eval (stencil (x) 1))
???> Cannot eval

When substituting an ABT with free variables into another ABT, both sets of free variables are preserved:

(let ((m (stencil (x z) (add x z)))
      (k (stencil (y) (mul y 2))))
  (subst m "z" k))
===> (stencil (x y) (let ((add_1 <builtin:add>)) (add_1 x (let ((mul <builtin:mul>)) (mul y 2)))))

Variables in lambda bindings are properly renamed to avoid capture:

(let ((m (stencil (x) (lambda (y) (add x y))))
      (k (stencil (y) y)))
  (subst m "x" k))
===> (stencil (y) (let ((add_1 <builtin:add>)) (lambda (y_1_1) (add_1 y y_1_1))))

Variables in let bindings are also properly renamed:

(let ((m (stencil (x) (let ((y x)) y)))
      (k (stencil (y) y)))
  (subst m "x" k))
===> (stencil (y) (let ((y_1 y)) y_1))

Free variables in the replacement are preserved in nested expressions:

(let ((m (stencil (x) (lambda (y) (add x y))))
      (k (stencil (y z) (mul y z))))
  (subst m "x" k))
===> (stencil (y z) (let ((add_1 <builtin:add>)) (lambda (y_1_1) (add_1 (let ((mul <builtin:mul>)) (mul y z)) y_1_1))))

Equality of ABT values

Basic equality of quoted expressions works:

(equal? (quote 42) (quote 42))
===> 1

(equal? (quote 42) (quote 43))
===> 0

Lambda expressions with the same parameter names are equal:

(equal? (quote (lambda (x) x))
       (quote (lambda (x) x)))
===> 1

Lambda expressions with different parameter names but alpha-equivalent bodies are equal:

(equal? (quote (lambda (x) x))
       (quote (lambda (y) y)))
===> 1

Lambda expressions with different bodies are not equal:

(equal? (quote (lambda (x) x))
       (quote (lambda (x) (add x 1))))
===> 0

Nested lambda expressions preserve alpha equivalence:

(equal? (quote (lambda (x) (lambda (y) (add x y))))
       (quote (lambda (a) (lambda (b) (add a b)))))
===> 1

Let expressions with alpha-equivalent bindings and bodies are equal:

(equal? (quote (let ((x 1)) x))
       (quote (let ((y 1)) y)))
===> 1

Let expressions with different bindings are not equal:

(equal? (quote (let ((x 1)) x))
       (quote (let ((x 2)) x)))
===> 0

Complex nested expressions maintain alpha equivalence:

(equal? (quote (let ((f (lambda (x) x))) (f 1)))
       (quote (let ((g (lambda (y) y))) (g 1))))
===> 1

TODO: also test with stencil and variables declared free.

subst Function

The subst function performs capture-avoiding substitution on ABT values.

Basic substitution works:

(let ((m (stencil (x) (add x 1))))
  (subst m "x" (quote 5)))
===> (quote (let ((add_1 <builtin:add>)) (add_1 5 1)))

And you can evaluate that:

(let ((m (stencil (x) (add x 1))))
  (eval (subst m "x" (quote 5))))
===> 6

Multiple variables can be substituted:

(let ((m (stencil (x y) (add x y))))
  (subst (subst m "x" (quote 2)) "y" (quote 3)))
===> (quote (let ((add_1_1 <builtin:add>)) (add_1_1 2 3)))

And you can evaluate that resulting ABT:

(let ((m (stencil (x y) (add x y))))
  (eval (subst (subst m "x" (quote 2)) "y" (quote 3))))
===> 5

Partially substituting results in an ABT that still has variables declared free:

(let ((m (stencil (x y) (add x y))))
  (subst m "x" (quote 2)))
===> (stencil (y) (let ((add_1 <builtin:add>)) (add_1 2 y)))

All free variables must be substituted before evaluation. Attempting to evaluate with remaining free variables fails:

(let ((m (stencil (x y) (add x y))))
  (eval (subst m "x" (quote 2))))
???> Cannot evaluate

destructABT Function

The destructABT function allows pattern-matching on ABT values, taking handlers for each type of node that can appear in an ABT. It takes 7 arguments:

  1. The ABT to destruct
  2. Handler for variables
  3. Handler for literals
  4. Handler for lambda expressions
  5. Handler for let expressions
  6. Handler for function applications
  7. Handler for builtin operations

Literal values are handled:

(destruct-abt
  (quote 42)
  (lambda (name) "var")
  (lambda (val) val)
  (lambda (param body) "lambda")
  (lambda (name expr body) "let")
  (lambda (fn arg) "app")
  (lambda (name arg) "builtin"))
===> 42

Lambda expressions are deconstructed properly. Note that we do not return the name we see inside the lambda, because that name will not be meaningful - we cannot reasonably expect it to be "x".

(destruct-abt
  (quote (lambda (x) x))
  (lambda (name) "var")
  (lambda (val) "lit")
  (lambda (param body)
    (add
      (destruct-abt body
        (lambda (name) 1)
        (lambda (val) 0)
        (lambda (param body) 0)
        (lambda (name expr body) 0)
        (lambda (fn arg) 0)
        (lambda (name arg) 0))
      2))
  (lambda (name expr body) "let")
  (lambda (fn arg) "app")
  (lambda (name arg) "builtin"))
===> 3

Let bindings can be analyzed:

(destruct-abt
  (quote (let ((x 1)) x))
  (lambda (name) "var")
  (lambda (val) "lit")
  (lambda (param body) "lambda")
  (lambda (name expr body)
    (add
      (destruct-abt expr
        (lambda (name) 0)
        (lambda (val) 1)
        (lambda (param body) 0)
        (lambda (name expr body) 0)
        (lambda (fn arg) 0)
        (lambda (name arg) 0))
      (destruct-abt body
        (lambda (name) 2)
        (lambda (val) 0)
        (lambda (param body) 0)
        (lambda (name expr body) 0)
        (lambda (fn arg) 0)
        (lambda (name arg) 0))))
  (lambda (fn arg) "app")
  (lambda (name arg) "builtin"))
===> 3

Function applications are handled:

(destruct-abt
  (quote (let ((f (lambda (x) x))) (f 1)))
  (lambda (name) 0)
  (lambda (val) 1)
  (lambda (param body) 2)
  (lambda (name expr body)
    (add
      (destruct-abt expr
        (lambda (name) 0)
        (lambda (val) 0)
        (lambda (param body) 100)
        (lambda (name expr body) 0)
        (lambda (fn arg) 0)
        (lambda (name arg) 0))
      (destruct-abt body
        (lambda (name) 0)
        (lambda (val) 0)
        (lambda (param body) 0)
        (lambda (name expr body) 0)
        (lambda (fn arg)
          (destruct-abt arg
            (lambda (name) 0)
            (lambda (val) 200)
            (lambda (param body) 0)
            (lambda (n e b) 0)
            (lambda (fn arg) 0)
            (lambda (name arg) 0)))
        (lambda (n as) 0))))
  (lambda (fn arg) 3)
  (lambda (name arg) 4))
===> 300

Body of a let expression can be extracted, although it should be noted that the resulting body ABT value will still contain bindings, in the form of a let expression. (Disappointing?)

(let ((cons
        (lambda (x y)
          (quote (x y))))
      (car
        (lambda (lst)
          (destruct-abt lst
            (lambda (name) (neg 1))
            (lambda (val) (neg 1))
            (lambda (param body) (neg 1))
            (lambda (name expr body) body)
            (lambda (fn arg) (neg 1))
            (lambda (name arg) (neg 1))))))
  (car (cons 1 2)))
===> (quote (let ((y_1 2)) (x_1 y_1)))