Интенсивное изучение типов систем и теории типов

Ответ 1

Теория типов - большая область. Прежде всего, термин "типы" является своего рода ошибочным в информатике, по нескольким причинам, хотя они в основном используются для одной и той же базовой идеи. Типы возникли во многих контекстах, философии, информатике и математике, в основном по тем же причинам. Происхождение типов в математике происходит от попыток формализовать теорию множеств и переходить в ничтожные парадоксы, хотя аналогичные парадоксы возникают в информатике. (Например, я хотел бы указать на парадокс Жирара на этом).

То, как вы, вероятно, интерпретируете типы в настоящий момент, - это идея, которая стала популярной на протяжении 70-х - 90-х годов в компьютерах: типы - это легкий анализ, нечувствительный к потоку, который позволяет нам делать краткие логические гарантии относительно программ, которые мы пишем. Для этого можно использовать типы, но вы можете фактически использовать их для кодирования логики более высокого порядка, где программы являются доказательствами. Когда вы пойдете сюда, вы можете взять доказательство, извлечь вычислительный компонент и превратить его в программу, которая вычисляет "правильный" результат (в отношении доказанной вами теоремы).

Есть несколько дорог, которые вы можете взять здесь:

• Возьмите себе экземпляр "Пина Берна" "Типы и языки программирования" . Это книга для чтения и одна из лучших книг по информатике. Он охватывает теорию, почему нам нужны типы, и как мы можем использовать их для ограничения ограничений наших программ!
• Изучайте язык, на котором вы регулярно используете типы, чтобы обеспечить выполнение семантики программы. В частности, вы можете узнать OCaml, Haskell или Agda. Haskell, кажется, лучший выбор на данный момент, у него появилось довольно много расширений, которые делают его действительно привлекательным и действительно активным сообществом пользователей. На самом деле, очень распространено, что результаты, опубликованные на ведущих конференциях, широко используются в сообществе всего за несколько лет!
• Научитесь использовать теоретическую проверку на основе теории конструктивного типа. На мой взгляд, это единственный реальный способ оценить реальные проблемы теории типов. Есть много хороших вариантов, хотя Кок и Изабель выделяются сейчас как настоящие соперники. У Кока есть одно большое преимущество: у Бен Пирса также есть книга, которая его охватывает! Основы программного обеспечения подробно описывают теорию программирования на языках программирования, и вы действительно можете доказать, что она использует ее.

Вы также можете просмотреть несколько связанных полей:

• Теория категорий - это математика, которая, как правило, лежит в основе этого материала. Например, можно категорически интерпретировать (ко) индуктивные типы данных, данные на этих языках.
• Logic. Изучение немного хорошей старой традиционной логики может быть полезным, хотя я уверен, что большинство из того, что вам нужно, можно получить от чтения через книгу Бен Пирса SF. Тем не менее, есть еще много ссылок на старые системы (последовательное исчисление и естественный вывод).
• Узнайте о сообществе Haskell! Как я уже сказал, они двигаются быстро и задают глубокие вопросы о типах компьютерных наук.
• Отличные работы на языках программирования содержит ряд замечательных статей!

Есть несколько замечательных рекомендаций, которые я имею для изучения за пределами этого, но я бы определенно начал с книг Бен Пирса (я никогда не попадал в книгу последующих исследований "расширенные темы по типам и информатике", но это также, возможно, вам интересно). В частности, я помню "Справочник по автоматизированному рассуждению", в котором была статья о теории высшего порядка.

P.s., я убежден, что ответ на этот вопрос конкретно: "получить степень доктора философии в языках программирования, философии или логике..."; -)