Tak, prognozy Futamury zadziałają wtedy i tylko wtedy, gdy języki źródłowe i obiektowe specjalisty będą takie same. Wynika to z faktu, że specjalisty można zastosować tylko do niego samego, jeśli jest napisany w tym samym języku, w którym może czytać. Jednak język docelowy specjalisty jest niezależny od dwóch pozostałych. Ma to ważne konsekwencje, które omówię później w tej odpowiedzi.
Aby udowodnić moją hipotezę, wprowadzę nową notację opisującą programy luźno oparte na tombstone diagrams. Schemat nagrobka (lub T-diagram) jest obrazowym przedstawieniem kompilatorów i innych związanych z nimi metaprograms. Służą one do zilustrowania i uzasadnienia transformacji programu z języka źródłowego (z lewej strony T) na język docelowy (prawo T) jako zaimplementowany w języku obiektowym (dół T). Załóżmy rozszerzyć ideę T diagramów do pracy dla wszystkich programów:
α → β : ℒ -- A program is a function from α to β as implemented in language ℒ.
W przypadku metaprograms α i β same są programy:
(α → β :) × α → β : -- 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 .
Ten zapis może być bezpośrednio przekształcony w definicji typu w Haskell. Uzbrojeni w to, możemy teraz napisać dowód występów Futamura w Haskell w odniesieniu do języków:
{-# 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)
Używamy przedłużenie RankNTypes język ukryć maszyn typu poziomu, co pozwala nam skoncentrować się na językach zaangażowanych . Konieczne jest również zastosowanie do siebie specjalisty.
W powyższym programie druga projekcja ma szczególne znaczenie. Mówi nam, że biorąc pod uwagę self-hosting Haskella do specjalisty LLVM, możemy zastosować go do dowolnego interpretera napisanego w Haskell dla jakiegoś języka źródłowego, aby dostać się do kompilatora LLVM. Oznacza to, że możemy napisać interpreter w języku wysokiego poziomu i użyć go do wygenerowania kompilatora, którego celem jest język niskiego poziomu. Jeśli specjalista jest dobry, wygenerowany kompilator byłby przyzwoicie dobry.
Innym wartym odnotowania szczegółem jest to, że self-hosting specjalista jest bardzo podobny do self-hosting kompilator. Jeśli twój kompilator wykonuje już częściową ocenę, to nie powinno to być zbyt wielkim wysiłkiem, aby przekształcić go w specjalistę. Oznacza to, że wdrożenie projekcji Futamura jest o wiele łatwiejsze i dużo bardziej satysfakcjonujące niż pierwotnie sądzono. Jeszcze tego nie przetestowałem, więc weź to z przymrużeniem oka.