Связь между расселевской теорией типов и системами типов

12

Недавно я понял, что существует некоторая связь между теорией Расселла и системами типов, как, например, в Haskell. На самом деле, некоторые из обозначений типов в Хаскеле, похоже, имеют предшественники в теории типов. Но, IMHO, мотивация Рассела в 1908 году состояла в том, чтобы избежать парадокса Рассела, и я не уверен, как это связано с системами типов в информатике.

Является ли парадокс Рассела в той или иной форме чем-то, о чем нам нужно было бы беспокоиться, например, если бы у нас не было хорошей системы типов в данном языке?

Фрэнк
источник

Ответы:

8

«Теория типов» в смысле языков программирования и в смысле Рассела тесно связана. Фактически, современная область теории зависимых типов стремится обеспечить конструктивную основу для математики. В отличие от теории множеств, большинство исследований в области теории типов основано на математика выполняется в помощниках по доказательствам, таких как Coq, NuPRL или Agda. Таким образом, доказательства, выполненные в этих системах, не только «формализуемы», но фактически полностью формальны и проверяются машиной. Используя тактику и другие методы автоматизации доказательств, мы пытаемся сделать доказательство с помощью этих Системы «высокого уровня» и, таким образом, напоминают неформальную математику, но поскольку все проверено, у нас гораздо лучшие гарантии на правильность.

Смотрите здесь

Типы в обычных языках программирования, как правило, более ограничены, но мета-теория та же самая.

Нечто похожее на парадокс Рассела является основной проблемой в теории зависимых типов. В частности, имея

Type : Type

обычно приводит к противоречию. Coq и подобные работы, вложив вселенные

Type_0 : Type_1

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

В некоторых системах (Agda, Idris) правило type in type включается с помощью флага компиляции. Это делает логику непоследовательной, но часто облегчает предварительное программирование / проверку.

Даже в более распространенных языках иногда появляется парадокс Рассела. Например, в Хаскеле возможно кодирование парадокса Рассела, сочетающего непредсказуемость и случай открытого типа, что позволяет строить расходящиеся термины без рекурсии даже на уровне типа. Haskell является `` непоследовательным '(когда интерпретируется как логика обычным способом), так как он поддерживает рекурсию как на уровне типов, так и на уровне значений, не говоря уже об исключениях. Тем не менее, этот результат довольно интересен.

Филипп JF
источник
Спасибо за ваш подробный ответ - что касается доказательств, то до сих пор не видно никаких инструментов для доказательства правильности программ на императивных языках, таких как C ++ или Java, верно? Я бы с удовольствием положил руки на одну из них ... Я понимаю, что это полная касательная. Я знаю о Coq и Agda, но они не были подходящими инструментами для доказательства правильности программ, написанных на C ++ или Java.
Фрэнк
3
Есть несколько инструментов. Несколько для C, много для Java и тонны для Ada. См. Например: Почему (Java, C, Ada), Krakatoa (Java) или SPARK (подмножество Ada с очень хорошим инструментарием). Для C ++, хотя, не так много. Вы также можете быть заинтересованы в YNot (Coq DSL).
Филипп JF
3

Ты прав насчет мотивации Рассела. Его парадокс преследует все теории множеств, которые допускают неограниченные аксиомы понимания того, что: любая пропозициональная функция определяет множество, а именно, всех тех сущностей, которые удовлетворяют этой функции. Среди теорий или основанных на множествах теорий, которые имели этот недостаток, были наивная теория множеств Кантора и система Грюндгесетце Фреге (в частности: аксиома 5).

Поскольку типы считаются особыми типами множеств, если не соблюдать осторожность, подобный парадокс может заползти в систему типов. При этом я не знаю ни о каких системах типов, которые постигли бы такую ​​участь. Я могу только вспомнить ранние попытки Черча сформулировать лямбда-исчисление в 30-х годах, которые оказались противоречивыми (парадокс Клини-Россера), но они не были связаны ни с типами, ни с парадоксом Рассела.

Обновление : см. Ответ Филиппа для фактического ответа на ваш вопрос.

Унан Ростомян
источник
1
Спасибо за Ваш ответ. Вероятно, есть альтернативы типам а-ля-Рассел, чтобы избежать парадокса Рассела. Будет ли у какого-нибудь из этих альтернативных решений что-нибудь интересное для компьютерных языков? Типы Mundane очень полезны для четкого определения контрактов между частями кода и даже до этого для предоставления семантики программам вообще. Существуют ли другие семантики, которые можно получить с помощью чего-то другого, кроме типов? (Я понятия не имею, что это будет :-)
Фрэнк
1
Да, множество альтернатив (Quine's NF, ZFC и т. Д.), Но я не вижу прямой связи между фундаментальным кризисом и языками программирования. Если вы рассматриваете теорию типов Мартина Лофа как язык программирования, там может быть какая-то связь, восходящая к интуиционизму. Что касается семантики языков программирования, существуют некоторые базовые языки, такие как PDL (пропозициональная динамическая логика), которые имеют семантику Крипке (или возможные миры). Но типы кажутся мне настолько фундаментальными, что они могут быть просто за кадром :)
Унан Ростомян
1
Но типы являются чем-то вроде обломка: вы хотите и нуждаетесь в них, но вы бы не хотели указывать их (следовательно, ИМХО, почему у нас есть системы вывода типов в таких языках, как Haskell или Ocaml (я люблю эти языки)). На другом конце спектра Python чувствует себя очень интуитивно, и приятно (и эффективно с точки зрения времени кодирования) не беспокоиться о типах в этом языке. Может быть, вывод типа является лучшим из обоих миров - но это говорит инженер. Я просто мечтал, что математика может внести еще одну важную концепцию (например, типы) в информатику :-)
Фрэнк
1
@Frank Каждый раз, когда я использую язык без статических типов (в основном, Ruby), я ненавижу этот опыт, потому что я ненавижу ошибки, которые можно избежать во время выполнения. Так что, похоже, дело вкуса. Я согласен, что мощный вывод типа может дать вам лучшее из обоих миров. Наверное, поэтому мне так нравится Scala.
Рафаэль
Я не уверен, что отсутствие типов «автоматически» приводит к ошибкам во время выполнения, как вы, вероятно, подразумеваете :-) У меня никогда не было проблем с Python.
Фрэнк
3

Поскольку вы упоминаете Python, вопрос не является чисто теоретико-типовым. Поэтому я стараюсь дать более широкий взгляд на типы. Типы разные вещи для разных людей. Я собрал как минимум 5 различных (но связанных) понятий типов:

  1. Системы типов - это логические системы и теории множеств.

  2. Система типов связывает тип с каждым вычисленным значением. Исследуя поток этих значений, система типов пытается доказать или гарантировать, что ошибки типа не могут возникнуть.

  3. Тип - это классификация, идентифицирующая один из различных типов данных, таких как вещественные, целочисленные или логические, которые определяют возможные значения для этого типа; операции, которые могут быть выполнены со значениями этого типа; значение данных; и как значения этого типа могут быть сохранены

  4. Абстрактные типы данных позволяют абстрагировать данные в языках высокого уровня. ADT часто реализуются как модули: интерфейс модуля объявляет процедуры, которые соответствуют операциям ADT. Эта стратегия сокрытия информации позволяет изменять реализацию модуля без нарушения работы клиентских программ.

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

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

Типы-1 возникли из работ Рассела, но сегодня они не просто защищают от парадоксов: типизированный язык теории гомотопических типов - это новый способ кодирования математики на формальном, машинно-понятном языке и новый способ понимания основ людьми. математики. («Старый» способ - это кодирование с использованием аксиоматической теории множеств).

Типы 2-5 возникли в программировании по нескольким причинам: чтобы избежать ошибок, для классификации данных, с которыми работают разработчики программного обеспечения и программисты, для проектирования больших систем и эффективной реализации языков программирования соответственно.

Системы типов в C / C ++, Ada, Java, Python не возникли из работы Рассела или из-за желания избежать ошибок. Они возникли из-за необходимости описывать различные виды данных (например, «фамилия - это символьная строка, а не число»), модульного проектирования программного обеспечения и оптимально выбирать низкоуровневые представления для данных. Эти языки не имеют типов-1 или типов-2. Java обеспечивает относительную безопасность от ошибок не путем доказательства правильности программы с использованием системы типов, а путем тщательного проектирования языка (без арифметики указателей) и системы времени выполнения (виртуальная машина, проверка байт-кода). Система типов в Java не является ни логической системой, ни теорией множеств.

Однако система типов в языке программирования Agda - это современный вариант системы типов Рассела (основанный на более поздних работах Пера Мартина-Лофа и других математиков). Система типов в Agda предназначена для выражения математических свойств программы и доказательства этих свойств, это логическая система и теория множеств.

Здесь нет черно-белых различий: между ними много языков. Например, система типов языка Haskell имеет корни в работе Рассела, ее можно рассматривать как упрощенную систему Агды, но с математической точки зрения она непоследовательна (внутренне противоречива), если рассматривать ее как логическую систему или теорию множеств.

Тем не менее, как теоретический инструмент для защиты программ на Haskell от ошибок, он работает довольно хорошо. Вы даже можете использовать типы для кодирования определенных свойств и их доказательств, но не все свойства могут быть закодированы, и программист может все еще нарушать проверенные свойства, если он использует нежелательные грязные хаки.

Система типов Scala еще дальше от работы Рассела и совершенного языка доказательства Агды, но все еще имеет корни в работе Рассела.

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

Интересные, но разные подходы см. В исследовательском проекте Coq и Microsoft Boogie. Coq опирается на теорию типов для создания императивных программ из программ Coq. Буги полагается на аннотацию императивных программ со свойствами и доказательство этих свойств с помощью средства доказательства теоремы Z3, используя совершенно иной подход, чем Coq.

nponeccop
источник