Где-то есть сообщение в блоге с реализацией на уровне типов комбинаторного исчисления, которое, как известно, является полным по Тьюрингу.
Системы типа полного по Тьюрингу имеют в основном те же преимущества и недостатки, что и Тьюринг.-полные языки есть: вы можете делать что угодно, но вы можете доказать очень мало.В частности, вы не можете доказать, что на самом деле что-то сделаете.
Одним из примеров вычислений на уровне типов являются новые сохраняющие тип преобразователи коллекций в Scala 2.8.В Scala 2.8 такие методы, как map, filter и т. Д. Гарантированно возвращают коллекцию того же типа, к которому они были вызваны.Итак, если вы filter a Set[Int], вы получите обратно Set[Int], а если вы map a 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].
Все эти вычисления выполняются во время времени компиляции или точнее во время проверки типа с использованием функций уровня типа.Таким образом, статически гарантируется безопасность типов, даже если типы фактически вычисляются и, следовательно, не известны во время разработки.