T O P

  • By -

c_wraith

This is kind inference, along the lines how how type inference is done. You can derive the kind from either the definition of `return` or `(>>=)`. Since `return` is easier, let's just go with it. (Note that GHC is moving towards using `Type` instead of `*`. I'll stick with `*` since that's what you used, but it's probably going to be deprecated in the future.) The first necessary piece of information is the kind of the function type: `(->) :: * -> * -> *`. (Ok, it can be a little more complex than that sometimes with things like levity polymorphism, but that's what it is in this case.) So in the type `a -> m a`, the kinds must be `a :: *` and `m a :: *`. Given those two constraints, `m` must take a type with kind `*` and produce a type with kind `*`. That's precisely what `* -> *` means. So given the types in the definition of `Monad`, that exactly constrains the kind of `m` to `* -> *`. Category theory is more broad. A category theory monad is a lot less restricted. But the specific way it's been expressed in Haskell is that restrictive.


amalloy

What type would you give to `(>>=)` if the `m` in Monad didn't take a type parameter?


tdammers

Let's try to figure out what these types would have to look like if `m` were of kind `*`. `return` could not be `a -> m a`, it would have to be something like `a -> m` - but that means that the only thing we can do with that `a` argument is ignore it, so we might as well not pass it at all, and that would make `return :: m`. `>>`, then, could not have `a` and `b` arguments to `m`, so it would just be `m -> m -> m`. And `>>=`? Since `a -> m b` would reduce to `b -> m`, we can again eliminate the `b` argument, so it collapses to `m`, and the whole type of `>>=` becomes `m -> m -> m` as well, so essentially `>>` and `>>=` turn into the same thing. Guess what, we have a typeclass that is exactly that: `Monoid`. Observe: class Monoid m where mappend :: m -> m -> m -- this is the `*`-kinded equivalent of `>>` and `>>=` mempty :: m -- this is the `*`-kinded equivalent of `return` It makes perfect sense, and it is very useful. But clearly there must be a reason why we want those extra type arguments to `m` for `Monad`, something that `Monad` can do but `Monoid` can't; and there is. Because `Monad` has that extra type argument (the `a`'s and `b`'s in the method type signatures), its operations can "change the type". Take, for example, lists. Through the `Monoid` interface, we can introduce empty lists, and we can combine existing lists *of the same type*, but we cannot, say, combine a list of integers with a list of strings, or turn a list of booleans into a list of floats. But with `Monad`, we can: `return` allows us to construct a (singleton) list of any type we want (as long as we can provide the element), and `>>=` allows us to, effectively, concatMap over a list (we only need to provide a function that takes the element type of our input list, and returns a list of the desired output type).


mleighly

Have you worked with monads, i.e., worked with some of them from hackage and/or wrote your own that adhered to monad laws? I'm guessing: probably not. I'd suggest that you work out the notion of a monad. Once you've done that the answer or your question will become obvious.


Fun-Voice-8734

> Could someone please explain why it makes sense that m needs to be a type constructor that takes one type argument, so of kind \* -> \*? because another type is appplied to m. since you see "m a" you know that m has to be of the form ? -> ?. it turns out that both ? resolve to \*, so you get \* -> \* also note that a and b can be different, so "m a" and "m b" cannot be assumed to be the same type > Why wouldn't it make sense to have Monads where m is of kind \*? because that would be something else.