Какую наиболее интуитивную теорию зависимых типов я смог выучить?

46

Я заинтересован в том, чтобы получить действительно твердое представление о зависимой типизации. Я прочитал большую часть TaPL и прочитал (если не полностью поглощен) «Зависимые типы» в ATTaPL . Я также прочитал и просмотрел кучу статей о зависимой типизации.

Многие дискуссии по теории типов, по-видимому, сосредоточены на добавлении дополнительных функций к предыдущим системам типов, а не на «что будет следующим большим обобщением по сравнению с системой типов X?». Зависимые типы, похоже, являются следующим большим обобщением из System F, но мне еще предстоит найти интуитивный, канонический язык с зависимой типизацией. Многочисленные ссылки на исчисление (индуктивных) конструкций заставляют меня думать, что CoC - это тот язык, но объяснения языка, которые я видел, не кажутся мне очень ясными или интуитивными.

Я ожидаю / думаю, что такой язык будет иметь такие функции, как: (и, пожалуйста, дайте мне знать, если что-то конкретное выскакивает как запутанный или нереалистичный)

  • Обобщенная абстракция (может иметь функции из любого домена в иерархии типов в другой, вид -> термин, термин-> тип '' 'и т. Д.)
  • Имеет бесконечную иерархию типирования (термины: типы: типы ': типы' ': ...)
  • Минимальное количество базовых элементов. Я представляю, что язык утверждает только один элемент для каждого уровня. Например, он может утверждать, что ((): Unit: Type: Type ': ...). Другие элементы построены из этих элементов.
  • Сумма и виды продукции являются производными.

Я также ищу объяснение этого языка, который в идеале будет обсуждаться:

  • Отношения между абстракцией и количественной оценкой на этом языке. Если они не едины, то объясните, почему они не едины.
  • Бесконечная иерархия типов явно

Я задаю этот вопрос, потому что я хочу изучать теорию зависимых типов, а также потому, что я хочу составить руководство, которое, имея небольшой опыт работы с CS, учит использованию и пониманию помощников по проверке и языков с зависимой типизацией.

(Крест отправил в Reddit)

Джон Сальватье
источник

Ответы:

35

Есть несколько разных подходов к этому:

  1. Зависимая теория типов . Вероятно, это не самый простой способ изучения зависимых типов, но вы можете, например, взглянуть на статьи «Исчисление конструкций» и их варианты, системы чистых типов и статью Мартина Хофманна о синтаксисе и семантике зависимых типов.

  2. Доказательство теорем . Во-первых, взгляните на мой ответ на смежный вопрос: как бы я изучил основную теорию ассистента по доказательству Coq? ,

  3. ΠΣсреди других. И, конечно, есть книга Адама Члипалы, приведенная в ответе Марка Хаманна.

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

Дэйв Кларк
источник
Я могу найти документы для Epigram, но я не могу найти фактическую загрузку для Epigram, только еще не законченную Epigram 2. Есть идеи?
Джон Сальватье
1
Вы нашли: e-pig.org/darcs/Pig09/web ? Эпиграмма доступна в нижней части страницы.
Дейв Кларк,
3
Эпиграмма 1 практически не поддерживается, поскольку AFAIK уже давно - автор использует Agda в эти дни (работая над Эпиграммой 2 в стороне).
Blaisorblade
В 2019 году я не думаю, что Epigram 2 когда-либо случится, но есть Idris (и Idris 2!) Сейчас.
xrq
14

λπ

Twelf - хорошая система доказательства теорем, основанная на LF. Просмотр продвинутых заметок курса, предложенных Фрэнком Пфеннингом, является хорошим введением в теорию и практику ЛФ.

Тем не менее, возможно, это не лучшая первая система для изучения, если вы заинтересованы в конструктивной математике, а не в основах теории типов: LF означает логическую структуру, и это система, используемая для аксиоматизации теорий, и которая не так часто используется в качестве целевая система напрямую. Использование системы, основанной на теории типов Мартина-Лофа, вероятно, является лучшим введением - Дейв упоминает Agda, среди прочего, - возможно, является лучшей отправной точкой, если это ваша цель, поскольку вы можете быстрее приступить к арифметическим и индуктивным типам в такой ситуации. фреймворк.

Чарльз Стюарт
источник
10

CoC - наиболее вероятный путь. Просто погрузитесь в Coq и поработайте над хорошим учебником, таким как Software Foundations (в который вовлечены Пирс из TaPL и ATTaPL).

Когда вы почувствуете практические аспекты зависимой типизации, вернитесь к теоретическим источникам: тогда они станут намного понятнее.

Ваш список функций звучит в основном правильно, но, увидев, как они разыгрываются на практике, стоит тысячи характерных черт.

(Другой, немного более продвинутый учебник - сертифицированное программирование Адама Члипалы с зависимыми типами )

Марк Хаманн
источник
«интуитивный» может быть камнем преткновения здесь: в CoC / CIC гораздо больше интуиции, чем просто зависимая типизация. Это хорошая конечная цель - на мой взгляд, выбор на самом деле между Coq и Twelf - но, возможно, не лучший первый шаг к «получению действительно твердого понимания зависимой типизации».
Чарльз Стюарт
@ Чарльз: Ваша точка зрения принята. Я все еще думаю, что с практической точки зрения это хорошая ставка. Несмотря на то, что полное понимание CoC / CIC может быть более сложным делом, Coq (плюс наличие хороших базовых учебных пособий для него) позволяет легко сосредоточиться на изучении только аспектов программирования или только базовых аспектов помощника по проверке (как ваши интересы диктуют) еще до того, как вы уловили все сложности. Я думаю, что это квалифицируется как «интуитивно понятное» для человека, не являющегося теоретиком.
Марк Хаманн