Skip to content
Create a gist now

Instantly share code, notes, and snippets.

Embed URL


Subversion checkout URL

You can clone with
Download ZIP
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
Something went wrong with that request. Please try again.