在类型和值之间建立联系 [英] Making connections between types and values

问题描述

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

I have implementations of type-level arithmetics capable of doing some compile time arithmetic validation, namely <,>,= in two ways:

• 简单实现
• 严格实施

• simple implementation
• rigorous implementation

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

With these, I can have a getFoo function that I can call like this:

getFoo[_2,_3]

其中_2和_3是整数值2和3的类型级别等效项.现在，理想情况下，我希望我的getFoo函数将整数值用作参数，并尝试从该值推断_2 2.

With _2 and _3 being the type-level equivalents of integer values 2 and 3. Now Ideally I would like my getFoo function to take integer values as arguments and attempt to infer _2 from the value 2.

我的计划是将以下relatedInt信息添加到Nat基类中:

My plan was to add the following associatedInt information to the Nat base class:

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

以便将后续类型定义为:

So that the subsequent types would be defined as:

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

然后更改getFoo的签名，使其采用整数:

And then change getFoo's signature so that it takes an integer:

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

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

Based on which, we would do our type level arithmetic assertions with types associated to the AssociatedInt type. Ie, something like:

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.

反思，我不应该期望如此.因为如果我们有:

On reflection, I shouldn't have expected it to. Since if we have:

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中，单例类型是针对对象的，与

I.e. the singleton types of the different "objects" with the same values is different. (I guess the reason is that currently in Scala the singleton types are for objects and are distinct from literal type)

因此，有了这些背景信息，我想知道是否有任何方法可以实现我要尝试的工作，即通过其他方法从关联值中推断出一个类型.

So with this background information, I would like to know if there is any way to achieve what I am trying to do, namely inferring the a type from an associated value, through other methods.

推荐答案

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

The trick is to realise that values can have type fields and that type information is available at compile time. With this in mind, we can define:

sealed trait NatEnum{
  type Nat_ <:Nat
}

并为以下类型定义枚举值":

and define enum "values" for these types like:

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

我们可以用它进行测试:

which we can test with:

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

这是要点的更新版本:简单和

here is the updated version of the gists: simple and rigorous

这篇关于在类型和值之间建立联系的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！