Type-safe way of dependent typing based on value?

Question
1

Hi,

I am wondering if it is possible to use the Scala type system to have “lego brick” type blocks that I can chain together, with the compiler checking that the blocks fit together? The main thing I would like to have is the type computed from the value of one of the members of the class. I can do this with an implicit conversion to a “typed” class, but this happens at runtime which is not really what I am looking for. From a bit of research, I think this may be “dependent typing”, which it seems Scala supports in some form, but I am not sure if what I want is possible.

Here is a minimal example which illustrates what I am after:

trait TypedBlock

case class TypedBlock_1() extends TypedBlock
case class TypedBlock_2() extends TypedBlock

def modelToTypedBlock(x: Block): TypedBlock = x.layers.headOption match
   case Some(Layer(1))      => TypedBlock_1()
   case Some(Layer(2))      => TypedBlock_2()

case class Layer(in: Int)

class Block(val layers: Seq[Layer])

class MyValidBlock() extends Block(List(
      Layer(1),
      Layer(2)))

class MyInvalidBlock() extends Block(List(
      Layer(3),
      Layer(2)))

object Conversions:
  given model2TypedBlock: Conversion[Block, TypedBlock] =
     modelToTypedBlock(_)
end Conversions

@main def example: Unit = {
    import Conversions.model2TypedBlock

    val myValidBlock = MyValidBlock()
    val myTypedValidBlock: TypedBlock = myValidBlock
    println(s"myTypedValidBlock: $myTypedValidBlock")

    val myInvalidBlock = MyInvalidBlock()
    val myTypedInvalidBlock: TypedBlock = myInvalidBlock
    println(s"myTypedInvalidBlock: $myTypedInvalidBlock")
}

This succeeds at compile time but throws an error at runtime. Is there a way to change this so that the conversion happens at compile time and throws an error then?

From a bit of research, I think this kind of thing is possible in F sharp, using the DependentTypes library so I was hoping I could do the same in Scala.

2

Hmm. I think the answer is probably yes, but let’s tease out a little more what you’re trying to do.

Is the “invalid” part of MyInvalidBlock the fact that Layer 3 comes before Layer 2, or simply that there shouldn’t be a Layer 3 in the first place? I’m going to assume the latter, but I may be misinterpretating.

Regardless, though, I think the fundamental problem is the parameter to Layer. That’s an Int, which is kind of a black box to the compiler – from the compiler’s POV, there is no difference between 1, 2, 3, etc, which is why you’re having trouble getting it to help you out.

While dependent types might be involved in the solution, I think the key concept you’re looking for here is refined types, and probably more specifically singleton types. You need that parameter to not be an Int per se, you need it to be a subtype of Int – a Singleton type that only holds that specific number. Off the top of my head, that would look something like this:

case class Layer[T <: Singleton with Int](in: T)

That is, the parameter isn’t just any old Int, it is a specific Int that the compiler now knows about.

Now the compiler is armed with enough information to be able to reason about that parameter. Assuming I’m correct about the problem you’re trying to deal with, there are probably multiple ways to slice it, and it’s possible that there might be a dependent-type-based solution, but I’ve probably go for a typeclass, along the lines of:

trait Typeable[T] {
  def toTyped(t: T): TypedBlock
}
object Typeable {
  implicit val layer1Typed: Typeable[1] = new Typeable[1] { def toTyped(t: 1) = TypedBlock_1() }
  implicit val layer2Typed: Typeable[2] = new Typeable[2] { def toTyped(t: 2) = TypedBlock_2() }
}

That allows you to go from a specific Singleton Int to a TypedBlock.

At that point, you can add Typeable as a type constraint to Layer:

case class Layer[T <: Singleton with Int : Typeable](in: T)

Now, the compiler will only allow you to declare a Layer if there exists a way to get a TypedBlock from its parameter, and will fail at compile-time if you pass in a bad value.

In general, the trick is to make sure the compiler has enough information where it needs it; that means being very precise about your types, and making sure you pass them around to where they are needed. Once you have that, while the compiler can’t do everything, there tend to be ways to make it enforce your constraints.

Note that that’s all Scala 2.13; for all that I’ve been following Scala 3 enthusiastically, I haven’t had enough chance to use it hands-on for me to be confident yet. The concepts are all the same, but it will need a little rewriting in terms of Scala 3 given/using.

Hopefully that’s at least helpful, and I haven’t entirely misunderstood what you’re looking for. Here’s a Scastie illustrating what I’m talking about. Please follow up with any additional questions you might have, and folks here may be able to help.

2 Likes
3

Hi jducoeur,

Thank you for the detailed and informative response! I especially appreciate you reading between the lines on my post and figuring out what it is I was trying to do. I agree that I think refined types are what I am after here. I found the “refined” library for Scala, however it doesn’t seem to support exactly what I want.

I think your solution kind of works, however I have another idea which I didn’t explain. I want to enforce that the last layer of one block has the same layer size as the layer I want to connect it to. An example of a valid connection would be:

class MyValidBlock1() extends Block(List(
  Layer(1),
  Layer(2)))

class MyValidBlock2() extends Block(List(
      Layer(2),
      Layer(4),
      Layer(8)))
val block1 = MyValidBlock1()
val block2 = MyValidBlock2() 
val newBlock = block1.connect(block2)  // Compilation succeeds

and an invalid connection would be (where the output of the first block does not equal the input of the second block):

class MyValidBlock() extends Block(List(
  Layer(1),
  Layer(2)))

class MyInvalidBlock() extends Block(List(
      Layer(3),
      Layer(4),
      Layer(8)))
val block1 = MyValidBlock()
val block2 = MyInvalidBlock() 
val newBlock = block1.connect(block2)  // Compilation error

I hope that makes sense. The idea is that one block can “plug” into another like a electrical plug into a socket or lego bricks. I would like that to be done at compilation time. The idea is that users will write definitions of the blocks and connections like above and I would like to give them compilation errors in Scala rather than writing a manual checker for these rules.
From what you have said so far, I think this should be possible but I am not so sure.

So I think what I need to do, is write something which will convert a block, to a “TypedBlock” with its input and output sizes as part of the type. For MyValidBlock1, that would be TypedBlock_1_2 and for MyValidBlock2, that would be TypedBlock_2_8. Then I would define a function which ensures that only functions with matching input and output types can be connected together. I am having trouble figuring out how to do that in a way which doesn’t involve handling every combination of input and output sizes.

I hope that makes sense. Any more guidance or things to look into would be appreciated.

4

Hmm. Needs more thought (and I encourage others here to chime in), but in airy theory it seems like you need that subtype of Int (which you get from Layer) to percolate up to Block as an inferred type. That in turn implies that you probably shouldn’t use the raw List constructor inside Block – instead, you need to construct that in a way that preserves the types of the first and last Layers.

Off the top of my head, it feels like you need a Layers[H, T], where H is the type of the head layer, and T the type of the last, and both are the same sort of subtype of Int with Singleton as Layer has. Then you add a .and() method to that:

case class Layers[H <: Singleton with Int, T <: Singleton with Int] {
  def and[N <: Singleton with Int](next: Layer[N]): Layers[H, N]
}

You’d also need a way to turn the head Layer into a Layers[T, T] to start that out (probably with an implicit to reduce the boilerplate of applying it), and a constructor on Block that takes a Layers and preserves the type parameters. (Actually, that may indicate that what I am calling Layers is exactly what you mean by Block.)

Given all that, you define connect() as:

case class Block[H, T] {
  def connect(to: Block[T, U]): Block[H, U]
}

and the compiler will enforce that they line up.

That’s all rather half-baked, but hopefully enough food for thought to help out. The heart of it is that that List() in the middle is getting in the way – if you can replace that with something that preserves the types you need, it can probably be done.