Блог

Главная - Вопросы по программированию - Зависящий от Scala тип не компилируется

Зависящий от Scala тип не компилируется

#scala #dependent-type #path-dependent-type

#scala #зависимый тип #тип, зависящий от пути

Вопрос:

Этот код должен компилироваться в Scala:

 trait Pipe {
  type Input
  type Output
  def apply(input: Input): Output
}

object Pipe {
  trait Start extends Pipe {
    override type Input = Seq[String]
  }

  abstract class Connect(val prev: Pipe) extends Pipe {
    override type Input = prev.Output
  }
}

object Pipe1 extends Pipe.Start {
  override type Output = Int
  override def apply(input: Input): Output = 
   input.length
}

object Pipe2 extends Pipe.Connect(prev = Pipe1) {
  override type Output = Boolean
  override def apply(input: Input): Output = 
   input%2 == 0
}

Pipe1 компилируется нормально, но Pipe2 не удается скомпилировать с: 

 value % is not a member of Pipe2.this.Input
     input%2 == 0
          ^

Я знаю, что могу решить это с помощью дженериков вместо зависимых типов, но это должно работать так, как Pipe2.Input должна быть проверка типов Int из Pipe1.Output

Ответ №1:

prev = Pipe Дело в том, что при вызове конструктора указан неправильный путь, компилятор не может привязать к нему какую-либо информацию о типе, поэтому в итоге вы получаете довольно бесполезный, prev.Output =:= Input для некоторого неопределенного prev: Pipe значения, для чего-то установлено значение в конструкторе.

С минимальными изменениями он работает так, как ожидалось:

 trait Pipe {
  type Input
  type Output
  def apply(input: Input): Output
}

object Pipe {
  trait Start extends Pipe {
    override type Input = Seq[String]
  }

  abstract class Connect extends Pipe {
    val prev: Pipe
    override type Input = prev.Output
  }

}

object Pipe1 extends Pipe.Start {
  override type Output = Int
  override def apply(input: Input): Output = 
    input.length
}

object Pipe2 extends Pipe.Connect {
  val prev = Pipe1
  override type Output = Boolean
  override def apply(input: Input): Output = input % 2 == 0
}

Вот почему он называется зависимым от пути (не зависит от элемента, не зависит от значения и т.д.).

Комментарии:

1. Это работает… но разве компилятор не должен знать? Аргументом Connect не может быть просто «некоторый канал`, а конкретный канал с определенным типом вывода?

2. @pathikrit Компилятор видит это следующим образом: 1) Существует переменная-член prev: Pipe . 2) Существует определение типа type Input = prev.Output . 3) Существует конструктор, который устанавливает prev значение some Pipe . Вот и все. Конструктор может делать что угодно. Он может проигнорировать аргумент и установить prev какое-то другое Pipe значение случайным образом. Он мог бы хэшировать аргумент и передавать хэш в нейронную сеть, которая конфабулирует другой Pipe экземпляр. Нет ничего, что связывало бы список аргументов конструктора с переменной-членом. Они просто разделяют имя prev , не более того.

3. Должна ли система типов языка X сделать шаг Y к какому-то более сложному варианту Z теории полностью зависимых типов — я не знаю, я бы предпочел воздержаться от заявлений типа «разработчики языка X должны реализовать Y», потому что такие заявления, как правило, намного проще сделать, чем выполнить фактическую реализацию. Можно ли представить, что существует более сложная система типов, которая заметила бы это? Да, это можно себе представить. Должны ли разработчики Scala попытаться реализовать это? Я не знаю.

Ответ №2:

Ответ @Andrey-Tyukin работает выше. Я также нашел эту работу вокруг:

 trait Pipe {
  type Input
  type Output
  def apply(input: Input): Output
}

object Pipe {
  trait Start extends Pipe {
    override type Input = Seq[String]
  }

  abstract class Connect[O](val prev: Pipe.Emitting[O]) extends Pipe {
    override type Input = O
  }

  type Emitting[O] = Pipe {type Output = O}
}

object Pipe1 extends Pipe.Start {
  override type Output = Int
  override def apply(input: Input): Output = 
   input.length
}

object Pipe2 extends Pipe.Connect(prev = Pipe1) {
  override type Output = Boolean
  override def apply(input: Input): Output = 
   input%2 == 0
}

Комментарии:

1. Этот O тип больше не зависит ни от каких путей: вы используете вариант Aux -pattern для перемещения элемента типа Output в универсальный тип, а затем используете универсальный тип для его установки Input . Я думаю, что стоило бы попытаться избавиться от элементов type Input и type Output и просто представить тип ввода / вывода как универсальные типы. Если тип относится к одному компоненту, переведите его в тип member; Если это «описание интерфейса» для подключения нескольких компонентов, сделайте его универсальным, к которому легко получить доступ извне.