Преодоление некоторых системных ограничений типа Scala - PullRequest
Новая
       63

Преодоление некоторых системных ограничений типа Scala

0 голосов
/ 01 февраля 2020

При попытке реализовать версию простейшего лямбда-исчисления я столкнулся с ограничениями системы типов Scala (2.13.1).

Приведенный ниже код не компилируется, даже хотя я считаю, что все типы могут быть выведены для соответствия через унификация . Итак, являются ли возможности вывода системы типов неполными (или я что-то упустил)?

Если это так, как обойти эти ограничения и исправить приведенный ниже код, чтобы он компилировался (при сохранении его предполагаемой семантики)?

Обратите внимание, что мой код динамически не зависит от аргументов типа c, поэтому проблема не в стирании типа. 

def eval[A <: T[A]](expression: T[A]): A = expression match {
  case n@Nat(_) => n
  case a@Abs(_) => a
  case App(f, e) => eval(eval(f).f(eval(e)))
  case Fix(f) =>
    val s = eval(f).f(s)
    eval(s)
}

sealed trait T[Type <: T[Type]]
final case class Nat(v: BigInt) extends T[Nat]
final case class Abs[I <: T[I], O <: T[O]](f: (=> T[I]) => T[O]) extends T[Abs[I, O]]
final case class App[I <: T[I], O <: T[O]](f: T[Abs[I, O]], e: T[I]) extends T[O]
final case class Fix[I <: T[I], O <: T[O]](f: T[Abs[Abs[I, O], Abs[I, O]]]) extends T[Abs[I, O]]

Текущие ошибки компиляции (исправлены в соответствии с кодом выше) : 

Error:(2, 20) type mismatch;
     found   : n.type (with underlying type Nat)
     required: A
        case n@Nat(_) => n
Error:(3, 20) type mismatch;
     found   : a.type (with underlying type Abs[Any,Any])
     required: A
        case a@Abs(_) => a
Error:(4, 36) inferred type arguments [Any] do not conform to method eval's type parameter bounds [A <: T[A]]
        case App(f, e) => eval(eval(f).f(eval(e)))
Error:(4, 41) type mismatch;
     found   : T[Any]
     required: T[A]
    Note: Any >: A, but trait T is invariant in type Type.
    You may wish to define Type as -Type instead. (SLS 4.5)
        case App(f, e) => eval(eval(f).f(eval(e)))
Error:(4, 40) type mismatch;
     found   : A
     required: T[Any]
    Note: A <: Any (and A <: T[A]), but trait T is invariant in type Type.
    You may wish to define Type as +Type instead. (SLS 4.5)
        case App(f, e) => eval(eval(f).f(eval(e)))
Error:(6, 23) recursive value s needs type
          val s = eval(f).f(s)

PS: Последняя ошибка связана с аннотацией отсутствующего типа. Однако мне нужно получить параметры типа I и O из Fix(f), чтобы указать тип s.

...