代码之家 › 专栏 › 技术社区 › Maths noob

在类型和值之间建立连接

type-variables type-level-computation type-deduction types scala

1

Maths noob · 技术社区 · 6 年前

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

simple 实施
rigorous 实施

有了这些,我就可以拥有 getFoo 我可以这样调用的函数:

getFoo[_2,_3]

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

我的计划是将以下信息添加到 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)

这不管用。Ie:

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中,singleton类型是用于对象的,与 literal type )

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

2 回复 | 直到 6 年前

1

Andrey Tyukin 6 年前

答案似乎只是“不”。值在运行时存在。类型检查在编译时进行。这两个时间间隔不相交,运行时总是严格在编译时之后,因此无法及时传播有关值的信息以获取有关类型的其他信息。

注意,如果一个排序是你想要的(你不想添加或减去版本号),那么你可以简单地重用子类型关系如下:

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

2

1

Maths noob 6 年前

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

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

以下是gist的更新版本: simple 和 rigorous