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

Question

В настоящее время я пытаюсь определить модель синхронизированного языка потока данных в scala.

Поток фактически представляет собой бесконечную последовательность значений некоторого типа T, перемещаемую некоторыми часами C (часы показывают, в какие моменты поток фактически доступен).

Сэмплированный поток SF может быть получен из потока F путем отбора его в соответствии с самой синхронизацией C, полученной из другого (булева) потока F ': SF содержит значения F, отсчитываемые, когда логический поток F' истинен.

«Базовые часы» - это часы, полученные из всегда истинного потока с именем «T».

В приведенном ниже примере, Р и Р «находятся на базовой частоте (и - используется, чтобы показать, что поток не имеет значения в некоторый момент времени)

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 
    } 

Это определяет тип часов и конкретные часы, базовую частоту, которая не имеет subclock.

Затем я попытался смоделировать потоки:

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, поэтому эти потоки не находятся на одних и тех же часах).

Так что я представил (неявное эв: SameClock [F1, F2]) аргумент к моему методу строителя, где

SameClock является признаком означал свидетель во время компиляции, что два потока имеет одинаковый ClockType, и что правильно пробовать первый, используя часы, полученные из второго.

Здесь я совершенно не знаю, как действовать. Я посмотрел исходный код Nat и HList в бесформенном виде и понял, что объекты, свидетельствующие об этих фактах, должны быть построены в структурном форвардном индуктивном режиме: вы предоставляете неявные сборщики для объектов, запускающих конструктор этого типа для типов, которые вы хотите статически проверять и механизм неявного разрешения генерирует объект, свидетельствующий об этом свойстве, если это возможно.

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

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

Answer 1

Я думаю, что вы слишком усложняете основную проблему (или это то, что вы слишком упростили ее для вопроса).

Вы не должны нуждаться в имплицитах, чтобы работать с зависимыми от типа типами. Фактически, в настоящее время в Scala нет способа доказать системе типов что-то вроде a.T <: b.T на основе неявного. Единственный способ для Scala понять, что 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 не имеет значения.)