Какой тип математики это: а -> б -> с

Question

Я часто вижу объявления типа, подобные этому, когда смотрю на Haskell:

a -> (b -> c)

Я понимаю, что она описывает функцию, которая принимает что-то типа a и возвращает новую функцию, которая принимает что-то типа b и возвращает что-то типа c. Я также понимаю, что типы являются ассоциативными (отредактируйте: я был неправ в этом - см. Комментарии ниже), поэтому вышеприведенное можно переписать так, чтобы получить тот же результат:

(a -> b) -> c

Это описало бы функцию, которая принимает что-то типа a и что-то типа b и возвращает что-то типа c.

Я также слышал, что вы можете сделать дополнение (редактировать: действительно, слово, которое я искал здесь, двойственное - см. Комментарии ниже) к функции, переключая стрелки:

a <- b <- c

который, я думаю, эквивалентен

c -> b -> a

но я не уверен.

Мой вопрос: как называется этот вид математики? Я хотел бы узнать больше об этом, чтобы я мог использовать его, чтобы помочь мне писать лучшие программы. Я заинтересован в изучении таких вещей, как дополнительная функция и какие другие преобразования могут быть выполнены для объявлений типов.

Спасибо!

Answer 1

Объявления типов не ассоциативны, a -> (b -> c) не эквивалентно (a -> b) -> c. Кроме того, вы не можете «переключать» стрелки, a <- b <- c недопустимый синтаксис.

Обычная ссылка на ассоциативность в этом случае такова: -> it правая ассоциативная , что означает, что a -> b -> c интерпретируется как a -> (b -> c).

Answer 2

В широком смысле это относится к области Лямбда-исчисление .

Поскольку эта нотация связана с типами функций вывод типа может представлять интерестакже.

(Неправильные предположения, которые вы сделали относительно ассоциативности, уже должны быть достаточно прояснены другими ответами, поэтому я не буду повторять это)

Answer 3

a -> (b -> c) 

и

(a -> b) -> c

являются не эквивалентными в Haskell. Это теория типов, которая может быть основана на теории категорий.

Первая - это функция, принимающая аргумент типа a и возвращающая функцию типа b -> c. Последний является функцией, принимающей в качестве аргумента функцию типа a -> b и возвращающей значение типа c.

Что вы подразумеваете под дополнением к функции? Тип обратной функции функции типа a -> (b -> c) имеет тип (b -> c) -> a.

Answer 4

Функции типа a->b->c, которые на самом деле являются цепочками функций, как вы сказали, являются примерами Curry