The Futamura projections type-checked by Haskell.

Futamura.hs

{-# LANGUAGE ImpredicativeTypes #-}

module Futamura where

newtype C a = C {runC :: a}
newtype L a = L a
newtype Executable a = Executable {run :: a}

-- Given:
-- - A high level language L
-- - A low level language C
-- - A way to execute programs written in C:
--      C a -> a
-- - A C program that specializes programs written in C:
--      C (C (a -> b) -> a -> Executable b)
-- - A C program that executes programs written in L:
--      C (L a -> a)
-- - An example program in L:
--      L a
-- We can create the following Futamura projections:

-- A function that runs an L program.
futamura0
  :: (forall a b. C (C (a -> b) -> a -> Executable b))
  -> (forall a. C (L a -> a))
  -> L a
  -> a
futamura0 _cSpecializeC cInterpretL lExample = runC cInterpretL lExample

-- A function that compiles an L program.
futamura1
  :: (forall a b. C (C (a -> b) -> a -> Executable b))
  -> (forall a. C (L a -> a))
  -> L a
  -> Executable a
futamura1 cSpecializeC cInterpretL lExample = runC cSpecializeC cInterpretL lExample

-- A function that creates an L compiler.
futamura2
  :: (forall a b. C (C (a -> b) -> a -> Executable b))
  -> (forall a. C (L a -> a))
  -> Executable (L a -> Executable a)
futamura2 cSpecializeC cInterpretL = runC cSpecializeC cSpecializeC cInterpretL

-- A function that creates an interpreter to compiler converter.
futamura3
  :: (forall a b. C (C (a -> b) -> a -> Executable b))
  -> Executable (C (L a -> a) -> Executable (L a -> Executable a))
futamura3 cSpecializeC = runC cSpecializeC cSpecializeC cSpecializeC

-- Compare the type of the specializer with how each projection uses it:
-- specializer:          C (      C (  a -> b)  ->               a -> Executable b )
-- ->futamura0:             (∀ a. C (L a -> a)) ->             L a ->            a
-- ->futamura1:             (∀ a. C (L a -> a)) ->             L a -> Executable a
-- ->futamura2:             (∀ a. C (L a -> a)) -> Executable (L a -> Executable a)
-- ->futamura3: Executable (      C (L a -> a)  -> Executable (L a -> Executable a))
-- With each extra specialize, the final argument of the previous projection is
-- accepted by a generated Executable instead.