在Scala中进行类型级计算测试

Question

我正在遵循Scala中的类型级编程.

我得到了以下代码

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

当我尝试运行测试时

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

我收到了消息

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

请问有人告诉我那个代码有什么问题吗？我正在将代码作为*.sc文件运行.(我真的是Scala的新手)

Answer 1

有两个问题.

首先,您无法将类型与值进行比较.==是一种运行时方法,因此即使它起作用,也会破坏在类型级别执行操作的目的.你可以做的是寻找隐含的证据A =:= B,在哪里A <: Bool和B <: Bool.

其次,您不能对类型成员使用中缀表示法,因此False && False必须写为False.&&[False].至少在你定义它的方式.只有在定义为具有两个参数的类型时,中缀类型才有效type &&[A, B]

现在我们尝试尝试一些计算.以下是一些成功解决的问题:

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>

而有些则没有:

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]
                 ^