Fun with Curry Howard

Tikhon Jelvis (tikhon@jelv.is)

Press → key to advance.
Zoom in/out: Ctrl or Command + +/-

$$ \newcommand{\ty}[1]{\mathbf{#1}} $$ $$ \newcommand{\ite}[3]{\text{if }#1\text{ then }#2\text{ else }#3} $$ $$ \newcommand{\case}[5]{\text{case }#1\text{ of }#2 \to #3 \quad|\ #4 \to #5} $$

1 Curry-Howard

  • correspondence between programming languages and formal logic systems
    • programming language ≡ logic
    • program ≡ proof
  • shows deep relationship between mathematics and programming

2 Why

  • useful for thinking by analogy—a new perspective on programming
  • underlies proof assistants like Coq and Agda
  • useful for practical programming in Haskell and OCaml

3 Basic Idea

  • type ≡ proposition
  • program ≡ proof
  • a type is inhabited if it has at least one element ≡ proposition with proof
  • \(\ty{unit}\) is trivially inhabited: \(()\) —like \(\top\)
  • \(\ty{void}\) is uninhabited: like \(\bot\)
    • Haskell: data Void

4 Comparing Inference Rules: True

  • STLC vs intuitionistic propositional logic
  • true introduction: $$ \frac{}{\quad \top \quad} $$
  • unit type: $$ \frac{}{() : \ty{unit}} $$

5 False

  • no way to introduce false (\(\bot\))
  • similarly, no rule for \(\ty{void}\) !
  • we can “eliminate” false: $$ \frac{\bot}{\quad C \quad} $$
  • this cannot actually happen!

6 Implication Introduction

  • if we can prove \(B\) given \(A\): $$ \frac{A \vdash B}{A \Rightarrow B} $$
  • just like rule for abstractions: $$ \frac{\Gamma, x : \tau \vdash e : \tau'}{\Gamma \vdash (\lambda x:\tau. e) : \tau \to \tau'} $$

7 Implication Elimination

  • $$ \frac{A \Rightarrow B \quad A}{B} $$
  • Just like function application: $$ \frac{\Gamma \vdash e_1 : \tau \to \tau' \quad \Gamma \vdash e_2 : \tau}{\Gamma \vdash e_1 e_2 : \tau'} $$

8 And Introduction

  • $$ \frac{A \quad B}{A \land B}$$
  • just like product type: $$ \frac{\Gamma \vdash e_1 : \tau_1 \quad \Gamma \vdash e_2 : \tau_2}{\Gamma \vdash (e_1, e_2) : \tau_1 \times \tau_2}$$

9 And Elimination

  • $$ \frac{A \land B}{A} \quad \frac{A \land B}{B} $$
  • just like \(\text{first}\) and \(\text{second}\): $$ \frac{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \text{first } e : \tau_1} \quad \frac{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \text{second } e : \tau_2} $$

10 Or Introduction

  • $$ \frac{A}{A \lor B} \quad \frac{B}{A \lor B} $$
  • just like sum type: $$ \frac{\Gamma \vdash e : \tau_1}{\Gamma \vdash \text{left } e : \tau_1 + \tau_2} \frac{\Gamma \vdash e : \tau_2}{\Gamma \vdash \text{right } e : \tau_1 + \tau_2} $$

11 Or Elimination

  • $$ \frac{A \vdash C \quad B \vdash C \quad A \lor B}{C} $$
  • just like pattern matching (case): $$ \frac{\Gamma\ \vdash\ e : \tau_1 + \tau_2 \atop \Gamma,\ x : \tau_1 \ \vdash\ e_1 : \tau' \quad \Gamma,\ y : \tau_2 \ \vdash\ e_2 : \tau'}{\Gamma \vdash (\case{e}{x}{e_1}{y}{e_2}) : \tau'}$$

12 Constructive Logic

  • we did not talk about \(\lnot\) and Curry-Howard
  • functional programming does not generally deal with \(\lnot\)
  • functional programming corresponds to intuitionistic or constructive logic
    • logic system without the law of the excluded middle

    $$ \forall x. x \lor \lnot x $$

13 Negation

  • what does it mean for \(\lnot x\) to be true?

$$ \lnot x \equiv x \Rightarrow \bot $$

  • beacuse only

$$ \bot \Rightarrow \bot $$

  • we can't directly write programs/proofs with this idea

14 Exceptions

  • control flow for handling errors
  • does not play well with proving things! $$ \frac{\Gamma \vdash e : \ty{exn}}{\text{raise } e : \tau} $$
  • we could even have: $$\text{raise } e : \ty{void}$$
  • \(\text{raise}\) does not return to context

15 Catching Exceptions

  • very similar to pattern matching

$$ \frac{\Gamma \vdash e_1 : \tau \quad \Gamma, x : exn \vdash e_2 : \tau}{\Gamma \vdash (\text{try }e_1\text{ with } x \Rightarrow e_2) : \tau} $$

  • error handler and body have the same type
  • exceptions not encoded in type system
  • good example of isolating the design of a language feature

16 Generalizing Exceptions

  • we can generalize exceptions with continuations
  • a continuation is a “snapshot” of the current execution
    • can be resumed multiple times
  • callCC is a very powerful construct for control flow

17 Continuations

  • very versatile
    • exceptions
    • threads
    • coroutines
    • generators
    • backtracking

18 Basic Idea

  • control what happens “next” as a program evaluates
  • the next step (continuation) is reified as a function
  • the continuation is a first class value
    • pass it around
    • call it multiple times—or none
    • be happy

19 Example

$$ \underset{\bullet}{e_1} + e_2 $$

  • split into current value (\(e_1\)) and “continuation”:

$$ \bullet + e_2 $$

  • we could get the continuation as a function:

$$ \lambda x. x + e_2 $$

20 callCC

  • introduce a new primitive for getting current continuation
  • \(\text{callCC}\) —“call with current continuation”
  • continuation as function
    • calling continuation causes \(\text{callCC}\) to return
  • calls a function with a function…
    • “body” function gets “continuation” function as argument

21 callCC Example

$$ \underset{\bullet}{e_1} + e_2 $$

  • get continuation out:

$$ \text{callCC } k \text{ in } body + e_2 $$

  • \(body\) gets \(\bullet + e_2\) as \(k\)
  • original expression doesn't return
  • calling \(k\) is like original expression returning

22 Early Exit

  • we can use continuations to return from an expression early
  • like a hypothetical (return 1) + 10 in a C-like language

$$ \text{callCC } exit \text{ in } (exit\ 1) + 10 $$

  • entire expression evaluates to \(1\)
  • similar to exception handling

23 Types

  • we can think of \(\text{callCC}\) with this type: $$ callCC : ((\tau \to \sigma) \to \tau) \to \tau $$
  • note how \(\sigma\) is never used—it can be anything including \(\bot\)
  • \(((\tau \to \sigma) \to \tau) \to \tau\) implies the law of the excluded middle
  • \(\text{callCC}\) turns our logic into a classical one!

24 Negation Again

  • remember that \(\lnot x \equiv x \Rightarrow \bot\)
  • in \(((\tau \to \sigma) \to \tau) \to \tau\), \(\sigma\) is not used
  • this means \(\sigma\) can be \(\bot\) ! $$ ((\tau \to \bot) \to \tau) \to \tau $$ $$ (\lnot \tau \to \tau) \to \tau $$

25 Peirce's Law

  • \(((\tau \to \sigma) \to \tau) \to \tau\) as an axiom is equivalent to the law of the excluded middle as an axiom
  • \(\text{callCC}\) moves our language from a constructive logic to a classical logic
  • a nice proof of this equivalence
  • side-note: apparently “Peirce” is pronounced more like “purse”

26 Continuation-Passing Style

  • we can emulate \(\text{callCC}\) by cleverly structuring our program
  • every continuation is explicitly represented as a callback
  • this is continuation-passing style (CPS)
  • used in node.js for concurrency (non-blocking operations)
  • normal code can be systematically compiled to CPS

27 CPS Example

$$ add\ x\ y = x + y $$

  • CPS version:

$$ add\ x\ y\ k = k (x + y) $$

  • \(k\) is the continuation—a function to call after finishing
    • \(k\) is the conventional name for “callback” or “continuation”

28 CPS Example Usage

$$ add\ 1\ (add\ 2\ 3) $$

  • CPS-transformed:

$$ add\ 2\ 3\ (\lambda x. add\ 1\ x\ (\lambda y. y)) $$

  • functions never return—call continuation instead
  • access result with a \(\lambda x. x\) continuation
  • \(\text{callCC}\) just gives access to \(k\)

29 Double Negation Translation

  • CPS means we can emulate \(\text{callCC}\)
  • similarly, we can embed classical logic into constructive logic
    • called double negation translation
  • for ever provable proposition \(\phi\) in classical logic, we can prove \(\lnot\lnot\phi\) in constructive logic
    • in constructive logic, \(\phi \equiv \lnot\lnot\phi\) does not necessarily hold

30 Double Negation Translation Intuition

  • \(\lnot\lnot\phi\) is like proving “\(\phi\) does not lead to a contradiction”
  • not a constructive proof for \(\phi\) because we have not constructed an example of \(\phi\)
  • a classical proof can be an example that “\(\phi\) does not lead to a contradiction”

31 Double Negation and CPS

  • CPS transform ≡ double negation
  • remember: \(\lnot x \equiv (x \to \bot)\)
  • for a constant (say \(3\)), the CPS version is:

$$ \lambda k. k (3) $$

  • we go from \(3 : \ty{int}\) to:

$$ ((\ty{int} \to \sigma) \to \sigma) $$

  • \(\sigma\) can be anything

32 Double Negation and CPS

  • same trick as before: take \(\sigma\) to be \(\bot\):

$$ ((\ty{int} \to \bot) \to \bot) $$

  • now translate to \(\lnot\):

$$ (\lnot \ty{int} \to \bot) $$ $$ \lnot (\lnot \ty{int}) $$

  • since CPS doesn't usually use \(\bot\), it's a bit more general

33 Curry-Howard Conclusion

  • programming languages ≡ logic systems
  • programs ≡ proofs
  • functional ≡ intuitionistic
  • imperative ≡ classical
    • “imperative” means exceptions, callCC or similar