Newest at the top
| 2024-10-28 12:33:08 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-10-28 12:30:10 +0100 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2024-10-28 12:19:39 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3406-c072-f489-680b-9cb7-dfd8.rev.sfr.net) alexherbo2 |
| 2024-10-28 12:17:43 +0100 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2024-10-28 12:06:19 +0100 | <xelxebar> | Cheers! |
| 2024-10-28 12:06:10 +0100 | <ncf> | xelxebar: ok, fixed it and added that reference |
| 2024-10-28 12:05:32 +0100 | <xelxebar> | And, well, the more general cata-fusion law itself follows directly from the definition of algebra homomorphism and cata as being initial. |
| 2024-10-28 12:02:54 +0100 | <xelxebar> | Well, I'm not actually sure that's the earliest original, but it's what I could track down. |
| 2024-10-28 12:01:52 +0100 | kuribas | (~user@ptr-17d51epnnpcnu3v8qjj.18120a2.ip6.access.telenet.be) kuribas |
| 2024-10-28 12:00:47 +0100 | <xelxebar> | ncf: Varmo Vene, Categorical Programming with Inductive and Coinductive Types. 2000. |
| 2024-10-28 11:59:46 +0100 | xff0x | (~xff0x@2405:6580:b080:900:b00a:f648:5747:c396) |
| 2024-10-28 11:58:50 +0100 | <ncf> | xelxebar: what's the original paper? |
| 2024-10-28 11:58:25 +0100 | <xelxebar> | Looks like the wiki is copying the error from E. Kmett reference, which is a defunct URL and needs to be viewed from archive.org. |
| 2024-10-28 11:57:36 +0100 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 2024-10-28 11:56:21 +0100 | <xelxebar> | Should say that `f . phi = psi . fmap f` implies `f . cata phi = cata psi`. |
| 2024-10-28 11:55:54 +0100 | acidjnk_new | (~acidjnk@p200300d6e72cfb165c062c18fa4bedb4.dip0.t-ipconnect.de) acidjnk |
| 2024-10-28 11:55:17 +0100 | <xelxebar> | Just for thoroughness, I tracked down the original paper where this was stated, and it indeed refers to a general algebra homomorphism. |
| 2024-10-28 11:54:32 +0100 | <xelxebar> | However, it should really apply to any algebra homomorphism. |
| 2024-10-28 11:54:15 +0100 | <xelxebar> | cata-fusion as stated on the wiki only applies to an algebra endomorphism. |
| 2024-10-28 11:53:21 +0100 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-28 11:53:20 +0100 | <xelxebar> | I think there's a typo in https://wiki.haskell.org/Catamorphisms#Laws |
| 2024-10-28 11:48:02 +0100 | alphazone | (~alphazone@2.219.56.221) |
| 2024-10-28 11:43:38 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-10-28 11:38:06 +0100 | mceresa | (~mceresa@user/mceresa) mceresa |
| 2024-10-28 11:35:45 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-28 11:33:43 +0100 | alphazone | (~alphazone@2.219.56.221) (Ping timeout: 264 seconds) |
| 2024-10-28 11:31:04 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-28 11:30:47 +0100 | euleritian | (~euleritia@dynamic-176-003-032-186.176.3.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-28 11:27:42 +0100 | euleritian | (~euleritia@dynamic-176-003-032-186.176.3.pool.telefonica.de) |
| 2024-10-28 11:27:06 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2024-10-28 11:26:08 +0100 | ubert | (~Thunderbi@178.165.189.55.wireless.dyn.drei.com) ubert |
| 2024-10-28 11:25:53 +0100 | <dminuoso> | Instead I was confused by the mixture of language and non-language constructs. :-) |
| 2024-10-28 11:25:06 +0100 | <Leary> | You can mentally replace the type-function expressions with `Kleisli f` and `Tannen f (->)`, I just didn't want to confuse my meta-notation with language constructs. They /are/ Categories in the same sense that many types /are/ Functor: their instance exists and is unique. |
| 2024-10-28 11:24:08 +0100 | <ncf> | well, we're talking about what the notation denotes, not the notation itself |
| 2024-10-28 11:23:43 +0100 | mceresa | (~mceresa@user/mceresa) (Ping timeout: 245 seconds) |
| 2024-10-28 11:22:58 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-28 11:22:56 +0100 | <ncf> | Monad f ⇔ Category (Kleisli f) |
| 2024-10-28 11:22:46 +0100 | <dminuoso> | How can "some abstract mathematical notation" "be a" (instance of?) Category? |
| 2024-10-28 11:22:40 +0100 | <ncf> | (a b ↦ a → f b) is Kleisli f |
| 2024-10-28 11:22:18 +0100 | <dminuoso> | I dont understand what that original statement by Leary means exactly. |
| 2024-10-28 11:22:07 +0100 | <ncf> | lambda abstraction |
| 2024-10-28 11:22:00 +0100 | <ncf> | dminuoso: no, that's just ↦ |
| 2024-10-28 11:21:50 +0100 | <ncf> | but anyway k is the type of objects there, so when you say (λ a b → a → f b) is a Category you mean the type of objects of that category is Type and the morphisms between a and b are functions a → f b |
| 2024-10-28 11:21:23 +0100 | Nixkernal | (~Nixkernal@52.131.63.188.dynamic.cust.swisscom.net) Nixkernal |
| 2024-10-28 11:21:19 +0100 | <dminuoso> | So :-> is meant as an actual type constructor? |
| 2024-10-28 11:21:00 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-10-28 11:20:59 +0100 | <ncf> | hm i guess that's not true any more, the argument to Category can have kind k → k → Type |
| 2024-10-28 11:20:13 +0100 | <ncf> | Haskell's Category is a typeclass for defining a category whose type of objects is Type |
| 2024-10-28 11:16:53 +0100 | habib | (~habib@146.70.119.186) (Ping timeout: 248 seconds) |
| 2024-10-28 11:15:34 +0100 | <dminuoso> | What is the difference between Category and category? |