Last active
May 12, 2016 18:43
-
-
Save raichoo/5371927 to your computer and use it in GitHub Desktop.
Playing with propositional equality in Scala (+inductive proof)
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
import scala.language.higherKinds | |
/* | |
* The usual peano numbers with addtion and multiplication | |
*/ | |
sealed trait Nat { | |
type Plus[N <: Nat] <: Nat | |
type Mult[N <: Nat] <: Nat | |
} | |
sealed trait Z extends Nat { | |
type Plus[N <: Nat] = N | |
type Mult[N <: Nat] = Z | |
} | |
sealed trait S[N <: Nat] extends Nat { | |
type Plus[M <: Nat] = S[N#Plus[M]] | |
type Mult[M <: Nat] = M#Plus[N#Mult[M]] | |
} | |
/* | |
* Equality with an upper bound to tackle subtyping | |
*/ | |
sealed trait Eq[Up, A <: Up, B <: Up] { | |
def cong[F[_ <: Up] <: Up] : Eq[Up, F[A], F[B]] | |
} | |
final case class refl[Up, A <: Up]() extends Eq[Up, A, A] { | |
def cong[F[_ <: Up] <: Up]: Eq[Up, F[A], F[A]] = refl() | |
} | |
/* | |
* Prove that n + 0 = 0 + n | |
*/ | |
sealed trait Plus0[N <: Nat] { | |
type Prop = Eq[Nat, N#Plus[Z], Z#Plus[N]] | |
val proof: Prop | |
} | |
// case: 0 | |
final case object Plus0_0 extends Plus0[Z] { | |
val proof: Prop = refl() | |
} | |
//case: n + 1 | |
final case class Plus0_S[N <: Nat](p: Plus0[N]) extends Plus0[S[N]] { | |
val proof: Prop = p.proof.cong[S] | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
By the way, is it intentional that
Eq
doesn't have the following method (note the absence of the second<: Up
)?Its implementation for
refl
is justPredef.identity
, and thecong
method can be derived from it like so:You probably know this stuff, but I wanted to post it here anyway in case anybody is interested :)
Naturally, scalaz also has this sort of equality :)