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

我正在尝试在 scala中定义一个时钟数据流语言的模型.

流程虚拟地表示某些类型T的值的无限序列,由一些时钟C(一个时钟表示在哪个时刻实际上可用).

可以从流F通过根据从另一(布尔)流F’导出的时钟C本身进行采样来从流F导出采样流SF.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是流,则fAsAslock是可用于定义采样流的时钟类型.

然后我提供了在基础时钟上构建流的方法：

// 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] = ???

这是我完全无知的地方,如何进行.我已经看过Natty和HList源代码,并且理解这样一个事实应该是以一种结构化的前向归纳的方式构建的：你为这个类型的构造函数提供了隐含的构建器,这些构造函数用于要静态检查的类型,隐式解析机制生成一个可见的属性的对象.

然而,我真的不明白编译器如何使用任何类型实例的正向归纳来构建正确的对象,因为我们通常通过简单地解构术语并证明更简单的情况来使用递归来进行证明.

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

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
                                      ^