Newest at the top
| 2025-01-29 00:10:35 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-29 00:09:59 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 2025-01-29 00:07:30 +0100 | mulk | (~mulk@pd9514894.dip0.t-ipconnect.de) mulk |
| 2025-01-29 00:04:15 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-28 23:59:58 +0100 | kuribas` | (~user@ptr-17d51epnlr9u1hv5k0s.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2025-01-28 23:43:44 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 23:43:39 +0100 | myme | (~myme@40.51-175-185.customer.lyse.net) (Ping timeout: 252 seconds) |
| 2025-01-28 23:39:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 23:35:30 +0100 | <mauke> | dead poset society |
| 2025-01-28 23:30:29 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 23:27:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2025-01-28 23:25:40 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 23:24:17 +0100 | nckx_ | nckx |
| 2025-01-28 23:23:55 +0100 | nckx | (nckx@libera/staff/owl/nckx) (Ping timeout: 608 seconds) |
| 2025-01-28 23:23:22 +0100 | nckx_ | (nckx@libera/staff/owl/nckx) nckx |
| 2025-01-28 23:23:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 23:22:54 +0100 | mulk | (~mulk@pd9514894.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2025-01-28 23:17:48 +0100 | <monochrom> | Probably. It's been a while. |
| 2025-01-28 23:17:32 +0100 | <tomsmeding> | this is not a normal form, this is just a triviality. I maintain that the theorem you're thinking of is probably slightly more subtle so that it doesn't allow my cop-out :) |
| 2025-01-28 23:17:14 +0100 | haritz | saimazoon |
| 2025-01-28 23:17:07 +0100 | <monochrom> | OTOH this kind of normal-form theorems are always welcome in theoretical work. |
| 2025-01-28 23:16:55 +0100 | <tomsmeding> | (that's a fun phrase out of context) |
| 2025-01-28 23:16:50 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-01-28 23:16:30 +0100 | <tomsmeding> | I'd say the plagiarism is not the part that's most useless about my construction |
| 2025-01-28 23:16:09 +0100 | confused_rust_en | (~confused_@2603:7081:1600:6425:187f:fcc6:e582:3131) (Quit: Client closed) |
| 2025-01-28 23:15:46 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-01-28 23:15:36 +0100 | <monochrom> | OK right but my point stands with errata on wording. Someone else has coded up f, so you just plagiarize that in the cata stage. |
| 2025-01-28 23:15:24 +0100 | <tomsmeding> | s/do/to/ |
| 2025-01-28 23:15:17 +0100 | <tomsmeding> | your non-constructive proof is probably about a more subtle statement where T is forced do actually be something useful somehow |
| 2025-01-28 23:14:25 +0100 | <tomsmeding> | which is extremely unhelpful |
| 2025-01-28 23:14:18 +0100 | <tomsmeding> | given `f :: A -> B`, do `cata f . ana id` |
| 2025-01-28 23:13:55 +0100 | <monochrom> | Oh wait, yeah, I misread, sorry! |
| 2025-01-28 23:13:44 +0100 | <tomsmeding> | monochrom: `data T = MkT A`, happy now? :p |
| 2025-01-28 23:13:29 +0100 | <tomsmeding> | if I read the venerable wikipedia correctly, the ana of my T would just be `ana :: (x -> A) -> x -> T` and the cata would be `cata :: (A -> r) -> T -> r` |
| 2025-01-28 23:13:23 +0100 | <monochrom> | OTOH I am not sure how to kind-check "T = T A" :) |
| 2025-01-28 23:12:49 +0100 | <monochrom> | I don't know. Too lazy to check. :) |
| 2025-01-28 23:12:44 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-01-28 23:12:37 +0100 | <tomsmeding> | doesn't my T work? |
| 2025-01-28 23:12:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 23:12:28 +0100 | <monochrom> | Hence completely unhelpful even though sounding very elegant and unifying. |
| 2025-01-28 23:12:00 +0100 | <monochrom> | So the theorem doesn't tell you how to design T. Instead, you have to design T and then the theorem just plagiarizes you! |
| 2025-01-28 23:11:59 +0100 | jespada | (~jespada@r190-133-42-215.dialup.adsl.anteldata.net.uy) (Ping timeout: 260 seconds) |
| 2025-01-28 23:11:40 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-01-28 23:11:28 +0100 | <monochrom> | IIRC it's even worse. The only known proof is non-constructive, or only relatively constructive. It goes: since we are told it's computable, someone must have found an algorithm, now just turn that into T. |
| 2025-01-28 23:11:18 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-01-28 23:09:46 +0100 | <tomsmeding> | ah, that's wrong. Set `data T = T A`. |
| 2025-01-28 23:09:25 +0100 | <tomsmeding> | if the function goes A -> B, set T = A. |
| 2025-01-28 23:08:58 +0100 | <monochrom> | Related unhelpful theorem: For every computable function, there exists an intermediate data structure T such that the function is composed of ana'ing input into T and then cata'ing T into output. |
| 2025-01-28 23:08:43 +0100 | img | (~img@user/img) (Ping timeout: 245 seconds) |
| 2025-01-28 23:07:24 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |