Skip to content

Instantly share code, notes, and snippets.

@gvolpe
Forked from SystemFw/Ex.scala
Created November 3, 2018 04:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gvolpe/fba7efc41e924bb194e6eaabac309a09 to your computer and use it in GitHub Desktop.
Save gvolpe/fba7efc41e924bb194e6eaabac309a09 to your computer and use it in GitHub Desktop.
Encoding existentials via abstract types (1) and higher-ranks (2)
// 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