Я прочитал Дэн Пипони отличный пост в блоге на Три прогноза доктора Футамуры. К концу статьи у него есть приложение с доказательством прогнозов Futamura в Haskell. Тем не менее, я считаю, что в его статье отсутствует информация о языках. Какими должны быть исходные, целевые и объектные языки специалиста для того, чтобы проекции Futamura работали? Например, будут ли проекции Futamura работать, если я напишу Haskell специалисту LLVM в Haskell? Было бы полезно, если бы вы написали программу Haskell, чтобы доказать это, как это сделал Дэн Пипони в своей статье.
Доказательство прогнозов Futamura в Haskell
Ответ 1
Да, прогнозы Futamura будут работать тогда и только тогда, когда исходный и предметный языки специалиста одинаковы. Это связано с тем, что специалист может применяться только к себе, если он написан на том же языке, который он может читать. Однако целевой язык специалиста не зависит от двух других. Это имеет важные последствия, о которых я расскажу позже в этом ответе.
Чтобы доказать свою гипотезу, я представлю новую нотацию для описания программ на основе метапрограмм. Они используются для иллюстрации и обоснования преобразования программы с исходного языка (слева от 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 относительно языков:
{-# 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 намного проще и намного более выгодна, чем первоначально предполагалось. Я еще не проверял это, поэтому возьмите его с солью.