Episode 1 - Why Types?

16 Dec 2018 - 1100 Words

Why using types? When are they useful? Why we should care about types? What are types? These are the questions this series of posts give some answers to. Let’s start by realizing a fundamental fact: types are everywhere! Business models are all about types: users, shipments, orders, etc. Placing a user in the cart or shipping a client just makes no sense. Types are specification, discriminating what makes sense from what makes not.

A real life example

They can be simple like the well known strings, integers, booleans, lists, chars and floating-point numbers. But these six are far from covering the whole picture. Take as an example, a business application about finding the best deal amount a list of prices expressed in various currencies. To do so it would need currency conversion rates. Which data structure would you use to store these rates? One euro (EUR) worths when i write these lines 1.13 dollars (USD) which i could represent as the triple ("EUR", 1.13 ,"USD"). To store many rates, using a list is straightforward:

scala> val rates = List( ("EUR", 1.13, "USD"), ("GBP",  142.79, "JPY") )
rates: List[(String, Double, String)] = List((EUR,1.13,USD), (GBP,142.79,JPY))

Are you sure the type (String, Double, String) is a faithful representation for rates? Among all the possible values of this type is ("EUR", -3.0, "USD") meaning when you give one euro, you have to pay three dollars more to get nothing. This is silly, currency trading don’t work that way. Another problematic value is ("EUR", 0, "USD"). What is the point in exchanging one euro for nothing? Using Double to encode rates is wrong as not all floating point number makes a valid rate, only those strictly positive! A faithful representation of rates is the type r:Double{r > 0} which is the types of value r:Double such that r > 0. Such types are called refinement types and used heavily in F*.

We’re not done yet! Are you sure String is faithful representation of currencies? The empty string "" is not a currency, neither are "⛱", "⛏", etc but they are all valid strings. Assuming currencies:Set[String] is the set of all valid currency names, the type of currencies would be cur:String{currencies.contains(cur)} if it was expressible in Scala. But it is in F*:

open FStar.Set

val currencies: set string
let currencies = Set.as_set ["EUR"; "USD"; "JPY"]

type currency = cur:string{Set.mem cur currencies}

For the rest of this section, we will assume Scala has refinement types so that we can write:

type Rate = r:Double{r > 0}

val currencies: Set[String] =
  Set("EUR", "USD", "JPY")

type Currency = cur:String{currencies.contains(cur)}

We’re still not done yet as the type (Currency, Rate, Currency) still does not faithfully encode a conversion rate: ("EUR", 2.0, "EUR") is a value of this type but one euro can not worth two euros, this would not make sense! We could define the type Rate such that the only possible value is 1.0 when there is the same currency on both sides, but for simplicity’s sake and without loss of generality, we will just forbid converting into the same currency. Once again, in a version of Scala with refinement and dependent types, conversion rates would be:

final case class ConvRate(
  from: Currency,
  rate: Rate,
  to:Currency{from != to}
)

We’re almost there! Now every value of ConvRate makes sense from a business perspective: currencies from and to are valid distinct currencies and rate is a strictly positive exchange rate. Does the type List[ConvRate] faithfully represents a valid set of conversion rates? Values like List(ConvRate("EUR", 2.0, "USD"), ConvRate("EUR", 1.13, "USB")), where there are several distinct rates for the same conversion, do not make sense. Likewise, there is a relation between a conversion rate and its opposite direction. If one euros worth 1.13 dollars, then one dollar worths 0.88 euros. Values like List(ConvRate("EUR", 1.13, "USD"), ConvRate("USD", 2.0, "EUR")) do not respect this rule, so are invalid business values. To be sure values do respect these business rules we can use the data structure Map and only allow one side of the conversion (from < to) in the type ConversionRates:

val currencies: Set[String] =
  Set("EUR", "USD", "JPY")

final case class Conversion(
  from: String{currencies.contains(from)},
  to: String{currencies.contains(to) && from < to }
)

type ConversionRates = Map[Conversion, rate:Double{rate > 0}]

The type ConversionRates is certainly more complex than List[(String, Double, String)] but we gained several major benefits:

• every piece of code taking ConversionRates values as input is sure they respect business rules.
• every piece of code outputting ConversionRates values is guaranteed to respect business rules.
• division by zero is impossible!
  • no need to check!
  • no risk of exceptions!
  • no need to write tests!
  • no need to test the tests!

Conclusion

You may think you are such an excellent developer than all of this is useless because you would never define a negative rate or an empty string currency. But how could you be sure that the previous developers on the project were as perfect as you? Have you written the thousands of tests required to reach the same level of confidence types provide? Will you be happy refactoring those thousands of test every time the specification change? Are you sure you know perfectly every one of the millions ones of the project? Even the one you never had to work with?

If we were as good as we think we are, there would not be null pointer exceptions, segfaults, exploits, undefined-is-not-a-function, java.util.NoSuchElementException: None.get and all the other so common bugs and vulnerabilities we see far too often! Software are complex beasts, made usually by many people, some who leave, some who join. Relying of people being perfect (perfect knowledge, perfect understanding, perfect execution) is not realistic.

You can see type systems as powerful linters whose job is to check your code. Types get more and more complex as business rules do from simple properties to heavy mathematical theorems.

Types are specification, so in an ideal world a program well-typed would be, by definition, a program without bugs. If you still find bugs in your application, it either means you need to tighten your types to fit the specification or your language’s type-system is not expressive enough to encode the specification.

Next Episode

In the next episode, we will see enumerations like you probably have never seen them before.

Episode 2 - Enumerations

16 Dec 2018 - 2000 Words

Now that we know what types are and why there are useful, it is about time to meet some remarkable ones. But before we start, there is some important things to state. As a developer i know how tempting it is to search ready-to-paste answers. But the subject of these post series is nothing like a ready-to-paste answers cookbook. On the contrary, this is a presentation of deep, difficult but rewarding concepts. Do not see them as patterns to follow blindly, like it is unfortunately too often the case in our field. Instead, take the time to develop a deep understanding of what is really going on.

As such, the example i give may look simple. They are indeed much simpler than in real-life applications. They are not meant to be applicable as-is but to shed light on the core ideas. If you understand the principles they rely on, you’ll be able to apply these powerful concepts in your day to day code. Do not skim through this but take the time to develop your understanding.

In this whole series is we will assume null (in Scala), undefined (in Haskell) and side-effects do not exist. null, undefined and side-effects are absurd in every possible way. They make interesting properties collapse and should be avoided at all costs! We will consider all functions from A to B to be mathematical functions:

• they always return a valid value of type B of any input input value of type A
• on the same argument (or an equal argument), they always return the same result (or an equal result)
• the only effect of executing them is obtaining a result, no side-effect allowed
• If b:B = f(a:A) we can always replace b by f(a) and vice-versa, anywhere in the program, without altering its behavior (apart from computation time and memory consumption)

Formally it means we will consider all functions referentially transparent and total. That being said, let the journey begin with a very useful concept.

Many equivalent ways to express it

There is often many ways to express the same idea. How would you represent a piece of text? The types List[Char] and String are two different ways to do so. These types are indeed not equal: they are not encoded the same way and have distinct performance properties. But despite their differences, they can be considered equivalent. There is indeed a one-to-one correspondence between them: we can define two functions list2string: List[Char] => String and string2list: String => List[Char]:

def list2string: List[Char] => String =
  (l:List[Char]) => l.foldLeft("") {
    case (str,char) => s"$str$char"
  }

def string2list: String => List[Char] =
  (str: String) => str.toList

such that list2string and string2list are the inverse of each other

which also means

• for any list there is a unique string

  $$\forall l:\texttt{List[Char]}\ \exists! s:\texttt{String} ,\quad \texttt{string2list}(s) = l$$

• for any string there is a unique list

  $$\forall s:\texttt{String}\ \exists! l:\texttt{List[Char]},\quad \texttt{string2list}(\texttt{list2string}(s)) = s$$

• list2string and string2list are injective

  $$\forall l1, l2:\texttt{List[Char]},\ \texttt{list2string}(l1) = \texttt{list2string}(l2) \implies l1 = l2$$$$\forall s1, s2:\texttt{String},\ \texttt{string2list}(s1) = \texttt{string2list}(s2) \implies s1 = s2$$

Basically it means we can always convert from one type to the other without loss of generality.

For any function f: A => B (i.e. from A to B), f is called a bjection if and only if there exists a function g: B => A (i.e. from B to A) such that f and g are inverse of each other:

$$\forall a:\texttt{A},\quad \texttt{g}(\texttt{f}(a)) = a$$$$\forall b:\texttt{B},\quad \texttt{f}(\texttt{g}(b)) = b$$

Two types A and B are called equivalent, which is written A ≅ B, if and only if there exists a bijection f: A => B.

This notion is fundamental as it tells us that similarity between types is how closely they behave, not how closely they look. Two types of apparent very different form may actually be equivalent while two whose form may seem close may be fundamentally at odds. Focus on properties, not on looks.

The empty type

The first type i want to present has many names. Scala names it Nothing, Elm calls it Never, Coq uses the name it usually has in Proof Theory which is False while Type Theory refers to it as 0. This is an uninhabited type which means there is no value of this type. You may look at it as the empty set (hence the name 0):

final abstract class False {
  def fold[A]: A
}

This class being final we cannot define sub-classes, but being also abstract we cannot instantiate it either! And even if we could, how would we write a function fold which meets the specification that it provides a value of type A for any A? Remember, null does not exists.

How a type without values can be useful? By representing impossible cases in the type-system. Let v be a value of type Either[False, Int]. v has to be Right(i) for some integer i because otherwise it would be Left(f) for some value f of type False which is impossible! It means the following pattern-matching is exhaustive.

def extractRight[A](v: Either[False,A]): A =
  v match {
    case Right(a) => a
  }

Unfortunately Scala protests it’s not, demanding we cover the case v = Left(f: False) by returning a value of type A. We know, assuming null does not exists, there can not be such a value f:False. How to make Scala happy? Fortunately, every hypothetical value of type False comes with a handy fold function able to return anything. It corresponds in logic to the principle of explosion stating that from a contradicton (having a value of an empty type for example), you can conclude anything:

def extractRight[A](v: Either[False,A]): A =
  v match {
    case Right(a) => a
    case Left(f) => f.fold[A]
  }

Note that extractRight and Right:A => Either[False, A] being inverse functions it means Either[False, A] is equivalent to A. This one is of the main properties of False: Either[False, A], Either[A, False] and A are all equivalent (i.e. Either[False, A] ≅ A ≅ Either[A, False]).

You could argue using Either[False, A] is pointless as it is equivalent to A which is true, but bare in mind it is just a toy example. A more realistic one would involve complex types such as bifunctors like IO[E,A]. The ability to express impossible cases let us write IO computations that never fails IO[False, A] and IO computation that never returns IO[E,False] with the same code and API instead of relying on code/API duplication which is a waste of time, effort and complexity.

The idea being False can be expressed in many equivalent ways. The three types False, FalseInd and FalseFun are equivalent (``False ≅ FalseInd ≅ FalseFun`):

final abstract class FalseInd

trait FalseFun {
  def fold[A]: A
}

This is even clearer in Haskell as shown below where ind2fun and fun2ind are inverse functions.

{-# LANGUAGE RankNTypes, EmptyCase #-}
module Iso where

data FalseInd
type FalseFun = forall a. a

ind2fun :: FalseInd -> FalseFun
ind2fun x = case x of { }

fun2ind :: FalseFun -> FalseInd
fun2ind x = x

In Scala like in Haskell FalseInd express the idea of a data type with no constructor (i.e. to way to build a value) while FalseFun is the type of a function with no argument (i.e. a constant) returning values of type A for any A, but such a function does not exists. It may seem weird having functions between empty types but it actually makes a lot of sense: there is indeed a one-to-one correspondence between these two types as both have no values at all.

The singleton type

Often called unit, () or 1, it is the type with only one value.

sealed abstract class Unit {
  def fold[A](x: A): A =
    this match {
      case Unique => x
    }
}
final case object Unique extends Unit

Note that the type Unit admits one and exactly one value which is UniqueInd. UniqueInd is called a constructor of the data type Unit as it one way (the only one actually) to build a value of type Unit. Unit is useful everywhere you have to fill a value and/or a type but you actually don’t care which. For example, let v = println("Hello World"):IO[Unit] be the value printing a message to the screen. We don’t care what the execution v returns, we are only interested into what is printed, but it still needs to return something for the program to continue.

Once again Unit can be equivalently expressed as both the data type UnitInd and the function type UnitFun. Indeed ind2fun and fun2ind are inverse functions showing Unit ≅ UnitInd ≅ UnitFun.

sealed abstract class UnitInd
final case object UniqueInd extends UnitInd

trait UnitFun {
  def fold[A](x: A): A
}

val uniqueFun: UnitFun =
  new UnitFun {
    def fold[A](x: A): A = x
  }

def ind2fun: UnitInd => UnitFun =
  (i: UnitInd) => i match {
    case UniqueInd => uniqueFun
  }

def fun2ind: UnitFun => UnitInd =
  (f: UnitFun) => f.fold[UnitInd](UniqueInd)

data UnitInd where
  UniqueInd :: UnitInd

type UnitFun = forall a. a -> a

uniqueFun :: UnitFun
uniqueFun x = x

ind2fun :: UnitInd -> UnitFun
ind2fun UniqueInd = uniqueFun

fun2ind :: UnitFun -> UnitInd
fun2ind u = u UniqueInd

The type UnitFun may surprise you. How is it possible that a function type like it has only one possible value? Try to write a referentially transparent and total instance of UnitFun. You will see there is only one way to do so.

One of the main properties of Unit is that (Unit, A), (A, Unit) and A are equivalent (i.e. (Unit, A) ≅ A ≅ (A, Unit)). Exercise: write the inverse functions between these types.

The two values type: Booleans

Here comes one of the most well known type: the one with exactly two values often called Boolean in programming and 2 in Type Theory. Its values are generally named true and false:

sealed abstract class Boolean {
  def fold[A](tt: A, ff: A): A =
    this match {
      case True  => tt
      case False => ff
    }
}
final case object True  extends Boolean
final case object False extends Boolean

I’m sure you’re already familiar with booleans, but did you recognize the fold function? It is generally named if-then-else:

def ifThenElse[A](b: Boolean)(tt: A, ff: A): A = b.fold[A](tt, ff)

True and False are called the constructors of Boolean because they are the only way to build values of type Boolean. Once again this idea of a type with two values is equivalently expressed both as the data type BoolInd and as the function type BoolFun . Functions ind2fun and fun2ind are indeed inverse of each other.

sealed abstract class BoolInd
final case object TrueInd  extends BoolInd
final case object FalseInd extends BoolInd

trait BoolFun {
  def fold[A](tt: A, ff: A): A
}

val trueFun: BoolFun =
  new BoolFun {
    def fold[A](tt: A, ff: A): A = tt
  }

val falseFun: BoolFun =
  new BoolFun {
    def fold[A](tt: A, ff: A): A = ff
  }

def ind2fun: BoolInd => BoolFun =
  (i: BoolInd) => i match {
    case TrueInd  => trueFun
    case FalseInd => falseFun
  }

def fun2ind: BoolFun => BoolInd =
  (f: BoolFun) => f.fold[BoolInd](TrueInd, FalseInd)

data BoolInd where
  TrueInd  :: BoolInd
  FalseInd :: BoolInd

type BoolFun = forall a. a ->  a -> a

trueFun :: BoolFun
trueFun tt _ = tt

falseFun :: BoolFun
falseFun _ ff = ff

ind2fun :: BoolInd -> BoolFun
ind2fun TrueInd  = trueFun
ind2fun FalseInd = falseFun

fun2ind :: BoolFun -> BoolInd
fun2ind u = u TrueInd FalseInd

Once again the type BoolFun may surprise you. Once again try to write a referentially transparent and total instance of BoolFun. You will see there are only two ways to do so.

I could continue forever presenting types with 3, 4, … values but by now you must see the same pattern repeating and repeating again.

Next Episode: Products

In the next episode, we will a convenient way to combine types: Products.

Episode 3 - Products

16 Dec 2018 - 800 Words

Products, often called tuples, records or case classes, are a convenient way to bundle values of different types into a single value. The product of n types (with n being 0, 1, 2, etc) A_1, A_2, …, A_n is precisely the type whose values are formed with exactly one value of each type A_i for 1 ≤ i ≤ n. It is written (A_1, A_2, ..., A_n) in many languages, Product_n[A_1, A_2, ..., A_n] in Scala and A_1 × ... × A_n in Type Theory. As an example, the product of two types A and B would be defined as

final case class Product2[A, B](a: A, b: B) {
  def fold[R](f: (A, B) => R): R = f(a,b)
}

data Product2 a b = Constructor a b

Although in practice this is the preferred way to define the product of two types A and B, we will in this presentation prefer the equivalent definition below:

sealed abstract class Product2[A,B] {
  def fold[C](f: (A, B) => C): C =
    this match {
      case Constructor(a,b) => f(a,b)
    }
}
final case class Constructor[A,B](a: A, b: B) extends Product2[A,B]

data Product2 a b where
  Constructor :: a -> b -> Product2 a b

This equivalent definition makes clear the distinction between the type Product2[A,B] and the constructor Constructor[A,B]. the constructor is a function taking as argument one value of type A, another value of type B and returning a value of type Product2[A,B]. Its type in Haskell is A -> B -> Product2 A B and in Scala (A, B) => Product2[A,B]. Note than in Scala functions of type (A, B) => C are functions of two arguments (precisely Function2[A,B,C]) and not of one argument (A,B) (which would be Function1[(A,B), C]):

scala> Constructor[Int, String] _ : ( (Int, String) => Product2[Int, String] )
res0: (Int, String) => Product2[Int,String] = $$Lambda$1620/2032136633@55be2608

Prelude> :t Constructor
Constructor :: a -> b -> Product2 a b

Besides, by definition constructors are injective functions, which means that for any values a1:A, a2:A, b1:B and b2:B, Constructor[A,B](a1,b1) == Constructor[A,B](a2,b2) if and only if a1 == a2 and b1 == b2

Besides, Constructor[A,B] being the only constructor of Product2[A,B] then for any value v of type Product2[A,B], there is a unique value a of type A and a unique value b of type B such that v = Constructor[A,B](a,b)

Equivalence of inductive and functional forms

Once again any product can be equivalently expressed as a data type Product_n_Ind[A_1, ..., A_n] and as a function type Product_n_Fun[A_1, ..., A_n] with inverse functions ind2fun and fun2ind converting back and forth types Product_n_Ind[A_1, ..., A_n] and Product_n_Fun[A_1, ..., A_n]. For example with n = 2:

sealed abstract class Product2Ind[A,B]
final case class ConstructorInd[A,B](a: A, b: B) extends Product2Ind[A,B]

trait Product2Fun[A,B] {
  def fold[C](f: (A, B) => C): C
}

def constructorFun[A,B](a: A, b: B): Product2Fun[A,B] =
  new Product2Fun[A,B] {
    def fold[C](f: (A, B) => C): C = f(a, b)
  }

def ind2fun[A,B]: Product2Ind[A,B] => Product2Fun[A,B] =
  (i: Product2Ind[A,B]) =>
    i match {
      case ConstructorInd(a,b) => constructorFun(a,b)
    }

def fun2ind[A,B]: Product2Fun[A,B] => Product2Ind[A,B] =
  (f: Product2Fun[A,B]) => f.fold[Product2Ind[A,B]](ConstructorInd[A,B] _)

data Product2Ind a b where
  ConstructorInd :: a -> b -> Product2Ind a b

type Product2Fun a b = forall c. (a -> b -> c) -> c

constructorFun :: a -> b -> Product2Fun a b
constructorFun a b f = f a b

ind2fun :: Product2Ind a b -> Product2Fun a b
ind2fun (ConstructorInd a b) = constructorFun a b

fun2ind :: Product2Fun a b -> Product2Ind a b
fun2ind f = f ConstructorInd

Generalization to a product of any number of types

The definition of Product2 above can be adapted to Product_n[A_1, ..., A_n] for any value of n (i.e. 0, 1, 2, 3, 4, …). With n = 0, which means a product of zero types, the constructor takes zero argument, which means it is a constant. Thus Product_0 is equivalent to Unit (i.e. Product_0 ≅ Unit). This is the reason why Unit is sometimes written (). With n = 1, Product_n[A] ≅ A.

Further more for any types A, B and C we have the following properties

• (A , B) is equivalent to (B , A)
• ((A, B), C) and (A, (B, C)) and (A, B, C) are all equivalent
• (Unit, A) and (A, Unit) and A are all equivalent
• (A) is equivalent to A
• (False, A) and (A, False) and False are all equivalent

Exercise: write conversion functions from and tofor each of these equivalence, such that from and to are inverse functions.

Next Episode: CoProducts

In the next episode, we will a convenient way to express alternatives: CoProducts.

Episode 4 - CoProducts

16 Dec 2018 - 1100 Words

CoProducts, often called sum types, discriminated unions or disjoint unions, are a convenient way to express an alternative between different types. The coproduct of n types (with n being 0, 1, 2, etc) A_1, A_2, …, A_n is precisely the type whose values are (i, a_i) where i is a number, called the tag, between 1 and n both included (1 ≤ i ≤ n) and a_i is a value of type A_i (the actual type then depends on the value of i). Is is often written Either[A_1, ..., A_n] in programming and A_1 + ... + A_n in Type Theory.

Let’s take, as an example, n = 4, A_1 = Char, A_2 = Boolean, A_3 = Char and A_4 = Double. The following values are all valid and distinct values of type Either4[Char, Boolean, Char, Double]: (1, 'C'), (2, true), (3, 'D'), (4, 3.2), (3, 'C'). Note that (1, 'C') and (3, 'C') are different values because the tag is different.

Instead of writing the tag explicitly, programming languages often let us write n constructors: Inj_i: A_i => Either_n[A_1, ..., A_n] such that

Note that:

• As usual constructors are injective functions $$\forall i\in{1,\dots,n},\quad \forall a_i,a'_i:\texttt{A}_i,\quad \texttt{Inj}_i(a_i) = \texttt{Inj}_i(a'_i) \Leftrightarrow a_i = a'_i$$
• The only way to get a value of type Either_n[A_1, ... , A_n] is by using one of the constructors $$\forall v:\texttt{Either}_n[\texttt{A}_1,\dots,\texttt{A}_n],\quad \exists! i\in{1,\dots,n},\quad \texttt{Inj}_i(a_i) = v$$
• Two different constructors produce different values (hense the disjoint and discriminated unions) $$\forall i,j\in{1,\dots,n},\quad \forall a_i:\texttt{A}_i,\quad \forall a_j:\texttt{A}_j,\quad \texttt{Inj}_i(a_i) = \texttt{Inj}_j(a_j) \Leftrightarrow i = j \textbf{ and } a_i = a_j$$

For example with n = 2, the coproduct of two types A and B is defined as

sealed abstract class Either2[A,B] {
  def fold[R](inj1: A => R, inj2: B => R): R =
    this match {
      case Inj1(a) => inj1(a)
      case Inj2(b) => inj2(b)
    }
}
final case class Inj1[A,B](value: A) extends Either2[A,B]
final case class Inj2[A,B](value: B) extends Either2[A,B]

Saying the pattern matching above is exhaustive is exactly equivalent to say a value of type Either2[A,B] has to be either Inj1(a) for some a:A or Inj2(b) for some b:B. Requiring that Inj1 and Inj2 produce different values is also mandatory as Eirher2[Error, Result] is often used to model computation that may fail. A failed computation would produce a Inj1(e) with e being the error that occurred while a successful computation would produce a Inj2(r) with r the result of the computation. We want to be able to discriminate these two cases, even when the types Error and Result are the same as it is usually the case when the computation need to compute a string or fail with an error message. Likewise, the injectivity of the constructors is mandatory to be able to the result produced r or the error that occurred e.

Equivalence of inductive and functional forms

Once again any *coproductù can be equivalently expressed as a data type Either_n_Ind[A_1, ..., A_n] and as a function type Either_n_Fun[A_1, ..., A_n] with inverse functions ind2fun and fun2ind converting back and forth types Either_n_Ind[A_1, ..., A_n] and Either_n_Fun[A_1, ..., A_n]. For example with n = 2:

sealed abstract class Either2Ind[A,B]
final case class Inj1_Ind[A,B](value: A) extends Either2Ind[A,B]
final case class Inj2_Ind[A,B](value: B) extends Either2Ind[A,B]

trait Either2Fun[A,B] {
  def fold[R](inj1: A => R, inj2: B => R): R
}

def inj1_fun[A,B]: A => Either2Fun[A,B] =
  (a: A) =>
    new Either2Fun[A,B] {
      def fold[R](inj1: A => R, inj2: B => R): R = inj1(a)
    }

def inj2_fun[A,B]: B => Either2Fun[A,B] =
  (b: B) =>
    new Either2Fun[A,B] {
      def fold[R](inj1: A => R, inj2: B => R): R = inj2(b)
    }

def ind2fun[A,B]: Either2Ind[A,B] => Either2Fun[A,B] =
  (i: Either2Ind[A,B]) =>
    i match {
      case Inj1_Ind(a) => inj1_fun(a)
      case Inj2_Ind(b) => inj2_fun(b)
    }

def fun2ind[A,B]: Either2Fun[A,B] => Either2Ind[A,B] =
  (f: Either2Fun[A,B]) =>
    f.fold[Either2Ind[A,B]](Inj1_Ind[A,B] _, Inj2_Ind[A,B] _)

data Either2Ind a b where
 Inj1_Ind :: a -> Either2Ind a b
 Inj2_Ind :: b -> Either2Ind a b

type Either2Fun a b = forall c. (a -> c) -> (b -> c) -> c

inj1_fun :: a -> Either2Fun a b
inj1_fun a f _ = f a

inj2_fun :: b -> Either2Fun a b
inj2_fun b _ g = g b

ind2fun :: Either2Ind a b -> Either2Fun a b
ind2fun (Inj1_Ind a) = inj1_fun a
ind2fun (Inj2_Ind a) = inj2_fun a

fun2ind :: Either2Fun a b -> Either2Ind a b
fun2ind f = f Inj1_Ind Inj2_Ind

Generalization to a product of any number of types

The definition of Either2 above can be adapted to Either_n[A_1, ..., A_n] for any value of n (i.e. 0, 1, 2, 3, 4, …). With n = 0, which means a coproduct of zero types, there is no constructor, which means it is impossible to build a value of this type. Thus Either_0 is equivalent to False (i.e. Either_0 ≅ False). With n = 1, Either_n[A] ≅ A.

Further more for any types A, B and C we have the following properties

• Either2[A,B] is equivalent to Either2[B,A]
• Either2[Either2[A,B], C] and Either2[A, Either2[B,C]] and Either3[A,B,C] are all equivalent
• Eithr2[False,A] and Either2[A,False] and A are all equivalent
• Either_1[A] is equivalent to A
• (C, Either2[A,B]) is equivalent to Either2[(C,A), (C,B)]

Exercise: write conversion functions from and tofor each of these equivalence, such that from and to are inverse functions.

Remember that in Type Theory, False is written 0, Unit is written 1, the product (A_1, ..., A_n) is written A_1 × ... A_n and the coproduct Either_n[A_1, ..., A_n] is written A_1 + ... + A_n. If we express the above properties using Type Theory notation, we get

• A + B ≅ B + A
• (A + B) + C ≅ A + (B + C) ≅ A + B + C
• 0 + A ≅ A + 0 ≅ A
• C × (A + B) ≅ (C × A) + (C × B)
• 1 × A ≅ A
• 0 × A ≅ A × 0 ≅ 0

Is arithmetic familiar to you? If so such equations should be familiar too. But these times there are not between numbers but between equivalent types. If you ever wonder why Algebraic Data Types are called this way, this should give you some hints.

Next Episode: Recursive Data Types

In the next episode, we will see Recursive Data Types.

Episode 5 - Recursive Data Types

16 Dec 2018 - 2000 Words

We have seen many types but we still don’t know how to represent numbers, lists, trees, free monads, or any type with an infinite number of values. One again we will start by simple examples. Like always, do no skim through them but take the time to develop a deep understanding. If you feel uncomfortable with complex examples, it means you missed something important in the simple ones.

A simple example

We will take as example an encoding of non-negative integers, also called natural numbers, i.e. numbers 0, 1, 2, 3 and so on. There are actually many encodings possible, but we will take a simple encoding known as Peano numbers. Did you ever wonder how natural numbers are built? There can actually be built starting from 0 then adding 1 to 0 to make 1, then adding 1 to 1 to make 2, then adding 1 to 2 to make 3, then adding 1 to 3 to make 4, and so on. Our encoding will mimic this construction. We need two constructors: one of represent 0 and the other to represent the operation of adding 1 to the previous number to make a new one.

Let’s call Nat the type of natural numbers. The first constructor, representing 0 should be a constant of type Nat while the second one, representing the operation of adding 1 should be a function of type Nat => Nat. Remember that constructors need to be injective, but we are lucky, this operation is actually injective. Let call the first constructor Zero:Nat and the second one Succ:Nat => Nat (for successor). This is easy to translate into Scala and Haskell:

sealed abstract class Nat {
  def fold[A](zero: A, succ: A => A): A =
    this match {
      case Zero => zero
      case Succ(p) =>
        val a = p.fold(zero, succ)
        succ(a)
    }
}
final case object Zero         extends Nat
final case class  Succ(n: Nat) extends Nat

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

Note that all the constructors we have seen in the previous episodes took as argument already defined types, but the first argument of Succ is of type Nat, the very same type we are defining. This is the reason why Nat is called a recursive data type: some of its constructors take as arguments values of type Nat itself. As usual:

• constructors are injective
• different constructors produces different value
• every value of type Nat is either a Zero or a Succ(n) for some n:Nat

The problem is, unlike enumerations, products and coproducts where these properties are enough to define their respective type (up to equivalence) without ambiguity. With recursive data types there can be several non-equivalent types for which these three properties hold. For example, the type {0, 1, 2, ...} of natural numbers and {O, 1, 2, ..., ∞} in which we added one special number called infinity such that Succ(∞) = ∞ both have the three properties above. So wee need to add a new constraint, which is that: among all the types for which these properties hold, Nat is taken as the smallest one.

Recursive types have amazing properties. For example the types Nat and Option[Nat] are equivalent! Indeed nat2opt and opt2nat are inverse bijections:

def opt2nat: Option[Nat] => Nat = {
  case Some(n) => Succ(n)
  case None => Zero
}

def nat2opt: Nat => Option[Nat] = {
  case Succ(n) => Some(n)
  case Zero => None
}

opt2nat :: Maybe Nat -> Nat
opt2nat (Just n) = Succ n
opt2nat Nothing  = Zero

nat2opt :: Nat -> Maybe Nat
nat2opt (Succ n) = Just n
nat2opt Zero     = Nothing

It means that Nat ≅ Option[Nat]. Note that Option[T] ≅ Either[Unit, T] ≅ 1 + T in Type Theory notation, so Nat is actually one of the solution of the type equation T ≅ 1 + T. Such an equation means we are looking for types T such that T and Option[T] are equivalent. Regarding Option as a function from types to type, where the type Option[T] is the one obtained by applying the argument T to the function Option, Nat is one of the fixed-point of this function. More precisely, Nat is the least fixed-point of Option.

Let μ: (Type -> Type) -> Type be the operator taking a type function F as argument (written F[_] in Scala and f :: * -> * in haskell) and returning the least fixed-point of F, which is defined as the smallest type T (up to equivalence) which is solution of the equation T ≅ F[T]. To simplify the notations, we may also write μT.F[T] instead of μ(F).

As an example Nat = μ(Option) which we also write Nat = μT.Either[Unit, T] and also Nat = μT.(1 + T).

Another solution to the equation, which is, this time the greatest fixed-point of Option is the type NatInf, representing {0, 1, 2, ..., ∞}, defined as below. It is the biggest type which is solution (up to equivalence) of the equation T ≅ 1 + T. The two inverse functions opt2natInf and natInf2opt proves the equivalence:

trait NatInf {
  def unfold: Option[NatInf]
}

val zero: NatInf =
  new NatInf {
    def unfold: Option[NatInf] = None
  }

def succ(n: NatInf): NatInf =
  new NatInf {
    def unfold: Option[NatInf] = Some(n)
  }
  
val ∞ : NatInf =
  new NatInf {
    def unfold: Option[NatInf] = Some(∞)
  }

def opt2natInf: Option[NatInf] => NatInf = {
  case Some(n) => succ(n)
  case None    => zero
}

def natInf2opt: NatInf => Option[NatInf] =
  (n: NatInf) => n.unfold

newtype NatInf = NatInf { unfold ::  Maybe NatInf }

zero :: NatInf
zero = NatInf Nothing

succ :: NatInf -> NatInf
succ n = NatInf (Just n)

inf :: NatInf
inf = NatInf (Just inf)

opt2natInf :: Maybe NatInf -> NatInf
opt2natInf (Just n) = succ n
opt2natInf Nothing  = zero

natInf2opt :: NatInf -> Maybe NatInf
natInf2opt = unfold

Equivalence of inductive and functional definitions

Nat can be equivalently defined as a data type NatInd as well as a function type NatFun. Inverse bijections ind2fun and fun2ind prove NatInf and NarInd are equivalent:

sealed abstract class NatInd
final case object ZeroInd extends NatInd
final case class  SuccInd(n: NatInd) extends NatInd

trait NatFun {
  def fold[A](zero: A, succ: A => A): A
}

val zeroFun : NatFun =
  new NatFun {
    def fold[A](zero: A, succ: A => A): A = zero
  }

def succFun(n: NatFun) : NatFun =
  new NatFun {
    def fold[A](zero: A, succ: A => A): A = {
      val a = n.fold[A](zero, succ)
      succ(a)
    }
  }

def ind2fun: NatInd => NatFun =
  (i: NatInd) =>
    i match {
      case ZeroInd =>
        zeroFun
      case SuccInd(p) =>
        val n = ind2fun(p)
        succFun(n)
    }

def fun2ind: NatFun => NatInd =
  (n: NatFun) => n.fold[NatInd](ZeroInd, SuccInd(_))

data NatInd where
  ZeroInd :: NatInd
  SuccInd :: NatInd -> NatInd

type NatFun = forall a. a -> (a -> a) -> a

zeroFun :: NatFun
zeroFun z _ = z

succFun :: NatFun -> NatFun
succFun n z s = s (n z s)

ind2fun :: NatInd -> NatFun
ind2fun  ZeroInd    = zeroFun
ind2fun (SuccInd n) = succFun (ind2fun n)

fun2ind :: NatFun -> NatInd
fun2ind n = n ZeroInd SuccInd

Lists

Similarly, given a type A, we want to define the the type of lists whose elements are of type A, written List[A]. Let l:List[A] be a list whose elements are of type A. There are two cases: either the list is empty or it is not. Let’s call the the empty list Nil. If the list is not empty, let head be its first element and tail the rest of the list (i.e. the same list as l but without the first element head). Then tail is also a list of type List[A] and l can be obtained by prepending head to tail. We will write this prepending operation Cons :: (A, List[A]) => List[A] such that l = Cons(head, tail).

Once again we see we have two constructors: Nil of type List[A] and Cons of type (A, List[A]) => List[A]. Besides, these constructors satisfy the usual thee properties:

• constructors are injective
• different constructors produces different value
• every value of type List[A] is either a Nil or a Cons(head, tail) for some head:A and some tail:List[A]

Furthermore List[A] is the smallest type satisfying these properties. It can easily be defined in Scala as

sealed abstract class List[+A] {
  def fold[R](nil: R, cons: (A,R) => R): R =
    this match {
      case Nil => nil
      case Cons(head,tail) =>
        val r = tail.fold[R](nil, cons)
        cons(head, r)
    }
}
final case object Nil extends List[Nothing]
final case class  Cons[+A](head: A, tail: List[A]) extends List[A]

Like any recursive data type, List[A] is the smallest solution of a type equation. This time the equation is T ≅ 1 + (A, T) which in a more Scalaish syntax is T ≅ Option[(A, T)]. Equivalently, List[A] is also the least fixed-point of the type-function:

type F[T] = Option[(A, T)]

Which means List[A] = μT.(1 + A × T). The biggest type which is solution (up to equivalence) of the equation, which is the greatest fixed-point of F is the type of streams whose elements are of type A, written Stream[A]:

trait Steam[A] {
  def unfold: Option[(A, Stream[A])]
}

newtype Stream a = Stream { runStream :: forall c. (Maybe (a, Stream a) -> c) -> c }

Exercise: write the bijections proving Stream[A] ≅ Option[(A, Stream[A])]

Equivalence of inductive and functional definitions

List[A] can equivalently be defined as the data type ListInd[A] as well as the type function ListFun[A]. The two inverse functions ind2fun and fun2ind prove ListInd[A] and ListFun[A] are equivalent:

sealed abstract class ListInd[+A]
final case object NilInd extends ListInd[Nothing]
final case class  ConsInd[+A](head: A, tail: ListInd[A]) extends ListInd[A]

trait ListFun[+A] {
  def fold[R](nil: R, cons: (A,R) => R): R
}

def nilFun[A]: ListFun[A] =
  new ListFun[A] {
    def fold[R](nil: R, cons: (A,R) => R): R = nil
  }

def consFun[A](head: A, tail: ListFun[A]): ListFun[A] =
  new ListFun[A] {
    def fold[R](nil: R, cons: (A,R) => R): R = {
      val r = tail.fold[R](nil, cons)
      cons(head, r)
    }
  }

def ind2fun[A]: ListInd[A] => ListFun[A] =
  (i: ListInd[A]) =>
    i match {
      case NilInd =>
        nilFun[A]
      case ConsInd(head, tail) =>
        val tailFun = ind2fun(tail)
        consFun(head, tailFun)
    }

def fun2ind[A]: ListFun[A] => ListInd[A] =
  (f: ListFun[A]) => f.fold[ListInd[A]](NilInd, ConsInd(_,_))

data ListInd a where
  NilInd  :: ListInd a
  ConsInd :: a -> ListInd a -> ListInd a

type ListFun a = forall r. r -> (a -> r -> r) -> r

nilFun :: ListFun a
nilFun nil _ = nil

consFun :: a -> ListFun a -> ListFun a
consFun head tail nil cons = cons head (tail nil cons)

ind2fun :: ListInd a -> ListFun a
ind2fun  NilInd             = nilFun
ind2fun (ConsInd head tail) = consFun head (ind2fun tail)

fun2ind :: ListFun a -> ListInd a
fun2ind f = f NilInd ConsInd

Algebraic Data Types

Algebraic Data Types are types that can be expressed using only False, Unit, products, coproducts and the least fixed-point operator μ. For example, binary trees whose elements are of type A, defined in Scala by

sealed abstract class Tree[+A] {
  def fold[R](empty: R, leaf: A => R, node: (R, R) => R): R =
    this match {
      case Empty   => empty
      case Leaf(a) => leaf(a)
      case Node(l, r) =>
        val al = l.fold[R](empty, leaf, node)
        val ar = r.fold[R](empty, leaf, node)
        node(al, ar)
    }
}
final case object Empty extends Tree[Nothing]
final case class  Leaf[+A](value: A) extends Tree[A]
final case class  Node[+A](left: Tree[A], right: Tree[A]) extends Tree[A]

can be expressed as the type Tree[A] = μT.(1 + A + (T × T)), which is the smallest type (up to equivalence) solution of the equation T ≅ Either3[Unit, A, (T, T)].

Exercise: write the bijection proving the equivalence.