В чем разница между зависимыми типами и зависимыми типами?

В Scala есть типы, зависящие от пути, но говорят, что Scala не поддерживает зависимую типизацию. В чем разница между зависимыми типами и зависимыми типами?

Насколько я понимаю, зависящие от пути типы - это один из видов зависимых типов.


scala path-dependent-type dependent-type
person rightfold    schedule 25.07.2014    source источник
comment
См. Ответ Майлза Сабина здесь на аналогичный вопрос (ваш вопрос гораздо лучше, поэтому я не отмечаю его как дубликат). ).   -  person Travis Brown    schedule 25.07.2014

Ответы (1)


arrow_upward
6
arrow_downward

Зависимый тип - это тип, который зависит от значения. Тип, зависящий от пути, - это особый вид зависимого типа, в котором тип зависит от пути.

Я не уверен, существует ли термин «зависимый от пути тип» за пределами сообщества Scala. В любом случае вопрос, что такое путь? Для Scala это определено в спецификации языка: в основном это последовательность выбора a.b.c... для значений, не являющихся переменными.

Тип, зависящий от пути, - это тип с путем, например a.T в

class A { type T; def f: T }
def f(a: A): a.T = a.f

Есть и другие виды зависимых типов. Например, в Scala это ожидающее предложение для добавления буквальные типы в язык, чтобы вы могли написать val x: 42.type = 21 + 21.

Чтобы проверить тип программы, использующей зависимые типы, система типов (и компилятор) должны знать семантику этих значений и свои операции. Компилятор Scala знает семантику выбора и может решить, совпадают ли два пути или нет. Для примера, использующего типы на основе литералов, компилятор должен быть расширен, чтобы знать, что означает операция + с целым числом.

person Lukas Rytz    schedule 19.12.2014