Type Level Programming: Equality

18 06 2010

Apocalisp has a great series on Type Level Programming with Scala. At some point the question came up whether it is possible to determine equality of types at run time by having the compiler generate types representing true and false respectively. Here is what I came up with.

trait True { type t = True }
trait False { type t = False }

case class Equality[A] {
  def check(x: A)(implicit t: True) = t
  def check[B](x: B)(implicit f: False) = f
object Equality {
  def witness[T] = null.asInstanceOf[T]
  implicit val t: True = null
  implicit val f: False = null

// Usage:
import Equality._
val test1 = Equality[List[Boolean]] check witness[List[Boolean]]
implicitly[test1.t =:= True]
// Does not compile since tt is True
// implicitly[test1.t =:= False]  

val test2 = Equality[Nothing] check witness[AnyRef]
// Does not compile since ft is False
// implicitly[test2.t =:= True]  
implicitly[test2.t =:= False]

Admittedly this is very hacky. For the time being I don’t see how to further clean this up. Anyone?



5 responses

18 06 2010
Tweets that mention Type Level Programming: Equality « Michid’s Weblog -- Topsy.com

[…] This post was mentioned on Twitter by Planet Scala, Planet Lang. Planet Lang said: [Scala] Type Level Programming: Equality: Apocalisp has a great series on Type Level Programming with Scala. At so… http://bit.ly/9YaHCt […]

20 06 2010
Jesper Nordenberg

An alternative solution is:

object typeeq {
trait True
trait False

class AreEqual[T1, T2, RT]

def value[T] = null.asInstanceOf[T]

implicit def areEqual[T] = new AreEqual[T, T, True]

def teq[T1, T2, RT](v1 : T1, v2 : T2)(implicit e : AreEqual[T1, T2, RT] =
new AreEqual[T1, T2, False]) = value[RT]


scala> import typeeq._
import typeeq._

scala> teq(value[Int], value[Int])
res0: typeeq.True = null

scala> teq(value[Int], value[Double])
res1: typeeq.False = null

21 06 2010

Not exactly I think. Solutions involving implicits seem to make it impossible to extract the desired static type at compile time. For your solution the following fails:

  val tv = teq(value[Int], value[Int])
  implicitly[tv.type =:= True]

  val fv = teq(value[Int], value[Double])
  implicitly[fv.type =:= False]
could not find implicit value for parameter e: =:=[tv.type,typeeq.True]
21 06 2010
Jesper Nordenberg

That’s because tv.type is not the same type as True. Use tv.t like in your original example and it works.

Relying on method overloading, like you do in your original example, doesn’t buy you anything compared to using implicits. In fact, it’s worse since you can’t propagate overload resolution control. For example:

scala> def check[T1, T2] = Equality[T1] check witness[T2]
check: [T1,T2]types.False

To my knowledge, there is unfortunately no way to implement type level equality checks in Scala.

21 06 2010

I see, nice approach!

I tried to refine this a bit. Now the equality check returns a value representing the result of the equality check. This value can at the same time be used to project out the type level encoding of the equality check result.

object typeeq {
  trait Bool
  case class True() extends Bool { type t = True }
  case class False() extends Bool { type t = False }

  trait AreEqual[T1, T2, RT] { val v: Bool }
  implicit def areEqual[T] = new AreEqual[T, T, True] { val v = True() }

  case class EQU[T1, T2]()  {
    def eval[RT](implicit e: AreEqual[T1, T2, RT] = 
        new AreEqual[T1, T2, False] { val v = False() }) = e.v.asInstanceOf[RT]


  import typeeq._

  val t = EQU[Int, Int].eval
  implicitly[t.t =:= True] 
  // implicitly[t.t =:= False] 
  val f = EQU[Int, String].eval
  // implicitly[f.t =:= True]
  implicitly[f.t =:= False]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: