Juan Salvador
Juan Salvador

Reputation: 452

Testing at type-level computing in Scala

I'm following Type-Level Programming in Scala.

I got the below code

sealed trait Bool {
  type && [b <: Bool] <: Bool
  type || [b <: Bool] <: Bool
  type IfThenElse[B, T <: B, F <: B] <: B
}

object True extends Bool {
  type && [B <: Bool] = B
  type || [B <: Bool] = True.type
  type IfThenElse[B, T <: B, F <: B] = T
}

object False extends Bool {
  type && [B <: Bool] = False.type
  type || [B <: Bool] = B
  type IfThenElse[B, T <: B, F <: B] = F
}

type True = True.type
type False = False.type

When I try to run the test

assert((False && False) == False)

I got the message

Error:(26, 16) value && is not a member of object A$A146.this.False
assert((False && False) == False)
              ^

Can anyone tell me please what is wrong in that code?. I'm runing the code as a *.sc file. (I'm really a new to Scala)

Upvotes: 0

Views: 78

Answers (1)

Michael Zajac
Michael Zajac

Reputation: 55569

There are two problems.

First, you cannot compare types as if they are values. == is a run time method, so that would defeat the purpose of doing things at the type level, even if it worked. What you can do is look for implicit evidence that A =:= B, where A <: Bool and B <: Bool.

Second, you cannot use infix notation for type members, so False && False must be written as False.&&[False]. At least in the way you have it defined. An infix type would only work if defined as a type with two parameters, like type &&[A, B]

Now we try try out some computations. Here are some that resolve successfully:

scala> implicitly[False.&&[False] =:= False]
res9: =:=[False.&&[False],False] = <function1>

scala> implicitly[False.&&[False] =:= False]
res12: =:=[False.&&[False],False] = <function1>

scala> implicitly[False.&&[True] =:= False]
res13: =:=[False.&&[True],False] = <function1>


scala> implicitly[True.&&[False] =:= False]
res15: =:=[True.&&[False],False] = <function1>

scala> implicitly[True.||[False] =:= True]
res17: =:=[True.||[False],True] = <function1>

And some that do not:

scala> implicitly[False.&&[False] =:= True]
<console>:20: error: Cannot prove that False.&&[False] =:= True.
       implicitly[False.&&[False] =:= True]
                 ^

scala> implicitly[(False && False) =:= True]
<console>:20: error: not found: type &&
       implicitly[(False && False) =:= True]
                         ^

scala> implicitly[True.||[False] =:= False]
<console>:19: error: Cannot prove that True.||[False] =:= False.
       implicitly[True.||[False] =:= False]
                 ^

scala> implicitly[True.&&[True] =:= False]
<console>:20: error: Cannot prove that True.&&[True] =:= False.
       implicitly[True.&&[True] =:= False]
                 ^

Upvotes: 5

Related Questions