Arrows are a generalization of functions. A type `P a b` is a bit like the type `a -> b` in that it "consumes" `a`s and "produces" `b`s in some sense or another

Arrows are a generalization of functions. A type `P a b` is a bit like the type `a -> b` in that it "consumes" `a`s and "produces" `b`s in some sense or another, but it may behave in many ways differently from the function type. I'll use another notation (a ~> b) to indicate some "arrow" as opposed to a plain function. Generally, we ask of arrows that they compose and have an identity (a ~> b) (b ~> c) ---> (a ~> c) for any choice a, (a ~> a) that they work "around" products like tuples ( a ~> b ) becomes ((a, x) ~> (b, x)) for any type x and that we can "inject" normal functions in to them for any function (a -> b) we immediately have (a ~> b) Generalizations of functions contain normal values as well. Any arrow from the empty tuple to a value behaves a whole lot like that value by itself (() ~> a) is a lot like plain (a) itself so, just like with functions, we might see a type (a ~> b) as a "plain value" of `b` with some "holes" in it of shape `a`. Unlike with a pure function, however, the construction of this `b` may be done with some set of effects depending on the concrete choice of what `~>` means. A good example is the standard "FRP" arrow (a ~> b) === ((Time -> a) -> (Time -> b)) values (Time -> x) are "time varying x's", little movies playing out. A value of type (() ~> b) is nothing more than ((Time -> ()) -> (Time -> b)) and since the first argument is necessarily meaningless, (() -> b) is equivalent to (Time -> b). But (a ~> b) is a movie of `b` which can observe the movie of `a` before deciding how to act. So the `a`-shaped "hole" we have in `b` allows us to observe all of time before constructing our `b`.