StringOrInt从Idris – > Scala？

Edwin在函数valToString中显示了使用StringOrInt,

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

换句话说,valToString采用一个Bool第一个参数,它将其第二个参数的类型固定为Int或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从值级别到类型级别.
>我们将函数StringOrInt编码为由单例Bool类型索引的类型类,每种情况下的Idris函数由不同的隐式实例表示.
>我们将valToString写为Scala依赖方法,允许我们使用Bool参数x的单例类型来选择隐式StringOrInt实例si,后者又决定了固定第二个参数类型v的类型参数T.
>我们通过使用所选的StringOrInt实例将v参数解压缩到Scala GADT中,使得Scala模式匹配可以改善案例RHS上的v类型,从而对Idris valToString中的依赖模式进行编码.

在Scala REPL上执行此操作,

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

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

许多篮球跳过,很多偶然的复杂性,但是,可以做到这一点.