Newest at the top
| 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 |
| 2024-10-08 04:06:54 +0200 | <monochrom> | It's even the same phenomenon. The termination proof assumes induction, so it only covers what induction reaches. |
| 2024-10-08 04:05:34 +0200 | <EvanR> | it's illogical! |
| 2024-10-08 04:05:08 +0200 | <EvanR> | a related phenomenon, if you write a recursive algorithm to process a natural number and it recurses on something smaller than its argument, you can be sure it terminates. But then that fails if someone gives you an infinite number |
| 2024-10-08 04:03:31 +0200 | <EvanR> | it misses something |
| 2024-10-08 04:03:01 +0200 | <monochrom> | so I guess "infinite natural" and even "uncountable natural" can be legit names. |
| 2024-10-08 04:02:59 +0200 | <EvanR> | thirdofmayyaddayaddagoya: if you do classic induction to prove something, you proved it for all finite natural numbers, and that's it |
| 2024-10-08 04:02:39 +0200 | <monochrom> | We also say "make a Xerox copy" and then go on to use a Konica photocopier. |
| 2024-10-08 04:01:57 +0200 | <monochrom> | But we also say "lazy Krivine machine" where Krivine only wrote an eager machine and it was Sestoft who modified it to make a lazy machine. |
| 2024-10-08 04:01:40 +0200 | <EvanR> | that comes with its own induction rule |
| 2024-10-08 04:01:26 +0200 | <EvanR> | ordinals? xD |
| 2024-10-08 04:01:09 +0200 | <monochrom> | You can do it in set theory. It is just not called "the natural numbers" there. |
| 2024-10-08 04:00:28 +0200 | <EvanR> | though I'm not sure set theory would fix it |
| 2024-10-08 04:00:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> ok i see |
| 2024-10-08 03:59:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> oh |
| 2024-10-08 03:59:59 +0200 | <EvanR> | not set theory |
| 2024-10-08 03:59:47 +0200 | <EvanR> | specifically define the potentially infinite natural numbers using the coinductive style |
| 2024-10-08 03:59:20 +0200 | <haskellbridge> | <thirdofmay18081814goya> if you use a set-theoretic semantics any natural number is a finite set the only infinite set is the set of natural numbers itself, proofs on the set of all natural numbers use that method yeah |
| 2024-10-08 03:58:04 +0200 | <EvanR> | no |
| 2024-10-08 03:57:59 +0200 | <EvanR> | to prove something for all potentially infinite natural numbers, can you just prove it for 0 and assuming P for n prove it for n+1 |
| 2024-10-08 03:57:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 03:56:22 +0200 | <EvanR> | but if you look at another example, the potentially infinite natural number type... you can see how induction would fail |
| 2024-10-08 03:54:56 +0200 | <EvanR> | like one that doesn't lead to infinite data |
| 2024-10-08 03:54:35 +0200 | <EvanR> | for |