“If” statements at compile time

Justin Luebke on unspash

“If” statements at run-time

def sqrt(x: Double): Double =
if x < 0 then throw new IllegalArgumentException("can't take square root of negative numbers")
else math.sqrt(x)

“If” statements at compile time

trait RuntimeList[+A]:
def toMap[K, V]: Map[K, V]
class NonEmptyRuntimeList[+A](head: A, tail: Run-timeList[A]) extends RuntimeList[A]:
def toMap[K, V]: Map[K, V] = (head match {
case h: (K, V) => Map(h._1 -> h._2)
case _ => throw new RuntimeException("elements of the list must be pairs!")
}) ++ tail.toMap[K, V]
object EmptyRuntimeList extends RuntimeList[Nothing]:
def toMap[K, V]: Map[K, V] = Map.empty
@ new NonEmptyRuntimeList(3, EmptyRuntimeList).toMap[Int, String]
java.lang.RuntimeException: elements of the list must be pairs!
@ new NonEmptyRuntimeList((3, "hello"), EmptyRuntimeList).toMap[Int, String]
res2: Map[Int, String] = Map(3 -> "hello")
def toMap[K, V](using ev: A <:< (K, V)): Map[K, V]
[imaginary language]
if A is a pair then "let the thing compile"
else "crash, aka, compile error"

An equality check

def print()(using ev: Unit =:= A): String = print(ev(()))
def printAsPair[K, V](a: A)(using ev: A =:= (K, V)): String =
val (key, value) = ev(a)
s"$key: $value"
def print()(using A =:= Nothing): String = "Nothing there!"

Note: the provided instances are often called ev (or evN if you need several of them). It stands for “evidence”, because we are asking the compiler for a piece of evidence that our types satisfy some predicate.

What about “not equal”?

[imaginary language]
if A != Foo then "let it go"
else "crash, aka don't compile"
type IsNotNothing[A] <: Boolean = A match {
case Nothing => false
case _ => true
}
trait IO[E, A]:
// elided content ...
def mapError[F](f: E => F)(using IsNotNothing[E] =:= true): IO[F, A] = ??? // do your thing
val ioNothing: IO[Nothing, Int] = ???
ioNothing.mapError(_ => 2)
// [error] 18 | ioNothing.mapError(_ => 2)
// [error] | ^
// [error] |Cannot prove that IsNotNothing[Nothing] =:= (true : Boolean).

Note: as we said for evidence earlier, we see that the compiler uses the mathematical nomenclature of “proving” things.

Other alternatives

extension [K, V](ls: List[(K, V)])
def toMap: Map[K, V] = ???

Related works

Closing words

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store