Проверка типов и детерминизм в Haskell

Согласно языковому отчету Haskell 2010, его средство проверки типов основано на на Хиндли-Милнера. Итак, рассмотрим функцию f этого типа,

f :: forall a. [a] -> Int

Например, это может быть функция длины. По словам Хиндли-Милнера, тип f [] проверяется на Int. Мы можем доказать это, создав экземпляр типа от f до [Int] -> Int и типа от [] до [Int], а затем сделать вывод, что приложение ([Int] -> Int) [Int] относится к типу Int.

В этом доказательстве я решил создать экземпляры типов forall a. [a] -> Int и forall a. [a], заменив Int на a. Я могу заменить вместо этого Bool, доказательство тоже работает. Разве не странно в Хиндли-Милнера, что мы можем применить полиморфный тип к другому, не указывая, какие экземпляры мы используем?

Более конкретно, что в Haskell мешает мне использовать тип a в реализации f? Я мог представить, что f - это функция, которая равна 18 для любого [Bool] и равна обычной функции длины для всех других типов списков. В этом случае f [] будет 18 или 0? В отчете Haskell говорится, что «ядро формально не указано», поэтому трудно сказать.


haskell hindley-milner
person V. Semeria    schedule 10.08.2018    source источник
comment
Это отличный вопрос. Обратите внимание, что ваша функция f, которая ведет себя на [Bool] иначе, чем на других типах списков [a], не может существовать (т.е. не может быть написана на Haskell) из-за параметричности. В Haskell нет возможности писать if a==Bool then ... и иметь неизменную подпись forall a. [a] -> Int.   -  person chi    schedule 10.08.2018
comment
Смотрите мой ответ ниже. Поначалу параметричность может показаться немного сложной, но вы можете начать с классических теорем из бесплатной статьи Вадлера, в которой приведены хорошие примеры.   -  person chi    schedule 10.08.2018
comment
У меня нет идеальной ссылки. На параметричность иногда влияет нижняя часть (seq, бесконечная рекурсия), но я напоминаю, что, предполагая строгие функции, можно получить более слабую форму параметричности. (Опять же, я не могу предоставить ссылку). Чтобы полностью нарушить параметричность, можно использовать forall a. Typeable a => [a] -> Int, который позволяет if a==Bool then ... - но здесь тип меняется, поэтому он на самом деле не нарушен: у нас есть тип для параметрического полиморфизма и еще один для специального (непараметрического) полиморфизма.   -  person chi    schedule 11.08.2018
comment
Нет, дополнительный аргумент a в Haskell вообще не нужен. И даже в Coq вы не можете исключить (a : Type), поэтому нет if. В Coq вам понадобится какой-то аргумент, который нужно исключить, например forall (a : Type), typeable a -> list a -> int, где typeable a определено соответствующим образом, например с индуктивным определением.   -  person chi    schedule 11.08.2018
comment
@chi Без лишних a лучшее, что я нашел, это f l = if typeOf l == typeOf ([True]) then 18 else length l. Но затем f [] вылетает с ошибкой типа. Вы видите другой путь?   -  person V. Semeria    schedule 11.08.2018
comment
f [] становится неоднозначным, поскольку теперь a имеет значение. Попробуйте f ([] :: [Bool]) или f ([] :: [Int]).   -  person chi    schedule 11.08.2018
comment
Вы также можете использовать if typeOf (undefined :: a) == typeOf (undefined :: Bool). Лично я часто предпочитаю eqT, поскольку он запускает уточнение GADT, но это уже другая проблема.   -  person chi    schedule 11.08.2018
comment
@chi Я не смог скомпилировать с undefined :: a, он говорит, что знаменитый a неизвестен. Можете ли вы дать с ним полную реализацию f?   -  person V. Semeria    schedule 11.08.2018
comment
Включите ScopedTypeVariables, а затем foo :: forall a. Typeable a => [a]->Int ; foo xs = if typeOf (undefined :: a) == ...   -  person chi    schedule 11.08.2018

Ответы (2)


arrow_upward
3
arrow_downward

Во время вывода типа такие переменные действительно могут быть созданы для любого типа. Это можно рассматривать как крайне недетерминированный шаг.

GHC в таких случаях использует внутренний тип Any. Например, составление

{-# NOINLINE myLength #-}
myLength :: [a] -> Int
myLength = length

test :: Int
test = myLength []

приводит к следующему Core:

-- RHS size: {terms: 3, types: 4, coercions: 0}
myLength [InlPrag=NOINLINE] :: forall a_aw2. [a_aw2] -> Int
[GblId, Str=DmdType]
myLength =
  \ (@ a_aP5) -> length @ [] Data.Foldable.$fFoldable[] @ a_aP5

-- RHS size: {terms: 2, types: 6, coercions: 0}
test :: Int
[GblId, Str=DmdType]
test = myLength @ GHC.Prim.Any (GHC.Types.[] @ GHC.Prim.Any)

где GHC.Prim.Any встречается в последней строке.

Разве это не детерминировано? Что ж, это действительно включает в себя своего рода недетерминированный шаг «посередине» алгоритма, но окончательный результирующий (наиболее общий) тип - Int, и детерминированно так. Неважно, какой тип мы выберем для a, в конце мы всегда получаем тип Int.

Конечно, одного и того же типа недостаточно: мы также хотим получить такое же значение Int. Я предполагаю, что можно доказать, что, учитывая

f :: forall a. T a
g :: forall a. T a -> U

тогда

g @ V (f @ V) :: U

одинаковое значение вне зависимости от типа V. Это должно быть следствием применения параметричности к этим полиморфным типам. .

person chi    schedule 10.08.2018

arrow_upward
3
arrow_downward

Чтобы продолжить ответ Чи, вот доказательство того, что f [] не может зависеть от экземпляров типов f и []. Согласно теоремам бесплатно (последняя статья здесь), для любых типов a,a' и любой функции g :: a -> a', то

f_a = f_a' . map g

где f_a - это экземпляр f на типе a, например, в Haskell

f_Bool :: [Bool] -> Int
f_Bool = f

Затем, если вы оцените предыдущее равенство на []_a, оно даст f_a []_a = f_a' []_a'. В случае исходного вопроса f_Int []_Int = f_Bool []_Bool.

Некоторые ссылки на параметричность в Haskell также были бы полезны, потому что Haskell выглядит сильнее, чем полиморфное лямбда-исчисление, описанное в статье Уолдера. В частности, на этой странице вики говорится, что параметричность в Haskell может быть нарушена с помощью функции seq.

На вики-странице также говорится, что моя функция, зависящая от типа, существует (на других языках, кроме Haskell), она называется ad -hoc полиморфизм.

person V. Semeria    schedule 10.08.2018
comment
Вы можете выполнить специальный полиморфизм (и, следовательно, написать свою функцию, зависящую от типа) в Haskell, используя класс типов. Если вы это сделаете, средство проверки типов заставит вас явно указать, какой тип вы используете для a. - person DarthFennec; 10.08.2018
comment
@DarthFennec гул ... Кажется, это противоречит уравнению параметризации, приведенному выше. Или тип функции не forall a. [a] -> Int. Можете ли вы привести точный пример, о котором вы думаете? - person V. Semeria; 10.08.2018
comment
Вы правы, извините, я не понял; если вы используете класс типов (назовем его Foo) для создания функции, зависящей от типа, тогда тип функции должен быть forall a. Foo a => [a] -> Int. Если мы не добавляем ограничение класса в a, тогда да, параметричность диктует, что функция не может быть зависимой от типа. - person DarthFennec; 10.08.2018