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?
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.
True.type
and False.type
to cross from the value level to the type level.StringOrInt
as a type class indexed by the singleton Bool
types, each case of the Idris function being represented by a distinct implicit instance.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
.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.
This would be one approach (but it's a lot more limited than in Idris):
trait Type {
type T
}
def stringOrInt(x: Boolean) = // Scala infers Type { type T >: Int with String }
if (x) new Type { type T = Int } else new Type { type T = String }
and then to use it
def f(t: Type): t.T = ...
If you are willing to limit yourself to literals, you could use singleton types of true
and false
using Shapeless. From examples:
import syntax.singleton._
val wTrue = Witness(true)
type True = wTrue.T
val wFalse = Witness(false)
type False = wFalse.T
trait Type1[A] { type T }
implicit val Type1True: Type1[True] = new Type1[True] { type T = Int }
implicit val Type1False: Type1[False] = new Type1[False] { type T = String }
See also Any reason why scala does not explicitly support dependent types?, http://www.infoq.com/presentations/scala-idris and http://wheaties.github.io/Presentations/Scala-Dep-Types/dependent-types.html.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With