В чем причина полной системы типов Тьюринга?

Question

Scala и Haskell имеют "системы полного типа Тьюринга". Обычно полнота по Тьюрингу относится к вычислениям и языкам. Что это действительно означает в контексте типов?

Кто-нибудь может привести пример того, как программист может извлечь из этого пользу?

PS Я не хочу сравнивать системы типов Haskell против Scala. Это больше о термине в целом.

PSS Если возможно больше примеров Scala.

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