Blog

Each of the terms defined thus far returns some value computed during their exeution. Constants return values:

```
eval 5
== 5
```

Mathematical expressions calculate and return values:

```
eval 5+2
== 7
```

```
eval 5<=3
== false
```

`lambda`

and `app`

both return values;

```
lambda x:nat in x+1
== lambda x:nat in x+1
```

```
(app (lambda x:nat in x+1) 4)
== 5
```

Even `bind`

that creates and uses local bindings returns a value upon execution:

```
bind x=4 in x + 1
== 5
```

They all return values upon evaluation. Because of this property, we call these terms *expressions*. Given a well-formed expression, evaluation always results in a value. For example, we studied the `if`

expression and include it in all our languages. Given three terms, evaluting the first determines whether the second or third should be evaluated and returned. The `if`

expression always returns a value.

*Statements* are programming language constructions that order execution rather than calculate values. Statements are structures such as loops, `if`

statements, assignment and sequence. Unlike expressions, none of these terms must return values. The `if`

statement does not return a value, but instead chooses and executes a nested statement. The assignment statement alters a variable value, but does not itself produce a value. Sequential execution of two statements does not result in a value.

So far we have introduced three types - `nat`

, `boolean`

, and function types of the form `T->T`

. Here we introduce the most trivial of types, the *Unit*. The unit type is named `unit`

and nas a single value, `u`

. Unit has no associated operations and no properties other than having one and only one value. Because `u`

is a value, it has no associated evaluation rule. Because it is a constant value, it’s typing rule is trivial:

```
u:unit
```

`unit`

has a number of special properties that we’ll skip for now. All we need is a trival type that conveys no infomration.

Executing statements sequentially is so common in imperative languages that we often overlook it as a paradigm.

The concrete syntax for sequential execution is two terms separated by a semicolon:

\[\begin{align*} t ::= & t\;;\;t \\ \end{align*}\]We’ve grown to view the semicolon as a line terminator, but in langauges like Pascal and formalisms like CSP it is an operator just like `while`

or `if`

. The notation `t0 ; t1`

indicates that term `t0`

is executed immediately followed by `t1`

. Combining the sequence operation with our existing language allows us to create operator sequences such as:

```
bind f = (lambda x:nat in x+1) in
app f 1 ; app f 2
```

or

```
lambds x:nat in x<=0 ; gtz x
```

Adding the abstract syntax term `seq`

includes sequence in FBAE:

```
Seq t1 t2
```

With syntax defined, lets think about what sequencing operations actually does. As we’ve done in the past, we’ll start by thinking about untyped sequencing and move to sequencing in a typed language.

Sequencing term execution is quite simple using a `Maybe`

or `Reader`

monad. In fact, we saw the `Reader`

at work sequencing execution for addition and subtraction. Recall the interpreter statement for the addition term `(Plus l r)`

:

```
evalM (Plus l r) = do { (NumV l') <- (evalM l) ;
(NumV r') <- (evalM r) ;
return (NumV (l'+r')) }
```

`l`

and `r`

are evaluated in sequence, the results added together, and finally returned. This is exactly what we want! Except of course that we can’t return the sum of evaluation results.

What should sequence return? In this untyped case let’s remember what Racket and Common Lisp do - return the last value calculated. This would make our evaluation case for `Seq`

the following:

```
evalM (Seq l r) = do { evalM l ;
evalM r }
```

What happened to the bind symbols? `l'`

and `r'`

are gone. All this means is the values resulting from evaluating `l`

and `r`

are not bound to variables. The result of `evalM l`

is discarded while the result of `evalM r`

is returned by the `do`

form. This is exactly what we want - evaluate `l`

, evaluate `r`

and return the result.

If we want to sequence more than two operations, such as `t0 ; t1 ; t2`

, nesting the sequnce operation works quite nicely:

```
(Seq t0 (Seq t1 t2))
```

and our monadic implementaiton serves us well.

By the way, which monad did we use in the implementation above? Is it `Maybe`

or `Reader`

?

Another mechanism for implementing sequence is to define it as a derived for using `app`

and `lambda`

. If we want to execute `t1`

followed by `t2`

we can translated `(Seq t1 t2)`

in the following manner:

```
Seq l r == (app (lambda x in r) l)
```

Assuming call-by-value semantics, `app`

evalutes the argument to its function, binds that value to the function’s formal parameter, and evaluates the function’s body. Here the parameter is named `x`

and `evalM l`

gets bound to `x`

. As long as `x`

does not appear free in `r`

, this derived form works just fine. However, `x`

*must not* be free in `r`

or we will run into all kinds of type problems at runtime. It is simple enough to check this property statically or we can use a wildcard parameter:

```
Seq t1 t2 == (app (lambda _ in r) l)
```

Here `x`

is replacec by the wildcard `_`

. This symbol is not a variable and is ignored by `app`

. No value is bound to it eliminating any messiness due to the result type of `evalM r`

.

What happens when we add static typing to sequencing? As it turns out, not much and quite alot. Let’s look again at the impelementation of `Seq`

evaluation:

```
evalM (Seq l r) = do { evalM l ;
evalM r }
```

Because `l`

does not interact with `r`

during evaluation, the type resulting from `evalM l`

makes no difference. Furthermore, the type of a sequence operation is easily determined to be the type of `r`

:

```
typeofM (Seq l r) = typeofM r
```

Life is more intresting if we defined sequence using a derived form as we did earlier. Recall the untyped definition:

```
Seq l r == (app (lambda x in r) l)
```

and note that `x`

has no type. In a statically typed language the lambda’s formal parmeter must have an ascribed type. There are several ways around this, but the most common is to make the type of `x`

the `unit`

type described earlier:

```
Seq l r == (app (lambda x:unit in r) l)
```

This forces `l`

to return a `u`

in every case and thus be of type `unit`

.

This sounds restrictive, but it is true to the concept that a statement need not return a value. Returning `unit`

is exactly that - returning a value that conveys no information. For completeness, the wildcard variable should be used rather than `x`

:

```
Seq l r == (app (lambda _:unit in r) l)
```

We’re going to skip the full implementation of sequence for now. It is quite important in our upcoming discussion of state, but as of right now sequence doesn’t do a thing. Literally. We can sequence FBAE terms as much as we want and the execution result will never differ from simply executing the last operation in the sequence. Why is this? By definition the execution of the first term in a sequence never passes anything to the second. The `Monad`

implementation drops the first term on the floor. The elaboration implementation makes sure the first result cannot be used in the second computation buy using a wildcard. So what is sequence for? When we add global state you will recognize its importance quickly.

- Can
`Seq l r`

be elaborated to a`bind`

? If so, implement it. If not, explain why. Assume you can use the`_`

symbol.