Skip to content

Instantly share code, notes, and snippets.

@paulp

paulp/Leibniz.scala

Last active August 29, 2015 14:02
Show Gist options
  • Save paulp/d7f705653bdb6985d4bc to your computer and use it in GitHub Desktop.
Save paulp/d7f705653bdb6985d4bc to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. paulp revised this gist Jun 2, 2014. 1 changed file with 14 additions and 6 deletions.
    20 changes: 14 additions & 6 deletions Leibniz.scala
    View file
    Original file line number Diff line number Diff line change
    @@ -24,10 +24,7 @@ class Refl[F <: Foo with Singleton](val z: F) extends FooEqual[F, F] {
    }

    object Leibniz {
    def compare(x: Foo, y: Foo): Option[FooEqual[x.type, y.type]] = if (x == y) {
    // XXXXXXXX: can you get rid of this cast? Pretty sure that if you can, it won't involve a boolean!
    Some(new Refl[x.type](x).asInstanceOf[FooEqual[x.type, y.type]])
    } else None
    def equate(x: Foo)(y: x.type): Option[FooEqual[x.type, y.type]] = Some(new Refl[x.type](x))

    case class FooA(x: Int) extends Foo {
    case class Bar() extends BarT { def zomg = s"zomgA $x" }
    @@ -49,10 +46,21 @@ object Leibniz {
    val b = x.newBar
    val c = y.newBar

    val Some(foo) = compare(x, z)
    // With a type ascription we get this lovely error message:
    // ./a.scala:55: error: type mismatch;
    // found : Option[FooEqual[x.type,z.type]]
    // required: Option[FooEqual[x.type,z.type]]
    // case z: x.type => equate(x)(z)
    // ^
    // one error found
    val compared = z match {
    case z: x.type => equate(x)(z)
    case _ => None
    }
    val Some(foo) = compared
    val bar = foo(a)
    println(a.zomg)
    println(bar.zomg)
    println(c.zomg)
    }
    }
    }
  2. @copumpkin copumpkin created this gist Jun 2, 2014.
    58 changes: 58 additions & 0 deletions Leibniz.scala
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,58 @@
    abstract class Foo {
    trait BarT { this: Bar => def zomg: String }
    type Bar <: BarT

    def newBar: Bar
    }

    // Or not sealed if you reject axiom K? :)
    sealed abstract class FooEqual[X <: Foo, Y <: Foo] {
    val x: X
    val y: Y

    def subst[F[_]](fx: F[x.Bar]): F[y.Bar]

    private type Id[A] = A
    def apply(fx: x.Bar): y.Bar = subst[Id](fx)
    }

    class Refl[F <: Foo with Singleton](val z: F) extends FooEqual[F, F] {
    val x: z.type = z
    val y: z.type = z

    def subst[F[_]](fx: F[z.Bar]): F[z.Bar] = fx
    }

    object Leibniz {
    def compare(x: Foo, y: Foo): Option[FooEqual[x.type, y.type]] = if (x == y) {
    // XXXXXXXX: can you get rid of this cast? Pretty sure that if you can, it won't involve a boolean!
    Some(new Refl[x.type](x).asInstanceOf[FooEqual[x.type, y.type]])
    } else None

    case class FooA(x: Int) extends Foo {
    case class Bar() extends BarT { def zomg = s"zomgA $x" }
    def newBar: Bar = Bar()
    }

    case class FooB(x: String) extends Foo {
    case class Bar(i: Int) extends BarT { def zomg = s"zomgB $i $x" }
    def newBar: Bar = Bar(5)
    }


    def main(args: Array[String]) {
    val x = FooA(5)
    val y = FooB("ahaha")
    val z = FooA(5)

    val a = x.newBar
    val b = x.newBar
    val c = y.newBar

    val Some(foo) = compare(x, z)
    val bar = foo(a)
    println(a.zomg)
    println(bar.zomg)
    println(c.zomg)
    }
    }