Correct by Construction in F#

Correct by Construction in F#

Jomo Fisher—a theme in the design of the F# language is that problems in the code are revealed as compilation errors. Consider this C# code which is used to compose a courteous letter to a customer:

enum Courtesy { Mr, Ms, Dr }

class Customer {

    public Courtesy Courtesy { get; set; }

    public string Name { get; set; }

}

class Letter {

    public string Introduction { get; set; }

    public string Body { get; set; }

}

static Letter Correspond(Customer customer, string message) {

    switch (customer.Courtesy)

    {

        case Courtesy.Mr:

            return new Letter { Introduction = "Mr. " + customer.Name,

                                Body = message };

        case Courtesy.Ms:

            return new Letter { Introduction = "Ms. " + customer.Name,

                                Body = message };

    }

    return null;

}

 

This compiles without errors despite having some problems (can you spot them?)

I want to stop now and claim that I’m not picking on C# which is a wonderful language. It’s just that I need to compare F# to something in order to illuminate my point and I happen to know C# pretty well.

Now, transliterate the code above into F#:

#light

type Courtesy = Mr | Ms | Dr

type Customer = {

    Courtesy:Courtesy

    Name:string

}

type Letter = {

    Introduction:string

    Body:string

}

let Correspond(customer,message) =

    match customer.Courtesy with

    | Mr -> {Introduction = "Mr. " + customer.Name; Body=message}

    | Ms -> {Introduction = "Ms. " + customer.Name; Body=message}

    | _ -> null

 

Compiling this gives a warning on the last line:

error FS0043: The type 'Letter' does not have 'null' as a proper value.

In C#, objects are allowed to be null by default and your code is responsible for handling the possibility of nullity everywhere. F# objects are not allowed to be null and, except in a few special cases such as interoperating with non-F# code, you can assume that object instances aren’t null.

So the caller of the Correspond function need not worry about receiving a null Letter instance and I can just delete the last line:

let Correspond(customer,message) =

    match customer.Courtesy with

    | Mr -> {Introduction = "Mr. " + customer.Name; Body=message}

    | Ms -> {Introduction = "Ms. " + customer.Name; Body=message}

 

Now I get a warning:

warning FS0025: Incomplete pattern match on expression. The value ‘Dr’ will not be matched

This is an easy mistake to make: I forgot one of the cases in the Courtesy enumeration.

An aside on pattern matching: If you code in F# you’ll find yourself using pattern matching for a significant amount of the logic in your program. It’s far more than just a synonym for switch. It can do complex matching against just about any type of object. This, combined with completeness checking, helps eliminate a large class of bug.

Here’s my final corrected code:

let Correspond(customer,message) =

    match customer.Courtesy with

    | Mr -> {Introduction = "Mr. " + customer.Name; Body=message}

    | Ms -> {Introduction = "Ms. " + customer.Name; Body=message}

    | Dr -> {Introduction = "Dr. " + customer.Name; Body=message}

 

This idea that F# should lead you to write code that is correct by construction is not just about the features I mentioned above. Its fundamentally weaved through the language. Take a look at how casting works for another example.

Honestly, it took me some time to get used to. I particularly struggled with the non-nullity of object instances. I was used to being able to smuggle the special “null” value around without changing my code to accommodate it. I realize now I was just sweeping a potential problem under the rug.

This posting is provided "AS IS" with no warranties, and confers no rights.