Типы, зависящие от пути scala, и доказательства уровня типа

В настоящее время я пытаюсь определить модель языка синхронизированного потока данных в 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, используя типы, зависящие от пути, и черпая вдохновение из shapeless. Часы моделируются следующим образом:

  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 - это тип Clock, который можно использовать для определения дискретных потоков.

Затем я предлагаю способы построения потоков на базовых часах:

  // 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

и пусть компилятор отклонит последний случай, потому что ClockType a1 и c1 не равны (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 в бесформенном виде и понял, что объекты, являющиеся свидетелями таких фактов, должны быть построены в структурной прямой индуктивной манере: вы предоставляете неявные построители для объектов, создающих экземпляры этого конструктора типов для типов, которые вы хотите статически проверять, и механизм неявного разрешения создает объект, свидетельствующий о свойстве, если это возможно.

Однако я действительно не понимаю, как компилятор может построить правильный объект, используя прямую индукцию для любого экземпляра типа, поскольку мы обычно делаем доказательства с использованием рекурсии, разбирая термин в более простых терминах и доказывая более простые случаи.

Было бы полезно руководство от кого-то, кто хорошо разбирается в программировании на уровне типов!