posts :: kangaroo courts & existential packing

(* Kangaroo Courts & Existential Packing *)

As a reasonable adult, you probably don't believe in elves. What's a surefire way of convincing you that elves are real? If I walked up to you — squiggly creatures in hand and no deceitful contraption in sight — would that be enough? 1 1 Proof by construction.

This post is meant to be an accessible rehash of §2.1 of Will Crichton's paper "Typed Design Patterns for the Functional Era". I urge you to read that paper for more typed patterns :)

Assume for a moment that elves are real and they are magical creatures that always tell the truth. Philosophical conundrums notwithstanding, it means that if you were unlucky enough to be spotted by an elf while you were stealing cookies you are going straight to jail.

Let's code up such a system! In this hypothetical world, there are only a few kinds of testimonies that anyone can establish: they saw or heard you in the act; they can vouch for your character or they have you on camera. 2

2 If you don't know OCaml syntax, this means that an evidence is a value with three possible cases and the 'a parameter refers to the type of any data that each case may contain. You can look up sum types. 

type 'a evidence =
  | Eyewitness
  | Character of bool
  | Video of Bytes.t

Now, all testimonies are not created equal. We know that the word of an elf is infallible.


type 'a testimony =
  | Human of 'a evidence
  | Elf of 'a evidence

Armed with these two types and a deus ex machina that determines whether the video evidence is legit or not, we can construct a function to determine if you are absolutely guilty. 3

3 If you don't know OCaml syntax, we are pattern matching on the structure of a testimony and defining what to do in each case. 

let guilty : 'a testimony -> bool =
  fun w -> match w with
  | Human (Character _) | Elf (Character _) -> false
  | Human Eyewitness -> false
  | Elf Eyewitness -> true
  | Human (Video b) | Elf (Video b) -> discern_video b

The process of jailing someone for sugary crimes is a messy business though. You might have dozens of functions that go through the necessary bureaucracy and you need to make sure at every step of the way that you have the right person.4 For example, you might want to remove the toys from their rooms ...

4 Or else, you might relive my childhood nightmare "I'm not Martin" by R.L Stine. 

let remove_toys (p : perpetrator) = remove (find_room p)

But this function does not check if our perpetrator is actually guilty. You can imagine a scheming sibling backdooring the judicial process by calling this function willy-nilly. Or more realistically, you make a mistake while you're coding up your system and forget to check some invariant. Maybe it's expensive to verify the invariants constantly, yet you still want to statically ensure that you do not call the wrong code at the wrong time.

In which case, let's reframe these functions and pretend that they are skeptical — they don't believe that the person is guilty, but you can convince them by presenting undeniable proof. So, let's modify our functions ... 5

5 proof is a type with a single case. 

type proof = Exists

let guilty : 'a testimony -> proof option =
  fun w ->
  match w with
  | Human (Character _) | Elf (Character _) -> None
  | Human Eyewitness -> None
  | Elf Eyewitness -> Some Exists
  | Human (Video b) | Elf (Video b) -> discern_video b

let remove_toys (_proof : proof) (p : perpetrator) = remove (find_room p)

Our incarceration apparatus now requires a proof value to be supplied and the only way to get a proof is to call our guilty function. 


let w = Elf Eyewitness

(* Ideally ... *)
let () = match (guilty w) with
  | Some p -> remove_toys p "Jamie"
  | None -> release ()

Except we can always just use an escape hatch and call the function directly, haha!


let () = remove_toys Exists "Jamie"

The problem here is that we have more information than we are supposed to. We know that our functions are gatekept by this proof type and we know how to construct one directly. The solution is to keep this information away, or keep it abstract as they say, by wrapping it in a module and specifying its signature.6

6 The sig part defines the interface of the module and the struct part is the implementation. 

module Proof : sig
  type t

  val guilty : 'a testimony -> t option
end = struct
  type t = Exists

  let guilty : 'a testimony -> t option =
    fun w ->
    match w with
    | Human (Character _) | Elf (Character _) -> None
    | Human Eyewitness -> None
    | Elf Eyewitness -> Some Exists
    | Human (Video b) | Elf (Video b) -> discern_video b
end

When you use this module, all you know is that there exists some type t and that there is a function that constructs t options from testimonies called guilty. When you implement this module you associate this "existence" with a concrete value, but as a user you can't access this information. Now, functions that accept this Proof.t don't actually care about the internals of the value but the fact that you can produce one — in a similar vein to how you did not care about how I brought an elf to our meeting, only that they are in the flesh. 


(* This function now requires you to present a Proof.t value when you call it. *)
let remove_toys (_proof : Proof.t) (p : perpetrator) = remove (find_room p)

(*  Proof.t has no constructor and you can't convince the compiler
    that it has a case called Exists. Backdoor doesn't work! *)
let () = remove_toys Proof.Exists "Jamie"

(*  But if I follow the treaded path and create a proper proof value, then I
    can proceed. *)
let () =
  let t = Elf Eyewintess in
  let po = Proof.guilty person in
  match po with
    | Some p -> remove_toys p "Jamie"
    | None -> Format.printf "not guilty!\n"

The fact that you cannot peer into the module and see how it works is precisely that which prevents you from creating fake testimonies and bypassing the safeguards that you put in place to begin with. Most importantly, you can rest assured within the body of the function that the suspect is guilty and go ham!

In summary,

  1. There is an operation that should only be performed under certain conditions.
  2. You define a structure that can only be minted by verifying these conditions.
  3. The operation takes this structure as a required parameter so you statically ensure you never call this function without verification.

(*** References ***)