Есть утверждения, что система типа Scala завершена. Мои вопросы:
Существует ли для этого формальное доказательство?
Как бы выглядели простые вычисления в системе типов Scala?
Это ли какая-либо польза для Scala - языка? Разве это делает Scala более "мощным" каким-то образом сравнивает языки без системы полного типа Тьюринга?
Я предполагаю, что это относится к языкам и типам систем вообще.
Существует сообщение в блоге где-то с реализацией уровня комбинатора SKI на уровне уровня, который, как известно, является завершением Turing.
Системы Turing-complete имеют в основном те же преимущества и недостатки, что и у Turing-полных языков: вы можете делать что угодно, но вы можете оказаться очень маленькими. В частности, вы не можете доказать, что на самом деле вы в конце концов что-то сделаете.
Одним из примеров расчета на уровне типа являются новые накопительные трансформаторы, сохраняющие тип в Scala 2.8. В Scala 2.8 методы, такие как map, filter и т.д. Гарантированно возвращают коллекцию того же типа, к которой они были вызваны. Итак, если вы filter a Set[Int], вы вернете a Set[Int], и если вы map a List[String], вы вернете a List[Whatever the return type of the anonymous function is].
Теперь, как вы можете видеть, map может фактически преобразовать тип элемента. Итак, что произойдет, если новый тип элемента не может быть представлен с исходным типом коллекции? Пример: a BitSet может содержать только целые числа фиксированной ширины. Итак, что произойдет, если у вас есть BitSet[Short] и вы сопоставляете каждое число с его строковым представлением?
someBitSet map { _.toString() }
Результат будет BitSet[String], но это невозможно. Таким образом, Scala выбирает самый производный супертип BitSet, который может содержать String, который в этом случае является Set[String].
Все это вычисление происходит во время компиляции или, точнее, во время проверки типа, используя функции уровня. Таким образом, статически гарантировано быть безопасным по типу, хотя типы фактически вычисляются и, таким образом, не известны во время разработки.
Мой пост в блоге по кодированию исчисления SKI в системе типа Scala показывает полноту Тьюринга.
Для некоторых простых вычислений уровня уровня также есть некоторые примеры того, как кодировать натуральные числа и добавление /multiplication.
Наконец, есть большая статья статей по программированию уровня на блоге Apocalisp.