Откуда взялось соединение? - программирование
Подтвердить что ты не робот

Откуда взялось соединение?

Используя плагин lambdabot pl,

let iterate f x = x : iterate f (f x) in iterate

преобразуется в

fix ((ap (:) .) . ((.) =<<))

Что означает (=<<) здесь? Я думал, что он используется только с монадами.

4b9b3361

Ответ 1

Здесь короткий, простой комбинаторы - определение стиля:

iterate f x 
   = x : iterate f (f x) 
   = (:) x ((iterate f . f) x)
   = ap (:) (iterate f . f) x            -- ap g f x = g x (f x)       (1)
   = ap (:) ((.) (iterate f) f) x
   = ap (:) ( ((.) =<< iterate) f) x     -- (g =<< f) x = g (f x) x    (2)
   = ap (:) ( ((.) =<<) iterate f) x
   = ((ap (:) .) . ((.) =<<)) iterate f x 
       -- ((f .) . g) x y = (f .) (g x) y = (f . g x) y = f (g x y)    (3)

так, по eta-сокращению,

iterate = ((ap (:) .) . ((.) =<<)) iterate
        = fix ((ap (:) .) . ((.) =<<))    -- fix f = x where x = f x   (4)

QED. (1) и (2) исходят из того, о чем вы спрашиваете, функционируют как монады, уже объясненные в Крисе:

  ap :: (Monad m) => m (a->b) ->   m a  ->  m b              m ~ (r ->)
  that            (r->a->b) -> (r->a) -> r->b 
  so            ap     g           f       x   = g x (f x)

  (=<<) :: (Monad m) => (a-> m b) ->   m a  ->  m b          m ~ (r ->)
  that                (a->r->b) -> (r->a) -> r->b
  so            (=<<)      g           f       x   = g (f x) x

(3) обсуждается, например, здесь и здесь.

Ответ 2

Начнем с определения

iterate f x = x : iterate f (f x) 

Мы хотим преобразовать это в бесплатную форму. Мы можем идти шаг за шагом, но чтобы понять это, вам сначала нужно знать, что

Функции образуют монаду

Или, более конкретно, конструктор типа (->) r, который вы должны рассматривать как "функции из типа r" или (r ->), является монадой. Лучший способ увидеть это - определить операции возврата и привязки. Общая форма для монады m равна

return :: a -> m a
(>>=)  :: m a -> (a -> m b) -> m b

Специализируется на функциях, у вас есть

return :: a -> r -> a
(>>=)  :: (r -> a) -> (a -> r -> b) -> r -> b

и вы можете убедить себя, что единственными разумными определениями являются

return x = \r -> x -- equivalent to 'const x'
f >>=  g = \r -> g (f r) r

Это полностью эквивалентно монаде читателя, также называемому монадой среды. Идея состоит в том, что у вас есть дополнительный параметр типа r (иногда называемый средой), который проходит через вычисление - каждая функция неявно получает r в качестве дополнительного аргумента.

Теперь мы знаем все, что нам нужно, чтобы сделать нашу функцию бессмысленной.

Избавление от рекурсии с помощью fix

Прежде всего, нужно удалить рекурсивную ссылку на iterate. Мы можем сделать это с помощью fix, который имеет определение

fix :: (t -> t) -> t
fix f = f (fix f)

Вы можете думать о fix как о канонической рекурсивной функции, поскольку его можно использовать для определения других рекурсивных функций. Стандартная идиома - это определение нерекурсивной функции g с дополнительным аргументом func, который представляет функцию, которую вы хотите определить. Применение fix to g вычисляет неподвижную точку g, которая является необходимой вами рекурсивной функцией.

iterate = fix g where g func f x = x : func f (f x)

Мы можем преобразовать это в лямбда-форму

iterate = fix (\func f x -> x : func f (f x))
        = fix (\func f x -> (:) x (func f (f x)))

где вторая строка просто удаляет инфикс : и заменяет его префиксом (:). Теперь, когда нет самореференций, мы можем продолжить.

Удаление некоторых точек с помощью ap

Мы можем использовать ap для вывода ссылок на x. Тип ap -

ap :: (Monad m) => m (a -> b) -> m a -> m b

Он принимает функцию в каком-то монадическом контексте и применяет ее к значению в другом монадическом контексте. Обратите внимание, что это уже использует тот факт, что функции (->) r образуют монаду! Специализируясь m - (->) r, вы получаете

ap :: (r -> a -> b) -> (r -> a) -> (r -> b)

Единственный способ, с помощью которого выполняются типы, - это если ap (специализированный для функций) имеет следующее определение

ap f g = \r -> f r (g r)

чтобы вы использовали вторую функцию g, чтобы построить второй аргумент для первой функции f. Обратите внимание, что это определение ap в точности эквивалентно комбинатору S в расчёте комбинаторов SKI.

Для нас это позволяет нам передать параметр x первой функции (:) и использовать другую функцию \y -> func f (f y) для построения второго аргумента, который является хвостом списка. В качестве плюса мы можем удалить все ссылки на x с помощью eta-сокращения.

iterate = fix (\func f x -> ap (:) (\y -> func f (f y)) x)
        = fix (\func f   -> ap (:) (\y -> func f (f y))  )

Теперь мы можем удалить ссылку на y, признав, что func f (f y) является просто композицией func f и y.

iterate = fix (\func f   -> ap (:) (      func f . f)    )

Аргументы Threading с помощью (>>=)

Теперь мы имеем выражение (func f . f) или (.) (func f) f, если использовать префиксную нотацию. Мы хотели бы описать это как некоторую функцию, применяемую к f, но это требует, чтобы мы вносили f в выражение в двух местах.

К счастью, это именно то, что делает экземпляр монады для (->) r! Это имеет смысл, если вы помните, что функция monad в точности эквивалентна монаде читателя, а работа монады-читателя - вносить дополнительный параметр в каждый вызов функции.

Определение привязки, специализированной для функций,

f >>= g = \r -> g (f r) r

Параметр r сначала передается через левый аргумент связывания, результат которого используется правым аргументом для создания функции, которая может потреблять другой r. Мнемоника заключается в том, что параметр r сначала пронизывается через левый аргумент, а затем через правый аргумент.

В нашем случае мы пишем (.) (func f) f = (func >>= (.)) f для получения (с использованием eta reduction)

iterate = fix (\func f   -> ap (:)  ((func >>= (.)) f))
        = fix (\func     -> ap (:) . (func >>= (.))   )

Цепочки композиций

Наконец, мы используем другой трюк, повторяющийся состав, чтобы вытащить параметр func. Идея состоит в том, что если у вас есть выражение

f . g a

то вы можете заменить его на

f . g a = (.) f (g a)
        = (((.) f) . g) a
        = ((f .) . g) a

Итак, вы выразили его как функцию, применяемую к аргументу (готово к сокращению eta!). В нашем случае это означает замену

iterate = fix (\func     -> (ap (:) .) . (>>= (.)) func)
        = fix (            ((ap (:) .) . (>>= (.))     )

Наконец, удалите внутренние скобки и описав раздел (=<<) вместо (>>=), дайте

iterate = fix ((ap (:) .) . ((.) =<<))

которое является тем же выражением, что и lambdabot.

Ответ 3

Да, а монада здесь ((->) a): iterate f x, очевидно, создает список, поэтому тип iterate равен (a->a)->a->[a], поэтому задан (a->a), он производит (a->[a])

Вы можете видеть, что ap задана функция (:) :: a->[a]->[a], которая должна быть m (a->b), поэтому m здесь (->) a.

(ap (:) .) . ((.) =<<) =
\f -> (ap (:) .) . ((.) =<<) $ f =
\f -> ap (:) . ((.) =<< f) = -- at this stage we can see =<< is of (->) a monad,
                       -- whose bind is the S-combinator: s f g x = f (g x) x
\f -> ap (:) . (f >>= (.)) =
\f g -> ap (:) (f g . g) = -- ok, ap is also the S-combinator with some
                           -- arguments swapped around
-- you see, for monad ((->) r), ap needs function of type (r->(a->b)) = (r->a->b)
-- whereas >>= needs (a->(r->b)) = (a->r->b) - the same function flipped
\f g -> (flip (:)) =<< (f g . g) =
\f g -> \x -> x : (f g $ g x)

Это функция из двух аргументов, a->(b->c), поэтому, когда она передается в fix :: (a->a)->a, она должна быть a=(b->c) и fix (ap...) :: b->c. В свою очередь, поскольку это все равно, что iterate, должно быть, что b->c = (x->x)->(x->[x]), поэтому b=(x->x) и c=(x->[x])

Действительно:

Prelude Control.Monad> :t ((ap (:) .) . ((.) =<<))
((ap (:) .) . ((.) =<<))
  :: (Monad ((->) (a -> b)), Monad ((->) a)) =>
     ((a -> b) -> b -> [a]) -> (a -> b) -> a -> [a]

который свяжет b=a после перехода к fix.

Теперь fix предоставляет первый аргумент выше, например:

fix h = let x = h x in x
hence, iterate = fix h = let iterate = h iterate in iterate 
-- supply iterate as the first
-- argument to the function passed to fix

поэтому имеем:

iterate =
fix (\f g -> \x -> x : (f g $ g x)) =
\g x -> x : (iterate g $ g x)