StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>A quick disclaimer: I'm a little shaky on category theory in general, while I get the impression you have at least some familiarity with it. Hopefully I won't make too much of a hash of this...</p> <blockquote> <p>Does anyone know of a tutorial that starts from category theory and explains IO, state, list monads in those terms?</p> </blockquote> <p>First of all, ignore <code>IO</code> for now, it's full of dark magic. It works as a model of imperative computations for the same reasons that <code>State</code> works for modelling stateful computations, but unlike the latter <code>IO</code> is a black box with no way to deduce the monadic structure from the outside.</p> <blockquote> <p>The functor is usually shown with the type: (a -> b) -> (m a -> m b) I included the second bracket just to emphasise the symmetry.</p> <p>But, this is an endofunctor, so shouldn't the domain and codomain be the same like this?:</p> </blockquote> <p>I suspect you are misinterpreting how type variables in Haskell relate to the category theory concepts. </p> <p>First of all, yes, that specifies an endofunctor, on the category of Haskell types. A type variable such as <code>a</code> is not anything in this category, however; it's a variable that is (implicitly) universally quantified over all objects in the category. Thus, the type <code>(a -> b) -> (a -> b)</code> describes only <em>endofunctors that map every object to itself</em>.</p> <p>Type constructors describe an injective function on objects, where the elements of the constructor's codomain cannot be described by any means except as an application of the type constructor. Even if two type constructors produce isomorphic results, the resulting types remain distinct. Note that type constructors are not, in the general case, functors.</p> <p>The type variable <code>m</code> in the functor signature, then, represents a one-argument type constructor. Out of context this would normally be read as universal quantification, but that's incorrect in this case since no such function can exist. Rather, the type class definition binds <code>m</code> and allows the definition of such functions for <em>specific</em> type constructors.</p> <p>The resulting function, then, says that for any type constructor <code>m</code> which has <code>fmap</code> defined, for any two objects <code>a</code> and <code>b</code> and a morphism between them, we can find a morphism between the types given by applying <code>m</code> to <code>a</code> and <code>b</code>.</p> <p>Note that while the above does, of course, define an endofunctor on <strong>Hask</strong>, it is not even remotely general enough to describe <em>all</em> such endofunctors.</p> <blockquote> <p>But the actual natural transformations we are using have type:</p> <p>a -> m a</p> <p>m a -> (a ->m b) -> m b</p> <p>Are these subsets of the general form above? and why are they natural transformations?</p> </blockquote> <p>Well, no, they aren't. A natural transformation is roughly a function (not a functor) between functors. The two natural transformations that specify a monad M look like <code>I -> M</code> where I is the identity functor, and <code>M ∘ M -> M</code> where <code>∘</code> is functor composition. In Haskell, we have no good way of working directly with either a true identity functor <em>or</em> with functor composition. Instead, we discard the identity functor to get just <code>(Functor m) => a -> m a</code> for the first, and write out nested type constructor application as <code>(Functor m) => m (m a) -> m a</code> for the second.</p> <p>The first of these is obviously <code>return</code>; the second is a function called <code>join</code>, which is not part of the type class. However, <code>join</code> can be written in terms of <code>(>>=)</code>, and the latter is more often useful in day-to-day programming.</p> <hr> <p>As far as specific monads go, if you want a more mathematical description, here's a quick sketch of an example:</p> <p>For some fixed type S, consider two functors F and G where F(x) = (S, x) and G(x) = S -> x (It should hopefully be obvious that these are indeed valid functors).</p> <p>These functors are also adjoints; consider natural transformations <code>unit :: x -> G (F x)</code> and <code>counit :: F (G x) -> x</code>. Expanding the definitions gives us <code>unit :: x -> (S -> (S, x))</code> and <code>counit :: (S, S -> x) -> x</code>. The types suggest uncurried function application and tuple construction; feel free to verify that those work as expected.</p> <p>An adjunction gives rise to a monad by composition of the functors, so taking G ∘ F and expanding the definition, we get G (F x) = S -> (S, x), which is the definition of the <code>State</code> monad. The <code>unit</code> for the adjunction is of course <code>return</code>; and you should be able to use <code>counit</code> to define <code>join</code>.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload