Ответ 1
Что это значит в контексте типов?
Это означает, что система типов имеет в ней достаточные возможности для представления произвольных вычислений. В качестве очень короткого доказательства я представляю ниже реализацию уровня SK на уровне уровня; есть много мест, которые обсуждают Тьюринга-полноту этого исчисления и что это значит, поэтому я не буду перефразировать это здесь.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
infixl 1 `App`
data Term = S | K | App Term Term
type family Reduce t where
Reduce S = S
Reduce K = K
Reduce (S `App` x `App` y `App` z) = Reduce (x `App` z `App` (y `App` z))
Reduce (K `App` x `App` y) = Reduce x
Reduce (x `App` y) = Reduce (Reduce x `App` y)
Вы можете увидеть это в действии в командной строке ghci; например, в исчислении SK, термин SKSK сводит (в конечном итоге) к просто K:
> :kind! Reduce (S `App` K `App` S `App` K)
Reduce (S `App` K `App` S `App` K) :: Term
= 'K
Здесь весело, чтобы попробовать:
> type I = S `App` K `App` K
> type Rep = S `App` I `App` I
> :kind! Reduce (Rep `App` Rep)
Я не буду испортить веселье - попробуйте сами. Но знайте, как сначала прервать программы с крайним предрассудком.
Может ли кто-нибудь привести пример того, как программист может извлечь из этого выгоду?
Произвольное вычисление уровня на уровне позволяет вам выражать произвольные инварианты в ваших типах и проверять компилятор (во время компиляции), чтобы они сохранялись. Хотите красно-черное дерево? Как насчет красно-черного дерева, которое может проверить компилятор, сохраняет инварианты красно-черного дерева? Это было бы удобно, правильно, так как это исключает целый класс ошибок реализации? Как насчет типа для значений XML, которые статически известны в соответствии с конкретной схемой? На самом деле, почему бы не пойти дальше и записать параметризованный тип, параметр которого представляет собой схему? Затем вы можете прочитать схему во время выполнения, и ваши проверки времени компиляции гарантируют, что ваше параметризованное значение может представлять только хорошо сформированные значения в этой схеме. Ницца!
Или, возможно, более прозаичный пример: что, если вы хотите, чтобы ваш компилятор проверял, что вы никогда не индексировали ваш словарь с помощью ключа, которого там не было? С достаточно развитой системой типов вы можете.
Конечно, всегда есть цена. В Haskell (и, вероятно, Scala?) Цена очень захватывающей проверки времени компиляции тратит много времени и усилий программиста, убеждая компилятора, что вещь, которую вы проверяете, верна - и это часто бывает как высокая стоимость обслуживания, а также высокая текущая стоимость обслуживания.