В чем причина полной системы Turing?

Ответ 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?) Цена очень захватывающей проверки времени компиляции тратит много времени и усилий программиста, убеждая компилятора, что вещь, которую вы проверяете, верна - и это часто бывает как высокая стоимость обслуживания, а также высокая текущая стоимость обслуживания.