|
|
|
|
|
by innguest
4089 days ago
|
|
> It... doesn't. It does! :) > How do you interpret (>>) :: Monad m => m a -> m b -> m b as combining two maps of any kind The answer is in your question. Is -> not an arrow? Isn't there one of those arrows pointing into and out of every m x in the signature above? (for the first and last m x, there could be arrows pointing in and out, respectively). That means they are maps. A morphism is any value that has arrows pointing to it (from other values) and out of it (to other values). Read my answer above as well. I am not debating your arguments. I know you know what you are talking about and you are right in what you're saying otherwise. What I am saying is in Haskell everything except Bottom is a categorical morphism, and you seem to be ignoring this concept, which is helpful for those who are trying to make sense of all this. |
|
Notably, the Haskell arrows, the type of functions, happen to internalize the categorical arrows. This makes Hask cartesian closed. Thus, we have a correspondence between the arrows
and the objects This is why we often talk about function types as being categorical arrows.---
All that said, the type `m a` is not a function type let alone an arrow unless we happen to specialize `m` to be one. More specifically, the type `forall m . m a` is never a function type no matter the choice of `a`.
The notation `(-> m a)` or `(m a ->)` is... not actually a type. It's a type constructor at best (though it's illegal Haskell notation) which fits into a different kind of categorical construction if you want to go there.
The type `(a -> b)` "is" a valid arrow via the correspondence I mentioned earlier. The thing that's being referred to is the fully applied type constructor. If we have
then `Arr` is a type constructor of kind `(* -> * -> )` (e.g. a "type constructor constructor") and `Arr a` a type constructor of kind `( -> )`.The type* `Arr a b` is in correspondence with the morphisms of Hask. A combination of arrows would be a morphism from pairs of internal arrows to... something else
we can represent that with an internal arrow and then use the currying natural isomorphism which is the (internal) type of "arrow combining morphisms".That's the clearest I can explain what I'm on about. Where do you fit your notion of categorical morphism into there?