Futamura.lagda.md

open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Relation.Binary.PropositionalEquality

Futamura projections

Let us represent programs from inputs I to outputs O as simple functions I → O, and assume we have a specialiser: a program that partially evaluates another program applied to the "static" part of its input.

module Futamura (specialise : ∀ {static dynamic output}
                            → (static × dynamic → output) × static → dynamic → output)
                (Program Input Output : Type)
                where

Further assume that we have an interpreted language with source code type Program, and given types of Inputs and Outputs. An interpreter is a program that turns a Program and an Input into an Output:

Interpreter : Type
Interpreter = Program × Input → Output

Given an interpreter, the first Futamura projection gives us a way to turn a program into a compiled executable, by specialising the interpreter to that program:

module I (interpreter : Interpreter) (program : Program) where
  executable : Input → Output
  executable = specialise (interpreter , program)

Now, notice that our specialiser is itself a program that takes two inputs; regarding program as the dynamic part of that input, we can iterate this process one level higher to get the second Futamura projection: a compiler that turns programs into executables.

Executable : Type
Executable = Input → Output

module II (interpreter : Interpreter) where
  compiler : Program → Executable
  compiler = specialise (specialise , interpreter)

Note that this is not a paradoxical self-application! Making type applications explicit:

  _ : compiler ≡ specialise {Interpreter} {Program} {Executable}
                   (specialise {Program} {Input} {Output} , interpreter)
  _ = refl

Finally, we can iterate this a third time by specialising our specialiser to itself. We get the third Futamura projection: a program that turns interpreters into compilers!

Compiler : Type
Compiler = Program → Executable

module III where
  interpreter→compiler : Interpreter → Compiler
  interpreter→compiler = specialise (specialise , specialise)

Schematically, we've been walking up the type of curry, discharging hypotheses as we go:

_ : (Program × Input → Output) → Program → Input → Output
--                                        [ executable  ]
--                              [        compiler       ]
--  [               interpreter→compiler                ]
_ = curry

By an obvious parametricity argument, the only possible definition for specialise (up to homotopy) is uncurry curry, so this isn't too interesting, but hopefully it illustrates the process for more concrete program representations. In particular, we can interpret this in any cartesian closed category, where specialise might be interpreted as an optimising program transformation.