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.
