Разве Scala 3 не будет завершена по Тьюрингу?
Я присутствовал на следующем выступлении Мартина Одерского о будущем Scala:
https://skillsmatter.com/skillscasts/8866-from-dot-to-dotty
В 1:01:00 ответ на вопрос аудитории говорит о том, что будущая Scala не будет завершена по Тьюрингу.
Я правильно понял? Scala 3 больше не будет завершена по Тьюрингу? Если да, то какое практическое влияние это окажет на кого-то вроде меня, который ежедневно использует Scala на работе для решения практических задач? Другими словами, что теряют промышленные программисты Scala и что они получают, удаляя полноту Тьюринга?
2 ответа
В 1:01:00 ответ на вопрос аудитории говорит о том, что будущая Scala не будет завершена по Тьюрингу.
Я правильно понял? Scala 3 больше не будет завершена по Тьюрингу?
Нет, это не вопрос и не ответ.
Во-первых, вопрос, который задают, заключается не в том, будет ли Scala не завершенным по Тьюрингу, а в том, что система типов Scala не будет завершена по Тьюрингу.
Во-вторых: Дается ответ не о том, что система типов будущей Scala не будет полной по Тьюрингу. Мартин Одерски ясно говорит, что с учетом последствий система типов определенно будет завершена по Тьюрингу, и без последствий он не хочет делать прогноз относительно того, будет ли она завершена по Тьюрингу.
Итак, чтобы ответить на ваш вопрос:
- Скала определенно все еще будет завершена по Тьюрингу.
- Вопрос, на который вы ссылаетесь, касается не Scala, а системы типов Scala.
- Система типов в Scala также все еще будет завершена по Тьюрингу из-за последствий.
- Система типов Scala без последствий может быть или не быть полной по Тьюрингу, мы пока не знаем, и Мартин Одерски не хочет делать какие-либо прогнозы.
Если да, то какое практическое влияние это окажет на кого-то вроде меня, который ежедневно использует Scala на работе для решения практических задач?
Никак нет. Прежде всего, опять же, система типов все еще будет завершена по Тьюрингу из-за последствий. И, во-вторых, даже если бы не было, AFAIK, полнота по Тьюрингу системы типов Scala не использовалась ни для чего прагматически интересного. Существуют библиотеки, которые выполняют сложные вычисления на уровне типов, но эти вычисления всегда заканчиваются. Никто не написал библиотеку, которая выполняет произвольные полные по Тьюрингу вычисления на уровне типов. (И на самом деле, это даже невозможно, потому что, хотя система типов Scala полна по Тьюрингу, все существующие в настоящее время реализации Scala (в любом случае, есть только одна) имеют строгое ограничение на глубину рекурсии средства проверки типов).
Другими словами, что теряют промышленные программисты Scala и что они получают, удаляя полноту Тьюринга?
Давайте сначала поговорим о системе типов: они ничего не теряют. Что они получают, так это тот факт, что компиляция гарантированно завершится, и тот факт, что это означает, что компилятор может доказать что-то о программе, которую он не может доказать иначе.
Давайте также ответим на гипотетический вопрос: что, если Scala не был завершен по Тьюрингу? Ну, мы больше не могли писать бесконечные циклы. Вот и все. Однако обратите внимание, что многие вещи, которые обычно моделируются как бесконечные циклы (или бесконечная рекурсия) над данными, все еще могут моделироваться как конечная совместная рекурсия над совместными данными! (Например, цикл событий в операционной системе, веб-сервере или графическом интерфейсе.)
ОТО, многие вещи, которые компиляторы не могут сделать, это "потому что это эквивалентно решению проблемы остановки". Ну, на языке, который не является полным по Тьюрингу, проблема остановки не существует! Таким образом, компилятор может доказать гораздо больше о программах, чем это можно сделать на языке, полном Тьюринга.
Но, повторюсь: нет никаких планов сделать Scala неполной по Тьюрингу. Нет никаких планов сделать следствие не завершенным по Тьюрингу. Существуют ограничения на систему типов, которые могут или не могут сделать систему типов неполной по Тьюрингу.
Правильно ли мое понимание выше, то есть Scala 3 больше не будет завершен по Тьюрингу?
Нет, Scala 3 все еще остается полным по Тьюрингу языком. Вы уже можете поэкспериментировать с этим, опробовав Dotty, текущий прототип для того, что станет Scala 3.
Если вы можете дать ссылку на конкретный слайд конкретного разговора, на который вы ссылаетесь, мы можем помочь вам выяснить, что он на самом деле пытался выразить.