What sorcery is this?

This library very clever. Imagine you want to listen on a TCP port. You represent that port number with an Int. But what if somebody misconfigures the value and you only realise the mistake at runtime? Wouldn't it be nice to catch it compile time? Now you can!

import eu.timepit.refined._
import eu.timepit.refined.api.Refined
import eu.timepit.refined.numeric._

  type Port = Int Refined Interval.ClosedOpen[W.`1`.T, W.`65535`.T]

Is all we need to have compile time checking that an Int representing a port is in a sensible range. For instance, if we had:

  def listenOn(port: Port) = ??? 

then this works:

    listenOn(1: Port)

but these fail to compile:

    listenOn(0: Port)

    listenOn(65536: Port)

exactly as we expect and desire.

But it gets better. A common error in neural nets judging by the forums is not getting the size of matrices correct and only finding out at runtime after they have been running for a while. Wouldn't it be good to know at compile time? Now we can (code taken from this GitHub repository):

type ExactInt = Int Refined Equal[A] forSome { type A <: Int }

case class Matrix2[ROWS ExactInt, COLS  ExactInt](nRows: ROWS, nCols: COLS) {

  val REQUIRED_COLS =  Witness.mkWitness(nCols)

  def multiply[T ExactInt](x: Matrix2[REQUIRED_COLS.T, T]): Matrix2[ROWS, T] = Matrix2(nRows, x.nCols)

}

Note we don't actually do the multiplication - this is just a PoC and we're just interested in types.

Also note that this forSome is nicely explained by Rob Norris on his blog here where he deals with F-Bound Types (where an "F-bounded type is parameterized over its own subtypes") and uses forSome to enforce that.

Now we can create some matrices:

    val _3x7: Matrix2[Exactly[W.`3`.T], Exactly[W.`7`.T]]   = Matrix2(3: Exactly[W.`3`.T], 7: Exactly[W.`7`.T])

    val _7x8: Matrix2[Exactly[W.`7`.T], Exactly[W.`8`.T]]   = Matrix2(7: Exactly[W.`7`.T], 8: Exactly[W.`8`.T])

    val _8x7: Matrix2[Exactly[W.`8`.T], Exactly[W.`7`.T]]   = Matrix2(8: Exactly[W.`8`.T], 7: Exactly[W.`7`.T])

and this compiles:

    _3x7.multiply(_7x8)

(which is good because a 3x7 matrix can be multiplied by a 7x8 matrix) but this doesn't:

    _3x7.multiply(_8x7) // doesn't compile as expected

which makes sense as a 3x7 matrix cannot be multiplied by an 8x7 matrix. 

To do

I'm still constructing the matrix with both a type and a value that corresponds to that type. I've not yet worked out how I can just use the type and derive the value inside the matrix. If I work it out, I'll write another blog post.