Skip to content

Instantly share code, notes, and snippets.

@milessabin
Created May 11, 2012 11:08
Show Gist options
  • Save milessabin/2659013 to your computer and use it in GitHub Desktop.
Save milessabin/2659013 to your computer and use it in GitHub Desktop.
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", http://philosophy.fas.nyu.edu/object/kitfine.
//
// Possibly also related to Oleg Kiselyov's "Interpreting types as
// abstract values", http://okmij.org/ftp/Computation/index.html#teval.
// 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