Проверка типов может быть разрешена путем надлежащего обогащения синтаксиса.Например, в статье у нас есть лямбды, записанные как \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] являются скобками замещения).Затем синтаксис сообщает нам, когда и сколько нужно добавить кодов, а также когда их устранить.
Итак, вопрос в том, можем ли мы перейти от Хаскелла к достаточно аннотированным терминам 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 делает вывод в этой ситуации?Ну, ответ в том, что он даже не пытается.Если вы хотите писать термины, используя эти функции, то вы должны добавить аннотации ввода, о которых мы говорили все время назад в первом абзаце: вы должны явно аннотировать, где вводятся и удаляются forall s.Итак, можем ли мы написать термин, который отклоняет средство проверки типов GHC?Да, это просто: просто используйте аннотированные типы ранга два (или выше) или непредсказуемость.Например, следующее не проверяет тип, даже несмотря на то, что оно имеет явную аннотацию типа и может быть напечатано с типами ранга два:
{-# LANGUAGE Rank2Types #-}
foo :: (String, Bool)
foo = (\f -> (f "hey", f True)) id
* На самом деле, ограничения до ранга два достаточно, чтобы сделать эторазрешимый, но алгоритм для типов ранга один может быть более эффективным.Три типа ранга уже дают программисту достаточно веревки, чтобы сделать проблему вывода неразрешимой.Я не уверен, были ли известны эти факты в то время, когда комитет решил ограничить Haskell типами первого ранга.