Created
May 10, 2019 00:45
-
-
Save Kraks/dea276c7f3e4631e9944d8b36565877e to your computer and use it in GitHub Desktop.
Some types of Futamura projections.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| trait Futamura1 { | |
| // Roughly follow the idea from http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html | |
| type P[_] // program representation type | |
| type M[_] // machine type | |
| /* To run a machine: */ | |
| def run[A](ma: M[A]): A | |
| /* The specializer: a machine that | |
| takes a program representation of A => B, | |
| specializes it wrt a value of A, and | |
| yields a machine of M[B]. | |
| */ | |
| def specializer[A, B]: M[P[A => B] => A => M[B]] | |
| /* The program representation of specializer */ | |
| def specializerProgram[A, B]: P[P[A => B] => A => M[B]] | |
| /* The interpreter: a machine that | |
| takes a program representation of A => B and a value of A, | |
| executes the program, and | |
| yields a value of B. | |
| */ | |
| def interpreter[A, B]: M[P[A => B] => A => B] | |
| def abstractInterpreter[A, B, α[_]]: M[P[A => B] => α[A] => α[B]] | |
| /* The program representation of interpreter */ | |
| def interpreterProgram[A, B]: P[P[A => B] => A => B] | |
| /* Yields executables */ | |
| def firstProjection[A, B](prog: P[A => B]): M[A => B] = | |
| run(specializer[P[A => B], A => B])(interpreterProgram[A, B])(prog) | |
| def specializedSpecializerProgram[A, B]: P[A => B] => M[A => M[B]] = | |
| run(specializer[P[A => B], A => M[B]])(specializerProgram[A, B]) | |
| /* A self-hosting specializer, ie a compiler */ | |
| def secondProjection[A, B]: M[P[A => B] => M[A => B]] = | |
| specializedSpecializerProgram(interpreterProgram[A, B]) | |
| /* A compiler-compiler, converting any interpreter to an equivalent compiler */ | |
| def thirdProjection[A, B]: M[P[A => B] => M[A => M[B]]] = | |
| specializedSpecializerProgram(specializerProgram[A, B]) | |
| /* The fourth projection is a quine */ | |
| def quine[A, B]: M[P[A => B] => M[A => M[B]]] = | |
| run(thirdProjection[P[A => B], A => M[B]])(specializerProgram[A, B]) | |
| } | |
| trait Futamura2 { | |
| // From Matt Brown and Jens Palsberg's POPL '18 paper | |
| type Rep[_] | |
| def unRep[A](x: Rep[A]): A | |
| def toRep[A](x: A): Rep[A] | |
| def mix[A, B]: Rep[A => B] => Rep[A] => Rep[B] | |
| def interp[A, B]: Rep[A => B] => A => B | |
| def compiler[A, B]: Rep[A] => Rep[B] | |
| def first[A, B](prog: Rep[Rep[A => B]]): Rep[A => B] = mix(toRep(interp[A, B]))(prog) | |
| def mixmix[A, B]: Rep[Rep[A => B]] => Rep[Rep[A] => Rep[B]] = mix(toRep(mix)) | |
| def second[A, B]: Rep[Rep[Rep[A => B]] => Rep[A => B]] = mixmix(toRep(toRep(interp[A, B]))) | |
| def third[A, B]: Rep[Rep[Rep[A => B]] => Rep[Rep[A] => Rep[B]]] = mixmix(toRep(toRep(mix[A, B]))) | |
| def fourth[A, B]: Rep[Rep[Rep[A => B]] => Rep[Rep[A] => Rep[B]]] = | |
| unRep(third[Rep[A => B], Rep[A] => Rep[B]])(toRep(toRep(mix[A, B]))) | |
| } | |
| trait Futamura3 { | |
| // From Jones, Gomard, and Sestoft's partial evaluation book | |
| // The difference is the type of mix: the second argument is A (instead of Rep[A] from Brown & Palsberg) | |
| type Rep[_] | |
| def toRep[A](x: A): Rep[A] | |
| def unRep[A](x: Rep[A]): A | |
| def mix[A, B]: Rep[A => B] => A => Rep[B] | |
| def interp[A, B]: Rep[A => B] => A => B | |
| def first[A, B](prog: Rep[A => B]): Rep[A => B] = | |
| mix[Rep[A => B], A => B](toRep(interp[A, B]))(prog) | |
| def mixmix[A, B]: Rep[A => B] => Rep[A => Rep[B]] = mix(toRep(mix[A, B])) | |
| def second[A, B]: Rep[Rep[A => B] => Rep[A => B]] = mixmix(toRep(interp[A, B])) | |
| def third[A, B]: Rep[Rep[A => B] => Rep[A => Rep[B]]] = mixmix(toRep(mix[A, B])) | |
| def fourth[A, B]: Rep[Rep[A => B] => Rep[A => Rep[B]]] = unRep(third[Rep[A => B], A => Rep[B]])(toRep(mix[A, B])) | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment