Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Where did bind come from?

Using lambdabot's pl plug-in,

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

is converted to

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

What does the (=<<) mean here? I thought that it is only used with monads.

like image 399
ThePiercingPrince Avatar asked Feb 04 '14 15:02

ThePiercingPrince


People also ask

What is bind based on Valorant?

Bind is one of VALORANT's seven playable maps. It is one of the 4 maps released with the initial release of VALORANT. The map was also playable in the Beta Test. Bind features two one-way teleporters that allow you to go from one site to the other and they make noise when you go through them.

Where is bind located in real life?

Bind is a map designed after Rabat, Morocco. It was present in the game since the beta version. Bind is also known as the hometown of Cypher.

When did bind come out Valorant?

Bind. This map is located in Rabat, Morocco and its beta was released on April 7, 2020.

Where is bind located?

Map coordinates at 34°2'A" N 6°51'Z" W, off the coast of Rabat, Morocco.


2 Answers

Let's start with the definition

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

We want to convert this to point-free form. We can proceed step-by-step, but to understand it, you first have to know that

Functions form a monad

Or, more specifically, the type constructor (->) r, which you should think of as "functions from type r" or (r ->), is a monad. The best way to see it is to define the return and bind operations. The general form for a monad m is

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

Specialized to functions, you have

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

and you can convince yourself that the only sensible definitions are

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

This is completely equivalent to the Reader monad, also called the environment monad. The idea is that you have an additional parameter of type r (sometimes called the environment) which is being threaded through the computation - every function implicitly receives r as an additional argument.

Now we know everything we need to start making our function pointless.

Getting rid of recursion with fix

First thing is to remove the recursive reference to iterate. We can do this using fix, which has the definition

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

You can think of fix as the canonical recursive function, in that it can be used to define other recursive functions. The standard idiom is to define a non-recursive function g with an additional argument called func, which represents the function that you'd like to define. Applying fix to g computes the fixed point of g, which is the recursive function that you wanted.

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

We can convert this to lambda form

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

where the second line is just removed the infix : and replacing it with a prefix (:). Now that there are no self-references, we can proceed.

Removing some of the points with ap

We can use ap to pull out the references to x. The type of ap is

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

It takes a function in some monadic context, and applies it to a value in another monadic context. Note that this is already using the fact that functions (->) r form a monad! Specializing m to (->) r you get

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

The only way to make the types work out is if ap (specialized to functions) has the following definition

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

so that you use the second function g to build the second argument to the first function f. Note that this definition of ap is exactly equivalent to the combinator S in the SKI combinator calculus.

For us, this allows us to feed the parameter x to the first function (:) and use another function \y -> func f (f y) to build the second argument, which is the tail of the list. As a plus, we can then remove all refernce to x using eta reduction.

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

We can now remove the reference to y as well, by recognizing that func f (f y) is just the composition of func f and y.

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

Threading arguments through with (>>=)

Now we have the expression (func f . f), or (.) (func f) f if we use prefix notation. We'd like to describe this as some function applied to f, but that requires that we thread f into the expression in two places.

Fortunately, this is exactly what the monad instance for (->) r does! This makes total sense if you remember that the function monad is exactly equivalent to the reader monad, and the job of the reader monad is to thread an additional parameter into every function call.

The definition of bind specialized to functions is

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

The parameter r is first threaded through the left-hand argument of the bind, whose result is used by the right-hand argument to create a function that can consume another r. The mnemonic is that the parameter r is first threaded through the left argument, then through the right argument.

In our case we write (.) (func f) f = (func >>= (.)) f to get (using eta reduction)

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

Chaining compositions

Finally, we use another trick, repeated composition, to pull out the parameter func. The idea is that if you have an expression

f . g a

then you can replace it with

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

So you have expressed it as a function applied to an argument (ready for eta reduction!). In our case that means making the replacement

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

Finally, remove the inner brackets and describing the section with (=<<) instead of (>>=) gives

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

which is the same expression that lambdabot came up with.

like image 189
Chris Taylor Avatar answered Oct 02 '22 22:10

Chris Taylor


Yes, and the monad here is ((->) a): iterate f x obviously constructs a list, so the type of iterate is (a->a)->a->[a], so given (a->a), it produces (a->[a])

You can see that ap is given a function (:) :: a->[a]->[a], which must be m (a->b), so m here is (->) 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)

This is a function of two arguments, a->(b->c), so when it is passed to fix :: (a->a)->a, it must be that a=(b->c), and fix (ap...) :: b->c. In its turn, since this all is the same as iterate, it must be that b->c = (x->x)->(x->[x]), so b=(x->x), and c=(x->[x])

Indeed:

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

which will bind b=a after passing to fix.

Now, fix supplies the first argument to the above like so:

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

so we have:

iterate =
fix (\f g -> \x -> x : (f g $ g x)) =
\g x -> x : (iterate g $ g x)
like image 24
Sassa NF Avatar answered Oct 02 '22 21:10

Sassa NF