scala - 来自 Idris -> Scala 的 StringOrInt？

Question

Type Driven Development with Idris介绍这个程序:

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

这样的方法怎么能用Scala写出来？

Answer 1

Alexey 的回答很好，但我认为如果我们将它嵌入到更大的上下文中，我们可以得到这个函数的更通用的 Scala 渲染。

Edwin 展示了 StringOrInt 的用法在函数中 valToString ,

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

换句话说， valToString需要一个 Bool第一个参数将其第二个参数的类型固定为 Int或 String并将后者呈现为 String适合其类型。

我们可以将其转换为 Scala，如下所示，

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
  }

这里我们使用 Scala 的各种有限的依赖类型特性来编码 Idris 的全谱依赖类型。

我们使用单例类型 True.type和 False.type从值(value)层面跨越到类型层面。

我们对函数 StringOrInt 进行编码作为由单例索引的类型类 Bool类型，Idris 函数的每种情况都由一个不同的隐式实例表示。

我们写 valToString作为 Scala 依赖方法，允许我们使用 Bool 的单例类型参数x选择隐式 StringOrInt实例si ，这又决定了类型参数 T它修复了第二个参数的类型 v .

我们对 Idris 中的依赖模式匹配进行编码 valToString通过使用选定的 StringOrInt实例解除 v参数转换成 Scala GADT，它允许 Scala 模式匹配来细化 v 的类型在案件的 RHS 上。

在 Scala REPL 上练习这个，

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

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

很多圈套要跳过，还有很多意外的复杂性，但是，它可以做到。