Haskell 中 Futamura 投影的证明

Question

我在The Three Projections of Doctor Futamura 上阅读了 Dan Piponi 的精彩博文。在文章的最后，他有一个附录，其中包含 Haskell 中 Futamura 投影的证明。但是，我发现他的文章缺乏有关所涉及语言的信息。为了使 Futamura 投影起作用，专业化程序的源语言、目标语言和目标语言必须是什么？例如，如果我为 Haskell 的 LLVM 专家写了一个 Haskell，Futamura 预测会起作用吗？如果您像 Dan Piponi 在他的文章中所做的那样编写一个 Haskell 程序来证明这一点，将会很有帮助。

Answer 1

是的，当且仅当专业化程序的源语言和目标语言相同时，Futamura 投影才会起作用。这是因为只有使用与它可以阅读的语言相同的语言编写的专门工具才能应用于它自己。然而，specialized 的目标语言独立于其他两种语言。这具有重要的后果，我将在此答案的后面讨论。

为了证明我的假设，我将引入一个新的符号来松散地描述基于tombstone diagrams 的程序。墓碑图（或 T 图）是编译器和其他相关metaprograms 的图形表示。它们用于说明和推理程序从源语言（T 的左侧）到目标语言（T 的右侧）的转换，如在目标语言（T 的底部）中实现的那样。让我们将 T 型图的想法扩展到适用于所有程序：

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

在元程序的情况下，α 和 β 本身就是程序：

(α → β : ?) × α → β : ? -- 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 语言扩展来隐藏类型级机制，使我们能够专注于所涉及的语言。对自己申请一个specialr也是必要的。

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

另一个值得注意的细节是自托管专用程序与自托管编译器非常相似。如果您的编译器已经执行了部分评估，那么将它变成一个专门器应该不会有太多的工作。这意味着实施 Futamura 预测比最初认为的要容易得多，回报也多得多。我尚未对此进行测试，因此请谨慎对待。