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:

 write(s, var, val) = \lambda var' \in Var. \left\{  \begin{array}{l l} val & \quad \text{if var = var' }\\ s \ var' & \quad \text{otherwise}\\ \end{array} \right.

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))
      | Variable(v)   -> read v
      | 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)

Comments are closed.