Haskell中Futamura投影的证据

问题描述：

我读过Dan Piponi在The Three Projections of Doctor Futamura上的优秀博客文章。在文章结尾处，他有一个附录，其中有Haskell中Futamura预测的证据。但是，我发现他的文章缺乏有关涉及语言的信息。为了使Futamura预测能够工作，专业人员必须具备哪些源语言，目标语言和对象语言？例如，如果我在Haskell中编写了一个Haskell到LLVM专家，那么Futamura预测会工作吗？如果你写了一个Haskell程序来证明这一点，就像Dan Piponi在他的文章中所做的那样，这将会很有帮助。Haskell中Futamura投影的证据

答

是的，当且仅当专家的源语言和对象语言相同时，Futamura投影才能工作。这是因为专家只能使用它可以读取的相同语言编写。但是，专业人员的目标语言是独立于其他两个人的。这具有重要的后果，我将在稍后的答案中讨论。

为了证明我的假设，我将引入一个新的表示法来基于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的二村突出的证明相对于语言：

{-# 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编译器的源语言。这意味着我们可以用高级语言编写解释器，并使用它来生成一个针对低级语言的编译器。如果专家有什么用处，那么生成的编译器也会很好。

另一个值得注意的细节是自托管专家与自承载编译器非常相似。如果您的编译器已经执行了部分评估，那么将其转换为专门工具不应该太多。这意味着实施Futamura预测比原先认为的要容易得多，收益也大得多。我还没有测试过这个，所以拿着一粒盐。

Haskell中Futamura投影的证据

相关推荐