На какой «вопрос» пытается ответить теория языка программирования?

10

Я давно интересовался различными темами, такими как комбинаторная логика, лямбда-исчисление, функциональное программирование, и изучал их. Однако, в отличие от «Теории вычислений», которая стремится ответить на вопрос «вычислимости», то есть вещей, которые могут / не могут быть вычислены с различными ограничениями, я изо всех сил пытаюсь найти аналог для «Теории программирования»

Википедия описывает это как:

Теория языка программирования (PLT) - это раздел компьютерных наук, который занимается проектированием, реализацией, анализом, характеристикой и классификацией языков программирования и их индивидуальных особенностей.

Это все равно, что сказать «все», что на самом деле не является конкретным.

Общая последовательность тем обычно такова:

Комбинаторная логика> Лямбда-исчисление> Теория типов Лофта Мартина> Типизированное лямбда-исчисление> (Здесь что-то происходит)> Разработаны языки программирования - которые очень мало связаны с CL /λ

Я могу видеть основную «математику», связанную с CL / и интересные доказательства, которые в результате получаются, включая теорему Черча-Россера, и это аккуратно. Тем не менее, я изо всех сил пытаюсь понять «конечную цель» всего этого начинания? Что за святой Грааль PLT, если хотите? На данный момент, кажется, просто чешется интеллектуальный зуд, но я не могу действительно перейти от исследования / теории к чему-то практическому.λ

Примечание: я получаю его до использования -calc для доказательства неразрешимости. Но помимо его применимости к «вычислимости», я просто не понимаю, и мне трудно даже понять необходимость исследования PLT из этого узкого POV. Существующие книги, ссылки, которые могут пролить свет на «большую картину» PLT?λ

кандидат наук
источник
1
Вы полностью игнорируете целые ряды PLT в своей «общей прогрессии». По какой-то причине ваш взгляд кажется искаженнымλ-калькул и теория типов. Давайте посмотрим на принятые документы POPL 2019 : параллельное рандомизированное программирование, вероятностное программирование, проверяемая сборка, алгебраические эффекты, сертификация нейронных сетей, модели слабой памяти в PL и аппаратном обеспечении, квантовое программирование и т. Д. Много чего не просто теория типов ", не правда ли?
Андрей Бауэр
Ты на 100% прав. Поэтому я назвал мой "узкий POV". Я знаком с «другими темами» только читая здесь и проверяя материалы SIGPLAN / POPL. Мне еще предстоит найти «целостный справочник / книгу», который дает широкий обзор кисти PLT, который включает в себя темы, которые вы упомянули. Бит теории типов только из "моего" POV (создания?) Языков программирования. Будете ли вы иметь несколько указателей, которые могли бы предоставить высокоуровневые введения в различные области PLT, чтобы получить общую картину? Мне любопытно узнать, какие базовые "модели" они используют и как?λ где угодно?
Доктор философии,
2
@PhD Там нет высокоуровневых введений в различные области PLT, которые вы хотите, c'est la vie ! Возможно, однажды это изменится. Но не задерживай дыхание. Поле развивается быстро и дифференцируется в подполя. Другие популярные простые модели включают в себяπ-калькул, структурная операционная семантика, простые императивные исчисления (например, язык WHILE) и многие другие. Часто кто-то придумывает игрушечное исчисление в соответствии с областью применения.
Мартин Бергер

Ответы:

13

Общая цель PLT - сделать промышленную разработку программного обеспечения (в общем смысле) более дешевой (также в общем смысле) путем оптимизации наиболее важного инструмента (языков программирования) и соответствующей инструментальной экосистемы.

Некоторые причины, почему математика вовлечена:

  • PL очень нетривиальны, и не ясно, что они делают правильные вещи без доказательств. Математика дает упрощенную модель реальных языков программирования. Эта модель позволяет нам изучать настоящие языки программирования в значительно упрощенной обстановке, устраняя (мы надеемся) большинство проблем уже на уровне модели. Реальные языки программирования в настоящее время математически неразрешимы. Другими словами: лямбда-исчисление - это плодовая муха, E.Coli, сферическая корова PLT.

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

  • Математика прекрасна и глубока.

  • Математика дает простую, проверенную и проверенную методологию исследования, которая важна для помощи аспирантам. Как правило, некоторые варианты, например: Исследовать элемент PL XYZ путем добавления его в лямбда-исчисление. Добавьте простые типы для XYZ и докажите добротность. Добавьте дженерики для XYZ и докажите добротность. Докажите теорему параметричности для обобщений XYZ. Добавьте зависимые типы для XYZ и докажите правильность типа. Разработайте частичный вывод типов для XYZ-зависимых типов. Добавьте постепенные типы для XYZ и докажите добротность. Добавить контракты для XYZ. Каждый из них - бумага. Вы можете остановиться, если у вашего аспиранта или постдока не хватает времени. Каждый из вышеперечисленных интересен и даст представление об обобщениях, параметричности, выводе типов и т. Д. Этот конвейер является отличнымспособ навигации по трудным водам всех возможных языков программирования. Второй способ обучения - реализация языков в компиляторе, но для человека это не так просто.

Нужен ли PLT - интересный вопрос. Кажется, большинство работающих программистов считают, что это не так. Они не правы: большинство языков, разработанных работающими программистами без знания PLT (например, Javascript, PHP), начинаются ужасно и допускают все ошибки, которых теоретики PL давно научились избегать. Если PL, разработанный любителем, попадает в мейнстрим, теоретикам PL нужно около десяти лет, чтобы исправить очевидные недостатки (например, модифицировать статическую систему типирования, см. Typescript). Позвольте мне обобщить эту ситуацию:

 Every successful programming language ends up being ML! Either because 
 it was designed by a PL theorist as ML from the start, or because a 
 decade of painful evolution removes all the obvious flaws, leaving ML. ;-)

За исключением: Такое положение дел является полностью ошибкой PLT, потому что большинство из них не имеет опыта промышленного программирования, поэтому не знаю, в чем заключаются болевые точки работающих инженеров-программистов. В частности, по социологическим причинам большинство теоретиков PL считают, что чисто функциональное программирование в таких языках, как Agda, является решением всех проблем, которое не выдерживает проверки.

Мартин Бергер
источник
1
@MartinBerger: Рассматривает ли CompCert пример способности теоретически обрабатывать язык программирования реального мира? Если нет, то как высоко вы устанавливаете планку, потому что CompCert довольно впечатляет.
Андрей Бауэр
2
@MartinBerger: Пожалуйста, подумайте над тем, чтобы смягчить «большинство теоретиков PL считают, что чисто функциональное программирование в таких языках, как Agda, является решением всех проблем», потому что это просто ваша ворчание и высказывание. Для начала, даже если вы посмотрите на темы, которые в настоящее время присутствуют в ICFP и POPL, большинство из них касаются нечистых языков программирования.
Андрей Бауэр
5
@PhD: PLT гораздо больше, чем теория типов. Просто теория типов - это первое, что вы замечаете, потому что это один из основных инструментов PLT.
Андрей Бауэр
1
@AndrejBauer CompCert, CakeML и т. Д. Впечатляют, но они далеки от широко используемых компиляторов, таких как LLVM, GCC и т. Д. Кроме того, компиляторы, в отличие от практически любого реального программного обеспечения, имеют (своего рода / своего рода) спецификацию, что вы просто не получите в обычной промышленной разработке программного обеспечения. Не говоря уже о том, что большая часть ранней работы Ксавьера над CompCert состояла в уточнении спецификации.
Мартин Бергер,
2
@PhD Относительно "" радикально более продуктивного ", чем> не-PLT C / C ++, Java, C #", имейте в виду, что если вы посмотрите на эти языки, а точнее на их эволюцию с течением времени, почти все, что они приобрели за время, например, лямбды, монады (LINQ), сопоставление с образцом, частичный вывод типа происходит из PLT. Команда C # имеет докторскую степень PLT. На самом деле они пытались нанять меня в какой-то момент. На собеседовании я пытался убедить Андерса Хейлсберга в том, что C # нужны дженерики, которые ему не нравились в то время ...
Мартин Бергер