StringOrInt от Идрис -> Скала?

Question

Type Driven Development с Idris представляет эту программу:

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

Как можно написать такой метод в Scala?

Answer 1

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

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

Осуществляя это на Scala REPL,

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

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

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

Answer 2

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

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.

Answer 3

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

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

Я нашел объяснение Майлза Сабина очень полезным, и этот подход основан на его. Я нашел более интуитивно понятным отделить GADT-подобную конструкцию от хитрости Scala apply() и попытаться сопоставить мой код с концепциями Idris/Haskell. Я надеюсь, что другие найдут это полезным. Я использую GADT явно в именах, чтобы подчеркнуть GADT-ность. 2 компонента этого кода: концепция 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-версией этого сравнения.)

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

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

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