StringOrInt from Idris -> Scala?

Question

Type Driven Development with Idris presents this program:

StringOrInt : Bool -> Type
StringOrInt x = case x of
                  True => Int
                  False => String

How can such a method be written in Scala?

Answer 1

Alexey's answer is good, but I think we can get to a more generalizable Scala rendering of this function if we embed it in a slightly larger context.

Edwin shows a use of StringOrInt in the function valToString,

valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
                         True => cast val
                         False => val

In words, valToString takes a Bool first argument which fixes the type of its second argument as either Int or String and renders the latter as a String as appropriate for its type.

We can translate this to Scala as follows,

sealed trait Bool
case object True extends Bool
case object False extends Bool

sealed trait StringOrInt[B, T] {
  def apply(t: T): StringOrIntValue[T]
}
object StringOrInt {
  implicit val trueInt: StringOrInt[True.type, Int] =
    new StringOrInt[True.type, Int] {
      def apply(t: Int) = I(t)
    }

  implicit val falseString: StringOrInt[False.type, String] =
    new StringOrInt[False.type, String] {
      def apply(t: String) = S(t)
    }
}

sealed trait StringOrIntValue[T]
case class S(s: String) extends StringOrIntValue[String]
case class I(i: Int) extends StringOrIntValue[Int]

def valToString[T](x: Bool)(v: T)(implicit si: StringOrInt[x.type, T]): String =
  si(v) match {
    case S(s) => s
    case I(i) => i.toString
  }

Here we are using a variety of Scala's limited dependently typed features to encode Idris's full-spectrum dependent types.

• We use the singleton types True.type and False.type to cross from the value level to the type level.
• We encode the function StringOrInt as a type class indexed by the singleton Bool types, each case of the Idris function being represented by a distinct implicit instance.
• We write valToString as a Scala dependent method, allowing us to use the singleton type of the Bool argument x to select the implicit StringOrInt instance si, which in turn determines the type parameter T which fixes the type of the second argument v.
• We encode the dependent pattern matching in the Idris valToString by using the selected StringOrInt instance to lift the v argument into a Scala GADT which allows the Scala pattern match to refine the type of v on the RHS of the cases.

Exercising this on the Scala REPL,

scala> valToString(True)(23)
res0: String = 23

scala> valToString(False)("foo")
res1: String = foo

Lots of hoops to jump through, and lots of accidental complexity, nevertheless, it can be done.