scala path dependent types and type level proofs

Question

I am currently trying to define a model of a clocked dataflow language in scala.

A flow virtually represents an infinite sequence of values of some type T, paced by some clock C (a clock indicates at which moments the flow is actually available).

A sampled flow SF can be derived from a flow F by sampling it according to a clock C itself derived from another (boolean) flow F': SF contains the values of F sampled when the boolean flow F' is true.

The "Base Clock" is the clock derived from the always true Flow named "T".

In the example below, F and F' are on the base clock (and - is used to show that the flow has no value at some instant)

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

so, (F sampled on F') takes the value of F when F' is true, and is not defined when F' is false.

The goal is to make this sampling relationship apparent in the type of the flows and to perform static checks. For instance, only allow to sample a flow from another one if they are on the same clock. (This is for a DSL for modelling digital circuits).

The system in question is a dependently typed system because a clock is part of the type of a flow and is itself derived from a flow value.

So I tried to model this in scala using path dependent types and taking inspiration from shapeless. Clocks are modeled as types as follows:

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

  trait BaseClock extends Clock {
    type SubClock = Nothing
  }

This defines the clock type and a particular clock, the base clock which has no subclock.

Then, I tried to model flows:

  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
    }

  }

I defined an internal class in the flow trait, to be able to lift a Flow to a clock using path dependent types. if f is a flow, f.AsClock is a Clock type that could be used to define sampled flows.

Then I provide ways to build flows on the 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] { }

So far so good. Then I provide a wat to build a sampled flow:

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

This is where the flow values are lifted to types using f2.AsClock.

The idea behind this would be to be able to write things like this:

  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

and have the compiler reject the last case because the ClockType of a1 and c1 are not equal (a1 is on the base clock, c1 is on clock b, so these flows are not on the same clock).

So I introduced an (implicit ev:SameClock[F1,F2]) argument to my builder method, where

SameClock is a trait meant to witness at compile time that two flows have the same ClockType, and that it is correct to sample the first one using the clock derived from the second one.

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

This is where I am totally clueless as how to proceed. I've looked at the Nat and HList source code in shapeless, and understood that objects witnessing such facts should be built in a structural forward inductive manner: you provide implicit builders for objects instanciating this type constructor for the types you want to statically check and the implicit resolution mechanism generates an object witnessing the property if it is possible.

However I really do not understand how the compiler can build the right object using forward induction for any type instance, since we usually do proofs using recursion by deconstructing a term in simpler terms and proving simpler cases.

Some guidance from someone with a good understanding of typelevel programming would be helpful!

Answer 1

I think you are over-complicating a basic problem (or it's that you have simplified it too much for the question).

You are not supposed to need implicits to make path-dependent types work. In fact, there is at the moment no way in Scala to prove to the type system something like a.T <: b.T based on an implicit. The only way is for Scala to understand that a and b are really the same value.

Here is a simple design that does what you required:

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

The last line does not compile, with error:

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

(Note that whether values are declared with val or object is irrelevant.)