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.


 

Comments (9)

  1. [ICR] says:

    I realise it’s not the same and perhaps not in the spirit of the post, but I always write my switch statements in C# as:

    switch(Value)

    {

     case A:

       …

       break;

     case B:

       …

       break;

     default:

       Debug.Assert("ERROR");

    }

    Not as good as a compile time but the extra runtime check allows you to catch missing code more often.

    But I understand the theme of the post. The non-nullilty of things does help to reduce a lot of errors.

  2. MichaelGG says:

    Yea, top on my wish list for C# 4 is a non-nullable type system and discriminated unions, hopefully with some primitive pattern matching. But I’m sure I’ll just be told to go use F# (which is fine by me, as soon as it’s shipping in VS!)

  3. Welcome to the forty-third issue of Community Convergence. The last few weeks have been consumed by the

  4. BlindWanderer@gmail.com says:

    I would assume that F# is implicitly adding some non-nullable attribute to it’s classes and method parameters. Otherwise how would other languages know not to pass those classes and methods nulls?

  5. MichaelGG says:

    Blind: Other languages don’t know and will pass null; hence with interop you gotta watch it. It’s just a sad result of C#/CLS not including some kind of non-nullable type system from the start.

  6. Now that we have covered the basics, in minutes 8 – 14 we will cover the foundational concepts and types

  7. David Nelson says:

    I am curious, how does F# deal with situations where null values are legitimate? Null values in programming languages are similar to null values in databases: they can cause problems if used carelessly, but they do have legitimate uses. And not all classes are well-suited to singleton "empty" values.

  8. Jonathan Allen says:

    > a few special cases

    Like everytime you deal with the String type?

    F# should have been so much more, but their unwillingness or inability to merge option and null means that my code isn’t any safer.