Система типов в Scala завершена по Тьюрингу. Доказательство? Пример? Выгоды?

Есть утверждения, что система типов Scala является полной по Тьюрингу. Мои вопросы:

  1. Есть ли формальное доказательство этому?

  2. Как будут выглядеть простые вычисления в системе типов Scala?

  3. Это какая-то польза для Scala - языка? Делает ли это Scala более "мощным" в некотором роде по сравнению с языками без полной системы типов Тьюринга?

Я думаю, что это относится к языкам и системам типов в целом.

Источник

2 ответа

Решение

Где-то есть пост в блоге с реализацией на уровне типов комбинаторного исчисления, которое, как известно, является полным по Тьюрингу.

Системы типа Тьюринга имеют в основном те же преимущества и недостатки, что и языки с тьюринговым набором: вы можете делать что угодно, но вы можете доказать очень мало. В частности, вы не можете доказать, что в конечном итоге вы что-то сделаете.

Одним из примеров вычислений на уровне типов являются новые сохраняющие тип преобразователи коллекций в Scala 2.8. В Scala 2.8 такие методы, как map, filter и так далее гарантированно возвращают коллекцию того же типа, к которому они были вызваны. Итак, если вы filter Set[Int]вернись Set[Int] и если вы map List[String] вы получите обратно List[Whatever the return type of the anonymous function is],

Теперь, как вы можете видеть, map действительно может преобразовать тип элемента. Итак, что произойдет, если новый тип элемента не может быть представлен с исходным типом коллекции? Пример: а BitSet может содержать только целые числа фиксированной ширины. Итак, что произойдет, если у вас есть BitSet[Short] а вы сопоставляете каждое число с его строковым представлением?

someBitSet map { _.toString() }

Результатом будет BitSet[String], но это невозможно. Итак, Scala выбирает самый производный супертип BitSet, который может держать String, который в данном случае является Set[String],

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

Источник

Мой пост в блоге о кодировании исчисления SKI в системе типов Scala показывает полноту по Тьюрингу.

Для некоторых простых вычислений на уровне типов есть также несколько примеров того, как кодировать натуральные числа и сложение / умножение.

Наконец, в блоге Apocalisp есть большая серия статей по программированию на уровне типов.

Источник
Другие вопросы по тегам