dzs dzs - 25 days ago 11
Scala Question

Erroneous Scala code using polymorphic ADT type checks

I'm doing some exercises to better understand IO monads (following Functional Programming in Scala), and managed to write some erroneous code that somehow passed the compilation and caused me some headache.

In the below example, I am writing a stack-safe interpreter of an IO monad. The code is in the pattern matching on a polymorphic Algebraic Data Type (

FlatMap[A, B]
). The error in the code is
k1 andThen k2
; the two functions can't compose because
k1
is returning a different type (
IO[B]
) than what
k2
expects (
B
). The code still type-checks somehow, and it is obviously a typechecking error because, in the runtime, there is a
ClassCastException
at an automatic unboxing (just as if I was using an unsafe cast in Java). There are also no compiler warnings issued.

The code (also found on gist):

object IOMonadExercise extends App {

sealed trait IO[A]
case class Return[A](value: A) extends IO[A]
case class Suspend[A](f: () => A) extends IO[A]
case class FlatMap[A, B](io: IO[A], cont: A => IO[B]) extends IO[B]

object IO {
def apply[A](a: => A): IO[A] = Suspend(() => a)
}

object Interpreter {
def run[A](io: IO[A]): A = {
io match {
case Return(a) => a
case Suspend(f) => f()

case FlatMap(Return(a), cont) => run(cont(a))
case FlatMap(Suspend(f), cont) => run(cont(f()))

// this case compiles for whatever reason but shouldn't type check (k1 returns IO[B] and k2 expects just B)
// accordingly, there is a ClassCastException in the runtime
case FlatMap(FlatMap(io1, k1), k2) => run(FlatMap(io1, k1 andThen k2))

// this case is the one that actually works
// case FlatMap(FlatMap(io1, k1), k2) => run(flatten(io1, k1, k2))
}
}

def flatten[A, B, C](io: IO[A], k1: A => IO[B], k2: B => IO[C]): FlatMap[A, C] = {
FlatMap(io, a => FlatMap(k1(a), k2))
}
}


def sum(i: Int): IO[Int] = {
Stream.range(0, i).foldLeft(IO(0))((io, i) => FlatMap(io, (s: Int) => IO(s + i)))
}

val n = 100000
val sumNIO: IO[Int] = sum(n)
val sumN: Int = Interpreter.run(sumNIO)
println(s"sum of 1..$n by IO loop : $sumN")
println(s"sum of 1..$n by math expr: ${n * (n - 1) / 2}")
assert(sumN == n * (n - 1) / 2)
}


What is going on? Is this a compiler bug? Or is this a known limitation of the type inference? Or is there an explanation for this?

I've tested on both Scala 2.11.8 and on 2.12.0, and the behavior seems to be the same: the code compiles without warnings.

Answer

I think this is a case of the SI-5195 bug. If you construct the nested FlatMap manually, you cannot write that andThen, because all the types are known and k1 and k2 are obviously not composable.

But in that pattern matching types of io1, k1 and k2 are not known in advance, they have to be inferred and as we see they are inferred wrong. [...]

EDIT Here is another try to explain how it type-checks: if you start inferring types for k1 and k2 yourself, you will come up with

  • k1: X => IO[Y] and k2: Y => IO[A] for some X and Y
  • plus from k1 andThen k2 you need IO[Y] <: Y

So does there exist any type Y which satisfies these restrictions? Yes, it's Any. But when you apply it, IO[Y] becomes Suspend[Int] and Y is just Int for which subtype relation doesn't hold.