Существуют ли типы подписей, которые Haskell не может проверить?

В этой статье установлено, что вывод типа (называемый "типизируемость" в документе) в System F неразрешим. То, что я никогда не слышал, упоминается в другом месте, является вторым результатом статьи, а именно, что "проверка типов" в F также неразрешима. Здесь вопрос "проверка типа" означает: заданный термин t, введите t и среду ввода A, является ли решение A ⊢ t : T выводимым? Тот факт, что этот вопрос неразрешимый (и что он эквивалентен вопросу о типизированности) удивляет меня, потому что кажется интуитивно похожим, что это должен быть более простой вопрос для ответа.

Но в любом случае, учитывая, что Haskell основан на System F (или F-omega, even), результат проверки типа может показаться, что существует термин Haskell t и тип t такой, что компилятор не сможет решить, действителен ли t :: T. Если это так, мне любопытно, что такое термин и тип... если это не так, то что я недопонимаю?

Предположительно осмыслить статью приведет к конструктивному ответу, но я немного из глубины:)

Ответ 1

Проверка типов может быть разрешима путем надлежащего обогащения синтаксиса. Например, в статье мы имеем lambdas, записанные как \x -> e; Чтобы проверить это, вы должны угадать тип x. Однако, с соответствующим образом обогащенным синтаксисом, это можно записать как \x :: t -> e вместо этого, что выводит гадость из процесса. Аналогичным образом, в документе они позволяют имплицировать ямбды на уровне типа; то есть, если e :: t, то также e :: forall a. t. Чтобы выполнить проверку типов, вы должны угадать, когда и сколько forall добавить, и когда их устранить. Как и прежде, вы можете сделать это более детерминированным, добавив синтаксис: мы добавляем две новые формы выражений /\a. e и e [t] и два новых правила ввода, которые говорят, что если e :: t, затем /\a. e :: forall a. t, а если e :: forall a. t, то e [t'] :: t [t' / a] (где скобки в t [t' / a] являются скобками замены). Затем синтаксис говорит нам, когда и сколько добавлений добавить, а также, когда их также устранить.

Итак, вопрос: можем ли мы перейти от Haskell к достаточно-аннотированным терминам System F? И ответ "да", благодаря нескольким критическим ограничениям, установленным системой типа Haskell. Наиболее важным является то, что все типы - это ранг один *. Не вдаваясь в подробности, "ранг" связан с тем, сколько раз вам нужно идти слева от конструктора ->, чтобы найти forall.

Int -> Bool -- rank 0?
forall a. (a -> a) -- rank 1
(forall a. a -> a) -> (forall a. a -> a) -- rank 2

В частности, это немного ограничивает полиморфизм. Мы не можем вводить что-то вроде этого с помощью ранга один:

foo :: (forall a. a -> a) -> (String, Bool) -- a rank-2 type
foo polymorphicId = (polymorphicId "hey", polymorphicId True)

Следующее наиболее важное ограничение состоит в том, что переменные типа могут быть заменены только мономорфными типами. (Это включает в себя другие переменные типа, такие как a, но не такие полиморфные типы, как forall a. a.) Это частично гарантирует, что подстановка типов сохраняет ранг-один.

Оказывается, если вы сделаете эти два ограничения, то не только тип-вывод можно разрешить, но вы также получите минимальные типы.

Если мы перейдем от Haskell к GHC, тогда мы можем говорить не только о том, что является типичным, но и как выглядит алгоритм вывода. В частности, в GHC существуют расширения, которые ослабляют два вышеуказанных ограничения; как GHC делает вывод в этой ситуации? Ну, ответ в том, что он просто даже не пытается. Если вы хотите писать термины с использованием этих функций, то вы должны добавить аннотации ввода, о которых мы говорили, все это в параграфе 1: вы должны явно аннотировать, где forall вводится и устраняется. Итак, можем ли мы написать термин, который отвергает тип GHC-checker? Да, это легко: просто используйте аннотированные ранга два (или более высокие) типы или impredicativity. Например, следующее не проверяет тип, даже если оно имеет явную аннотацию типа и является типичным для двух типов:

{-# LANGUAGE Rank2Types #-}
foo :: (String, Bool)
foo = (\f -> (f "hey", f True)) id

* На самом деле, ограничение на ранг два достаточно, чтобы сделать его разрешимым, но алгоритм для ранговых типов может быть более эффективным. Ранг три типа уже дают программисту достаточно веревки, чтобы сделать проблему вывода неразрешимой. Я не уверен, были ли эти факты известны в то время, когда комитет решил ограничить Haskell рангами одного типа.

Ответ 2

Вот пример реализации уровня SKI в Scala: http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

В последнем примере показана неограниченная итерация. Если вы сделаете то же самое в Haskell (и я уверен, что вы можете), у вас есть пример для "непищевого выражения".