TDD, as in
Type-Directed Development

I'm online!

λ

Example time

Example time

GET /endpoint?number=5

10

def addFiveAction(
    params: Map[String, String]
) = {

    val nbS = params("number")
    if(nbS != "") {
        val nb = nbS.toInt
        nb + 5
    } else {
        0
    }
}

addFiveAction(Map("number" -> "12"));
    // 17

addFiveAction(Map("yolo" -> "12"));
    // java.lang.NullPointerException

addFiveAction(Map("number" -> "yolo"));
    // java.lang.NumberFormatException

Pokemon Driven Development


def addFiveAction(
  params: Map[String, String]) = {
    val nbS = params("number")

    if(nbS != null) {
        if(!nbS != "") {
            try {
                val nb = nbS.toInt
                nb + 5
            } catch {
                case e: NumberFormatException e => 0
            }
        }
    } else {
        0
    }
}

De plous en plous difficile

GET /endpoint?n1=20&n2=22

42

def addNumbersAction(
  params: Map[String, String]) = {
    val nbS1 = params("n1");
    val nbS2 = params("n2");

    if(nbS1 != null) {
        if(!nbS1 != "") {
            try {
                val nb1 = nbS1.toInt
                if(nbS2 != null) {
                    if(!nbS2 != "") {
                        try {
                            val nb2 = nbS2.toInt
                            nbS1 + nbS2
                        } catch {
                            case e: NumberFormatException => 0
                        }
                    }
                }
            } catch {
                case e: NumberFormatException => 0
            }
        }
    } else {
        0
    }
}

Hard to read, easy to get wrong, information lost. The code's structure si not correlated to the problem structure anymore. accidental complexity

Thinking with types

Encode that information in the type system

From a map, I can get a value…

maybe

def getKeyAt(
  values: Map[String, String],
  key: String
): MaybeString

from a string, I can get an int…

maybe

def parseInt(
  string: String
): MaybeInt

Aka maybe, optional

def parseInt(str: String):
  Option[Int]

map[A,B]#get(key: A): Option[B]
def getInt(
    index: String,
    vals: Map[String, String]
): Option[Int]

Chain the computations, fail if one fails: sequentiality

def addNumbersAction(
  params: Map[String, String]
): Int = {
    val i1 = getInt("n1", params)
    val i2 = getInt("n2", params)
    i1.getOrElse(0) + i2.getOrElse(0)
}

We can change the default data injection point, and the types will change


def addNumbersAction(
  params: Map[String, String]) = {
    val nbS1 = params("n1");
    val nbS2 = params("n2");

    if(nbS1 != null) {
        if(!nbS1 != "") {
            try {
                val nb1 = nbS1.toInt
                if(nbS2 != null) {
                    if(!nbS2 != "") {
                        try {
                            val nb2 = nbS2.toInt
                            nbS1 + nbS2
                        } catch {
                            case e: NumberFormatException => 0
                        }
                    }
                }
            } catch {
                case e: NumberFormatException => 0
            }
        }
    } else {
        0
    }
}

Correct

by construction

Impossible to express an incorrect program.

Why not tests?

Not the real question

Why not only tests?

∃

« there exists »

tests show the presence of bugs, not their absence

Int -> Int

232

if the code is deterministic

264

if the code is deterministic

String -> String

∞

if the code is deterministic

∀

« for all »

Type ⇔ Property

Program ⇔ Proof



provably > probably

not necessarily a formal proof (expensive), but it's doable and the program has the same structure as the proof

Expressive type systems

not necessarily a formal proof (expensive), but it's doable and the program has the same structure as the proof

Typed control strucures

Everything is an expression

homogeneous branches

val myValue = if(expression) {
  "if true"
} else {
  "if false"
}

Typed control structures

val myValue =
  for(x <- xs)
  yield x*x

Maybe

NonEmptyList

list guaranteed to have at least one element

newtype + smart constructor

email / string. No runtime cost. Gateway when you construct value

Tagged types

perfect for physical quantities. Type + unit

sealed trait Meter
sealed trait Mile

type RegularLength = Int @@ Meter
type ImperialGobbledygook = Int @@ Mile


val marsProbeAltitude: RegularLength = …

Memory management

Rust's lifetimes

Resource management

A GC can't handle that

Parametricity

Parametricity
(aka generics)

Most important feature in a type system. I don't take seriously languages with static types and no parametricity

Ignorance is bliss

Prevents you from assuming too much. You can only use the properties you've explicitely asked for

Parametricity

def f[A](x: A): A

Assuming it returns a value and doesn't crash or do stupid things, it can only return its argument: no way to construct an A

Parametricity

def compose[A,B,C](
    g: (B => C),
    f: (A => B)
): (A => C)

only way to get a C is to apply g to a B, only way to get a B is to apply f to an A, which you have.

Parametricity

def rev[A](xs: List[A]): List[A]

types aren't always once-inhabited, but they still prove interesting things and reduce dramatically the number of tests needed

rev(Nil)
==
Nil

you can't create As out of thin air, so nil -> nil

x in rev(a) => x in a

Theorems for free

trait List[A] {
    def filter(p: A => Boolean): List[A]

    def map[B](f: A => B): List[B]
}

l.filter(compose(p,f)).map(f) ==
l.map(f).filter(p)

mathematical proof of that equality. No test needed

Discipline

no nulls

type ⇔ property

proof ⇔ program

null can inhabit any type

null can prove any property

no reflection

reflection breaks blissful ignorance

Reflection

def f[A](x: A): String
def f[A](x: A): String =

x match {
  case v: String => v
  case v: Int => "int"
  case _ => "whatever"
}

toString / equals / hashCode

same as reflection: breaks ignorance by giving behaviour to all types

def f[A](x: A): String =
x.toString

no exceptions

same as null: bottom

Side effects

def f[A](x: A): String = {
  launchBallisticMissile()

  System.getenv("JAVA_HOME")
}

side effects not encoded in types => hidden information. Includes unrestricted mutability

Fast and loose reasoning is morally correct

Let's program in a safe subset. It's ok to do so even though it isn't enforced by the compiler

Type-Directed Development

Not a silver bullet

types can't always prove everything

Just helpful

but they bring a lot

Confidence

Big Refactoring

Dependencies update

Play Framework

minor version but changes in the streaming layer, which I used extensively

Scalaz 6.x -> 7.x

major bump, whole different architecture, type changes

DB access library

It typechecks, ship it

4 evenings / nights of mindless refactoring. When it compiled, it was ok (I also ran tests to be sure, though)

Modular thinking

Properties are enforced at the boundaries, you can safely ignore the rest of the world when working on a function

Not just about safety

often the first argument but imo not the most important

Types lay out algorithms

just as TDD is important for design

Ensure consistency,
step by step



def myMethod(a: Input): Output = ???

def myOtherMethod(
  a: List[Input]
): List[Output] = {

  a.map(myMethod)

}

Type check /= compilation

Hole-Driven-Development

step by step, compiler assisted code writing


case object Hole

def compose[A,B,C](
    g: (B => C),
    f: (A => B)
): (A => C) = Hole

Hole: A => C

def compose[A,B,C](
    g: (B => C),
    f: (A => B)
): (A => C) = (x: A) => Hole

x: A
Hole: C

def compose[A,B,C](
    g: (B => C),
    f: (A => B)
): (A => C) = (x: A) => g(Hole)

X: A
Hole: B

def compose[A,B,C](
    g: (B => C),
    f: (A => B)
): (A => C) = (x: A) => g(f(Hole))

x: A
Hole: A
Hole = x

def compose[A,B,C](
    g: (B => C),
    f: (A => B)
): (A => C) = (x: A) => g(f(x))

def fmap[A,B](
    f: (A => B),
    xs: List[A]
): List[B] = Hole

Hole: List[B]

def fmap[A,B](
    f: (A => B),
    xs: List[A]
): List[B] = xs match {
    case Nil => Nil
    case (head :: tail) =>
        Hole1 :: Hole2
}

head: A, tail: List[A]
Hole1: B, Hole2: List[B]

def fmap[A,B](
    f: (A => B),
    xs: List[A]
): List[B] = xs match {
    case Nil => Nil
    case (head :: tail) =>
        f(head) :: fmap(f, tail)
}

Test-Driven Development

Type-Driven Development

Types make communication easy

With machines

obvious

Type checking

Tooling

Haskell type syntax

a -> a

Int -> Int

a -> b -> a

function which takes an a and a b, produces an a

(a, b) -> a

function which takes an a and a b, produces an a

a -> (b -> a)

currying. function which takes an a, produces a function that takes a b, produces an a. allows for very effective composition

(Ord a) =>
[a] -> [a]

The only thing we know about a is that it has a total order

Intent

Hoogle <3 <3

http://www.haskell.org/hoogle

Remove duplicates

Eq a =>
[a] -> [a]

[Maybe a] ->
Maybe [a]

With humans

I use types when I program in javascript. I'm just not helped by a compiler

Types can't always prove everything

And that's ok


def reverse[A](
    xs: List[A]
): List[A]

How many tests do i have to write to completely specify its behaviour?


def reverseProp[A: Equal](
  xs: List[A],
  ys: List[A]
) = {

    reverse(xs ++ ys) ==
    reverse(ys) ++ reverse(xs)
}

Property-based reasoning

Perfect for edge cases

Test the specification

used by John Hugues to assess the consistency of norms in embeded systems for cars

Types then

Property-based tests then

Unit tests

Lay out the function types

Write property-based tests

Operations on a type + Laws

Algebra

Figure out the data structure

Implement

Unit test for regressions

???

Profit

Types are

Safety feature

High level reasoning tool

Communication tool

Let's use them

Read this

Read this

Read this

Read this

Dependent types

Try Idris

Try Idris

Thanks

devoxxroxx