StringOrInt от Idris -> Scala?

Ответ Алексея хорош, но я думаю, что мы можем получить более обобщенную визуализацию этой функции на 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.

• Мы используем одноэлементные типы True.type и False.type для перехода от уровня значений к уровню типов.
• Мы кодируем функцию StringOrInt как класс типов, индексированный одноэлементными Bool типами, причем каждый случай функции Идриса представлен отдельным неявным экземпляром.
• Мы пишем valToString как метод, зависящий от Scala, что позволяет нам использовать одноэлементный тип Bool аргумента x для выбора неявного StringOrInt экземпляра si, который, в свою очередь, определяет параметр типа T, который фиксирует тип второго аргумента v.
• Мы кодируем сопоставление зависимого шаблона в Idris valToString, используя выбранный экземпляр StringOrInt для поднятия аргумента v в Scala GADT, что позволяет сопоставлению шаблона Scala уточнять тип v в правой части случаев.

Выполнив это на Scala REPL,

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

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

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

Это был бы один подход (но он намного более ограничен, чем в Идрисе):

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.

Я заметил, что пример getStringOrInt не был реализован ни в одном из двух ответов.

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
      True => 10
      False => "Hello"

Я нашел объяснение Майлза Сабина очень полезным, и этот подход основан на его. Мне показалось более интуитивным отделить конструкцию, подобную GADT, от хитрости Scala apply() и попытаться сопоставить мой код с концепциями Idris/Haskell. Я надеюсь, что другие найдут это полезным. Я использую GADT явно в именах, чтобы подчеркнуть принадлежность GADT. Два компонента этого кода: концепция GADT и имплициты Scala.

Вот немного измененное решение Майлза Сабина, которое реализует как getStringOrInt, так и valToString.

sealed trait StringOrIntGADT[T]
case class S(s: String) extends StringOrIntGADT[String]
case class I(i: Int) extends StringOrIntGADT[Int]

/* this compiles with 2.12.6
   before I would have to use ah-hoc polymorphic extract method */
def extractStringOrInt[T](t: StringOrIntGADT[T]) : T =
 t match {
  case S(s) => s
  case I(i) => i
 }
/* apply trickery gives T -> StringOrIntGADT[T] conversion */
sealed trait EncodeInStringOrInt[T] {
   def apply(t: T): StringOrIntGADT[T] 
}
object EncodeInStringOrInt {
 implicit val encodeString : EncodeInStringOrInt[String] = new EncodeInStringOrInt[String]{
        def apply(t: String) = S(t)
     }
 implicit val encodeInt : EncodeInStringOrInt[Int] = new EncodeInStringOrInt[Int]{
        def apply(t: Int) = I(t)
     }
 } 
 /* Subtyping provides type level Boolean */
 sealed trait Bool
 case object True extends Bool
 case object False extends Bool

 /* Type level mapping between Bool and String/Int types. 
    Somewhat mimicking type family concept in type theory or Haskell */
 sealed trait DecideStringOrIntGADT[B, T]
 case object PickS extends DecideStringOrIntGADT[False.type, String]
 case object PickI extends DecideStringOrIntGADT[True.type, Int]

 object DecideStringOrIntGADT {
   implicit val trueInt: DecideStringOrIntGADT[True.type, Int] = PickI
   implicit val falseString: DecideStringOrIntGADT[False.type, String] = PickS
 }

Вся эта работа позволяет мне реализовать достойные версии getStringOrInt и valToString

def pickStringOrInt[B, T](c: DecideStringOrIntGADT[B, T]): StringOrIntGADT[T]=
  c match {
    case PickS => S("Hello")
    case PickI => I(2)
  }

def getStringOrInt[T](b: Bool)(implicit ev: DecideStringOrIntGADT[b.type, T]): T =
  extractStringOrInt(pickStringOrInt(ev))

def valToString[T](b: Bool)(v: T)(implicit ev: EncodeInStringOrInt[T], de: DecideStringOrIntGADT[b.type, T]): String =
  ev(v) match {
    case S(s) => s
    case I(i) => i.toString
  }

Вся эта (досадная) сложность оказывается нужна, например вот это не скомпилируется

//  def getStringOrInt2[T](b: Bool)(implicit ev: DecideStringOrIntGADT[b.type, T]): T =
//    ev match {
//      case PickS => "Hello"
//      case PickI => 2
//    }

У меня есть любимый проект, в котором я сравнил весь код в книге Идриса с Haskell. https://github.com/rpeszek/IdrisTddNotes/wiki (я начинаю работу над Scala-версия этого сравнения.)

С Boolean на уровне типа (что фактически то, что мы имеем здесь) StringOrInt примеры становятся очень простыми, если у нас есть семейства типов (частичные функции между типами). См. нижнюю часть https://github.com/rpeszek/IdrisTddNotes/wiki/Part1_Sec1valToString5.

Это делает код Haskell/Idris намного проще, его легче читать и понимать.

Обратите внимание, что valToString соответствует конструкторам StringOrIntGADT[T]/StringOrIntValue[T], а не непосредственно Bool. Это один из примеров, где сияют Идрис и Хаскелл.