tipi di scala scala dipendenti e prove di livello di tipo

Question

Attualmente sto cercando di definire un modello di un linguaggio di flusso di dati in scala.

Un flusso rappresenta virtualmente una sequenza infinita di valori di qualche tipo T, stimolati da un certo clock C (un orologio indica in quali momenti il ​​flusso è effettivamente disponibile).

Un flusso SF campionato può essere derivato da un flusso F campionandolo secondo un clock C derivato da un altro flusso (booleano) F ': SF contiene i valori di F campionati quando il flusso booleano F' è vero.

Il "Base Clock" è l'orologio derivato dal flusso sempre vero denominato "T".

Nell'esempio che segue, F e F 'sono sulla base clock (e - è usato per indicare che il flusso non ha valore ad un certo istante)

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

così, (F campionati sul F') prende il valore di F quando F 'è vero, e non è definito quando F' è falso.

L'obiettivo è rendere evidente questa relazione di campionamento nel tipo di flussi e eseguire controlli statici. Ad esempio, consente solo di campionare un flusso da un altro se si trovano sullo stesso orologio. (Questo è per una DSL per la modellazione di circuiti digitali).

Il sistema in questione è un sistema tipizzato in modo dipendente perché un orologio fa parte del tipo di un flusso ed è esso stesso derivato da un valore di flusso.

Così ho provato a modellare questo in scala usando tipi dipendenti dal percorso e prendendo ispirazione da informi. Orologi sono modellate come tipi come segue:

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

    trait BaseClock extends Clock { 
    type SubClock = Nothing 
    } 

Questo definisce il tipo di orologio e di un particolare orologio, l'orologio di base che non ha subclock.

Poi, ho cercato di modellare flussi:

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 
    } 

    } 

ho definita una classe interna del tratto di flusso, per poter sollevare un flusso di un orologio con percorso di tipi dipendenti. se f è un flusso, f.AsClock è un tipo di orologio che può essere utilizzato per definire i flussi campionati.

Poi mi forniscono modi per costruire i flussi sulla base 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] { } 

Fin qui tutto bene. Poi Fornisco un wat di costruire un flusso di campionato:

// 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] {} 

Questo è dove i valori di portata sono sollevati a tipi utilizzando f2.AsClock.

L'idea dietro questo potrebbe essere quella di essere in grado di scrivere cose del genere:

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 

ed avere il compilatore respingere l'ultimo caso, perché il ClockType di A1 e C1 non sono uguali (a1 è alla base orologio, c1 è sull'orologio b, quindi questi flussi non sono sullo stesso orologio).

Così ho introdotto un (ev implicita: SameClock [F1, F2]) argomento al mio metodo costruttore, dove

SameClock è un tratto destinato a testimoniare in fase di compilazione che due flussi hanno la stessa ClockType, e che è corretto campionare il primo usando l'orologio derivato dal secondo.

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

Questo è il punto in cui sono totalmente all'oscuro di come procedere. Ho esaminato il codice sorgente di Nat e HList in forma informe e ho capito che gli oggetti che assistono a tali fatti dovrebbero essere costruiti in modo strutturale e induttivo: fornisci costruttori impliciti per gli oggetti che instanziano questo tipo di costruttore per i tipi che vuoi controllare staticamente e il meccanismo implicito di risoluzione genera un oggetto che testimonia la proprietà se è possibile.

Tuttavia, in realtà non capisco come il compilatore possa costruire l'oggetto giusto usando l'induzione diretta per qualsiasi istanza di tipo, dal momento che di solito le dimostrazioni utilizzano la ricorsione decostruendo un termine in termini più semplici e dimostrando casi più semplici.

Alcuni consigli da parte di qualcuno con una buona comprensione della programmazione di programmi di testo sarebbe utile!

Answer 1

Penso che si stia complicando eccessivamente un problema di base (o che lo abbia semplificato troppo per la domanda).

Non si suppone che abbia bisogno di impliciti per far funzionare i tipi dipendenti dal percorso. In effetti, al momento in Scala non c'è modo di dimostrare al sistema tipo qualcosa come a.T <: b.T basato su un implicito. L'unico modo è che Scala capisca che a e b sono in realtà lo stesso valore.

Ecco un design semplice che fa quello che avete richiesto:

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 

L'ultima riga non viene compilato, con l'errore:

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

(Si noti che se i valori vengono dichiarati con val o object è irrilevante.)