Last active
November 3, 2018 17:41
-
-
Save SystemFw/1ee2621fff9d8f73bb6fda8421a0fbf6 to your computer and use it in GitHub Desktop.
Encoding existentials via abstract types (1) and higher-ranks (2)
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
// This is the traditional encoding, using abstract type members | |
// to encode existentials | |
object AbstractExistentials { | |
trait E { | |
type X | |
val x: X | |
def f(p: X): String | |
} | |
// Calling code, can be unaware of X | |
def exTest(in: E): String = in.f(in.x) | |
val e1 = new E { | |
type X = Int | |
val x = 1 | |
def f(p: Int) = p.toString | |
} | |
val e2 = new E { | |
type X = String | |
val x = "hello" | |
def f(p: String) = p.toUpperCase.toString | |
} | |
val r1 = exTest(e1) // res0: String = 1 | |
val r2 = exTest(e2) // res1: String = HELLO | |
} | |
// This is an encoding which uses the equivalence | |
// exists a. (a, a -> String) <=> forall r. (forall a. (a, a -> String) -> r) -> r | |
// Which is basically CPS. | |
// Note the use of higher rank polymorphism, which we need to simulate with a custom trait. | |
// This is noisy, but allows to encode existential quantification in languages without | |
// abstract type members like Java. | |
object HigherRankExistentials { | |
trait E { | |
def f[R](p: E.HRF[R]): R | |
} | |
object E { | |
trait HRF[R] { | |
def apply[X](x: X, f: X => String): R | |
} | |
} | |
def exTest(in: E): String = in.f { | |
new E.HRF[String] { | |
def apply[X](x: X, f: X => String): String = f(x) | |
} | |
} | |
val e1 = new E { | |
def f[R](p: E.HRF[R]): R = p[Int](1, _.toString) | |
} | |
val e2 = new E { | |
def f[R](p: E.HRF[R]): R = p[String]("hello", _.toUpperCase.toString) | |
} | |
val r1 = exTest(e1) // res3: String = 1 | |
val r2 = exTest(e2) // res4: String = HELLO | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment