This article is independent of our framework but at least for me, the mental model described here can be handy when it comes to developing reusable functional code. Also, such mental model helps understanding F# library primitives such as the lock expression.

Anatomy of ML like languages

Traditionally, imperative programming languages consist of a sequence of statements, separated by the "do that after this" operator ;.

F# on the other hand is expression based and there are no statements. Beside arithmetic expressions, there are bindings which persistently assign a value to identifier (let). Identifiers are immutable variables and cannot be changed after binding a value to it.

1: 
2: 
3: 

let x = 1 // from now on, x has value 1 
          // i.e. `x` and 1 can be used interchangably if 1 is pure. 
          // (see referential transparency)

Everything is a let expression

A mental model for programming reusable F# code is to think of programs being bindings. Unlike to Haskell, expression can have side effects, while computing their value. Expressions which have an effect but yield no useful value have the predefined type unit (a type with one single constructor named ()).

1: 

let useless = printf "abc" // useless has type unit ( useless :: unit )

Let expressions have the grammar let v = e0 in e1 where e0 and e1 are expressions again. Informally, let expressions evaluate the right hand side (e0) and assign its value to the binding variable v.

Sidenode: - F# is not a pure functional programming language, i.e. the evaluation of each expression might additionally have side effects, not visible in their type. Uncontrolled side effects are problematic, if the semantics of a program cannot be deduced easily. F# uses call-by-value semantics which means, that each function argument is evalauted before calling the function. For now, it is important to note, that e1 is always evaluted before continuing in the rest of the expression (after the in). Later you might recognize that this semantics arises naturally out of the definition of let and lambda expressions.

Consider the expression:

1: 

let s1 = printfn "abc" in (let s2 = printfn "def" in ()) 

The nesting structure of the let bindings can be used to model side effects, occuring sequentially. In F# it is possible to neglect all those in keywords resuting in this code:

1: 
2: 
3: 
4: 
5: 

let s1' = printfn "abc"
let s2' = printfn "def"
()

 

Here, each line stands for an implicit in keyword. Again consider s1'' which has type unit. In order not to bind unit values to useless variable all the time, F# allows to use do keyword to bind a useless value and forget about it.

1: 
2: 

do printfn "abc"  // let _ = printfn "abc"
                  // <=> do printfn "abc" 

Since writing do is boring one can ommit this construction and simply write the right hand side of the invisible let binding.

1: 

printfn "abc" // do printfn "abc"  <=> printfn "abc"

It is also possible to write multiple nested expressions in a single line by using the ; thingy.

1: 

printfn "abc"; printfn "cde"

So everything invisibly is a let binding i.e. everything is the same, and therefore composes :) This has some advantages when it comes to providing libraries which look like language primitives. Let us define a function for locking on objects.

1: 
2: 
3: 
4: 
5: 

let myLock o f = 
    try
        System.Threading.Monitor.Enter o
        f ()
    finally System.Threading.Monitor.Exit o

Let us look at the type: val myLock : o:'a -> f:(unit -> 'b) -> 'b

Given this we can use myLock similarly to the lock statement in C#.

1: 
2: 
3: 
4: 
5: 
6: 
7: 

let mon = obj() // obj is defiend as type alias for System.Object
let mutableState = ref 0
let someValueComputedInMutex = 
    myLock mon (fun () ->
        // do some stuff
        !mutableState // ! has type ref<'a> -> 'a
    )

Did i just say as beautiful as the lock statement in C#? From a composability point of view the higher order function is even more composable than the statement. As exercise, try to write equivalent C# code using the uncomposable lock statement.

There is no let expression. Everything is a lambda expression!!

Finally, let us understand the semantics of let expressions. Informally, let expressions bind the evaluated value of the right handside to a variable. In the continuation we can now refer to the new variable. If you remember your basic computer science courses this might sound a bit like variable substituion, doesn't it? In fact the let expression is totally useless, when defining semantics for the programming language.

from here very sketsch and buggy.

Let us now grab some theory by writing code. The syntax of lambda expressions (lambda calculus) is given as:

1: 
2: 
3: 
4: 

type Identifier = string 
type Expr = Application of Expr * Expr       // Function application
          | Abstraction of Identifier * Expr // Lambda abstraction or function definition
          | Var of Identifier

Let expressions can now be implemented by simple using Application and Abstraction!!!

1: 
2: 
3: 

// let v = e¹ in e² ⇔ (λ v . e²) e¹
let Let (v : Identifier) (e : Expr) (rest : Expr) =
    Application (Abstraction(v,rest), e)

Let us now write a simple and inefficient interpreter (which informally defines the semantics of lambda terms)

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 

let rec replaceVariables (v : Identifier) (vShouldBe : Expr) (rest : Expr) =
    match rest with
     | Application(e0,e1) -> Application(replaceVariables v vShouldBe e0, 
                                         replaceVariables v vShouldBe e1)
     | Abstraction(v',e) -> Abstraction(v',replaceVariables v vShouldBe e) 
     | Var x -> if x = v then vShouldBe else Var x

let rec freeVars (e : Expr) =   
    match e with
       // FV(a) = {a}
     | Var x -> Set.singleton x
       // FV(λ x. T) = FV(T) \ {x}
     | Abstraction(v,e) -> 
        let inner = freeVars e
        Set.difference inner (Set.singleton v)
       // FV(T¹ T²) = FV(T¹) ∪ FV(T²)
     | Application(e0,e1) -> Set.union (freeVars e0) (freeVars e1)

now let us implement evaluation

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 

// evals open/closed terms to normal form (strongly)
let rec eval (e : Expr) = 
    match e with
     | Var x -> Var x
       // β-reduction
     | Application (Abstraction(v, e0), Var v') when v' = v -> 
        eval e0
     | Application (Abstraction(v,e0),e1) ->  // β-reduction
        let freeInArgument = freeVars e1
        if Set.contains v freeInArgument then // α-conversion
            let freshIdentifier = v + "_" 
            let e0' = replaceVariables v (Var freshIdentifier) e0
            eval (Application (Abstraction(freshIdentifier,e0'), e1))
        else
            let body = replaceVariables v e1 e0
            eval body
       // reduce under lambda bodies (strong normalization)
     | Abstraction (v,e) as a -> Abstraction(v,eval e)
     | Application(e1, e2) -> // strong normalization again
        let r = Application(eval e1, eval e2) 
        if r = e then r else eval r
     | _ -> failwithf "should have been type error:%A" e

now let us use church encoding to represent numbers. and compute with them

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 

let one  = Abstraction ("f", ( Abstraction ("x", ( Var "x" ) ) ) )
let succ = Abstraction ("n", 
                ( 
                    Abstraction ("f", 
                        Abstraction("x", 
                            Application(Var "f", Application((Application(Var "n", Var "f")), Var "x"))
                        )
                    )
                )
          )

let p = Let "succ" succ 
            (Let "one" one
                (Application (Var "succ", Var "one"))
            )

let result = eval p 

// validate if one is indeed succ zero
assert (result = Abstraction ("f",Abstraction ("x",Application (Var "f",Var "x"))))

Success! We implemented a full fledged turing complete functional programing language in less than 50 lines of code.

Conclusions

F# is syntactically and semantically based on ML. The functional parts of the language have strong foundation and compose surprisingly well. As one can argue working with church encoding as numbers is rather useless in reality. Still, the implementation shows the imposing connection between theory and practical programming languages.