# Semantics in F# (utilizing combinators)

Functional languages are convenient for defining semantics of programming languages. In this post, I'll show an example of such a semantic in F# for a simple programming language. I will also show how some combinators can help to produce readable code.

Given the grammar:


expr  := var | number | bool | expr + expr | expr - expr | expr * expr | expr == expr | expr /\ expr | !expr
stmnt := var = expr; |  if ( expr ) stmnt [else stmnt] | { stmnt+ } | while ( expr ) stmnt


Let's define the following f# data structures:


type Op = Plus | Subtr | Div | Mul | Eq | And | Not

type Expr =
| Variable of string
| Int of int
| Bool of bool
| BinOp of Op * Expr * Expr
| UnOp of Op * Expr

type Statement =
| Block of list<Statement>
| If of Expr * Statement * option<Statement>
| While of Expr * Statement
| Assign of string * Expr


At this point, we do not care about types: let's assume all expressions are correctly typed. Now consider the operational semantics of this language. Since the language supports variables, there must be some state $s$ that maps variables to values. Let $s$ be of type $Variable \rightarrow \mathbb{Z} \cup \{ tt, ff \}$. Each statement has the ability to mutate this state. It is possible to model the semantics of statements as some function $sems \in Statement \rightarrow State \hookrightarrow State$. Semantics of expressions can be modelled by a function $seme \in Expr \rightarrow State \rightarrow \mathbb{Z} \cup \{ tt, ff \}$. Note that the function produced by $sems$ is partial since there is a while construct in our language, therefore allowing non-termination. Now let's go back to F# and define some more constructs:


type Result        = Int of int | Bool of bool
type State         = string -> Result
type Sem           = State  -> Result * State


The f# implementation is slightly different from the functions that we defined earlier. Statements also produce values (e.g. a return statement produces the value of an expression) and expressions can mutate state. Let us see how an implementation of $sems$ looks like in F#:


let rec sems stmnt s =
match stmnt with
| If(cond, tt, ff) ->
let ((Bool b), s') = seme cond s
if b then sems tt s' else (match ff with | Some(ff) -> sems ff s' | _ -> s')
... etc


In the above implementation, state is passed around very explicitly and results in many $s$'s all over the place. It is possible to abstract from this and implicitly pass state around through the use of a few combinators:


let zero      = fun s -> (Int(0), s)
let ret x     = fun s -> (x, s)
let (>>=) f g = fun s -> (fun (r, s') -> g r s') (f s)
let (>>|) f g = f >>= fun _ -> g


Note the types of the combinators in the context of semantics: $ret \in Result \rightarrow Sem$, $(>>=) \in Sem \rightarrow (Result \rightarrow Sem) \rightarrow Sem$ and $(>>|) \in Sem \rightarrow Sem \rightarrow Sem$. Now we apply these combinators in the implementation of $sems$:


let rec sems stmnt =
match stmnt with
| If(cond, tt, ff) ->
seme cond
>>= fun ((Bool b)) -> if b then sems tt else (match ff with | Some(ff) -> sems ff | _ -> zero)
... etc


Ok, so the problem of explicit state passing is solved. Now we will look at the "... etc" part and fill in the semantics for other statements. Consider the semantics of the block statement: a sequence of statements $S_0$ to $S_n$ is 'executed'. The state is mutated by each of these statements. If we forget about the result and only consider state, such a semantic will look like this: $sems \ [ S_0; S_1; \ ... \ S_n ] (s) \ = \ sems \ S_n \ (sems \ S_{n-1} \ ( \ ... \ sems \ S_1 \ ( \ sems \ S_0 \ s \ ) \ ... \ ) )$. We can utilize our >>| combinator to create such a chain: $S_0 \ >>| \ S_1 \ >>| \ ... \ >>| \ S_n$. In f#, we use the fold function. Each chain begins with 'zero' that has no effect on the state:


List.fold (fun chain S -> chain >>| sems S) zero slist


Now consider the semantics for the while statement: while some condition holds, execute the body. We can change this into the equivalent statement: if some condition holds, execute the body and execute the while statement again. Formally, this is defined like this: <$\textrm{while} \ ( \ B \ ) \{ \ P \ \}, s$> $\rightarrow$ <$\textrm{if} \ ( \ B \ ) \{ \ P; \ \textrm{while} \ ( \ B \ ) \{ \ P \ \} \}, s$>. In f#:


sems (While(B, P)) = sems (If(B, Block([P; While(B, P)]), None))


The semantic of the assign statement is remaining. $State$ is a function that maps variables to values. The assign statement needs to mutate this state, but the problem is that a function cannot be mutated. Instead, we construct a new state that maps the variable to the new value. Formally, we define a function $write \in State \times Var \times Result \rightarrow State$ with definition:

In f#, we can write this like:


let write var v = fun s -> (v, fun var' -> if var' = var then v else s var')
let read var    = fun s -> (s var, s)


Let's now fill in the blanks:


let intBinOp f (Int(l)) (Int(r)) = Int(f l r)

let binOpMap =
dict [
Plus,   intBinOp (+);
Subtr,  intBinOp (-);
Div,    intBinOp (/);
Mul,    intBinOp (*);
Eq,     fun (Int(l)) (Int(r)) -> Bool(l = r);
And,    fun (Bool(l)) (Bool(r)) -> Bool(l && r);
]

let unOpMap =
dict [
Not,    fun (Bool(n))           -> Bool(not n)
]

let rec sems stmnt : Sem =
match stmnt with
| If(cond, tt, ff) ->
seme cond
>>= fun ((Bool b)) -> if b then sems tt else (match ff with | Some(ff) -> sems ff | _ -> zero)
| While(B, P)      -> sems (If(B, Block([P; While(B, P)]), None))
| Block(slist)     -> List.fold (fun chain S -> chain >>| sems S) zero slist
| Assign(var, v)   -> seme v >>= write var

and seme expr : Sem =
match expr with
| Expr.Int(n)   -> ret (Int(n))
| Expr.Bool(b)  -> ret (Bool(b))
| BinOp(op, l, r) ->
let opf = binOpMap.[op]
seme l
>>= fun l ->
seme r
>>= fun r -> ret (opf l r)
| UnOp(op, e) ->
let opf = unOpMap.[op]
seme e
>>= fun e -> ret (opf e)