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

• Anonymous
  April 22, 2008
  PingBack from http://microsoftnews.askpcdoc.com/?p=3805

• Anonymous
  April 22, 2008
  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.

• Anonymous
  April 22, 2008
  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!)

• Anonymous
  April 23, 2008
  Welcome to the forty-third issue of Community Convergence. The last few weeks have been consumed by the

• Anonymous
  April 24, 2008
  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?

• Anonymous
  April 24, 2008
  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.

• Anonymous
  May 09, 2008
  Now that we have covered the basics, in minutes 8 - 14 we will cover the foundational concepts and types

• Anonymous
  June 20, 2008
  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.

• Anonymous
  June 04, 2009
  > 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.