StringOrInt от Идриса → Scala?

Ответ 1

Ответ Alexey хороший, но я думаю, что мы можем перейти к более обобщаемому Scala рендерингу этой функции, если мы вставим его в несколько больший контекст.

Эдвин показывает использование 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.

Мы используем singleton-типы True.type и False.type для перехода от уровня значения к типу уровня.
Мы кодируем функцию 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

Множество обручей, которые нужно перепрыгнуть, и много случайной сложности, тем не менее, это можно сделать.

Ответ 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 = ...

Если вы хотите ограничить себя литералами, вы можете использовать singleton-типы 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.

StringOrInt от Идриса &#8594; Scala?

Ответы

Ответ 1

Ответ 2