Haskell 中的 Futamura 投影的证明

我读了 Dan Piponi 的优秀博客文章二村博士的三个投影 http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html。在文章的最后，他有一个附录，其中包含 Haskell 中 Futamura 投影的证明。然而，我发现他的文章缺乏有关所涉及语言的信息。为了让 Futamura 投影发挥作用，专家的源语言、目标语言和对象语言必须是什么？例如，如果我用 Haskell 编写一个 Haskell 到 LLVM 专用程序，Futamura 投影会起作用吗？如果您像 Dan Piponi 在他的文章中所做的那样编写一个 Haskell 程序来证明这一点，将会很有帮助。

是的，当且仅当专门化器的源语言和目标语言相同时，二村投影才会起作用。这是因为，如果专用化器是用它可以读取的相同语言编写的，则它只能应用于其自身。然而，专家的目标语言独立于其他两种语言。这会产生重要的后果，我将在本答案后面讨论。

为了证明我的假设，我将引入一种新的符号来松散地描述基于墓碑图 https://en.wikipedia.org/wiki/Tombstone_diagram。墓碑图（或 T 图）是编译器和其他相关的图形表示元程序 https://en.wikipedia.org/wiki/Metaprogramming。它们用于说明和推理以对象语言（T 底部）实现的程序从源语言（T 左侧）到目标语言（T 右侧）的转换。让我们将 T 图的想法扩展到适用于所有程序：

α → β : ℒ -- A program is a function from α to β as implemented in language ℒ.

对于元程序α and β本身就是程序：

(α → β : ????) × α → β : ???? -- An interpreter for language ???? as implemented in ????.
(α → β : ????) → (α → β : ????) : ???? -- A compiler from ???? to ???? as implemented in ????.
(ι × α → β : ????) × ι → (α → β : ????) : ???? -- A self-hosting specializer from ???? to ????.
(ι × α → β : ????) → (ι → (α → β : ????) : ????) : ???? -- A compiler compiler from ???? to ????.

这种表示法可以直接转换为 Haskell 中的类型定义。有了这个，我们现在可以用 Haskell 编写关于语言的 Futamura 投影的证明：

{-# LANGUAGE RankNTypes #-}

module Futamura where

newtype Program a b language = Program { runProgram :: a -> b }

type Interpreter source object = forall a b.       Program (Program a b source, a) b object
type Compiler    source target = forall a b.       Program (Program a b source) (Program a b target) target
type Specializer source target = forall input a b. Program (Program (input, a) b source, input) (Program a b target) source
type Partializer source target = forall input a b. Program (Program (input, a) b source) (Program input (Program a b target) target) target

projection1 :: Specializer object target -> Interpreter source object -> Program a b source -> Program a b target
projection1 specializer interpreter program = runProgram specializer (interpreter, program)

projection2 :: Specializer object target -> Interpreter source object -> Compiler source target
projection2 specializer interpreter = runProgram specializer (specializer, interpreter)

projection3 :: Specializer source target -> Partializer source target
projection3 specializer = runProgram specializer (specializer, specializer)

我们使用RankNTypes语言扩展隐藏类型级机制，使我们能够专注于所涉及的语言。对自身应用专门化器也是必要的。

在上面的程序中，第二个投影特别令人感兴趣。它告诉我们，给定一个自托管 Haskell 到 LLVM 专用程序，我们可以将其应用于用 Haskell 编写的任何源语言 ???? 的解释器，以获得 ???? 到 LLVM 编译器。这意味着我们可以用高级语言编写解释器，并使用它生成针对低级语言的编译器。如果专门化器有任何好处，那么生成的编译器也会相当不错。

另一个值得注意的细节是自托管专用程序与自托管编译器非常相似。如果您的编译器已经执行部分评估，那么将其转变为专用器应该不需要太多工作。这意味着实施二村预测比最初认为的要容易得多，回报也大得多。我还没有对此进行过测试，所以请持保留态度。