Deceitful Contracts - Fix with Church-encoded Sum Types

C# does not support sum types, which are commonly used to encode failure at the type level in statically typed functional languages. So in C#, how can we encode failure in the type system in order to keep our functions total and our signatures true (rather than throw exceptions and perforate our information pipelines in the process, making them as air tight as a strainer)?

In a previous post, I lamented the prevalent use of exceptions in C# because it break the contract stated a function’s signature, and it forces the caller of the function to know implementation details, thus violating the “program to an interface, not an implementation” mantra¹.

As an alternative to restricting the function’s input type to only valid values, I gave an example, in F#, of using Option as the return type. This Option<'T>² type can be simply defined as the collection of all values of T, tagged with a Some data constructor, plus an additional None value.³ Sum types like this one are supported in F# and other (predominantly functional) languages (e.g., Haskell, OCaml, SML, Scala, Rust, etc.), and specifying such a type in those languages is trivial. In F#, for example, the type is defined as

type Option<'T> = None | Some of 'T

But how might you do this in languages that do not have native support for sum types, like C#? Church encoding is one way to do it.⁴ Church encoding, named after Alonzo Church, is a means of representing data and operators in the untyped lambda calculus, i.e., using only functions. To represent our two options None and Some of 'T using Church encoding, we need two functions, one for each case. What might these functions look like?

In Haskell syntax:

none = \n s -> n
some = \x n s -> s x

In JavaScript syntax:

const none = n => s => n
const some = x => n => s => s(x)

Each function takes as arguments each of the possible cases: n (None) and s (Some). We define none simply as the function than returns n, and some as the function that “loads” an x value (this corresponds to the T value in Option<'T>), ignores the n value, and returns s applied to x. These functions serve as a kind of pattern matching mechanism. For example, say we have a match function that takes an o function that is either none or some, a default d in case o is none, and a function f in case o it some:

Haskell:

match = \d f o -> o d f

JavaScript:

const match = d => f => o => o(d)(f)

Then applying match to some would yield f applied to the x in some, e.g.,

Haskell:

match 0 (+1) (some 2)
== (some 2) 0 (+1)
== (\n s -> s 2) 0 (+1)
== 3

JavaScript:

match(0)(x => x+1)(some(2)) 
== some(2)(0)(x => x+1) 
== (n => s => s(2))(0)(x => x+1) 
== 3

Applying match to none would yield d, e.g.,

Haskell:

match 0 (+1) none
== none 0 (+1) 
== (\n s -> n) 0 (+1) 
== 0

JavaScript:

match(0)(x => x+1)(none) 
== none(0)(x => x+1) 
== (n => s => n)(0)(x => x+1) 
== 0

How do we encode this in C#? Since we want to tie these two option together as one type, let’s define two classes None and Some that implement a common interface IOption with a Match function.

public interface IOption<T>
{
  R Match<R>(R none, Func<T, R> some);
}

public class None<T> : IOption<T>
{
  public R Match<R>(R none, Func<T, R> some)
  {
    return none;
  }
}

public class Some<T> : IOption<T>
{
  private readonly T value;

  public Some(T value)
  {
    this.value = value;
  }

  public R Match<R>(R none, Func<T, R> some)
  {
    return some(value);
  }
}

The Some constructor take a value, which corresponds to the x in the \x n s -> s x lambda function above, and serves as a kind of partial application of it.

The Match method, as the match function previously shown, is used to transform the Option type values (None and Some) into other values or even other types. For example, if we have a value IOption opt, we can call

opt.Match("this is None", s => s.ToString());

to perform a transformation on opt into a string. We don’t need to know if opt is None or Some, but if it is None, the expression will return "this is None", and if it is Some, it will return the string representation of that value.

We can make the code more powerful by introducing a few more functions, for example, a LINQ-like Select and SelectMany (using extension methods). These functions take a function to apply for the case where we have Some-thing, and otherwise simply return None if None is the value⁵:

public static class Option
{
  public static IOption<R> Select<T, R>(this IOption<T> source, Func<T, R> selector)
  {
    return source.Match<IOption<R>>(new None<R>(), x => new Some<R>(selector(x)));
  }

  public static IOption<R> SelectMany<T, R>(this IOption<T> source, Func<T, IOption<R>> f)
  {
    return source.Match<IOption<R>>(new None<R>(), f);
  }
}

And here’s how you’d use them:

var n = new Some<int>(42);
var nplus1 = n.Select(i => i+1);
var nplus10 = n.SelectMany(i => (new Some<int>(i+10)));

To sum up, we can encode sum types using functions a-la lambda calculus. In C#, we can use this in combination with classes and interfaces to have a form of sum type encoding in the type system. Here, we have only demonstrated the implementation of one particular sum type (Option<'T>), but Curch encoding is generic, so any other sum type can be encoded this way.

References

• Church encoding
• Seemann’s Church-encoded Maybe in C#