Как я прочитал эту ошибку отверстия

Question

Я пытаюсь написать реализацию flatMap. Но это несущественно, мне очень интересно понять сообщение об ошибке. Но для контекста до сих пор у меня есть:

flatMap :: 
(a -> List b) 
    -> List a 
    -> List b 
flatMap f xs = foldRight undefined undefined _undefined 

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

Found hole ‘_undefined’ with type: List a0 
    Where: ‘a0’ is an ambiguous type variable 
    Relevant bindings include 
     xs :: List a (bound at src/Course/List.hs:266:11) 
     f :: a -> List b (bound at src/Course/List.hs:266:9) 
     flatMap :: (a -> List b) -> List a -> List b 
     (bound at src/Course/List.hs:266:1) 
    In the third argument of ‘foldRight’, namely ‘_undefined’ 
    In the expression: foldRight undefined undefined _undefined 
    In an equation for ‘flatMap’: 
     flatMap f xs = foldRight undefined undefined _undefined 

Я знаю правильный колышек для этого отверстия хз, но я не понимаю, почему Haskell компилятор дал ему тип, обозначенный List a0, и как это относится к типу, который я собираюсь использовать List a?

Я думаю, что это имеет какое-то отношение к тому, что целое может взять надмножество типа List или что-то еще? почему тогда он просто не назвал его List b вместо специально List a0.

Приветствия, Джим

Answer 1

Грубо говоря, компилятор выводит типы следующим образом.

Дадим каждому undefined отдельный тип неизвестного:

flatMap :: (a -> List b) -> List a -> List b 
flatMap f xs = 
    foldRight (undefined :: a1) (undefined :: b1) (_undefined :: c1) 

Теперь foldRight ожидает бинарную функцию, имеющую вид как a2 -> b2 -> b2, так давайте сделаем a1 более точным.

flatMap :: (a -> List b) -> List a -> List b 
flatMap f xs = 
    foldRight (undefined :: a2 -> b2 -> b2) (undefined :: b1) (_undefined :: c1) 

Теперь foldRight требует, чтобы второй undefined имеет тип b1 ~ b2, а последний должен иметь тип c1 ~ List a2.

flatMap :: (a -> List b) -> List a -> List b 
flatMap f xs = 
    foldRight (undefined :: a2 -> b2 -> b2) (undefined :: b2) (_undefined :: List a2) 

(предполагая, что мы имеем Nil и Cons как конструктор вашего List типа)

Результат foldRight является b2, но подписи типа говорит, что это на самом деле List b. Следовательно,

flatMap :: (a -> List b) -> List a -> List b 
flatMap f xs = 
    foldRight (undefined :: a2 -> List b -> List b) (undefined :: List b) 
      (_undefined :: List a2) 

Теперь все готово. Обратите внимание, что нет ограничений, которые могут позволить нам вывести a2 ~ a, так что a2 остается неизвестным, и компилятор не может предложить более точный тип для него, и ваше отверстие генерирует сообщение GHC, которое вы отправили.

Более конкретно, посмотреть на этой специализации, где a2 ~ Int:

flatMap :: (a -> List b) -> List a -> List b 
flatMap f xs = 
    foldRight (g :: Int -> List b -> List b) (Nil :: List b) (Cons 3 Nil :: List Int) 
    where g :: Int -> List b -> List b 
     g y ys = ys 

Вышеуказанные проверки типа, даже если мы выбрали a2 ~ Int вместо a2 ~ a. Следовательно, компилятор не может вывести a2 ~ a, так как существует больше решений неизвестного типа a2.