| 2024-10-08 00:00:11 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 00:02:58 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-08 00:04:00 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-10-08 00:09:12 +0200 | andrewboltachev | (~andrey@178.141.123.3) (Quit: Leaving.) |
| 2024-10-08 00:12:22 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 00:24:21 +0200 | mantraofpie | (~mantraofp@user/mantraofpie) (Ping timeout: 260 seconds) |
| 2024-10-08 00:36:43 +0200 | xff0x | (~xff0x@2405:6580:b080:900:31d8:fed5:6c70:b7b9) (Ping timeout: 264 seconds) |
| 2024-10-08 00:41:44 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-10-08 00:42:05 +0200 | tuxpaint | (~a@put.gay) (Quit: gn) |
| 2024-10-08 00:42:24 +0200 | tuxpaint | (~a@put.gay) |
| 2024-10-08 00:49:33 +0200 | xff0x | (~xff0x@2405:6580:b080:900:8633:3fd0:abbc:825) |
| 2024-10-08 00:51:47 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
| 2024-10-08 01:03:49 +0200 | thegeekinside | (~thegeekin@189.217.93.202) thegeekinside |
| 2024-10-08 01:08:13 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb09b827840f1f57a57d.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-10-08 01:15:00 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 265 seconds) |
| 2024-10-08 01:16:39 +0200 | troojg | (~troojg@user/troojg) troojg |
| 2024-10-08 01:18:29 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Quit: quit) |
| 2024-10-08 01:20:39 +0200 | motherfsck | (~motherfsc@user/motherfsck) motherfsck |
| 2024-10-08 01:23:53 +0200 | thegeekinside | (~thegeekin@189.217.93.202) (Remote host closed the connection) |
| 2024-10-08 01:27:24 +0200 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Ping timeout: 260 seconds) |
| 2024-10-08 01:29:30 +0200 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan |
| 2024-10-08 01:32:17 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-10-08 01:36:45 +0200 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2024-10-08 01:38:01 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-10-08 01:45:43 +0200 | Digit | (~user@user/digit) (Read error: Connection reset by peer) |
| 2024-10-08 01:47:26 +0200 | Digit | (~user@user/digit) Digit |
| 2024-10-08 01:59:34 +0200 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-10-08 02:05:08 +0200 | gentauro | (~gentauro@user/gentauro) gentauro |
| 2024-10-08 02:26:42 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2024-10-08 02:27:02 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 02:34:07 +0200 | TonyStone | (~TonyStone@user/TonyStone) TonyStone |
| 2024-10-08 02:35:20 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-08 02:37:41 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:e06c:ffe4:c8a0:d22b) (Ping timeout: 248 seconds) |
| 2024-10-08 02:39:25 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-08 02:39:57 +0200 | morb | (~morb@108.41.100.120) |
| 2024-10-08 02:44:39 +0200 | hgolden__ | (~hgolden@23.162.40.28) hgolden |
| 2024-10-08 02:47:20 +0200 | hgolden_ | (~hgolden@146.70.173.37) (Ping timeout: 272 seconds) |
| 2024-10-08 02:48:04 +0200 | xff0x | (~xff0x@2405:6580:b080:900:8633:3fd0:abbc:825) (Ping timeout: 260 seconds) |
| 2024-10-08 02:52:05 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 248 seconds) |
| 2024-10-08 02:54:24 +0200 | morb | (~morb@108.41.100.120) (Remote host closed the connection) |
| 2024-10-08 03:12:56 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-10-08 03:23:30 +0200 | krei-se | (~krei-se@p57af2362.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-10-08 03:24:12 +0200 | krei-se | (~krei-se@p5085d9ca.dip0.t-ipconnect.de) krei-se |
| 2024-10-08 03:24:13 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-08 03:24:22 +0200 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 2024-10-08 03:25:26 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-08 03:28:54 +0200 | <haskellbridge> | <thirdofmay18081814goya> what are some useful coinductive types? |
| 2024-10-08 03:29:09 +0200 | troojg | (~troojg@user/troojg) troojg |
| 2024-10-08 03:29:17 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-08 03:29:43 +0200 | <monochrom> | Infinite lists. Infinite free monads. |
| 2024-10-08 03:30:14 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm right i see ty |
| 2024-10-08 03:31:06 +0200 | <talismanick> | infinite (nonempty) lists are often referred to in literature as streams |
| 2024-10-08 03:31:13 +0200 | <talismanick> | you can even do calculus on them: https://www.cs.ox.ac.uk/people/ralf.hinze/publications/CSC.pdf |
| 2024-10-08 03:32:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> are these the streams you usually encounter in programming? |
| 2024-10-08 03:33:35 +0200 | <geekosaur> | I think mathematical streams are used to model those streams, since their size is from the standpoint of programs "infinite" or at least indeterminate? |
| 2024-10-08 03:34:17 +0200 | <EvanR> | object oriented programming via copatterns |
| 2024-10-08 03:34:18 +0200 | <geekosaur> | for example, a network stream could hypothetically last forever, although in practice something will cause the remote to close the connection or be lost or etc. |
| 2024-10-08 03:34:33 +0200 | <monochrom> | I didn't think of the elegant "join s = head (head s) : join (tail (tail s))". (I only knew to wrote it as [s !! i !! i | i <- [0..]]) |
| 2024-10-08 03:35:05 +0200 | <talismanick> | there are types which are isomorphic to streams (can be exchanged one-for-one); these are given a `Comonad` instance, which lets them use any operation defined on comonads (generalized from the case specialized to the stream type given in the paper) |
| 2024-10-08 03:35:14 +0200 | <EvanR> | chalk up remote host closed connection to "thread died" xD |
| 2024-10-08 03:35:26 +0200 | <EvanR> | thread's code itself has no idea |
| 2024-10-08 03:35:44 +0200 | <EvanR> | it never observed the end of the stream so it's still infinite xD |
| 2024-10-08 03:35:57 +0200 | <talismanick> | https://hackage.haskell.org/package/comonad-5.0.8/ shows 164 reverse dependencies and 8416 indirect |
| 2024-10-08 03:36:15 +0200 | <talismanick> | so there are few cases :D |
| 2024-10-08 03:36:31 +0200 | <haskellbridge> | <thirdofmay18081814goya> i see thanks for comments! |
| 2024-10-08 03:37:12 +0200 | <geekosaur> | fwiw what I am aiming for is "the size isn't defined statically by your program, but by something synamic / outside of it" |
| 2024-10-08 03:37:45 +0200 | <geekosaur> | *dynamic |
| 2024-10-08 03:38:58 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-08 03:39:07 +0200 | <EvanR> | the basic haskell list type really is a conundrum for ultrafinitists right |
| 2024-10-08 03:39:09 +0200 | <monochrom> | It is the same as "unbounded" Integer where there is a bound but it's outside of your model. |
| 2024-10-08 03:39:23 +0200 | <EvanR> | if all haskell lists are "really" finite, then what is the answer to length (repeat ()) |
| 2024-10-08 03:39:54 +0200 | <EvanR> | or is the length function broken |
| 2024-10-08 03:40:11 +0200 | <geekosaur> | ⊥ because `length` breaks when it hits `maxBound :: Int` |
| 2024-10-08 03:40:28 +0200 | <EvanR> | >_< |
| 2024-10-08 03:41:35 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-08 03:41:58 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm can we not do induction on coinductive structures or does coinduction capture something completely different? |
| 2024-10-08 03:42:12 +0200 | <haskellbridge> | <thirdofmay18081814goya> (is coinduction the type eliminator for coinductive types?) |
| 2024-10-08 03:43:42 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-10-08 03:45:53 +0200 | geekosaur | is wondering if it would be a type introducer |
| 2024-10-08 03:46:34 +0200 | <geekosaur> | (or "co-eliminator", whatever that works out to be) |
| 2024-10-08 03:48:24 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-08 03:51:04 +0200 | <EvanR> | the only reason you can do induction on an inductive type is because it comes with an induction rule |
| 2024-10-08 03:51:59 +0200 | <EvanR> | unless you can figure out how to synthesize one as a theorem |
| 2024-10-08 03:52:09 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah the induction rule associated to a particular inductive type is the elimination rule for that type |
| 2024-10-08 03:54:08 +0200 | <monochrom> | induction rule is part of what "inductive type" means. What does "coinductive type" mean? Perhaps it contains the coinduction rule. |
| 2024-10-08 03:54:31 +0200 | <EvanR> | you can probably come up with a coinductive type which it is possible to derive a synthetic induction rule |
| 2024-10-08 03:54:35 +0200 | <EvanR> | for |
| 2024-10-08 03:54:56 +0200 | <EvanR> | like one that doesn't lead to infinite data |
| 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:57:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 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:58:04 +0200 | <EvanR> | no |
| 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:59:47 +0200 | <EvanR> | specifically define the potentially infinite natural numbers using the coinductive style |
| 2024-10-08 03:59:59 +0200 | <EvanR> | not set theory |
| 2024-10-08 03:59:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> oh |
| 2024-10-08 04:00:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> ok i see |
| 2024-10-08 04:00:28 +0200 | <EvanR> | though I'm not sure set theory would fix it |
| 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:01:26 +0200 | <EvanR> | ordinals? xD |
| 2024-10-08 04:01:40 +0200 | <EvanR> | that comes with its own induction rule |
| 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:02:39 +0200 | <monochrom> | We also say "make a Xerox copy" and then go on to use a Konica photocopier. |
| 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:03:01 +0200 | <monochrom> | so I guess "infinite natural" and even "uncountable natural" can be legit names. |
| 2024-10-08 04:03:31 +0200 | <EvanR> | it misses something |
| 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:05:34 +0200 | <EvanR> | it's illogical! |
| 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:07:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm looks like coalgebras sort disassemble things |
| 2024-10-08 04:07:09 +0200 | <haskellbridge> | <thirdofmay18081814goya> sort of disassemble things |
| 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:08:41 +0200 | <monochrom> | On recent exams I became careful to write "Prove by induction: For all finite lists xs, ..." :) |
| 2024-10-08 04:12:37 +0200 | <EvanR> | is final coalgebra the categorical wonkery for coinductive types? |
| 2024-10-08 04:12:40 +0200 | <monochrom> | Hagino says "co-natural number" instead of "infinite natural number". :) |
| 2024-10-08 04:12:54 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: yes |
| 2024-10-08 04:13:33 +0200 | td_ | (~td@i5387091A.versanet.de) (Ping timeout: 246 seconds) |
| 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:14:45 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: was planning to return to his thesis after foray into coinduction |
| 2024-10-08 04:14:56 +0200 | <EvanR> | disassemble might give you the wrong idea |
| 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: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: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:36 +0200 | <monochrom> | I don't, I didn't really read it. |
| 2024-10-08 04:15:39 +0200 | td_ | (~td@i5387092D.versanet.de) td_ |
| 2024-10-08 04:16:02 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 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:17:41 +0200 | <EvanR> | and in the case of infinite data, assembling from the ground up is impossible |
| 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:19:25 +0200 | <dolio> | To build codata, you say what happens for all the ways of observing it, corecursively. |
| 2024-10-08 04:21:28 +0200 | <dolio> | Like unfoldr, but that only has one thing to observe. |
| 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:27:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> ty for comments helpful stuff |
| 2024-10-08 04:29:21 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 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:36:59 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2024-10-08 04:39:49 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 248 seconds) |
| 2024-10-08 04:52:19 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 260 seconds) |
| 2024-10-08 04:52:51 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-10-08 04:59:04 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2024-10-08 05:01:04 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-10-08 05:09:12 +0200 | zlqrvx_ | (~zlqrvx@101.175.150.247) (Ping timeout: 272 seconds) |
| 2024-10-08 05:22:21 +0200 | motherfsck | (~motherfsc@user/motherfsck) motherfsck |
| 2024-10-08 05:27:37 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-08 05:27:37 +0200 | ethantwardy | (user@user/ethantwardy) (Read error: Connection reset by peer) |
| 2024-10-08 05:29:52 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-08 05:31:20 +0200 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 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:43:57 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-10-08 05:44:40 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 272 seconds) |
| 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:49:41 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 06:04:53 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2024-10-08 06:07:51 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 2024-10-08 06:08:05 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
| 2024-10-08 06:15:45 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 06:19:30 +0200 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 265 seconds) |
| 2024-10-08 06:24:28 +0200 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) {-d0t-} |
| 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:39:57 +0200 | simendsjo | (~user@84.211.91.108) (Ping timeout: 276 seconds) |
| 2024-10-08 06:45:50 +0200 | <jackdk> | Axman6: Is this about how finger trees use polymorphic recursion? |
| 2024-10-08 06:45:56 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-08 06:55:47 +0200 | <mauke> | Axman6: non-regular? nested type? |
| 2024-10-08 06:57:53 +0200 | michalz | (~michalz@185.246.207.222) |
| 2024-10-08 07:03:41 +0200 | astra | amish |
| 2024-10-08 07:03:44 +0200 | amish | (sid289983@id-289983.hampstead.irccloud.com) (Changing host) |
| 2024-10-08 07:03:44 +0200 | amish | (sid289983@user/amish) amish |
| 2024-10-08 07:04:04 +0200 | amish | astra |
| 2024-10-08 07:08:47 +0200 | st_aldini1 | (~Thunderbi@136.48.22.91) st_aldini |
| 2024-10-08 07:09:05 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-08 07:10:13 +0200 | st_aldini | (~Thunderbi@136.48.22.91) (Ping timeout: 248 seconds) |
| 2024-10-08 07:10:13 +0200 | st_aldini1 | st_aldini |
| 2024-10-08 07:12:38 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-10-08 07:21:51 +0200 | dtman34 | (~dtman34@2601:447:d080:1a3c:e9e9:5bc8:51:a5ea) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 2024-10-08 07:22:12 +0200 | dtman34 | (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) dtman34 |
| 2024-10-08 07:23:01 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 248 seconds) |
| 2024-10-08 07:32:01 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-10-08 07:38:13 +0200 | <Axman6> | yeah I think both of those work |
| 2024-10-08 07:53:12 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb34519e9ca14c5ce943.dip0.t-ipconnect.de) acidjnk |
| 2024-10-08 07:57:33 +0200 | ubert | (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) ubert |
| 2024-10-08 08:04:00 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2024-10-08 08:08:25 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-10-08 08:08:38 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 08:09:11 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2024-10-08 08:09:33 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 08:10:24 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 08:10:57 +0200 | mari-estel | (~mari-este@185.238.219.10) |
| 2024-10-08 08:11:38 +0200 | mari77696 | (~mari-este@185.238.219.10) |
| 2024-10-08 08:14:05 +0200 | foul_owl | (~kerry@185.219.141.162) (Ping timeout: 255 seconds) |
| 2024-10-08 08:17:16 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2024-10-08 08:32:05 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-10-08 08:32:17 +0200 | mari77696 | (~mari-este@185.238.219.10) (Ping timeout: 248 seconds) |
| 2024-10-08 08:32:49 +0200 | mari-estel | (~mari-este@185.238.219.10) (Ping timeout: 248 seconds) |
| 2024-10-08 08:42:16 +0200 | rosco | (~rosco@175.136.22.30) rosco |
| 2024-10-08 08:44:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-08 08:57:37 +0200 | foul_owl | (~kerry@185.219.141.162) foul_owl |
| 2024-10-08 09:00:00 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-10-08 09:00:37 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2024-10-08 09:01:40 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-10-08 09:05:21 +0200 | <yin> | Axman6: regular |
| 2024-10-08 09:13:21 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2024-10-08 09:13:36 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-08 09:13:53 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-08 09:14:09 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-08 09:16:47 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-10-08 09:24:55 +0200 | zlqrvx | (~zlqrvx@user/zlqrvx) zlqrvx |
| 2024-10-08 09:24:57 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:9869:a17b:401:f55) |
| 2024-10-08 09:29:19 +0200 | <Athas> | Some time ago I asked for recommendations on how to teach Erlang-style message-based concurrency in Haskell. Following the suggestions in this channel, I ended up with Control.Concurrent.Chan and wrote these notes: https://diku-dk.github.io/ap-notes/chapter_6.html |
| 2024-10-08 09:32:13 +0200 | mari68681 | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 2024-10-08 09:32:13 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 2024-10-08 09:32:41 +0200 | briandaed | (~root@185.234.210.211.r.toneticgroup.pl) |
| 2024-10-08 09:37:30 +0200 | <tomsmeding> | yay normal channels :) |
| 2024-10-08 09:38:28 +0200 | rosco | (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 2024-10-08 09:40:07 +0200 | <tomsmeding> | Athas: this is nitpicking level, but why is 'send' written out and 'receive' eta-reduced here https://diku-dk.github.io/ap-notes/chapter_6.html#channels |
| 2024-10-08 09:40:36 +0200 | <Athas> | tomsmeding: meaningless inconsistency. I suppose I can never decided whether eta-reduction would confuse my students. |
| 2024-10-08 09:40:42 +0200 | <Athas> | Today I feel like it won't, so I will fix it. |
| 2024-10-08 09:41:11 +0200 | <tomsmeding> | I can relate to that sentiment, even s/my students/myself/ |
| 2024-10-08 09:42:46 +0200 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 244 seconds) |
| 2024-10-08 09:43:03 +0200 | <tomsmeding> | only tangentially related: I often find myself writing code like this: https://github.com/tomsmeding/ad-dualrev-th/blob/17b758dbb3966de66394a756b708dae6ab57687e/src/Lang… (older example because this is the first I found in public code) |
| 2024-10-08 09:43:34 +0200 | <tomsmeding> | that is: the function takes arguments, but I write the function as an explicit lambda expression (instead of binding the arguments normally) in order to _not_ make those arguments available in the functions defined in the 'where' block |
| 2024-10-08 09:43:45 +0200 | <tomsmeding> | because I want to reuse those same names in the 'where' block |
| 2024-10-08 09:44:09 +0200 | <tomsmeding> | it feels awkward to write code this way; are there better ways? |
| 2024-10-08 09:45:09 +0200 | mari68681 | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 252 seconds) |
| 2024-10-08 09:45:09 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 252 seconds) |
| 2024-10-08 09:45:21 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 2024-10-08 09:45:56 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-10-08 09:47:02 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale |
| 2024-10-08 09:53:29 +0200 | chele | (~chele@user/chele) chele |
| 2024-10-08 09:58:08 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) sourcetarius |
| 2024-10-08 09:58:36 +0200 | <briandaed> | maybe making go function top-level (with more verbose name) and just not exporting it from module |
| 2024-10-08 09:58:57 +0200 | <tomsmeding> | that is indeed an option |
| 2024-10-08 09:59:01 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-10-08 09:59:29 +0200 | <briandaed> | ddrType just process result from 'meat' produced by 'go' |
| 2024-10-08 09:59:57 +0200 | <briandaed> | but it's a matter of taste only |
| 2024-10-08 10:00:16 +0200 | <tomsmeding> | but I feel like that would unnecessarily increase the scope of that 'go' function; it is really only intended to be used through the API of ddrType, so it feels like a bit of a violation of modularity to lift it to the top level in a large module like this |
| 2024-10-08 10:00:25 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 10:00:36 +0200 | <Lears> | tomsmeding: `ddrType (go &&& show -> (ebr, showty)) = case ebr of ...` >:) |
| 2024-10-08 10:00:54 +0200 | <tomsmeding> | Lears: I mean, sure, you can always make code more pointless :p |
| 2024-10-08 10:01:37 +0200 | <tomsmeding> | I don't think that's any less awkward ;) |
| 2024-10-08 10:02:05 +0200 | <Lears> | The lambda is fine, really; I do the same thing. |
| 2024-10-08 10:02:36 +0200 | <Lears> | Or give the top-level (usually single-use) variable a 0 suffix. |
| 2024-10-08 10:02:39 +0200 | <tomsmeding> | in the past I just gave the argument names of the top-level functions longer names (e.g. "topTy"), but I settled on this lambda style as least-bad |
| 2024-10-08 10:02:44 +0200 | <tomsmeding> | right |
| 2024-10-08 10:02:53 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2024-10-08 10:03:43 +0200 | raym_ | raym |
| 2024-10-08 10:07:25 +0200 | <tomsmeding> | Athas: out of sequence in the conversation, but I just wanted to thank you for making these notes public. Increase collective wisdom by sharing materials. Our university wants us to close everything off in an LMS, because 1. they want to have IT stop spending time maintaining the open cource website server and 2. apparently some teachers aren't diligent and put privacy-sensitive information out in |
| 2024-10-08 10:07:27 +0200 | <tomsmeding> | the open, and they want to prevent that by construction (instead of instructing those teachers to do a better job) |
| 2024-10-08 10:08:15 +0200 | <tomsmeding> | I have just realised that our uni does actually have a github organisation too, so a github pages website in there is actually not too bad an idea |
| 2024-10-08 10:10:46 +0200 | kuribas | (~user@2a02:1808:7:f56b:d4a9:b96f:9d61:d1a7) kuribas |
| 2024-10-08 10:12:08 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-08 10:20:53 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale |
| 2024-10-08 10:22:46 +0200 | CiaoSen | (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-08 10:24:12 +0200 | raym | (~ray@user/raym) (Ping timeout: 252 seconds) |
| 2024-10-08 10:25:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-08 10:30:26 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-08 10:33:15 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) Maeda |
| 2024-10-08 10:33:29 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Client Quit) |
| 2024-10-08 10:33:38 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-10-08 10:37:13 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-08 10:40:24 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Remote host closed the connection) |
| 2024-10-08 10:40:59 +0200 | raym | (~ray@user/raym) raym |
| 2024-10-08 10:41:07 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale |
| 2024-10-08 10:42:54 +0200 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |
| 2024-10-08 10:44:33 +0200 | kuribas | (~user@2a02:1808:7:f56b:d4a9:b96f:9d61:d1a7) (Ping timeout: 248 seconds) |
| 2024-10-08 10:52:35 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-10-08 10:54:10 +0200 | synchromesh | (~john@2406:5a00:241a:5600:1537:bb1c:ebe9:2fdf) (Read error: Connection reset by peer) |
| 2024-10-08 10:54:33 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 10:55:10 +0200 | synchromesh | (~john@2406:5a00:241a:5600:dc23:4239:fb04:33f4) synchromesh |
| 2024-10-08 10:55:18 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-10-08 11:01:04 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-08 11:03:34 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-08 11:04:04 +0200 | gorignak | (~gorignak@user/gorignak) (Ping timeout: 252 seconds) |
| 2024-10-08 11:04:30 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-08 11:10:26 +0200 | fmira | (~user@user/fmira) (Quit: fmira) |
| 2024-10-08 11:17:25 +0200 | rosco | (~rosco@175.136.22.30) rosco |
| 2024-10-08 11:17:59 +0200 | supercode | (~supercode@user/supercode) supercode |
| 2024-10-08 11:22:26 +0200 | arahael | (~arahael@user/arahael) (Remote host closed the connection) |
| 2024-10-08 11:22:29 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2024-10-08 11:27:40 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-10-08 11:30:47 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-10-08 11:31:00 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 11:32:17 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-08 11:36:42 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-08 11:36:55 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-08 11:37:37 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-10-08 11:42:04 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-10-08 11:44:31 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 11:48:47 +0200 | Guest41 | (~Guest41@ip-38-9-3-83.internet.url.net.au) |
| 2024-10-08 11:49:13 +0200 | Guest41 | (~Guest41@ip-38-9-3-83.internet.url.net.au) (Client Quit) |
| 2024-10-08 11:52:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-08 11:55:01 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:9869:a17b:401:f55) (Ping timeout: 252 seconds) |
| 2024-10-08 12:08:58 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2024-10-08 12:15:29 +0200 | andrewboltachev | (~andrey@178.141.244.27) andrewboltachev |
| 2024-10-08 12:18:34 +0200 | aforemny | (~aforemny@2001:9e8:6cd9:9400:c5f2:6987:2beb:3640) aforemny |
| 2024-10-08 12:19:09 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-10-08 12:19:22 +0200 | euleritian | (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) |
| 2024-10-08 12:21:07 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2024-10-08 12:28:44 +0200 | CiaoSen | (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 2024-10-08 12:31:21 +0200 | supercode | (~supercode@user/supercode) (Killed (NickServ (GHOST command used by supercode63))) |
| 2024-10-08 12:31:23 +0200 | euleritian | (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-08 12:31:40 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 12:35:26 +0200 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 12:38:26 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-10-08 12:39:21 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:446d:e3f8:e9a4:2f3b) |
| 2024-10-08 12:40:59 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 2024-10-08 12:42:42 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-10-08 12:42:58 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 12:47:44 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 2024-10-08 12:48:49 +0200 | euleritian | (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) |
| 2024-10-08 12:51:31 +0200 | euleritian | (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-08 12:51:48 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 12:58:31 +0200 | rosco | (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 2024-10-08 13:00:05 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-10-08 13:02:34 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2024-10-08 13:05:28 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-10-08 13:10:26 +0200 | xff0x | (~xff0x@2405:6580:b080:900:da07:5be8:5f56:f410) |
| 2024-10-08 13:12:14 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2024-10-08 13:14:58 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 272 seconds) |
| 2024-10-08 13:17:56 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 2024-10-08 13:19:46 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 13:21:39 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Client Quit) |
| 2024-10-08 13:25:17 +0200 | srazkvt | (~sarah@user/srazkvt) srazkvt |
| 2024-10-08 13:33:37 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 2024-10-08 13:39:01 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 13:40:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-08 13:50:23 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2024-10-08 13:52:48 +0200 | rosco | (~rosco@175.136.22.30) rosco |
| 2024-10-08 13:53:15 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 13:55:26 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-10-08 13:55:55 +0200 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-10-08 14:01:58 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-08 14:04:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a mental picture to use when structuring a program through algebraic effects and handlers? |
| 2024-10-08 14:06:41 +0200 | <probie> | <bad joke>A burrito</bad joke> |
| 2024-10-08 14:07:40 +0200 | <Rembane> | I'm usually thinking about it as building a very small EDSL |
| 2024-10-08 14:08:41 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 255 seconds) |
| 2024-10-08 14:08:41 +0200 | <haskellbridge> | <thirdofmay18081814goya> Rembane: hm I see, each effect/handler pair a fragment? |
| 2024-10-08 14:09:36 +0200 | <Rembane> | Are you using a particular library? Something to make this more concrete. |
| 2024-10-08 14:13:54 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-08 14:13:58 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm no particular library atm, maybe it would make more sense to use one |
| 2024-10-08 14:15:08 +0200 | <Rembane> | Or create a datatype for effects and then create an interpreter for it |
| 2024-10-08 14:15:43 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 264 seconds) |
| 2024-10-08 14:22:41 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-08 14:30:03 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds) |
| 2024-10-08 14:30:23 +0200 | ash3en | (~Thunderbi@193.32.248.167) ash3en |
| 2024-10-08 14:34:17 +0200 | CiaoSen | (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-08 14:38:11 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-10-08 14:40:17 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-08 14:41:08 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 14:41:34 +0200 | identity | (~identity@user/ZharMeny) identity |
| 2024-10-08 14:45:52 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-08 14:51:33 +0200 | AlexZenon | (~alzenon@178.34.151.120) (Quit: ;-) |
| 2024-10-08 14:52:01 +0200 | AlexNoo | (~AlexNoo@178.34.151.120) (Quit: Leaving) |
| 2024-10-08 14:52:13 +0200 | Pixi` | (~Pixi@user/pixi) Pixi |
| 2024-10-08 14:55:13 +0200 | Pixi | (~Pixi@user/pixi) (Ping timeout: 248 seconds) |
| 2024-10-08 15:01:35 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-08 15:02:45 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-08 15:04:13 +0200 | ash3en | (~Thunderbi@193.32.248.167) (Quit: ash3en) |
| 2024-10-08 15:04:47 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-08 15:07:42 +0200 | Angelz | (Angelz@user/angelz) (Ping timeout: 272 seconds) |
| 2024-10-08 15:08:18 +0200 | zfnmxt | (~zfnmxt@107.189.30.63) (Ping timeout: 245 seconds) |
| 2024-10-08 15:12:19 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 2024-10-08 15:21:38 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3202-2f93-5c9a-6ec5-11de-f4fb.rev.sfr.net) alexherbo2 |
| 2024-10-08 15:27:34 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 2024-10-08 15:28:22 +0200 | AlexNoo | (~AlexNoo@178.34.151.120) |
| 2024-10-08 15:30:33 +0200 | AlexZenon | (~alzenon@178.34.151.120) |
| 2024-10-08 15:31:06 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-08 15:54:17 +0200 | ash3en | (~Thunderbi@193.32.248.167) ash3en |
| 2024-10-08 16:00:49 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:446d:e3f8:e9a4:2f3b) (Ping timeout: 260 seconds) |
| 2024-10-08 16:01:29 +0200 | mari-estel | (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 244 seconds) |
| 2024-10-08 16:02:14 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-08 16:02:34 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 16:04:09 +0200 | ash3en | (~Thunderbi@193.32.248.167) (Ping timeout: 276 seconds) |
| 2024-10-08 16:06:31 +0200 | ash3en | (~Thunderbi@193.32.248.167) ash3en |
| 2024-10-08 16:09:53 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-10-08 16:09:59 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-10-08 16:10:07 +0200 | euleritian | (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) |
| 2024-10-08 16:10:30 +0200 | euleritian | (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-08 16:10:47 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 16:11:31 +0200 | ash3en | (~Thunderbi@193.32.248.167) (Ping timeout: 264 seconds) |
| 2024-10-08 16:13:15 +0200 | synchromesh | (~john@2406:5a00:241a:5600:dc23:4239:fb04:33f4) (Ping timeout: 276 seconds) |
| 2024-10-08 16:14:22 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-08 16:14:49 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 16:15:56 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-08 16:16:27 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-08 16:19:35 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-08 16:23:24 +0200 | biberao | (~m@user/biberao) biberao |
| 2024-10-08 16:23:26 +0200 | <biberao> | hi |
| 2024-10-08 16:27:45 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-08 16:35:46 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 2024-10-08 16:35:53 +0200 | ash3en | (~Thunderbi@193.32.248.167) ash3en |
| 2024-10-08 16:36:10 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2024-10-08 16:43:35 +0200 | synchromesh | (~john@180.148.124.74) synchromesh |
| 2024-10-08 16:46:31 +0200 | ash3en | (~Thunderbi@193.32.248.167) (Ping timeout: 252 seconds) |
| 2024-10-08 16:49:02 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 16:53:46 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-08 16:55:41 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-08 17:00:09 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2024-10-08 17:04:46 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:1e84:aaa4:b350:85e4) |
| 2024-10-08 17:07:35 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-08 17:08:05 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 17:08:19 +0200 | CiaoSen | (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 2024-10-08 17:10:51 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 2024-10-08 17:11:11 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-08 17:16:33 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-08 17:16:58 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 17:18:27 +0200 | jinsun | (~jinsun@user/jinsun) jinsun |
| 2024-10-08 17:20:36 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 2024-10-08 17:21:11 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 17:25:26 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3202-2f93-5c9a-6ec5-11de-f4fb.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-08 17:31:44 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-08 17:31:51 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-08 17:32:00 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2024-10-08 17:32:15 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 17:35:31 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 2024-10-08 17:38:00 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-08 17:44:17 +0200 | rosco | (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 2024-10-08 17:45:35 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-08 17:48:05 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:1e84:aaa4:b350:85e4) (Ping timeout: 248 seconds) |
| 2024-10-08 17:50:16 +0200 | califax | (~califax@user/califx) (Ping timeout: 260 seconds) |
| 2024-10-08 17:50:26 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 2024-10-08 17:50:54 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 17:51:36 +0200 | califax | (~califax@user/califx) califx |
| 2024-10-08 17:52:29 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-08 17:53:12 +0200 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-10-08 17:53:41 +0200 | Digit | (~user@user/digit) (Ping timeout: 255 seconds) |
| 2024-10-08 17:55:32 +0200 | <monochrom> | I think it is the other way round. People already have a mental picture of effects and handlers. (They already understand exception handlers and Python's yield. If you can unify the two, you pretty much have it.) Then algebraic effects is designed to formalize that. |
| 2024-10-08 17:57:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm i see |
| 2024-10-08 17:57:44 +0200 | spew | (~spew@201.141.99.170) spew |
| 2024-10-08 17:57:53 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-10-08 17:58:11 +0200 | califax | (~califax@user/califx) califx |
| 2024-10-08 18:00:30 +0200 | berberman | (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-10-08 18:00:57 +0200 | berberman | (~berberman@user/berberman) berberman |
| 2024-10-08 18:04:19 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2024-10-08 18:04:56 +0200 | euleritian | (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) |
| 2024-10-08 18:08:21 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-08 18:09:09 +0200 | berberman | (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-10-08 18:10:11 +0200 | berberman | (~berberman@user/berberman) berberman |
| 2024-10-08 18:12:41 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 2024-10-08 18:13:02 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-08 18:13:09 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-10-08 18:13:23 +0200 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2024-10-08 18:13:26 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-08 18:17:22 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-10-08 18:18:33 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-08 18:18:41 +0200 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-10-08 18:19:03 +0200 | Digitteknohippie | Digit |
| 2024-10-08 18:25:00 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-08 18:30:18 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2024-10-08 18:31:44 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2024-10-08 18:34:22 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2024-10-08 18:34:28 +0200 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2024-10-08 18:35:11 +0200 | pavonia | (~user@user/siracusa) siracusa |
| 2024-10-08 18:35:29 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 2024-10-08 18:35:30 +0200 | Pixi` | Pixi |
| 2024-10-08 18:37:00 +0200 | euleritian | (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-08 18:37:17 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 18:40:22 +0200 | rvalue- | rvalue |
| 2024-10-08 18:42:04 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:cf3a:e88a:f2c8:6274) |
| 2024-10-08 18:42:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> i just need a free monad to model algebraic effect rights? |
| 2024-10-08 18:44:39 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 2024-10-08 18:44:54 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-10-08 18:49:41 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-08 18:49:49 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-10-08 18:51:32 +0200 | EvanR | (~EvanR@user/evanr) (Quit: Leaving) |
| 2024-10-08 18:53:12 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-10-08 18:53:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2024-10-08 18:53:37 +0200 | euleritian | (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) |
| 2024-10-08 18:56:14 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 18:57:23 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Quit: Lost terminal) |
| 2024-10-08 19:07:30 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-10-08 19:08:00 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2024-10-08 19:09:10 +0200 | CiaoSen | (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-08 19:10:16 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 19:11:11 +0200 | euleritian | (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-08 19:11:29 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 19:12:11 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 19:17:14 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-08 19:23:06 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 2024-10-08 19:23:06 +0200 | andrewboltachev | (~andrey@178.141.244.27) (Quit: Leaving.) |
| 2024-10-08 19:23:59 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-10-08 19:24:49 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 260 seconds) |
| 2024-10-08 19:27:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm yeah only if the effect actually is algebraic |
| 2024-10-08 19:27:59 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 19:29:56 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 19:30:43 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2024-10-08 19:31:17 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2024-10-08 19:31:59 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 19:33:06 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-08 19:35:20 +0200 | ss4 | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2024-10-08 19:37:29 +0200 | causal | (~eric@50.35.88.207) causal |
| 2024-10-08 19:38:05 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-10-08 19:38:13 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-08 19:39:09 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 252 seconds) |
| 2024-10-08 19:43:26 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-08 19:43:46 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 19:48:37 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-08 19:48:45 +0200 | kaskal | (~kaskal@2001:4bb8:2af:db4a:8acd:a0ac:f117:1e24) (Quit: ZNC - https://znc.in) |
| 2024-10-08 19:49:07 +0200 | kaskal | (~kaskal@2001:4bb8:2af:db4a:8213:de4d:dd34:38f3) kaskal |
| 2024-10-08 19:52:57 +0200 | ss4 | (~wootehfoo@user/wootehfoot) (Ping timeout: 246 seconds) |
| 2024-10-08 19:55:37 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-10-08 19:55:40 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-08 19:56:11 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-08 19:59:27 +0200 | <haskellbridge> | <thirdofmay18081814goya> nvm i don't know what i'm talking about |
| 2024-10-08 19:59:33 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 20:01:07 +0200 | Batzy_ | (~quassel@user/batzy) Batzy |
| 2024-10-08 20:03:17 +0200 | Batzy | (~quassel@user/batzy) (Ping timeout: 255 seconds) |
| 2024-10-08 20:04:33 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-10-08 20:05:00 +0200 | ubert | (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 2024-10-08 20:08:13 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 2024-10-08 20:10:40 +0200 | mrtz | (~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) |
| 2024-10-08 20:11:14 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 20:11:47 +0200 | samanklesaria | (~samankles@68-168-167-245.fttp.usinternet.com) |
| 2024-10-08 20:14:16 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 20:16:13 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-10-08 20:17:17 +0200 | briandaed | (~root@185.234.210.211.r.toneticgroup.pl) (Remote host closed the connection) |
| 2024-10-08 20:17:45 +0200 | lol_ | (~lol@2603:3016:1e01:b9e0:835:2698:e6f:bd82) |
| 2024-10-08 20:19:19 +0200 | samanklesaria | (~samankles@68-168-167-245.fttp.usinternet.com) (Remote host closed the connection) |
| 2024-10-08 20:20:24 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-10-08 20:20:51 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds) |
| 2024-10-08 20:21:34 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b9e0:9c4e:1030:31bf:f76b) (Ping timeout: 260 seconds) |
| 2024-10-08 20:24:22 +0200 | mrtz | (~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2024-10-08 20:27:01 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 20:35:24 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-10-08 20:38:57 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 20:43:55 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2024-10-08 20:50:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 20:54:42 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 20:56:25 +0200 | Pixi | (~Pixi@user/pixi) (Quit: Leaving) |
| 2024-10-08 20:59:54 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-10-08 21:00:01 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-10-08 21:00:37 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2024-10-08 21:01:51 +0200 | CiaoSen | (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 2024-10-08 21:07:43 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-08 21:08:14 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-08 21:15:33 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 21:17:34 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2024-10-08 21:17:55 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-10-08 21:18:32 +0200 | <tomsmeding> | goya: You don't _need_ a free monad to model algebraic effects; free monads _can be used_ to model algebraic effects |
| 2024-10-08 21:18:49 +0200 | <tomsmeding> | and they are traditional vehicle in haskell, but not all effects libraries use them |
| 2024-10-08 21:19:18 +0200 | <tomsmeding> | if you are willing to give up some of the more exotic effects, ReaderT r IO can suffice just fine, with the right API |
| 2024-10-08 21:20:04 +0200 | <tomsmeding> | https://hackage.haskell.org/package/effectful-core-2.3.1.0/docs/src/Effectful.Internal.Monad.html#… |
| 2024-10-08 21:20:06 +0200 | <tomsmeding> | for example |
| 2024-10-08 21:20:06 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-10-08 21:20:40 +0200 | Pixi | (~Pixi@user/pixi) Pixi |
| 2024-10-08 21:21:42 +0200 | <tomsmeding> | this cannot model nondeterminism (search for "Any downsides" here https://hackage.haskell.org/package/effectful-core-2.3.1.0 ), but can implement many of the common "practical" effects |
| 2024-10-08 21:21:56 +0200 | <tomsmeding> | there's also 'eff' based on delimited continuations |
| 2024-10-08 21:24:50 +0200 | <dolio> | Most of the time what you see of algebraic effects showing up in actual languages, they are by definition giving rise to free monads. |
| 2024-10-08 21:25:03 +0200 | <dolio> | E.G. they cannot do state. |
| 2024-10-08 21:25:46 +0200 | tomsmeding | has difficulty parsing that |
| 2024-10-08 21:26:16 +0200 | <dolio> | They can do get/put |
| 2024-10-08 21:26:39 +0200 | <dolio> | And it's up to the handler whether that satisfies the expected equations for state or not. |
| 2024-10-08 21:26:59 +0200 | <tomsmeding> | I would not call that "giving rise to free monads" |
| 2024-10-08 21:27:06 +0200 | <tomsmeding> | sure, free monads are one way to implement that semantics |
| 2024-10-08 21:27:29 +0200 | <tomsmeding> | as in: you don't need to actually reify the computation as a data type |
| 2024-10-08 21:27:33 +0200 | <tomsmeding> | which is what "free monad" means to me |
| 2024-10-08 21:27:51 +0200 | <haskellbridge> | <thirdofmay18081814goya> aren't free monads their canonical abstract implementation-independent representation |
| 2024-10-08 21:27:59 +0200 | <tomsmeding> | perhaps |
| 2024-10-08 21:28:07 +0200 | <tomsmeding> | but "need" is too strong, I think |
| 2024-10-08 21:28:25 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm right |
| 2024-10-08 21:28:59 +0200 | <tomsmeding> | [] is surely the canonical free monoid. But that doesn't mean I _need_ [] in order to represent a free monoid; I can easily write my own data type that does the same thing |
| 2024-10-08 21:29:12 +0200 | <tomsmeding> | and there are actually other data types, such as Bag, that are better in certain circumstances |
| 2024-10-08 21:30:15 +0200 | <Franciman> | dolio: can you also define equations in those effect systems? |
| 2024-10-08 21:30:15 +0200 | <tomsmeding> | (data Bag a = Empty | Single a | Many (Bag a) (Bag a)) |
| 2024-10-08 21:30:29 +0200 | <dolio> | Franciman: No. That's why they're free. |
| 2024-10-08 21:30:46 +0200 | <Franciman> | can't you do the presentation of a struct? |
| 2024-10-08 21:31:00 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 21:31:39 +0200 | supercode | (~supercode@user/supercode) supercode |
| 2024-10-08 21:32:05 +0200 | <dolio> | I'm sure there are papers on how you'd include equations, but I've never seen it in some language with built-in algebraic effects. Maybe whatever they do in Idris would include them. |
| 2024-10-08 21:32:07 +0200 | <Franciman> | of a set of equation* |
| 2024-10-08 21:32:23 +0200 | <Franciman> | t looks interesting |
| 2024-10-08 21:33:18 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 2024-10-08 21:33:39 +0200 | mantraofpie | (~mantraofp@user/mantraofpie) mantraofpie |
| 2024-10-08 21:34:08 +0200 | <dolio> | Anyhow, 'free' doesn't mean data type. That's something from the category end that hasn't really trickled into Haskell so much. |
| 2024-10-08 21:34:38 +0200 | <tomsmeding> | I see |
| 2024-10-08 21:34:38 +0200 | <Franciman> | free is not about categories |
| 2024-10-08 21:34:44 +0200 | <Franciman> | it has a wider meaning |
| 2024-10-08 21:34:58 +0200 | <tomsmeding> | s/category end/category theory end/ |
| 2024-10-08 21:35:39 +0200 | <dolio> | Data types are free, but other things can also be free. What matters is if it satisfies a universal property, and many differen't implementation details can realize such a universal property. |
| 2024-10-08 21:35:52 +0200 | <tomsmeding> | right, that makes sense |
| 2024-10-08 21:35:58 +0200 | <tomsmeding> | (with my limited CT knowledge) |
| 2024-10-08 21:36:11 +0200 | <dolio> | And if all you say is 'free,' you don't necessarily specify or know what the implementation is. You could even look at data types that way. |
| 2024-10-08 21:36:15 +0200 | <tomsmeding> | okay in that case, "free monad" is indeed appropriate, I guess |
| 2024-10-08 21:36:34 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-08 21:38:12 +0200 | <haskellbridge> | <thirdofmay18081814goya> Franciman: warning free adjunct |
| 2024-10-08 21:38:19 +0200 | <dolio> | Maybe A × B and B × A (for distinct A and B) are actually implemented exactly the same way, but the compiler systematically picks different projection functions depending on which you're talking about. |
| 2024-10-08 21:39:11 +0200 | <haskellbridge> | <thirdofmay18081814goya> x is not about categories is in general inaccurate |
| 2024-10-08 21:39:16 +0200 | ubert | (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) ubert |
| 2024-10-08 21:40:12 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 21:40:58 +0200 | causal | (~eric@50.35.88.207) (Ping timeout: 252 seconds) |
| 2024-10-08 21:41:22 +0200 | causal | (~eric@50.35.88.207) causal |
| 2024-10-08 21:48:00 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) (Quit: Bye) |
| 2024-10-08 21:48:19 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 21:49:03 +0200 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2024-10-08 21:53:21 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-08 21:53:27 +0200 | zfnmxt | (~zfnmxt@user/zfnmxt) zfnmxt |
| 2024-10-08 21:55:29 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 2024-10-08 21:57:12 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-08 21:58:46 +0200 | codaraxis | (~codaraxis@user/codaraxis) Codaraxis |
| 2024-10-08 21:59:27 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) TimWolla |
| 2024-10-08 22:00:24 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-10-08 22:04:05 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 22:05:13 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3215-f56e-1190-0b59-796f-612e.rev.sfr.net) alexherbo2 |
| 2024-10-08 22:05:44 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-10-08 22:08:49 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-08 22:09:30 +0200 | <sam113101> | does haskell have something like the pipe operator (|>) in elixir? |
| 2024-10-08 22:10:04 +0200 | <tomsmeding> | :t (&) |
| 2024-10-08 22:10:05 +0200 | <lambdabot> | a -> (a -> b) -> b |
| 2024-10-08 22:10:10 +0200 | <tomsmeding> | :t ($) |
| 2024-10-08 22:10:10 +0200 | <lambdabot> | (a -> b) -> a -> b |
| 2024-10-08 22:10:27 +0200 | <tomsmeding> | > map toUpper "hello" |
| 2024-10-08 22:10:28 +0200 | <lambdabot> | "HELLO" |
| 2024-10-08 22:10:34 +0200 | <tomsmeding> | > hello & map toUpper |
| 2024-10-08 22:10:36 +0200 | <lambdabot> | error: Variable not in scope: hello :: [Char] |
| 2024-10-08 22:10:39 +0200 | <tomsmeding> | > "hello" & map toUpper |
| 2024-10-08 22:10:40 +0200 | <lambdabot> | "HELLO" |
| 2024-10-08 22:10:50 +0200 | <tomsmeding> | sam113101: is that what you're looking for? (&) is in Data.Function |
| 2024-10-08 22:11:10 +0200 | <sam113101> | I think yes |
| 2024-10-08 22:11:24 +0200 | <sam113101> | what's $ |
| 2024-10-08 22:11:33 +0200 | <tomsmeding> | normal function application :) |
| 2024-10-08 22:11:38 +0200 | <tomsmeding> | > map toUpper $ "hello" |
| 2024-10-08 22:11:39 +0200 | <lambdabot> | "HELLO" |
| 2024-10-08 22:11:50 +0200 | Angelz | (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) |
| 2024-10-08 22:12:04 +0200 | <tomsmeding> | (&) is seldomly used in haskell; the conventional code style is to put the function to apply on the _left_ side of the thing you're applying it to, not on the right |
| 2024-10-08 22:12:16 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-08 22:12:22 +0200 | <tomsmeding> | there are various ways to do that: |
| 2024-10-08 22:12:40 +0200 | <tomsmeding> | > map toUpper (reverse (show (Just 42))) |
| 2024-10-08 22:12:42 +0200 | <lambdabot> | "24 TSUJ" |
| 2024-10-08 22:12:49 +0200 | <tomsmeding> | > map toUpper $ reverse $ show $ Just 42 |
| 2024-10-08 22:12:50 +0200 | <lambdabot> | "24 TSUJ" |
| 2024-10-08 22:12:56 +0200 | <tomsmeding> | > map toUpper . reverse . show $ Just 42 |
| 2024-10-08 22:12:57 +0200 | <lambdabot> | "24 TSUJ" |
| 2024-10-08 22:13:09 +0200 | <tomsmeding> | the first version you should be able to read: that's just applying functions as usual |
| 2024-10-08 22:13:38 +0200 | <sam113101> | yeah |
| 2024-10-08 22:13:41 +0200 | <tomsmeding> | in the second version, I'm using ($) to save parentheses; this style is sometimes used, but is typically reserved if the function to apply is short and the argument is a long, typically multi-line expression |
| 2024-10-08 22:14:11 +0200 | <tomsmeding> | in the third version, I'm using (.) to _compose_ three functions, then applying the whole composition at once to the argument (Just 42) |
| 2024-10-08 22:14:16 +0200 | <tomsmeding> | :t (.) |
| 2024-10-08 22:14:17 +0200 | <lambdabot> | (b -> c) -> (a -> b) -> a -> c |
| 2024-10-08 22:15:24 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |