Newest at the top
| 2024-10-23 11:37:48 +0200 | JamesMowery42 | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) JamesMowery |
| 2024-10-23 11:37:31 +0200 | aforemny | (~aforemny@2001:9e8:6cf3:ad00:f9bd:7d15:f62e:4b46) aforemny |
| 2024-10-23 11:28:32 +0200 | euleritian | (~euleritia@176.7.156.149) |
| 2024-10-23 11:28:02 +0200 | euleritian | (~euleritia@dynamic-176-006-134-024.176.6.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 2024-10-23 11:21:21 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-23 11:18:49 +0200 | <Leary> | elates directly to the structure of a fixpoint; it essentially arises from the same logic that gives you an implementation for `cata`. |
| 2024-10-23 11:18:48 +0200 | <Leary> | As for how you'd arive at these properties, it's a matter of mathematical taste. There's no real methodology other than to ask "what properties do I want?" Here's my view: identity and composition laws are bread and butter; that's cata-refl and cata-compose. I think cata-fusion is what cat theorists might call a /naturality/ condition; it arises from not wanting `cata` to care about what we're folding down to. cata-cancel is the only one that actually r |
| 2024-10-23 11:17:41 +0200 | ridcully | (~ridcully@p57b52138.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2024-10-23 11:13:53 +0200 | <Leary> | The line of questioning might need to be made more precise---I rather suspect the type signature alone already determines `cata`, and these properties follow. I'm not really sure why they're being called laws. I guess if you start with the properties alone in an untyped calculus, then `cata-cancel` alone gives you a definition for `cata`: just compose `outF` on the right. |
| 2024-10-23 11:05:50 +0200 | euleritian | (~euleritia@dynamic-176-006-134-024.176.6.pool.telefonica.de) |
| 2024-10-23 11:05:05 +0200 | euleritian | (~euleritia@dynamic-176-004-248-165.176.4.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 2024-10-23 11:04:13 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-23 11:02:50 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-23 11:02:44 +0200 | <xelxebar> | Even more, if you only knew the category theory def, how do you go about figuring out the necessary laws? |
| 2024-10-23 11:02:24 +0200 | fmira | (~user@user/fmira) (Remote host closed the connection) |
| 2024-10-23 11:00:43 +0200 | <xelxebar> | Leary: Yeah, they're each straightforward in isolation, but together do they imply the standard def? |
| 2024-10-23 10:58:19 +0200 | euleritian | (~euleritia@dynamic-176-004-248-165.176.4.pool.telefonica.de) |
| 2024-10-23 10:57:53 +0200 | euleritian | (~euleritia@dynamic-176-004-248-165.176.4.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 2024-10-23 10:55:21 +0200 | <lambdabot> | f . g = h . $map_F f => f . cata g = cata h |
| 2024-10-23 10:55:21 +0200 | <Leary> | @free cata :: (F a -> a) -> FixF -> a |
| 2024-10-23 10:55:07 +0200 | <Leary> | xelxebar: The first two should follow directly from the definition. The third one is a free theorem. Not sure about the last. |
| 2024-10-23 10:53:53 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-10-23 10:53:18 +0200 | <xelxebar> | I'd like to *derive* the cata-* ones from the initial morphism definition. |
| 2024-10-23 10:52:38 +0200 | <xelxebar> | More generally, if I'm reading about cats, what should I be thinking about to come up with similar laws on my own? |
| 2024-10-23 10:51:50 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-23 10:51:23 +0200 | fmira | (~user@user/fmira) (Remote host closed the connection) |
| 2024-10-23 10:50:53 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-23 10:50:43 +0200 | <xelxebar> | Are the cata laws essentially what guarantee its uniqueness? |
| 2024-10-23 10:50:40 +0200 | fmira | (~user@user/fmira) (Remote host closed the connection) |
| 2024-10-23 10:49:47 +0200 | <xelxebar> | I mean, cata-refl from above is pretty much Lambek's Theorem: https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#LambeksTheorem |
| 2024-10-23 10:49:21 +0200 | <xelxebar> | However, it's not entirely clear to me where the laws come from. |
| 2024-10-23 10:48:59 +0200 | <xelxebar> | Rather, I grok the definition of catamorphism in Haskell and also grok the cat theory definition. |
| 2024-10-23 10:48:13 +0200 | <xelxebar> | Trying to understand Catamorphism laws: https://wiki.haskell.org/Catamorphisms#Laws |
| 2024-10-23 10:47:43 +0200 | <haskellbridge> | <maerwald> those things are hard to manage correctly and deletion of files is always a dangerous thing to do automatically |
| 2024-10-23 10:45:55 +0200 | <haskellbridge> | <sm> I guess packages (and big caches like ghcide's, haskell-wasm's etc) are the big thing not managed by ghcup |
| 2024-10-23 10:44:04 +0200 | <haskellbridge> | <sm> cleaned up a little too hard.. never mind |
| 2024-10-23 10:36:59 +0200 | <haskellbridge> | <sm> ghcup tui is a big improvement, it gathers things in one place, you can see and delete easily |
| 2024-10-23 10:35:51 +0200 | ft | (~ft@p4fc2a216.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-10-23 10:35:33 +0200 | <haskellbridge> | <sm> cough, present company excepted |
| 2024-10-23 10:33:44 +0200 | eugenrh | (~eugenrh@user/eugenrh) (Quit: WeeChat 3.7.1) |
| 2024-10-23 10:31:18 +0200 | <haskellbridge> | <sm> I mean, it's not a fair comparison because I use a ton of haskell versions and don't build much with the others. But I know they'll be smaller. |
| 2024-10-23 10:30:44 +0200 | <haskellbridge> | <sm> I should clean up, but that's pretty bad. Compared to other languages, we look lazy |
| 2024-10-23 10:29:58 +0200 | <haskellbridge> | <sm> and finally: .stack, 106G. 2.4G for setup-exe-cache; 2.7G for pantry; 6.7G for three old ghc versions from before I switched to ghcup; and.. 94G of stack snapshot packages, spread across ~200 obscure directories under snapshots. |
| 2024-10-23 10:28:27 +0200 | <haskellbridge> | <maerwald> now add nix and another 500 GB |
| 2024-10-23 10:27:39 +0200 | euleritian | (~euleritia@dynamic-176-004-248-165.176.4.pool.telefonica.de) |
| 2024-10-23 10:27:17 +0200 | euleritian | (~euleritia@176.2.79.59) (Ping timeout: 255 seconds) |
| 2024-10-23 10:26:45 +0200 | <haskellbridge> | <sm> .cabal: 23.6G - packages for ~15 ghc versions, averaging ~1.5G each, plus 1G for the hackage index |
| 2024-10-23 10:24:48 +0200 | <haskellbridge> | <sm> .ghcup: 16G. 2G each for the last 7 ghc versions and another 2G for hls |
| 2024-10-23 10:24:28 +0200 | <haskellbridge> | <sm> .local/bin, mostly a bunch of fat haskell executables: 4.2G |
| 2024-10-23 10:24:07 +0200 | <haskellbridge> | <sm> .cache/ghcide: 2.8G; .ghc-wasm: 3.8G |