Я заинтересован в том, чтобы получить действительно твердое представление о зависимой типизации. Я прочитал большую часть TaPL и прочитал (если не полностью поглощен) «Зависимые типы» в ATTaPL . Я также прочитал и просмотрел кучу статей о зависимой типизации.
Многие дискуссии по теории типов, по-видимому, сосредоточены на добавлении дополнительных функций к предыдущим системам типов, а не на «что будет следующим большим обобщением по сравнению с системой типов X?». Зависимые типы, похоже, являются следующим большим обобщением из System F, но мне еще предстоит найти интуитивный, канонический язык с зависимой типизацией. Многочисленные ссылки на исчисление (индуктивных) конструкций заставляют меня думать, что CoC - это тот язык, но объяснения языка, которые я видел, не кажутся мне очень ясными или интуитивными.
Я ожидаю / думаю, что такой язык будет иметь такие функции, как: (и, пожалуйста, дайте мне знать, если что-то конкретное выскакивает как запутанный или нереалистичный)
- Обобщенная абстракция (может иметь функции из любого домена в иерархии типов в другой, вид -> термин, термин-> тип '' 'и т. Д.)
- Имеет бесконечную иерархию типирования (термины: типы: типы ': типы' ': ...)
- Минимальное количество базовых элементов. Я представляю, что язык утверждает только один элемент для каждого уровня. Например, он может утверждать, что ((): Unit: Type: Type ': ...). Другие элементы построены из этих элементов.
- Сумма и виды продукции являются производными.
Я также ищу объяснение этого языка, который в идеале будет обсуждаться:
- Отношения между абстракцией и количественной оценкой на этом языке. Если они не едины, то объясните, почему они не едины.
- Бесконечная иерархия типов явно
Я задаю этот вопрос, потому что я хочу изучать теорию зависимых типов, а также потому, что я хочу составить руководство, которое, имея небольшой опыт работы с CS, учит использованию и пониманию помощников по проверке и языков с зависимой типизацией.
источник
Twelf - хорошая система доказательства теорем, основанная на LF. Просмотр продвинутых заметок курса, предложенных Фрэнком Пфеннингом, является хорошим введением в теорию и практику ЛФ.
Тем не менее, возможно, это не лучшая первая система для изучения, если вы заинтересованы в конструктивной математике, а не в основах теории типов: LF означает логическую структуру, и это система, используемая для аксиоматизации теорий, и которая не так часто используется в качестве целевая система напрямую. Использование системы, основанной на теории типов Мартина-Лофа, вероятно, является лучшим введением - Дейв упоминает Agda, среди прочего, - возможно, является лучшей отправной точкой, если это ваша цель, поскольку вы можете быстрее приступить к арифметическим и индуктивным типам в такой ситуации. фреймворк.
источник
CoC - наиболее вероятный путь. Просто погрузитесь в Coq и поработайте над хорошим учебником, таким как Software Foundations (в который вовлечены Пирс из TaPL и ATTaPL).
Когда вы почувствуете практические аспекты зависимой типизации, вернитесь к теоретическим источникам: тогда они станут намного понятнее.
Ваш список функций звучит в основном правильно, но, увидев, как они разыгрываются на практике, стоит тысячи характерных черт.
(Другой, немного более продвинутый учебник - сертифицированное программирование Адама Члипалы с зависимыми типами )
источник
Я думал, что эта статья помогла демистифицировать концепцию на элементарном уровне: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html
источник
Взгляните на http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf и более раннюю систему PiSigma, упомянутую там.
источник