来自Idris的StringOrInt - > Scala？

Question

使用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从值级别跨越到类型级别.
• 我们将函数编码StringOrInt为由单例Bool类型索引的类型类,Idris函数的每个案例由不同的隐式实例表示.
• 我们编写valToString一个Scala依赖方法,允许我们使用Bool参数的单例类型x来选择隐式StringOrInt实例si,而后者又确定了T修复第二个参数类型的类型参数v.
• 我们valToString通过使用所选StringOrInt实例将v参数提升到Scala GADT来编码Idris中的依赖模式匹配,该Scala GADT允许Scala模式匹配来细化v案例的RHS上的类型.

在Scala REPL上执行此操作,

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

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

尽管如此,还是可以通过大量的箍跳,以及许多意外的复杂性.

Answer 2

这将是一种方法(但它比伊德里斯更有限):

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 }

然后使用它

def f(t: Type): t.T = ...

如果您愿意将自己限制为文字,可以使用单身类型true并false使用Shapeless.从例子:

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 }

另请参阅scala未明确支持依赖类型的任何原因？,http://www.infoq.com/presentations/scala-idris和http://wheaties.github.io/Presentations/Scala-Dep-Types/dependent-types.html.