tag:blogger.com,1999:blog-3857512306503018420.post1613371941756742937..comments2023-12-29T08:31:12.200+00:00Comments on Nattermorphisms: The Category Theory of AppendagesBenhttp://www.blogger.com/profile/05535385464025706733noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-3857512306503018420.post-23943152106037552562010-06-25T10:56:27.902+01:002010-06-25T10:56:27.902+01:00Homes For Sale, Foreclosures listings from homesby...Homes For Sale, <a href="http://www.homesbylender.com/" rel="nofollow">Foreclosures</a> listings from homesbylender.com register free. If you are selling your home by owner visit homes by lender and list it here for free. <a href="http://www.homesbylender.com/" rel="nofollow">Homes For Sale</a>kristinawilshttps://www.blogger.com/profile/03461986298833928790noreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-46620423262698720842009-01-19T19:05:00.000+00:002009-01-19T19:05:00.000+00:00dysfunctor, unfortunately _|_ inhabits 'a' as well...dysfunctor, unfortunately _|_ inhabits 'a' as well. this seems like it works until you realize that there can't be a natural isomorphism between Either a Whatever and a because the extra member Right _|_ has no place it can be mapped to uniquely in a.Edward Kmetthttps://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-62657816764466234172009-01-19T13:47:00.000+00:002009-01-19T13:47:00.000+00:00In the coproduct monoidal category, shouldn't the ...In the coproduct monoidal category, shouldn't the coidentity be 'a' (the type of 'undefined')?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-4382829758613846052009-01-19T03:16:00.000+00:002009-01-19T03:16:00.000+00:00Hi there.Actually the choice of Void over () is de...Hi there.<BR/><BR/>Actually the choice of Void over () is deliberate and somewhat subtle.<BR/><BR/>() has two distinguishable members. _|_ and (), so there is extra 'information' available in a pair of () and another value, while Void is always _|_, so there is no information lost, hence its status as an identity. Technically since (,) introduces a bottom, it is already a bit of an approximation to say that Hask is Monoidal. If you go back to ~1.4 with strict pairs its true though. You can't have any extra information imparted because of the requirement that idr/coidr reflects a natural isomorphism. coidr should be called opidr or something, but see below.<BR/><BR/>> Why do you define inl and indr as methods of Monoidal? To me it seems<BR/>as if they'd belong to HasIdentity, as they are defined for this<BR/>property (based on http://en.wikipedia.org/wiki/Monoidal_category)<BR/><BR/>In Hask^op, (,) is the Sum, which has an identity, but coidr and coidl are defined, not idl and idr, so integrating them into HasIdentity is flawed because of lax scenarios where one way exists but not the other.<BR/> <BR/> * Are you sure<BR/>> HasIdentity Hask (,) Void<BR/>and<BR/>> Monoidal Hask (,) Void<BR/>is correct?<BR/><BR/>Yeah<BR/><BR/> <BR/>I'd expect<BR/>> HasIdentity Hask Either Void<BR/>> Monoidal Hask Either Void<BR/>> HasIdentity Hask (,) ()<BR/>> Monoidal Hask (,) ()<BR/><BR/>The use of the terms Monoidal and Comonoidal in that file are non-standard and apparently I dropped my documentation to that effect. ;) Mainly because idl and idr only witness the 'forward half' of the natural isomorphism between I * A and A for an identity I for * and so should probably be called something like LaxMonoidal, while coidl/coidr witness the 'backwards half' of the natural transformation, which is required for a lax comonoidal category. Since you need a full natural isomorphism to be truly monoidal, the irony is you need both definitions for idr/idl and coidr/coidl to be truly monoidal, and similarly you need the same definitions to be truly comonoidal. However, this then necessitates 4 functions with the exact same signature and no ambiguity, I should go through and clarify that in the commentary, and probably rename Monoidal/Comonoidal. Arguably they should be something like idr/idl/opidr/opidl and coidr/coidl/coopidr/coopidl, but the signatures are the same, co and op 'cancel' and it gets really confusing fast, i.e. which comes first in the name, co or op?<BR/><BR/>With that in mind, in a perfect world, a language's category could be a monoidal category over (,) and a comonoidal category over Either, which means in the terminology above, that Either would have a Monoidal Void-like Identity, unfortunately, for Either to have a true identity the type has to be truly uninhabited, which isn't possible in Haskell because _|_ is a member of every type. An Monoidal Identity for Either wouldn't even have _|_ as a member, so calling that identity 'Absurd' for the nonce, it would mean that if you have Either a Absurd, that you cannot have used the Right constructor at all, because you couldn't have applied it to a value. This means that it'd be safe to idr to always reduce Either a Absurd -> a without creating a _|_. Unfortunately the decision to allow _|_ in the Right slot is a decision of how Either and laziness interact and has nothing to do with the definition of Absurd. This is clearly required by the requirement that idr/opidr (er.. coidr currently) reflect a natural isomorphism. Either a Absurd can't have any more members than 'a', but Right _|_ is an extra member in Haskell. Contradiction.<BR/><BR/>An arguably more correct choice of terminology would be to move idl and idr into something like HasLaxIdentity and coidl and coidr into something like HasColaxIdentity, then make Monoidal and Comonoidal both require HasLaxIdentity and HasColaxIdentity, then correctness would be restored.Edward Kmetthttps://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-88073920440960194462009-01-19T00:09:00.000+00:002009-01-19T00:09:00.000+00:00I wrote a patch and submitted it, you can have a l...I wrote a patch and submitted it, you can have a look at it here:<BR/>http://darcswatch.nomeata.de/repo_http:__comonad.com_haskell_category-extras.htmlnomeatahttps://www.blogger.com/profile/05986291481431063004noreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-74167552176755046352009-01-18T23:26:00.000+00:002009-01-18T23:26:00.000+00:00While I’m at it, I find it strange that this libra...While I’m at it, I find it strange that this library defines these instances:<BR/>> HasIdentity Hask (,) Void<BR/>> Monoidal Hask (,) Void<BR/><BR/>I’d expect<BR/>> HasIdentity Hask Either Void<BR/>> Monoidal Hask Either Void<BR/>> HasIdentity Hask (,) ()<BR/>> Monoidal Hask (,) ()<BR/><BR/>Also I’d expect the methods "idl" and "idr", which correspond λ and ρ, as methods of HasIdentiy and I’m missing an method of Monoidal representing α (using the notation of http://en.wikipedia.org/wiki/Monoidal_category). Maybe I should submit a patch.nomeatahttps://www.blogger.com/profile/05986291481431063004noreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-31769969575934060372009-01-18T23:23:00.000+00:002009-01-18T23:23:00.000+00:00I think the coproduct monoid would correspond to a...I think the coproduct monoid would correspond to a Haskell class with methods "copappend :: Either a a -> a" and "copempty :: Void -> a". The latter function is completely useless, since there are no values of type Void.Twan van Laarhovenhttps://www.blogger.com/profile/18138442561179666544noreply@blogger.comtag:blogger.com,1999:blog-3857512306503018420.post-57889579640636493392009-01-18T23:18:00.000+00:002009-01-18T23:18:00.000+00:00> Under this definition, "monoids" wo...> Under this definition, "monoids" would be objects (ie Sets - as before), equipped with (a) a function to the set from the disjoint union of the set with itself, and (b) a function to the set from the empty set - ie the empty function.<BR/><BR/>Let’s see what we can make out of this. I’m going to write the elements of S={x,y,..}, and the elements of the disjoint union of S with itself as {Lx,Rx,Ly,Ry,...}, and the function that you describe in (a) as f.<BR/><BR/>Looking at the diagrams on http://en.wikipedia.org/wiki/Monoid_object, I think associativity requires f(f(LRx))=f(f(RLx)) and the other diagram implies that f(Lx) = x and f(Rx) = x (given that α, λ and ρ are chosen in the expected way).<BR/><BR/>It seems to me that this shows that each set is a categorial monoid in exactly one way. Basically, it’s forgetting which copy in a disjoint union an element lies.<BR/><BR/>In Haskell, this would be the function<BR/>> forgetEither :: Either a a -> a<BR/>> forgetEither (Left x) = x<BR/>> forgetEither (Right x) = x<BR/>and the empty function could be this one:<BR/>http://hackage.haskell.org/packages/archive/category-extras/latest/doc/html/Data-Void.htmlAnonymousnoreply@blogger.com