RankNTypes с путаницей псевдонимов типов

Я пытаюсь понять, как ограничения типов работают с псевдонимами типов. Во-первых, предположим, что у меня есть псевдоним следующего типа:

type NumList a = Num a => [a]

И у меня есть следующая функция:

addFirst :: a -> NumList a -> NumList
addFirst x (y:_) = x + y

Эта функция завершается со следующей ошибкой:

Type.hs:9:13: error:
    • No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            addFirst :: a -> NumList a -> a
    • In the pattern: y : _
      In an equation for ‘addFirst’: ad

Что очевидно. Эта проблема уже описана здесь:

Понимание псевдонима типа ранга 2 с ограничением класса

И я понимаю, почему нам нужно {-# LANGUAGE RankNTypes #-} для работы таких псевдонимов типов и почему предыдущий пример не работает. Но я не понимаю, почему следующий пример компилируется нормально (на ghc 8):

prepend :: a -> NumList a -> NumList a
prepend = (:)

Конечно, в ghci произойдет сбой, если я попытаюсь передать неправильное значение:

λ: prepend 1 []
[1]
λ: prepend "xx" []

<interactive>:3:1: error:
    • No instance for (Num [Char]) arising from a use of ‘prepend’
    • When instantiating ‘it’, initially inferred to have
      this overly-general type:
        NumList [Char]
      NB: This instantiation can be caused by the monomorphism restriction.

Похоже, что проверка типа задерживается во время выполнения :(

Более того, какой-то простой и вроде бы одинаковый кусок кода не компилируется:

first :: NumList a -> a
first = head

И выдает следующую ошибку:

Type.hs:12:9: error:
    • No instance for (Num a)
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            first :: NumList a -> a
    • In the expression: head
      In an equation for ‘first’: first = head

Может кто-нибудь объяснить, что здесь происходит? Я ожидаю некоторой согласованности в том, проверяет ли тип функции или нет.


types functional-programming haskell higher-rank-types
person Shersh    schedule 26.10.2016    source источник
comment
Просто подумайте о Num a => a как о функции NumDict a -> a, и все должно быть ясно.   -  person Reid Barton    schedule 26.10.2016
comment
Хотя вы уже связались с вопросом, предложенным @Alec, стоит отметить, что второй ответ (от luqui), вероятно, более понятен, чем принятый, и показывает, почему prepend работает, а другие функции - нет (в Короче говоря, компилятор может переместить ограничение туда, где вы хотите, только если у вас есть синоним в самой правой позиции подписи). Кстати, обратите внимание, что в ваших примерах использования prepend нет ничего странного или запоздалого — она делает именно то, что вы ожидаете от функции Num a => a -> [a] -> [a].   -  person duplode    schedule 26.10.2016
comment
Да, ответ Луки на связанный вопрос точно актуален.   -  person Reid Barton    schedule 26.10.2016
comment
Ой! Я не собирался просто ссылаться на тот же вопрос, который вы связали, - это действительно был ответ Луки, который я считал уместным.   -  person Alec    schedule 26.10.2016
comment
@duplode Да, второй ответ @luqui теперь все проясняет. Похоже, что проверка типов зависит от того, является ли мой аргумент с псевдонимом типа ковариантным или контравариантным. Я понял раньше только почему foo :: forall a . a -> (forall b . b) это то же самое, что и foo :: forall a b . a -> b. Но теперь я вижу, что такие правила также распространяются на ограничения, если вы представляете их в виде словарей. Теперь это выглядит довольно элегантно :)   -  person Shersh    schedule 26.10.2016
comment
@Shersh Играя с вашим вопросом, я наткнулся на нечто, что кажется действительно странным, и на новый вопрос.   -  person duplode    schedule 27.10.2016

Ответы (1)


arrow_upward
1
arrow_downward

Похоже, что проверка типа задерживается во время выполнения :(

Не совсем. Здесь это может быть немного неожиданно, потому что вы получаете ошибку типа в ghci после загрузки файла. Однако это можно объяснить: сам файл в полном порядке, но это не означает, что все выражения, которые вы можете построить с помощью определенных в нем функций, будут правильно типизированы.

Полиморфизм более высокого ранга здесь ни при чем. Например, (+) определено в прелюдии, но если вы попытаетесь оценить 2 + "argh" в ghci, вы также получите ошибку типа:

No instance for (Num [Char]) arising from a use of ‘+’
In the expression: 2 + "argh"
In an equation for ‘it’: it = 2 + "argh"

Теперь давайте посмотрим, в чем проблема с first: он утверждает, что при наличии NumList a он может произвести a, без вопросов. Но мы знаем, как построить NumList a из воздуха! Действительно, ограничения Num a означают, что 0 является a и делает [0] вполне допустимым NumList a. Это означает, что если бы first было принято, то все типы были бы обитаемы:

first :: NumList a -> a
first = head

elt :: a
elt = first [0]

В частности, Void тоже будет:

argh :: Void
argh = elt

Арг действительно!

person gallais    schedule 26.10.2016
comment
› это не означает, что все выражения, которые вы можете составить с помощью определенных в нем функций, будут правильно типизированы. Да, это хороший момент. Я понял только после некоторого размышления и наблюдения за ошибкой. - person Shersh; 26.10.2016