Hi,
I have a question about monoidal categories. The axioms for a monoid are 1) composition, 2) existence of a left/right unit, and 3) associativity. For a monoidal category the tensor product define composition, there is a unit and laws for this unit, but I'm not sure I understand the associator. I mean there is an associator but there is also a daunting pentagram axiom diagram. Is there an explanation of this pentagram, I mean why do we need it to define a monoidal category and not to define a monoid ? Would not having it makes a monoidal category not equivalent to a monoid for the category of set ?
In Haskell I sometimes see the squiggle arrow to means "natural transformation" in some module doc. Are natural transformations really a thing in Haskell ? I mean Haskell can't check any law and natural transformation doesn't really provide any special operation like functors have fmap or monads have unit/join
NTs are useful for when you're talking about transforming the functor-y things and you don't care about what the a is. I believe Servant uses this and you also see it show up in foldFree iirc
Hi,
I have a question about monoidal categories. The axioms for a monoid are 1) composition, 2) existence of a left/right unit, and 3) associativity. For a monoidal category the tensor product define composition, there is a unit and laws for this unit, but I'm not sure I understand the associator. I mean there is an associator but there is also a daunting pentagram axiom diagram. Is there an explanation of this pentagram, I mean why do we need it to define a monoidal category and not to define a monoid ? Would not having it makes a monoidal category not equivalent to a monoid for the category of set ?
it might be more appropriate to post the question in the #Category Theory channel :sweat_smile:
hmm yes I didn't see there was a stream for category theory (I only have announcements/coq/f#/general/haskell/programming languages)
In Haskell I sometimes see the squiggle arrow to means "natural transformation" in some module doc. Are natural transformations really a thing in Haskell ? I mean Haskell can't check any law and natural transformation doesn't really provide any special operation like functors have fmap or monads have unit/join
the builtin operator
~is the type equality constraint.What kind of semantics would you expect for natural transformation functionality?
the usual commutaty square
I mean, what would it do in haskell?
I don't know, that's why I wonder if it's really a thing in Haskell like it is in category theory
you can require an NT as a parameter as
f :: (∀ a . g a -> h a) -> ...I guess you could do law checking with LiquidHaskell, though I don't know how satisfactory
but if I pass any function that have the type
forall a. g a -> h ait will type even if it's not a natural transformation ?ok
yep
All polymorphic functions in haskell are natural transformations, due to parametricity
NTs are useful for when you're talking about transforming the functor-y things and you don't care about what the
ais. I believe Servant uses this and you also see it show up infoldFreeiircThey technically pop up in stuff like
sequencetoo, or in general when threading functors through each other