scala依赖路径的类型和类型级别证明

Question

我目前正在尝试在scala中定义时钟数据流语言的模型。

流程实际上代表某种类型T的无限序列值，由某个时钟C（一个时钟表示流量实际可用时刻）。

采样流SF可以通过根据从另一个（布尔）流F'导出的时钟C自己对流F进行采样来导出：SF包含当布尔流F'为真时采样的F的值。

“基准时钟”是从始终为真的流名为“T”派生的时钟。

在下面的示例中，F和F“是在基时钟（和 - 用于显示该流不具有值，在某些时刻）

T    : 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 ... (always 1) 
F    : 0 0 0 1 1 1 0 1 0 1 0 0 0 1 1 1 1 ... 
F'    : 0 1 0 0 0 1 0 1 1 1 0 0 0 1 0 0 1 ... 
F sampled on F': - 0 - - - 1 - 1 0 1 - - - 1 - - 1 ... 

所以，（F F上采样” ）当F'为真时取F的值，当F'为假时未定义。

目标是使这种采样关系在流类型中显而易见并执行静态检查。例如，如果它们在同一个时钟上，只允许从另一个流程中采样。 （这是用于建模数字电路的DSL）。

所讨论的系统是一个独立类型的系统，因为时钟是流类型的一部分，并且它本身是从流量值派生的。

所以我试图在scala中使用路径依赖类型对其进行建模，并从无形中获取灵感。时钟被建模为如下类型：

trait Clock { 
    // the subclock of this clock 
    type SubClock <: Clock 
    } 

    trait BaseClock extends Clock { 
    type SubClock = Nothing 
    } 

这定义了时钟类型和一个特定的时钟，没有子时钟的基本时钟。

然后，我试图建模流动：

trait Flow { 

    // data type of the flow (only boolean for now) 
    type DataType = Boolean 

    // clock type of the flow 
    type ClockType <: Clock 

    // clock type derived from the Flow 
    class AsClock extends Clock { 

     // Subclock is inherited from the flow type clocktype. 
     type SubClock = ClockType 
    } 

    } 

我在流性状限定的内部的类，以能够解除使用路径依赖类型的流的时钟。如果f是一个流，f.AsClock是一个时钟类型，可以用来定义采样流。

然后我提供的方法来建立在基础时钟流量：

// used to restrict data types on which flows can be created 
    trait DataTypeOk[T] { 
    type DataType = T 
    } 

    // a flow on base clock 
    trait BFlow[T] extends Flow { type DataType = T; type ClockType = BaseClock } 

// Boolean is Ok for DataType 
    implicit object BooleanOk extends DataTypeOk[Boolean] 


    // generates a flow on the base clock over type T 
    def bFlow[T](implicit ev:DataTypeOk[T]) = new BFlow[T] { } 

到目前为止好。然后，我提供了一种笏建立一个采样流：

// a flow on a sampled clock 
    trait SFlow[T, C <: Clock] extends Flow { type DataType = T; type ClockType = C } 

    // generates a sampled flow by sampling f1 on the clock derived from f2 (f1 and f2 must be on the same clock, and we want to check this at type level. 
    def sFlow[F1 <: Flow, F2 <: Flow](f1: F1, f2: F2)(implicit ev: SameClock[F1, F2]) = new SFlow[f1.DataType, f2.AsClock] {} 

这就是流量值被提升到使用f2.AsClock类型。

这背后的想法是可以这样写：

val a1 = bFlow[Boolean] 
    val a2 = bFlow[Boolean] 
    val b = bFlow[Boolean] 
    val c1: SFlow[Boolean, b.AsClock] = sFlow(a1, b) // compiles 
    val c2: SFlow[Boolean, b.AsClock] = sFlow(a2, b) 
    val d: SFlow[Boolean, c1.AsClock] = sFlow(a1, c1) // does not compile 

，并让编译器拒绝最后一种情况，因为A1和C1的ClockType是不相等的（A1是在底座上时钟，c1在时钟b上，所以这些数据流不在同一个时钟上）。

所以我介绍的（隐式EV：SameClock [F1，F2]）参数来我的助洗剂的方法，其中

SameClock是指在编译时地看到，两个流具有相同的ClockType的性状，并且采用从第二个时钟导出的时钟对第一个进行采样是正确的。

//type which witnesses that two flow types F1 and F2 have the same clock types. 
    trait SameClock[F1 <: Flow, F2 <: Flow] { 

    } 

    implicit def flowsSameClocks[F1 <: Flow, F2 <: Flow] = ??? 

这是我完全不知道如何进行。我以无形的形式查看了Nat和HList源代码，并且了解到目击此类事实的对象应该以结构化的前向归纳方式构建：您为要静态检查的类型提供实例化此类构造函数的对象的隐式构建器，以及如果可能的话，隐式解析机制产生见证该属性的对象。

但是我真的不明白编译器如何使用任何类型实例的向前归纳来构建正确的对象，因为我们通常通过用简单的术语解构术语来证明递归，并证明更简单的情况。

某些对类型级编程有深入理解的人的指导将会很有帮助！

Answer 1

我想你已经过分复杂化了一个基本问题（或者说你已经简化了太多的问题）。

你不应该需要implicits使路径依赖类型工作。实际上，目前在Scala中没有办法根据隐式来向类型系统证明类似a.T <: b.T的东西。唯一的办法是让斯卡拉明白a和b是真正的价值。

下面是一个简单的设计已经做了你需要什么：

trait Clock { sub => 

    // This is a path-dependent type; every Clock value will have its own Flow type 
    class Flow[T] extends Clock { 
    def sampledOn(f: sub.Flow[Boolean]): f.Flow[T] = 
     new f.Flow[T] { /* ... */ } 
    } 

} 

object BaseClock extends Clock 

object A1 extends BaseClock.Flow[Int] 
object A2 extends BaseClock.Flow[Boolean] 
object B extends BaseClock.Flow[Boolean] 

val c1: B.Flow[Int] = A1 sampledOn B 
val c2: B.Flow[Boolean] = A2 sampledOn B 
val d1 = c1 sampledOn c2 
//val d2: c2.Flow[Int] = A1 sampledOn c2 // does not compile 

最后一行无法编译，错误：

Error:(133, 38) type mismatch; 
found : B.Flow[Boolean] 
required: BaseClock.Flow[Boolean] 
    val d2: c2.Flow[Int] = A1 sampledOn c2 // does not compile 
            ^

（请注意，是否值与val或object声明是无关紧要的）。