Logs: freenode/#haskell
| 2021-03-24 16:33:13 | <ski> | mu r. F r = F (F (F (F (...))) >---> ... >---> F (F (F r)) >---> F (F r) >---> F r >---> r |
| 2021-03-24 16:33:26 | <ski> | that's what `ana' and `cata' does |
| 2021-03-24 16:33:43 | <peanut_> | 🤔 |
| 2021-03-24 16:34:00 | <ski> | tomsmeding : no. `mu r. a * r' would be `0' |
| 2021-03-24 16:34:01 | × | emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer) |
| 2021-03-24 16:34:12 | <tomsmeding> | lol |
| 2021-03-24 16:34:13 | → | emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) |
| 2021-03-24 16:34:19 | <tomsmeding> | I guess it satisfies the relation indeed |
| 2021-03-24 16:34:20 | <ski> | with no starting points to generate from, you can't get off the ground |
| 2021-03-24 16:34:48 | <ski> | ij : algebra / coalgebra |
| 2021-03-24 16:35:16 | <siraben> | I wish Algebra of Programming went into coalgebras more |
| 2021-03-24 16:35:23 | <siraben> | they only talked about least fixed points of functors which is Mu |
| 2021-03-24 16:36:18 | → | son0p joins (~son0p@181.136.122.143) |
| 2021-03-24 16:36:46 | <siraben> | IIRC there was some comprehensive overview bringing algebras, coalgebras and program calculation together |
| 2021-03-24 16:36:54 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-03-24 16:36:55 | <siraben> | Ah yes, https://www.springer.com/gp/book/9783540436133 |
| 2021-03-24 16:37:23 | <siraben> | ski: if Hask is not a category, what should one use to analyze Haskell programs? Does CCC suffice? |
| 2021-03-24 16:38:05 | <sclv> | one uses Hask |
| 2021-03-24 16:38:10 | × | kritzefitz quits (~kritzefit@2003:5b:203b:200::10:49) (Remote host closed the connection) |
| 2021-03-24 16:38:18 | <sclv> | actual haskell doesn't correspond quite to Hask, but the total fragment does |
| 2021-03-24 16:38:20 | ski | . o O ( "A Tutorial on (Co)Algebras and (Co)Induction" by Bart Jacobs,Jan Rutten in 1997 at <https://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf> ) |
| 2021-03-24 16:38:59 | <sclv> | so people do proofs in the total fragment and then make ad hoc arguments about how they extend to the language with partiality |
| 2021-03-24 16:39:02 | <siraben> | ski: thanks for the reference. |
| 2021-03-24 16:39:06 | → | heatsink_ joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2021-03-24 16:39:08 | <siraben> | Coalgebras should be given just as much weight! |
| 2021-03-24 16:39:14 | <ski> | yes |
| 2021-03-24 16:39:33 | <tomsmeding> | ski: I think I get the feeling, but I need to digest a bit more. Thanks for the intro :) |
| 2021-03-24 16:39:34 | <ski> | coalgebras are related to state machines, dynamical systems, objects (in the sense of object-orientation) |
| 2021-03-24 16:39:43 | <siraben> | sclv: something like "Fast and Loose Reasoning is Morally Correct" https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf ? |
| 2021-03-24 16:39:54 | <sclv> | people have speculated about a sort of enriched notion of a category where you might do everything directly (with partiality baked into the arrows) but its never been adequately worked out |
| 2021-03-24 16:40:01 | <sclv> | siraben: yeah, basically |
| 2021-03-24 16:40:02 | <siraben> | ski: how does bisimulation fit into the picture? |
| 2021-03-24 16:40:12 | <ski> | (it's no coincidence that existentials often comes up when people are doing some kind of OO-like stuff) |
| 2021-03-24 16:40:36 | <sclv> | bisimulation is an equality relation one can use for coinductive stuff, which can be used in some proofs |
| 2021-03-24 16:40:36 | × | emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer) |
| 2021-03-24 16:40:47 | → | emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) |
| 2021-03-24 16:40:53 | <ski> | siraben : behavioural equivalence of objects or processes. related to coinduction in some not totally obvious way |
| 2021-03-24 16:40:59 | <sclv> | the other thing i'm fond of is clocked/guarded recursive type theory |
| 2021-03-24 16:41:15 | <siraben> | I see. |
| 2021-03-24 16:41:22 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 260 seconds) |
| 2021-03-24 16:41:26 | <sclv> | so one can work in a language with richer typing (a guarded delay modality) and project the proofs down to a system lacking them |
| 2021-03-24 16:41:26 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:b09b:3609:dd4b:42c9) (Ping timeout: 264 seconds) |
| 2021-03-24 16:41:32 | <siraben> | btw sclvare you a researcher? |
| 2021-03-24 16:41:53 | <sclv> | sporadically, i'm really more in industry, but i try to keep up |
| 2021-03-24 16:41:55 | <ski> | anyway, above, each `F' could be thought of as a "layer" in a data structure. with `ana', you're building up layers. with `cata', you're tearing them down |
| 2021-03-24 16:42:05 | <siraben> | oh, very nice. |
| 2021-03-24 16:42:39 | → | Merfont joins (~Kaiepi@47.54.252.148) |
| 2021-03-24 16:43:17 | <ski> | for termination, `cata' assumes that all paths/branches are finite (but they be of unbounded depth, e.g. in the infinitely-wide tree case). while `ana' assumes that you'll only ever inspect a path to finite depth (or else you'd not get progress) |
| 2021-03-24 16:43:41 | <ski> | (s/they be/they could be/) |
| 2021-03-24 16:43:56 | × | ozataman quits (~ozataman@pool-151-202-25-12.nycmny.fios.verizon.net) (Ping timeout: 240 seconds) |
| 2021-03-24 16:44:37 | → | LKoen joins (~LKoen@194.250.88.92.rev.sfr.net) |
| 2021-03-24 16:44:39 | <ski> | inductive data types are associated with termination, and coinductive are associated with progress. as in a server eventually making progress, not getting stuck, while still potentially never terminating |
| 2021-03-24 16:44:50 | <tomsmeding> | cool! |
| 2021-03-24 16:45:25 | <ski> | (in general, in total programming, one would commonly use "termination" (or "termination and progress") as an umbrella term for both) |
| 2021-03-24 16:45:33 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-24 16:45:55 | <ski> | if you have a `Stream a' (infinite depth), you can inspect it with a `Nat' (finite depth), and you'll terminate |
| 2021-03-24 16:46:15 | <ski> | if you attempted to inspect it with an "infinite natural" (`inf = Succ inf'), you'd not terminate |
| 2021-03-24 16:46:43 | × | Kaeipi quits (~Kaiepi@47.54.252.148) (Ping timeout: 245 seconds) |
| 2021-03-24 16:46:45 | × | notzmv quits (~zmv@unaffiliated/zmv) (Ping timeout: 264 seconds) |
| 2021-03-24 16:47:12 | × | beardhatcode quits (robbertbea@gateway/shell/matrix.org/x-czxkutvkgyyqphjm) (Ping timeout: 260 seconds) |
| 2021-03-24 16:47:44 | × | mrus[m] quits (mrusmatrix@gateway/shell/matrix.org/x-nyxisannhqxusqip) (Ping timeout: 268 seconds) |
| 2021-03-24 16:47:44 | × | unclechu quits (unclechuma@gateway/shell/matrix.org/x-wfyfrzflxiiafrog) (Ping timeout: 268 seconds) |
| 2021-03-24 16:48:21 | × | invent[m] quits (inventmatr@gateway/shell/matrix.org/x-vetnnuxstyqknlip) (Ping timeout: 268 seconds) |
| 2021-03-24 16:48:21 | × | jkaye[m] quits (jkayematri@gateway/shell/matrix.org/x-qbldkaokruodskkg) (Ping timeout: 268 seconds) |
| 2021-03-24 16:48:58 | × | arcontethegreat[ quits (arcontethe@gateway/shell/matrix.org/x-godgukqzijrupgty) (Ping timeout: 268 seconds) |
| 2021-03-24 16:48:58 | × | plumenator[m] quits (plumenator@gateway/shell/matrix.org/x-ljfdmyhcpdaqbemc) (Ping timeout: 268 seconds) |
| 2021-03-24 16:49:45 | <siraben> | How would you ensure a long lived process such as a server doesn't get stuck? |
| 2021-03-24 16:50:21 | × | idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 264 seconds) |
| 2021-03-24 16:50:49 | <monochrom> | That sounds very broad. But most causes of deadlocks are well known, so "just don't do that". |
| 2021-03-24 16:50:57 | <ski> | there are also coalgebras in (non-CS related) math. e.g. "comonoids in a monoidal category" (confusingly, usually (it seems) called just "coalgebras", <https://en.wikipedia.org/wiki/Coalgebra>, specifically in the monoidal category of vector spaces, with tensor multiplication) |
| 2021-03-24 16:51:53 | <davean> | siraben: my question is "How could it possibly get stuck?" |
| 2021-03-24 16:53:15 | <ski> | (dolio recently linked to the talk "Coalgebra in Continuous Mathematics" by Larry Moss in 2020 at <https://youtu.be/XqywV-wkKSE?t=2486>) |
| 2021-03-24 16:53:47 | <siraben> | I mean, would that entail modeling the server as a stream that is always productive? |
| 2021-03-24 16:54:16 | <ski> | siraben : ensure that all subdivisions of its evolution, that involves at least one interaction with the environment, terminates ? |
| 2021-03-24 16:54:34 | <ski> | yes |
| 2021-03-24 16:54:55 | <ski> | (or perhaps in some other way, that implies such a modelling would be possible) |
| 2021-03-24 16:56:42 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 2021-03-24 16:57:08 | × | geekosaur quits (ac3a8f06@172.58.143.6) (Quit: Connection closed) |
| 2021-03-24 16:57:30 | × | heatsink_ quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-03-24 16:57:53 | ski | . o O ( "Hask is not a category" by Andrej Bauer in 2016-08-06 at <http://math.andrej.com/2016/08/06/hask-is-not-a-category/> ) |
| 2021-03-24 16:58:22 | × | andreas31 quits (~andreas@gateway/tor-sasl/andreas303) (Ping timeout: 268 seconds) |
| 2021-03-24 16:59:00 | → | jaroslawj joins (~jaroslawj@185.234.208.208.r.toneticgroup.pl) |
| 2021-03-24 16:59:01 | <Uniaika> | maralorn: great, thanks :) |
| 2021-03-24 16:59:34 | → | andreas31 joins (~andreas@gateway/tor-sasl/andreas303) |
| 2021-03-24 17:01:10 | × | jaroslawj quits (~jaroslawj@185.234.208.208.r.toneticgroup.pl) (Client Quit) |
| 2021-03-24 17:01:34 | → | Cale joins (~cale@cpef48e38ee8583-cm0c473de9d680.cpe.net.cable.rogers.com) |
| 2021-03-24 17:02:26 | → | beardhatcode joins (robbertbea@gateway/shell/matrix.org/x-wsgksmmgbbxtiufa) |
| 2021-03-24 17:02:33 | → | unclechu joins (unclechuma@gateway/shell/matrix.org/x-rroohkjsifdpbejc) |
| 2021-03-24 17:02:59 | → | mrus[m] joins (mrusmatrix@gateway/shell/matrix.org/x-yhszxvhsbugdebak) |
| 2021-03-24 17:03:09 | × | xff0x quits (~xff0x@2001:1a81:53c9:9f00:27ac:86d9:28a4:2240) (Ping timeout: 268 seconds) |
| 2021-03-24 17:03:48 | → | xff0x joins (~xff0x@2001:1a81:53c9:9f00:1ee:8e19:4d6b:903d) |
| 2021-03-24 17:04:45 | × | romesrf quits (~romesrf@44.190.189.46.rev.vodafone.pt) (Quit: WeeChat 3.1) |
| 2021-03-24 17:05:09 | → | ph88 joins (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) |
| 2021-03-24 17:06:21 | → | jkaye[m] joins (jkayematri@gateway/shell/matrix.org/x-oneawtzvjyybiofe) |
| 2021-03-24 17:06:35 | → | invent[m] joins (inventmatr@gateway/shell/matrix.org/x-atepmcggudcmcggg) |
| 2021-03-24 17:07:56 | → | plumenator[m] joins (plumenator@gateway/shell/matrix.org/x-qptmeamoejhofhvo) |
| 2021-03-24 17:08:03 | → | arcontethegreat[ joins (arcontethe@gateway/shell/matrix.org/x-yotrsdwouhpxhcjs) |
| 2021-03-24 17:10:19 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 256 seconds) |
| 2021-03-24 17:10:33 | → | bitmagie joins (~Thunderbi@200116b8066df900d5323f70f4278fa3.dip.versatel-1u1.de) |
| 2021-03-24 17:11:08 | × | acidjnk_new quits (~acidjnk@p200300d0c72b958398d78e73e557de79.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
All times are in UTC.