Почему функция (+) соответствует типу (a -> b -> b)? Функция

Question

раз:

fold :: b -> (a -> b -> b) -> [a] -> b 
fold z f []  = z 
fold z f (x:xs) = f x (fold z f xs) 

http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html взят из

Prelude> :t (+) 
(+) :: Num a => a -> a -> a 

*Main> fold (0) (+) [1,2,3] 
6 

Что типом (a -> b -> b) матча с типом a -> a -> a для (+) функции?

Как правило, определение типа допуска (a -> b -> b) означает, что первые 2 параметра (a -> b) должны быть разных типов?

Answer 1

Нет, все это означает, что a и bможет быть разными, но это не является обязательным для того, чтобы быть по-другому. В вашем случае это одно и то же.

Гораздо более простой пример, чтобы передать точку:

data SomeType a b = Test a b deriving (Show) 

Сейчас в ghci:

Answer 2

Вы соберетесь в обратном направлении. Вам не нужно проверить, является ли + идентичен или соответствует a -> b -> b, вы хотите типа + быть специализацией из a -> b -> b и проверить это, вы должны объединить типы.

Унификация означает, что вы хотите увидеть, является ли тип + и тип a -> b -> b могут быть сделаны равными по переименования переменных типа.

So + имеет тип Num x => x -> x -> x. Давайте теперь проигнорируем ограничение класса, и давайте посмотрим, можем ли мы соответствовать функциональным типам. Типы становятся x -> x -> x и a -> b -> b. На самом деле лучше, если мы посмотрим на них так, как они есть на самом деле, без использования ассоциативности: x -> (x -> x) и a -> (b -> b).

-> является конструктором типа . То есть это функция, которая отображает определенное количество типов в другой тип. В этом случае конструктор -> отображает два типа t_1 и t_2 функциональному типу (->) t_1 t_2 (который обычно обозначается t_1 -> t_2).

Так тип x -> (x -> x) фактически (->) x ((->) x x), который является конструктором типа -> применяется к x и к типу конструктора -> применяется к x и x. Другой тип: (->) a ((->) b b).

При объединении вы рассматриваете внешний конструктор типа для двух типов (-> для обоих в этом случае). Если это не соответствует, вы не можете объединиться. В противном случае вам нужно объединить аргументы конструктора.

Таким образом, мы должны объединить x с a. Они являются переменными типа, поэтому мы можем переименовать один из них. Предположим, что мы переименовали a с x. Итак, теперь мы применяем переименование к типам, получив: (->) x ((->) x x) и (->) x ((->) b b), и вы увидите, что x и x теперь соответствуют.

Рассмотрим второй аргумент. Это не переменная типа, поэтому мы должны сопоставлять конструктор типов, и это снова -> для обоих. Поэтому мы рекурсивно обрабатываем аргументы.

Мы хотим соответствовать x и b. Они являются переменными типа, поэтому мы можем переименовать один из них. Скажем, мы переименовываем x в b. Мы применяем эту замену к типам, получая: (->) b ((->) b b) и (->) b ((->) b b). Теперь все соответствует. Следовательно, два типа объединяются.

Что касается ограничения класса, когда мы переименуем x с b мы применили замену на ограничение тоже так Num x стал Num b и два последних типа являются как Num b => b -> b -> b.

Надеюсь, это дало вам некоторое представление о том, как работают типы и как проверяются типы.

---

Сторона примечания: Это то, что haskell делает при выполнении вывода типа. Сначала он присваивает неизвестной функции новую переменную типа t. Затем он использует унификацию, чтобы получить тип выражения, которое определяет его, и проверить, какой тип был связан с t, и это тип функции.