Adding Identifiers

The following steps are required to add identifiers:

Create the concrete syntax
Create inference rules

Note

In a bind, a variable cannot use itself in its declaration

Concrete Syntax

bind x in x + x

Inference Rules

Substitution Operator

$[x \to v] t$ means 'replace all free instances of $x$ in $t$ with $v$ '

`bind`

\frac{a ⇓ v_{a} [i \to v_{a}] s ⇓ v_{s}}{bind i = a in s ⇓ v_{s}} BindE

$a$ evaluates to $v_{a}$
substitute $v_{a}$ for free $i$ in the body of bind, evaluate to $v_{s}$
result is $v_{s}$

Identifiers

\frac{}{x ⇓ ⊥} IDE

Evaluating an identifier means the identifier was no replaced
No bind defined the identifier or it would no longer be there

Evaluating

When evaluating bind we have to substitute an identifier with a value.

To do this we recursively descend into the expressions within bind to substitute and evaluate. We first evaluate value we want to substitute. When we have this value we substitute it into the body of the bind.

We always substitute into the bound value of a but conditionally substitute into the scope of a bind if the identifiers collide.

Note

This method is not very efficient. It is mathematically correct and works as intended but recursively descends into our AST every time we hit a bind to substitute. There are much better ways to do this.

eval (Id s) = Nothing
eval (Bind i a b) = do { v  <- eval a;
						 b' <- subst i v b;
						 eval b'
						}

-- Takes the identifier, the value and the expression to sub into
subst :: String -> BAE -> BAE -> BAE
subst x v (Nat n) = (Nat n)
subst x v (Id x') = if x == x' then (Nat x) else (Id x')
subst x v (Plus l r ) = Plus((subst x v l) (subst x v r))
subst x v (Minus l r ) = Minus((subst x v l) (subst x v r))
subst x v (Mult l r ) = Mult((subst x v l) (subst x v r))
subst x v (Div l r ) = Div((subst x v l) (subst x v r))
subst x v (Bind x' v' t') = if x == x'
								then Bind( x' (subst x v v') t')
								else Bind( x' (subst x v v') (subst x v t'))

Deferring Substitution

Immediately substituting in the value of an identifier is very inefficient.

Instead we can "remember" what bindings exist in our scope and replace identifiers with values.

We will use an environment to do this.

Type Env = [(String, BAE)]

lookup :: A -> [(A, B)] -> Maybe B

-- We give our evaluator an environment to start with
eval :: Env -> BAE -> Maybe BAE
eval _ (Num n) = Just (Num n)
eval e (Plus l r) = do { (Num l') <- (eval e l);
						 (Num r') <- (eval e r);
						 return (Nat l' + r')
						}
eval e (Bind x a s) = do { a' <- (eval e a);
						   eval (x:a'):e s
						  }
eval e (Id x) = lookup x e

Note

We can curry the eval function with a default Env.

eval' = eval [("pi", (Num 3))]

This method has a few upsides as compared to using direct substitution.

No more substitution
No more walking the code

evals uses direct substitution
eval uses deferred substitution

Definitions

Instance: occurrence of an identifier

bind x = 5 in x + 4
-- 'x' is the identifier

Binding Instance: Where an identifier is declared and given a value

bind x = 5 in x + 4
-- 'x' is bound to the left of '=' sign

Scope: The region where the identifier is defined and can be used

bind x = 5 in x + 4
-- the scope is after the 'in'

Bound Value: A value given to an identifier in a binding instance

bind x = 5 in x + 4
-- the value of 'x' is the expression between the '=' and 'in'; 
    '5' in this case

Bound Instance: Where an identifier is used in the scope

bind x = 5 in x + 4
-- 'x' is being used in 'x + 4'

Free Instance: Where an identifier is used outside the scope

bind x = x + 5 in x + 4
-- 'x' is being used in its bound value 'x + 5'

Reference Interpreter - defines what we want our language to be, but is not necessarily its implementation.
Environment - a list of identifiers and the values in scope.
Direct Substitution - is a method of interpreting that walks the AST every time we encounter a bind to substitute values of the bind's identifier in the bind's scope.
Deferred Substitution - is a method of interpreting that only substitutes the value of an identifier when we encounter it in our recursive descent. When we encounter a bind we add a (key, value) pair of the id and value to the Environment