Система типов в Scala завершена. Доказательство? Пример? Выгоды?
Существуют утверждения, что система типа Scala является полной. Мои вопросы:
-
Есть ли для этого формальное доказательство?
-
Как бы выглядели простые вычисления в системе типа Scala?
-
Это какая-то польза для Scala – языка? Это делает Scala более «мощным» в некотором роде сравнением языков без полной системы Turing?
Я предполагаю, что это относится к языкам и типам систем в целом.
Существует где-то сообщение в блоге с реализацией на уровне типа вычислений комбинатора SKI, который, как известно, является Turing-complete.
Системы Turing-полного типа имеют в основном те же преимущества и недостатки, что и у Turing-полных языков: вы можете делать что угодно, но вы можете оказаться очень маленькими. В частности, вы не можете доказать, что на самом деле вы в конце концов что-то сделаете.
Одним из примеров расчета на уровне типа являются новые накопительные трансформаторы, сохраняющие тип в 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 есть большая серия статей по программированию на уровне.