TwoFace values: closing the gap between run&compile time functionality

Language Design
1

Introduction

In Scala, we have two possible representations for numbers and strings, either as literal constants or runtime values. SIP23 (implemented in TypeLevel Scala and Dotty) adds literal types support. The refined library enables constraining function arguments, while the singleton-ops library enables constraining and performing operations on literal types. Nat from shapeless also provides compile-time operation, but it is disregarded in this discussion. While the compiler and libraries offer great flexibility, they may lead to a very verbose code if we wish to support both compile-time and run-time values.

Why support both compile-time and run-time values?
Well, it depends on the use case, but generally it is best to apply compile-time operations and checks when possible, and if not possible, fall-back to run-time operations and checks.

Example: A fixed-sized vector

Let’s assume we are required to implement a fixed-sized vector with a given length.

  • length must be positive.
  • A vector can be concatenated with another vector. The result is a vector with a length as the sum of the two vector lengths.
  • A vector can sum its elements with another vector’s elements. The two vectors must have the same length for the operation to work.

We will now explore different implementation options, without the backend implementation of the vector elements.

length as a run-time integer value

class FixedSizeVector private (val length : Int) {
  def concat(that : FixedSizeVector) = FixedSizeVector.create(this.length + that.length)
  def +(that : FixedSizeVector) = {
    require(this.length == that.length, "lengths must be the same for addition")
    FixedSizeVector.create(this.length)
  }
}
object FixedSizeVector {
  protected def create(length : Int) = new FixedSizeVector(length)
  def apply(length : Int) = {
    require(length > 0, "length must be positive")
    create(length)
  }
}

val v5 = FixedSizeVector(5) //works
var four = 4
val v4 = FixedSizeVector(four) //works
val fail1 = FixedSizeVector(-5) //fails at run-time
val v9 = v5 concat v4 //works
val v5_add = v5 + v5 //works
val fail2 = v5 + v4 //fails at run-time

:white_check_mark: Simple.
:x: Run-time only. Very unsafe (Can only check length at run-time).

length as a compile-time literal value

class FixedSizeVector[L <: Int with Singleton] private (val length : L) {
  def concat[R <: Int with Singleton](that : FixedSizeVector[R]) = FixedSizeVector.create(this.length + that.length) //COMPILE ERROR!!!
  def +(that : FixedSizeVector[L]) = FixedSizeVector.create(this.length)
}
object FixedSizeVector {
  protected def create[L <: Int with Singleton](length : L) = new FixedSizeVector(length)
  def apply[L <: Int with Singleton](length : L) = {
    require(length > 0, "length must be positive")
    create(length)
  }
}

val v5 = FixedSizeVector(5) //works
var four = 4
val v4 = FixedSizeVector(four) //does not work (run-time value not supported)
val fail1 = FixedSizeVector(-5) //fails at run-time
val v9 = v5 concat v4 //does not work (implementation is not possible)
val v5_add = v5 + v5 //works
val fail2 = v5 + FixedSizeVector(4) //fails at compile-time

:white_check_mark: Compile-time protection for addition.
:x: concat does not work at all and is impossible to implement with just compiler externals.
:x: Does not accept run-time values.
:x: Length check is still done at run-time.

length as a compile-time literal type

class FixedSizeVector[L <: Int with Singleton] private (implicit l : ValueOf[L]) {
  val length : Int = valueOf[L]
  def concat[R <: Int with Singleton](that : FixedSizeVector[R]) = FixedSizeVector.create[???] //IMPOSSIBLE
  def +(that : FixedSizeVector[L]) = FixedSizeVector.create[L]
}
object FixedSizeVector {
  protected def create[L <: Int with Singleton](implicit l : ValueOf[L]) = new FixedSizeVector[L]
  def apply[L <: Int with Singleton](implicit l : ValueOf[L]) = {
    require(valueOf[L] > 0, "length must be positive")
    create[L]
  }
}

val v5 = FixedSizeVector[5] //works
var four = 4
val v4 = FixedSizeVector[four] //not possible, of course
val v0_fail = FixedSizeVector[0] //fails at run-time
val v9 = v5 concat v4 //does not work (implementation is not possible)
val v5_add = v5 + v5 //works
val v9_fail = v5 + FixedSizeVector[4] //fails at compile-time

:white_check_mark: Compile-time protection for addition.
:x: concat does not work at all and is impossible to implement with just compiler externals.
:x: Does not accept run-time values.
:x: Length check is still done at run-time.
:x: Awkward calling with length in just type position.

length as a compile-time literal singleton-ops operation - Method 1

import singleton.ops._
type CheckPositive[I] = RequireMsg[I > 0, "length must be positive"]

class FixedSizeVector[L <: Int with Singleton] private (val length : Int) {
  def concat[R <: Int with Singleton](that : FixedSizeVector[R])(implicit l : SafeInt[L + R]) = FixedSizeVector.create[l.Out](l.value)
  def + (that : FixedSizeVector[L]) = FixedSizeVector.create[L](length)
}
object FixedSizeVector {
  protected def create[L <: Int with Singleton](length : Int) = new FixedSizeVector[L](length)
  implicit def apply[L <: Int with Singleton](implicit check : CheckPositive[L], length : SafeInt[L]) = create[L](length)
  def apply[L <: Int with Singleton](length : L)(implicit check : CheckPositive[L]) = create[L](length)
}

val v5 = FixedSizeVector[5] //works
var four = 4
val v4 = FixedSizeVector(four) //not possible, compile-time only
val v0_fail = FixedSizeVector[0] //fails at compile-time
val v9 = v5 concat FixedSizeVector(4) //works
val v5_add = v5 + v5 //works
val v9_fail = v5 + FixedSizeVector[4] //fails at compile-time
val v3 = implicitly[FixedSizeVector[3]] //works
val v6 = FixedSizeVector(3+3) //works
val v6_fail = FixedSizeVector[3+3] //fails. Type operation is not an `Int with Singleton`

:white_check_mark: Complete compile-time protection and working functionality.
:white_check_mark: Dual use of length in both type position and value position.
:white_check_mark: Can be constructed implicitly.
:x: Does not accept run-time values.
:x: Does not accept type operation in length type position.

length as a compile-time literal singleton-ops operation - Method 2

import singleton.ops._
type CheckPositive[I] = RequireMsg[I > 0, "length must be positive"]

class FixedSizeVector[L] private (val length : Int) {
  def concat[R](that : FixedSizeVector[R]) = FixedSizeVector.create[L+R](this.length + that.length)
  def + (that : FixedSizeVector[L]) = FixedSizeVector.create[L](length)
}
object FixedSizeVector {
  protected def create[L](length : Int) = new FixedSizeVector[L](length)
  implicit def apply[L](implicit check : CheckPositive[L], length : SafeInt[L]) = create[L](length)
  def apply[L <: Int with Singleton](length : L)(implicit check : CheckPositive[L]) = create[L](length)
}

val v5 = FixedSizeVector[5] //works
var four = 4
val v4 = FixedSizeVector(four) //not possible, compile-time only
val v0_fail = FixedSizeVector[0] //fails at compile-time
val v9 = v5 concat FixedSizeVector(4) //works, but returns FixedSizeVector[5+4] and not FixedSizeVector[9]
val v5_add = v5 + v5 //works
val v9_fail = v5 + FixedSizeVector[4] //fails at compile-time
val v3 = implicitly[FixedSizeVector[3]] //works
val v6 = FixedSizeVector(3+3) //works
val v7 : FixedSizeVector[7] = FixedSizeVector[3+4] //works (implicit conversion)

:white_check_mark: Complete compile-time protection and working functionality.
:white_check_mark: Dual use of length in both type position and value position.
:white_check_mark: Can be constructed implicitly.
:white_check_mark: Accepts type operation in length type position.
:white_check_mark: Less implicits.
:x: concat returns a type operation in length and not a number (see comment of v9). However, implicit conversion produces evidence of equivalence in literal value (e.g., val a : 5+4 = 9; val b : 3+3 = implicitly[2*3])
:x: Does not accept run-time values.

length as a compile-time literal refined value - To be completed
Maybe I’ll add this later (feel free to comment with your own solution)

length as a compile-time literal Nat value - To be completed
Maybe I’ll add this later (feel free to comment with your own solution)

Even bigger problems :angry:

Lets assume we are willing to go ahead and create a FixedSizeVector.Safe and FixedSizeVector.Unsafe for compile&run time usage, respectively. What happens if we want to interact between safe and unsafe vectors (e.g, concatenating safe and unsafe vectors should result in an unsafe vector)? We end up duplication functionality in various combination of safety. Horrible!

TwoFace and Checked values to the rescue…

In a recent branch of singleton-ops, two value classes were added under a twoface sub-package. The package adds TwoFace.XXX[T] and Checked.XXX[T, Cond, Param, Msg], where XXX can be Char, Int, Long, Float, Double, String, and Boolean.

TwoFace

TwoFace holds both run-time values and type representation.

import singleton.ops._
import singleton.twoface._

val tf2_a = TwoFace.Int(2) //returns TwoFace.Int[2] {val value = 2}
val tf2_b = TwoFace.Int[2]  //returns TwoFace.Int[2] {val value = 2}
var two = 2
val tf2_c = TwoFace.Int(two)  //returns TwoFace.Int[Int] {val value = 2}
tf2_a + tf2_b //returns TwoFace.Int[4] {val value = 4}
tf2_a + tf2_c //returns TwoFace.Int[4+Int] {val value = 4}. The type remains as its non-literal representation.

The type T holds the literal type or a fall-back indication if non-literal representation is available.

Checked

Checked is a constrained TwoFace.

Example

Let’s take a look at our FixedSizeVector now.

import singleton.ops._
import singleton.twoface._

class FixedSizeVector[L] private (val length : TwoFace.Int[L]) {
  def concat[R](that : FixedSizeVector[R]) = FixedSizeVector.create(this.length + that.length)
  def +(that : FixedSizeVector[L]) = FixedSizeVector.create(this.length)
}

object FixedSizeVector {
  //For compile-time check
  protected type CondCheckedLength[L, P] = L > 0
  protected type ParamCheckedLength = 0
  protected type MsgCheckedLength[L, P] = "Length must be positive (received value of " + ToString[L] + ")"
  type CheckedLength[L] = Checked.Int[L, CondCheckedLength, ParamCheckedLength, MsgCheckedLength]

  //For run-time check
  implicit object RuntimeCheckedLength extends Checked.Runtime[Int, Int, CondCheckedLength, MsgCheckedLength] {
    def cond(l : Int, p : Option[Int]) : scala.Boolean = l > 0
    def msg(l : Int, p : Option[Int]) : java.lang.String = s"Length must be positive (received value of $l)"
  }

  protected def create[L](length : TwoFace.Int[L]) : FixedSizeVector[L] = new FixedSizeVector[L](length)
  def apply[L](checkedLength : CheckedLength[L]) = create(checkedLength.unsafeCheck())
  implicit def apply[L](implicit checkedLength : CheckedLength[L], di : DummyImplicit) = create(checkedLength.unsafeCheck())
}

:white_check_mark: Supports both compile-time and run-time constrained functionality.
:white_check_mark: If compile-time check passed, run-time check is not performed (should be dropped from the byte code).
:white_check_mark: Compile-time calculations can save run-time calculations (still unknown if the compiler identified the compiled execution as final and removed the run-time byte code).
:white_check_mark: Dual use of length in both type position and value position.
:white_check_mark: Can be constructed implicitly (the safe values).
:white_check_mark: Accepts type operation in length type position.
:white_check_mark: No more implicits, just use TwoFace and Checked :slight_smile:
:white_check_mark: Equivalent error message between run-time and compile-time, supporting placing values inside the error message for better reporting.
:x: concat still returns a type operation in length and not a number, but this is insignificant.

Discussion

Basically, I wish to hear your thoughts on this. Is this truly the right way to do this? Can’t the compiler provide us the means to achieve this with less mechanics?

2 Likes
2

Thanks for detailed post, it’s very interesting theme. I think, we should have internal mechanism for resolve run-time values.
Example:

// doesn't work
val v5 = FixedSizeVector(5) //works
var four = 4
val v4 = FixedSizeVector(four) //does not work (run-time value not supported)

// but...
if(four == 4){
  // in this scope we can guarantee `four` equal 4
  val v4 = FixedSizeVector(four) // works 
  v4 + v5 // compile-time error
}

like in LiquidHaskell, you just write contract and analyzer(or compiler) tries to prove it. If it doesn’t have enough information about value you should write explicit check for this value.
Or we should have cleaner API for this checks, which will be in standard library or language.