在类型和值之间建立联系

Question

我有类型级算术的实现，能够进行一些编译时算术验证，即<,>,=，有两种方式：

• simple 实现
• rigorous 实现

有了这些，我可以有一个 getFoo 函数，我可以这样调用：

getFoo[_2,_3]

_2 和 _3 是整数值 2 和 3 的类型级等价物。现在理想情况下，我希望我的 getFoo 函数将整数值作为参数并尝试从值推断 _2 2.

我的计划是将以下 associatedInt 信息添加到 Nat 基类：

trait Nat {
  val associatedInt: Int
  type AssociatedInt = associatedInt.type
}

这样后续的类型会被定义为：

type _1 = Succ[_0] {
  override val associatedInt: Int = 1
}

然后将getFoo的签名改成整数：

def getFoo(i:Int)(implicit ...)

基于此，我们将使用与AssociatedInt 类型关联的类型进行类型级别的算术断言。即，类似：

def getFoo(i: Integer)(implicit ev: Nat{type I = i.type } =:= ExpectedType)

这不起作用。即：

trait Nat {
  val i: Integer
  type I = i.type
}

type ExpectedType = _1

trait _1 extends Nat {
  override val i: Integer = 1
}

def getFoo(i: Integer)
          (implicit ev: Nat{type I = i.type } =:= ExpectedType)= ???

getFoo(1) //this fails to prove the =:= implicit.

回想起来，我不应该期望它。因为如果我们有：

val x : Integer = 1
val y : Integer = 1
type X = x.type
type Y = y.type
def foo(implicit ev: X =:= Y) = 123
foo //would fail to compile.

即具有相同值的不同“对象”的单例类型是不同的。 （我猜原因是目前在 Scala 中，单例类型用于对象，与 literal type 不同）

因此，有了这些背景信息，我想知道是否有任何方法可以实现我想要做的事情，即通过其他方法从关联值推断 a 类型。

Answer 1

答案似乎只是“不”。这些值在运行时存在。类型检查发生在编译时。这两个时间间隔不相交，运行时总是严格地在编译时间之后出现，因此无法及时传播有关值的信息以获取有关类型的一些附加信息。

请注意，如果您只需要排序（您不想添加或减去版本号），那么您可以简单地重用子类型关系，如下所示：

sealed trait Num
class _9 extends Num
class _8 extends _9
class _7 extends _8
class _6 extends _7
class _5 extends _6
class _4 extends _5
class _3 extends _4
class _2 extends _3
class _1 extends _2
class _0 extends _1

trait Version[+Major <: Num, +Minor <: Num]

println(implicitly[Version[_2, _4] =:= Version[_2, _4]])
println(implicitly[Version[_2, _3] <:< Version[_2, _4]])

Answer 2

诀窍是意识到值可以具有类型字段，并且类型信息在编译时可用。考虑到这一点，我们可以定义：

sealed trait NatEnum{
  type Nat_ <:Nat
}

并为这些类型定义枚举“值”，例如：

object __0 extends NatEnum{ override type Nat_ = _0 }
object __1 extends NatEnum{ override type Nat_ = _1 }
object __2 extends NatEnum{ override type Nat_ = _2 }
object __3 extends NatEnum{ override type Nat_ = _3 }

并重构getFoo如下：

def getFoo(maj: NatEnum, min: NatEnum)(implicit
                     maj_check: FooClient.Major =:= maj.Nat_,
                     min_check: FooClient.Minor <:< min.Nat_
                    ) = FooClient.foo

我们可以用它来测试：

getFoo(__2,__2) //compiles
getFoo(__1,__0)// doesn't compile

这里是要点的更新版本：simple 和 rigorous