Какой тип математики это: а -> б -> с
Я часто вижу объявления типа, похожие на это, когда смотрю на Haskell:
a -> (b -> c)
Я понимаю, что она описывает функцию, которая принимает что-то типа a и возвращает новую функцию, которая принимает что-то типа b и возвращает что-то типа c. Я также понимаю, что типы являются ассоциативными (отредактируйте: я был неправ в этом - см. Комментарии ниже), поэтому вышеприведенное можно переписать так, чтобы получить тот же результат:
(a -> b) -> c
Это описало бы функцию, которая принимает что-то типа a и что-то типа b и возвращает что-то типа c.
Я также слышал, что вы можете сделать дополнение (редактировать: действительно, слово, которое я искал здесь, двойственное - см. Комментарии ниже) к функции, переключая стрелки:
a <- b <- c
который я думаю эквивалентен
c -> b -> a
но я не уверен.
У меня вопрос, как называется этот вид математики? Я хотел бы узнать больше об этом, чтобы я мог использовать его, чтобы помочь мне писать лучшие программы. Я заинтересован в изучении таких вещей, как дополнительная функция и какие другие преобразования могут быть выполнены в объявлениях типов.
Спасибо!
4 ответа
В широком смысле это относится к сфере лямбда-исчисления.
Поскольку эта нотация связана с типами функций, вывод типов может быть также интересен для вас.
(Неправильные предположения, которые вы сделали относительно ассоциативности, уже должны быть достаточно прояснены другими ответами, поэтому я не буду повторять это)
Объявления типов не являются ассоциативными, a -> (b -> c) не эквивалентно (a -> b) -> c, Кроме того, вы не можете "переключать" стрелки, a <- b <- c неверный синтаксис
Обычная ссылка на ассоциативность в этом случае -> это право ассоциативно, что означает, что a -> b -> c интерпретируется как a -> (b -> c),
a -> (b -> c)
а также
(a -> b) -> c
не эквивалентны в Haskell. Это теория типов, которая может быть основана на теории категорий.
Первая - это функция, принимающая аргумент типа a и возвращая функцию типа b -> c, В то время как последний является функцией, принимающей функцию типа a -> b в качестве аргумента и возвращая значение типа c,
Что вы подразумеваете под дополнением к функции? Тип обратной функции функции типа a -> (b -> c) имеет тип (b -> c) -> a,
Функции типа a->b->c, которые на самом деле являются цепочками функций, как вы сказали, являются примерами карри