Created

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist

Proving equality of type constructors in Scala via an "arbitrary object" encoding of universal quantification.

View gist:2659013
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
// 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
Something went wrong with that request. Please try again.