Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Proving equality of type constructors in Scala via an "arbitrary object" encoding of universal quantification.
// Universal quantification is encoded in terms of quantifier-free
// assertions about an "abitrary" type (cp. "all swans are white" vs.
// "the arbitrary swan is white". Inspired by Kit Fine's 1985 "Reasoning
// with Arbitrary Objects",
// Possibly also related to Oleg Kiselyov's "Interpreting types as
// abstract values",
// What I wouldn't give for kind-polymorphism here ...
trait Eq1[T[_], U[_]]
trait Eq2[T[_, _], U[_, _]]
trait Arbitrary1
trait Arbitrary2
implicit def eq1[T[_], U[_]]
(implicit ev : T[Arbitrary1] =:= U[Arbitrary1]) = new Eq1[T, U] {}
implicit def eq2[T[_, _], U[_, _]]
(implicit ev : T[Arbitrary1, Arbitrary2] =:= U[Arbitrary1, Arbitrary2]) = new Eq2[T, U] {}
implicitly[Eq1[Option, Option]] // OK
implicitly[Eq1[List, List]] // OK
implicitly[Eq1[Option, List]] // Does not compile
implicitly[Eq2[Map, Map]] // OK
implicitly[Eq2[Tuple2, Tuple2]] // OK
implicitly[Eq2[Map, Tuple2]] // Does not compile
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment