Definition-of-Argyle.md @master — view 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:
- It honors lexical scope - variables must be bound either in the current scope or within a
lambda
binding in the quoted expression - 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:
- The ABT to destruct
- Handler for variables
- Handler for literals
- Handler for lambda expressions
- Handler for let expressions
- Handler for function applications
- 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)))