Делают ли Self Types исчисление индуктивных конструкций устаревшим?

10

Self Types - это расширение исчисления конструкций [1], которое позволяет языку выражать алгебраические типы данных, закодированные с помощью кодировки Скотта. Кодирование Скотта предоставляет возможность сопоставления с образцом O(1), что является одним из основных мотиваторов для включения индуктивных определений в CC. Тем не менее, Self Types создают гораздо более простую и элегантную базовую теорию и, по-видимому, не менее мощны.

Делают ли Self Types, с теоретической точки зрения, CIC устаревшим, или все же есть какой-то аспект, по которому CIC благоприятен по отношению к Self Tyes?

[1] http://staff.computing.dundee.ac.uk/pengfu/document/talks/mvd-2012.pdf

lambda-calculus type-theory functional-programming inductive-datatypes MaiaVictor
источник
2
Может быть, я что-то упускаю, но почему самотипы не являются обычными рекурсивными типами (например, необоснованными?). Это не цель для всех зависимых типов вещей, но, безусловно, это импорт в CiC, чтобы быть надежным. Связанная презентация также имеет тип по типу, но я не думаю, что это связано / необходимо.
Даниэль Гратцер
@jozefg Действительно: «Будет логически непоследовательность, но не проблема для программ». Вы должны опубликовать это как ответ.
Жиль "ТАК - перестань быть злым"
Разве этот комментарий не адресован * : *, @GIlles, не для Self?
MaiaVictor
@srvm с правилами написания, которые они написали, оба являются источником необоснованности. У вас есть ссылка на газету?
Даниэль Гратцер
@jozefg Полагаю, это так: staff.computing.dundee.ac.uk/pengfu/document/papers/…
Галлей

Ответы:

5

Я не эксперт в этой работе, но мне кажется, что основной проблемой является отсутствие доказательства SN, даже с ограничениями. Хотя эти доказательства заведомо хитры, даже когда исчисление верно, поэтому я бы уделил ему немного времени. Работа, безусловно, очень перспективная.

Следует отметить, что эти ограничения на самом деле довольно нетривиальны для выражения, что является большой частью сложности формулировки индуктивных семейств в CIC. Реальным преимуществом такого подхода было бы сжатое формулирование этих условий.

Это была довольно давняя открытая проблема иметь зависимо типизированный язык, который

  • Последовательная / Нормализация
  • Можно выразить все семейства типов из Coq (или даже Agda)
  • Позволяет для простого выражения рекурсии по этим семьям
  • Простой или имеет небольшое количество основных конструкций ( ).Π,Σ,μ

Одна такая попытка, о которой я знаю, - это язык Altenkirch & al , в котором также не хватает полного мета-теоретического изучения (а также непоследовательности без дополнительных ограничений).ΠΣ

Коди
источник