Комментатор недавно заявил:
Свободные монады — это числа Чёрча — просто использующие (эндо-) функторы вместо функций!
Он продолжает объяснять это, говоря:
они оба являются эндофункцией (ионом | или), составленной 0 - n раз
Я понимаю, что числительные Черча представляют собой набор анонимных функциональных композиций с композицией для каждого числа. Я просто не понимаю, как это относится к Free Monads.
У меня вопрос: Являются ли монады Free числами Чёрча?
Вроде, как бы, что-то вроде.
Обобщение числительных Черча состоит в том, что числительное n равно f^n, где f является эндоморфизмом (стрелка, домен и домен которой являются одним и тем же объектом) в некоторой категория, а f^n означает "составить f сам с собой n раз". Обычные цифры Черча относятся к категории наборов, где стрелки являются функциями, например. число 3, примененное к f и x, равно f(f(f(x))). Например, если f(x) = x + 10, то 3 f 0 равно 30.
В категории из категорий стрелки являются функторами. Там число 3, примененное к некоторому функтору f и объекту x (например, типу), снова равно f(f(f(x))). Если f, например. конструктор типа f x = Int => x, тогда 3 f String равен Int => Int => Int => String, типу функций, которые принимают три аргумента Int и возвращают String.
Теперь для функтора f Free f — это свободная монада, сгенерированная f, где экземпляр типа Free f x является либо просто x, либо f (Free f x). Таким образом, он будет иметь тип формы f(f(f(...(x))), состав из нуля или более f, примененный к x.
Таким образом, дело не в том, что «свободные монады являются числами Черча», а в том, что свободная монада является конструкцией типа на некотором функторе, а числа Черча на этом функторе встраиваются в этот тип.
