Матан для лямбда-исчисления

Интересная и очень полезная вещь мне открылась в Haskell.

Разбираясь с Cont монадой, я не мог понять, почему первое приближение оператора bind в виде простой аппликации плохое, то есть:

m >>= f = m f

В принципе оно работало хорошо для некоторых случаев, а придумать сходу пример для которого это не работало бы, было сложно. Но несмотря на все плюсы простой аппликации, тип какой то странный получался (хотел быть рекурсивным), а правильная реализация такая:

m >>= f = \k -> m (\a -> f a k)

Мне хотелось быстро сравнить два подхода и понять предельно чисто, где кроется суть. Но как? И тут пришло просветление. Нужно как в матане перебрать все варианты аргументов и посмотреть какие будут результаты.

Итак начнем. Есть у нас две функции: простая реализация и правильная.

bind1 m f = m f
bind2 m f = \k -> m (\a -> f a k)

Нужно выписать все возможные значения для аргументов. Начнем с m. m имеет тип:

m :: (a -> r) -> r

То есть m принимает один аргумент — функцию. Какие есть варианты? Можно проигнорировать аргумент и вернуть значение нужного типа, а можно воспользоваться аргументом. Получаем всего два варианта. Больше быть не может, так как все, что можно использовать для построения m — это ее аргумент.

m k = r   where r :: r
m k = k a where a :: a

*(еще мы использовали здесь переменные r и a — не могу пока их строго охарактеризовать — но они не должны использоваться при комбинировании возможных вариантов, т.е. для увеличения количества решений, а лишь как затычки в нужных местах)

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

-- 1.
m k = r
bind1 m f = r
bind2 m f = \k -> r

-- 2.
m k = k a
bind1 m f = f a
bind2 m f = f a

Видим, что в случае использования аргумента k, получаем одинаковое поведение для обоих реализаций, а в случае игнорирования — результаты разные. Если наполнить это смыслом, то если у нас m игнорирует свой аргумент, то мы имеем так называемый fail continuation, и используя простой подход результирующее выражение перестает быть continuation'ом, поскольку тип его больше не:

m :: (a -> r) -> r

Такой анализ возможен благодаря подходам к типизации в Haskell. Если сравнить с C++ Templates, которые типизируются только во время использования, где шаблонные типы наполнены лишним смыслом, в Haskell полиморфные функции типизируются сразу без привязки к использованию. Благодаря этому все чем можно пользоваться для реализации таких функций — это пара-тройка ее аргументов. Поэтому и количество возможных вариантов настолько маленькое, что такой анализ можно проводить на коленке.