-
-
Save gvolpe/fba7efc41e924bb194e6eaabac309a09 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 or Rust. | |
object HigherRankExistentials { | |
trait E { | |
def f(p: E.HRF): String | |
} | |
object E { | |
trait HRF { | |
def apply[X](x: X, f: X => String): String | |
} | |
} | |
def exTest(in: E): String = in.f { | |
new E.HRF { | |
def apply[X](x: X, f: X => String): String = f(x) | |
} | |
} | |
val e1 = new E { | |
def f(p: E.HRF): String = p[Int](1, _.toString) | |
} | |
val e2 = new E { | |
def f(p: E.HRF): String = 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