Newest at the top
| 2024-10-08 06:34:45 +0200 | <Axman6> | I'm forgetting the name of something; "a finger-tree is an example of a non-??? recursive structure", I want to say ??? = uniform but I don't think that's right |
| 2024-10-08 06:24:28 +0200 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) {-d0t-} |
| 2024-10-08 06:19:30 +0200 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 265 seconds) |
| 2024-10-08 06:15:45 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 06:08:05 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
| 2024-10-08 06:07:51 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 2024-10-08 06:04:53 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2024-10-08 05:49:41 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 05:46:59 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 2024-10-08 05:44:40 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 272 seconds) |
| 2024-10-08 05:43:57 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-10-08 05:43:38 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 2024-10-08 05:31:20 +0200 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 2024-10-08 05:29:52 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-08 05:27:37 +0200 | ethantwardy | (user@user/ethantwardy) (Read error: Connection reset by peer) |
| 2024-10-08 05:27:37 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-08 05:22:21 +0200 | motherfsck | (~motherfsc@user/motherfsck) motherfsck |
| 2024-10-08 05:09:12 +0200 | zlqrvx_ | (~zlqrvx@101.175.150.247) (Ping timeout: 272 seconds) |
| 2024-10-08 05:01:04 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-10-08 04:59:04 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2024-10-08 04:52:51 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-10-08 04:52:19 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 260 seconds) |
| 2024-10-08 04:39:49 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 248 seconds) |
| 2024-10-08 04:36:59 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2024-10-08 04:31:07 +0200 | identity | (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.91)) |
| 2024-10-08 04:29:21 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-08 04:27:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> ty for comments helpful stuff |
| 2024-10-08 04:26:10 +0200 | <dolio> | It's nicer when the outermost level is a product, so there are multiple observations, like when data is a sum, with multiple constructors. |
| 2024-10-08 04:21:28 +0200 | <dolio> | Like unfoldr, but that only has one thing to observe. |
| 2024-10-08 04:19:25 +0200 | <dolio> | To build codata, you say what happens for all the ways of observing it, corecursively. |
| 2024-10-08 04:18:52 +0200 | <EvanR> | but maybe that's just prejudice leaking through from "a monad is this thing you wrap like a burrito" PTSD |
| 2024-10-08 04:17:41 +0200 | <EvanR> | and in the case of infinite data, assembling from the ground up is impossible |
| 2024-10-08 04:16:30 +0200 | <EvanR> | so if the value was assembled somehow yeah you could diassemble it, but it might just have multiple ways to proceed to the next observation which for all you know is unrelated to any construction sequence |
| 2024-10-08 04:16:02 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-10-08 04:15:39 +0200 | td_ | (~td@i5387092D.versanet.de) td_ |
| 2024-10-08 04:15:36 +0200 | <monochrom> | I don't, I didn't really read it. |
| 2024-10-08 04:15:28 +0200 | <EvanR> | the coinductive style gives you options for how to observe a value of the type, if you could ever obtain one to start with |
| 2024-10-08 04:15:17 +0200 | <monochrom> | And if that is not enough, look for "Bart Jacobs coalgebra". He's the coalgebra guy. |
| 2024-10-08 04:15:11 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: by any chance do you know how Hagino's type formation through adjunction works? |
| 2024-10-08 04:14:56 +0200 | <EvanR> | disassemble might give you the wrong idea |
| 2024-10-08 04:14:45 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: was planning to return to his thesis after foray into coinduction |
| 2024-10-08 04:13:58 +0200 | <monochrom> | Hagino's thesis has a toy language that lets you declare inductive types and coinductive types. (Or more accurately, initial algebra types and final coalgebra types.) You may find many answers there. You can just google "Hagino thesis". (I just did.) |
| 2024-10-08 04:13:33 +0200 | td_ | (~td@i5387091A.versanet.de) (Ping timeout: 246 seconds) |
| 2024-10-08 04:12:54 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: yes |
| 2024-10-08 04:12:40 +0200 | <monochrom> | Hagino says "co-natural number" instead of "infinite natural number". :) |
| 2024-10-08 04:12:37 +0200 | <EvanR> | is final coalgebra the categorical wonkery for coinductive types? |
| 2024-10-08 04:08:41 +0200 | <monochrom> | On recent exams I became careful to write "Prove by induction: For all finite lists xs, ..." :) |
| 2024-10-08 04:08:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm so then in a sense the final coalgebra gives you a canonical way to disassemble a thing |
| 2024-10-08 04:07:09 +0200 | <haskellbridge> | <thirdofmay18081814goya> sort of disassemble things |
| 2024-10-08 04:07:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm looks like coalgebras sort disassemble things |