2024/10/08

2024-10-08 00:00:11 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 00:02:58 +0200tromp(~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 +0200andrewboltachev(~andrey@178.141.123.3) (Quit: Leaving.)
2024-10-08 00:12:22 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-08 00:24:21 +0200mantraofpie(~mantraofp@user/mantraofpie) (Ping timeout: 260 seconds)
2024-10-08 00:36:43 +0200xff0x(~xff0x@2405:6580:b080:900:31d8:fed5:6c70:b7b9) (Ping timeout: 264 seconds)
2024-10-08 00:41:44 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!)
2024-10-08 00:42:05 +0200tuxpaint(~a@put.gay) (Quit: gn)
2024-10-08 00:42:24 +0200tuxpaint(~a@put.gay)
2024-10-08 00:49:33 +0200xff0x(~xff0x@2405:6580:b080:900:8633:3fd0:abbc:825)
2024-10-08 00:51:47 +0200talismanick(~user@2601:644:937c:ed10::ae5) talismanick
2024-10-08 01:03:49 +0200thegeekinside(~thegeekin@189.217.93.202) thegeekinside
2024-10-08 01:08:13 +0200acidjnk(~acidjnk@p200300d6e72cfb09b827840f1f57a57d.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2024-10-08 01:15:00 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 265 seconds)
2024-10-08 01:16:39 +0200troojg(~troojg@user/troojg) troojg
2024-10-08 01:18:29 +0200motherfsck(~motherfsc@user/motherfsck) (Quit: quit)
2024-10-08 01:20:39 +0200motherfsck(~motherfsc@user/motherfsck) motherfsck
2024-10-08 01:23:53 +0200thegeekinside(~thegeekin@189.217.93.202) (Remote host closed the connection)
2024-10-08 01:27:24 +0200remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) (Ping timeout: 260 seconds)
2024-10-08 01:29:30 +0200remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan
2024-10-08 01:32:17 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-10-08 01:36:45 +0200supercode(~supercode@user/supercode) (Quit: Client closed)
2024-10-08 01:38:01 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-10-08 01:45:43 +0200Digit(~user@user/digit) (Read error: Connection reset by peer)
2024-10-08 01:47:26 +0200Digit(~user@user/digit) Digit
2024-10-08 01:59:34 +0200gentauro(~gentauro@user/gentauro) (Read error: Connection reset by peer)
2024-10-08 02:05:08 +0200gentauro(~gentauro@user/gentauro) gentauro
2024-10-08 02:26:42 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2024-10-08 02:27:02 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 02:34:07 +0200TonyStone(~TonyStone@user/TonyStone) TonyStone
2024-10-08 02:35:20 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-08 02:37:41 +0200alp_(~alp@2001:861:e3d6:8f80:e06c:ffe4:c8a0:d22b) (Ping timeout: 248 seconds)
2024-10-08 02:39:25 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection)
2024-10-08 02:39:57 +0200morb(~morb@108.41.100.120)
2024-10-08 02:44:39 +0200hgolden__(~hgolden@23.162.40.28) hgolden
2024-10-08 02:47:20 +0200hgolden_(~hgolden@146.70.173.37) (Ping timeout: 272 seconds)
2024-10-08 02:48:04 +0200xff0x(~xff0x@2405:6580:b080:900:8633:3fd0:abbc:825) (Ping timeout: 260 seconds)
2024-10-08 02:52:05 +0200troojg(~troojg@user/troojg) (Ping timeout: 248 seconds)
2024-10-08 02:54:24 +0200morb(~morb@108.41.100.120) (Remote host closed the connection)
2024-10-08 03:12:56 +0200spew(~spew@201.141.99.170) (Quit: spew)
2024-10-08 03:23:30 +0200krei-se(~krei-se@p57af2362.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
2024-10-08 03:24:12 +0200krei-se(~krei-se@p5085d9ca.dip0.t-ipconnect.de) krei-se
2024-10-08 03:24:13 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-08 03:24:22 +0200ethantwardy(user@user/ethantwardy) ethantwardy
2024-10-08 03:25:26 +0200morb(~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 +0200troojg(~troojg@user/troojg) troojg
2024-10-08 03:29:17 +0200morb(~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 +0200morb(~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 +0200youthlic(~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 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds)
2024-10-08 03:45:53 +0200geekosauris 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 +0200xff0x(~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 +0200raehik(~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 +0200td_(~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 +0200td_(~td@i5387092D.versanet.de) td_
2024-10-08 04:16:02 +0200athan(~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 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-08 04:31:07 +0200identity(~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.91))
2024-10-08 04:36:59 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
2024-10-08 04:39:49 +0200motherfsck(~motherfsc@user/motherfsck) (Ping timeout: 248 seconds)
2024-10-08 04:52:19 +0200troojg(~troojg@user/troojg) (Ping timeout: 260 seconds)
2024-10-08 04:52:51 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-10-08 04:59:04 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 272 seconds)
2024-10-08 05:01:04 +0200sourcetarius(~sourcetar@user/sourcetarius) (Quit: sourcetarius)
2024-10-08 05:09:12 +0200zlqrvx_(~zlqrvx@101.175.150.247) (Ping timeout: 272 seconds)
2024-10-08 05:22:21 +0200motherfsck(~motherfsc@user/motherfsck) motherfsck
2024-10-08 05:27:37 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-08 05:27:37 +0200ethantwardy(user@user/ethantwardy) (Read error: Connection reset by peer)
2024-10-08 05:29:52 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-08 05:31:20 +0200ethantwardy(user@user/ethantwardy) ethantwardy
2024-10-08 05:43:38 +0200floyza(~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection)
2024-10-08 05:43:57 +0200floyza(~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown
2024-10-08 05:44:40 +0200infinity0(~infinity0@pwned.gg) (Ping timeout: 272 seconds)
2024-10-08 05:46:59 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
2024-10-08 05:49:41 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 06:04:53 +0200infinity0(~infinity0@pwned.gg) infinity0
2024-10-08 06:07:51 +0200talismanick(~user@2601:644:937c:ed10::ae5) (Remote host closed the connection)
2024-10-08 06:08:05 +0200talismanick(~user@2601:644:937c:ed10::ae5) talismanick
2024-10-08 06:15:45 +0200vanishingideal(~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 +0200simendsjo(~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 +0200LukeHoersten(~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 +0200michalz(~michalz@185.246.207.222)
2024-10-08 07:03:41 +0200astraamish
2024-10-08 07:03:44 +0200amish(sid289983@id-289983.hampstead.irccloud.com) (Changing host)
2024-10-08 07:03:44 +0200amish(sid289983@user/amish) amish
2024-10-08 07:04:04 +0200amishastra
2024-10-08 07:08:47 +0200st_aldini1(~Thunderbi@136.48.22.91) st_aldini
2024-10-08 07:09:05 +0200euphores(~SASL_euph@user/euphores) euphores
2024-10-08 07:10:13 +0200st_aldini(~Thunderbi@136.48.22.91) (Ping timeout: 248 seconds)
2024-10-08 07:10:13 +0200st_aldini1st_aldini
2024-10-08 07:12:38 +0200takuan(~takuan@178-116-218-225.access.telenet.be)
2024-10-08 07:21:51 +0200dtman34(~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 +0200dtman34(~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) dtman34
2024-10-08 07:23:01 +0200jinsun(~jinsun@user/jinsun) (Ping timeout: 248 seconds)
2024-10-08 07:32:01 +0200weary-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 +0200acidjnk(~acidjnk@p200300d6e72cfb34519e9ca14c5ce943.dip0.t-ipconnect.de) acidjnk
2024-10-08 07:57:33 +0200ubert(~Thunderbi@178.165.187.120.wireless.dyn.drei.com) ubert
2024-10-08 08:04:00 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 272 seconds)
2024-10-08 08:08:25 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-10-08 08:08:38 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 08:09:11 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2024-10-08 08:09:33 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 08:10:24 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 08:10:57 +0200mari-estel(~mari-este@185.238.219.10)
2024-10-08 08:11:38 +0200mari77696(~mari-este@185.238.219.10)
2024-10-08 08:14:05 +0200foul_owl(~kerry@185.219.141.162) (Ping timeout: 255 seconds)
2024-10-08 08:17:16 +0200sord937(~sord937@gateway/tor-sasl/sord937) sord937
2024-10-08 08:32:05 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-10-08 08:32:17 +0200mari77696(~mari-este@185.238.219.10) (Ping timeout: 248 seconds)
2024-10-08 08:32:49 +0200mari-estel(~mari-este@185.238.219.10) (Ping timeout: 248 seconds)
2024-10-08 08:42:16 +0200rosco(~rosco@175.136.22.30) rosco
2024-10-08 08:44:10 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-08 08:57:37 +0200foul_owl(~kerry@185.219.141.162) foul_owl
2024-10-08 09:00:00 +0200caconym(~caconym@user/caconym) (Quit: bye)
2024-10-08 09:00:37 +0200caconym(~caconym@user/caconym) caconym
2024-10-08 09:01:40 +0200lortabac(~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 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 276 seconds)
2024-10-08 09:13:36 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-08 09:13:53 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-10-08 09:14:09 +0200gorignak(~gorignak@user/gorignak) gorignak
2024-10-08 09:16:47 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Quit: au revoir)
2024-10-08 09:24:55 +0200zlqrvx(~zlqrvx@user/zlqrvx) zlqrvx
2024-10-08 09:24:57 +0200alp_(~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 +0200mari68681(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef)
2024-10-08 09:32:13 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef)
2024-10-08 09:32:41 +0200briandaed(~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 +0200rosco(~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 +0200cfricke(~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 +0200mari68681(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 252 seconds)
2024-10-08 09:45:09 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 252 seconds)
2024-10-08 09:45:21 +0200floyza(~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection)
2024-10-08 09:45:56 +0200econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2024-10-08 09:47:02 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale
2024-10-08 09:53:29 +0200chele(~chele@user/chele) chele
2024-10-08 09:58:08 +0200sourcetarius(~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 +0200machinedgod(~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 +0200merijn(~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 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 245 seconds)
2024-10-08 10:03:43 +0200raym_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 +0200kuribas(~user@2a02:1808:7:f56b:d4a9:b96f:9d61:d1a7) kuribas
2024-10-08 10:12:08 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-08 10:20:53 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale
2024-10-08 10:22:46 +0200CiaoSen(~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) CiaoSen
2024-10-08 10:24:12 +0200raym(~ray@user/raym) (Ping timeout: 252 seconds)
2024-10-08 10:25:52 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-08 10:30:26 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-10-08 10:33:15 +0200Maeda(~Maeda@91-161-10-149.subs.proxad.net) Maeda
2024-10-08 10:33:29 +0200Maeda(~Maeda@91-161-10-149.subs.proxad.net) (Client Quit)
2024-10-08 10:33:38 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-10-08 10:37:13 +0200euphores(~SASL_euph@user/euphores) euphores
2024-10-08 10:40:24 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) (Remote host closed the connection)
2024-10-08 10:40:59 +0200raym(~ray@user/raym) raym
2024-10-08 10:41:07 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale
2024-10-08 10:42:54 +0200kuribas`(~user@ip-188-118-57-242.reverse.destiny.be) kuribas
2024-10-08 10:44:33 +0200kuribas(~user@2a02:1808:7:f56b:d4a9:b96f:9d61:d1a7) (Ping timeout: 248 seconds)
2024-10-08 10:52:35 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 265 seconds)
2024-10-08 10:54:10 +0200synchromesh(~john@2406:5a00:241a:5600:1537:bb1c:ebe9:2fdf) (Read error: Connection reset by peer)
2024-10-08 10:54:33 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-08 10:55:10 +0200synchromesh(~john@2406:5a00:241a:5600:dc23:4239:fb04:33f4) synchromesh
2024-10-08 10:55:18 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2024-10-08 11:01:04 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-08 11:03:34 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-08 11:04:04 +0200gorignak(~gorignak@user/gorignak) (Ping timeout: 252 seconds)
2024-10-08 11:04:30 +0200gorignak(~gorignak@user/gorignak) gorignak
2024-10-08 11:10:26 +0200fmira(~user@user/fmira) (Quit: fmira)
2024-10-08 11:17:25 +0200rosco(~rosco@175.136.22.30) rosco
2024-10-08 11:17:59 +0200supercode(~supercode@user/supercode) supercode
2024-10-08 11:22:26 +0200arahael(~arahael@user/arahael) (Remote host closed the connection)
2024-10-08 11:22:29 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 248 seconds)
2024-10-08 11:27:40 +0200Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2024-10-08 11:30:47 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2024-10-08 11:31:00 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-08 11:32:17 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-08 11:36:42 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-08 11:36:55 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-08 11:37:37 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2024-10-08 11:42:04 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-10-08 11:44:31 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-08 11:48:47 +0200Guest41(~Guest41@ip-38-9-3-83.internet.url.net.au)
2024-10-08 11:49:13 +0200Guest41(~Guest41@ip-38-9-3-83.internet.url.net.au) (Client Quit)
2024-10-08 11:52:45 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-08 11:55:01 +0200alp_(~alp@2001:861:e3d6:8f80:9869:a17b:401:f55) (Ping timeout: 252 seconds)
2024-10-08 12:08:58 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
2024-10-08 12:15:29 +0200andrewboltachev(~andrey@178.141.244.27) andrewboltachev
2024-10-08 12:18:34 +0200aforemny(~aforemny@2001:9e8:6cd9:9400:c5f2:6987:2beb:3640) aforemny
2024-10-08 12:19:09 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
2024-10-08 12:19:22 +0200euleritian(~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 +0200CiaoSen(~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds)
2024-10-08 12:31:21 +0200supercode(~supercode@user/supercode) (Killed (NickServ (GHOST command used by supercode63)))
2024-10-08 12:31:23 +0200euleritian(~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-08 12:31:40 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 12:35:26 +0200comerijn(~merijn@77.242.116.146) merijn
2024-10-08 12:38:26 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 265 seconds)
2024-10-08 12:39:21 +0200alp_(~alp@2001:861:e3d6:8f80:446d:e3f8:e9a4:2f3b)
2024-10-08 12:40:59 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef)
2024-10-08 12:42:42 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2024-10-08 12:42:58 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 12:47:44 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds)
2024-10-08 12:48:49 +0200euleritian(~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de)
2024-10-08 12:51:31 +0200euleritian(~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-08 12:51:48 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 12:58:31 +0200rosco(~rosco@175.136.22.30) (Quit: Lost terminal)
2024-10-08 13:00:05 +0200caconym(~caconym@user/caconym) (Quit: bye)
2024-10-08 13:02:34 +0200caconym(~caconym@user/caconym) caconym
2024-10-08 13:05:28 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2024-10-08 13:10:26 +0200xff0x(~xff0x@2405:6580:b080:900:da07:5be8:5f56:f410)
2024-10-08 13:12:14 +0200comerijn(~merijn@77.242.116.146) (Ping timeout: 260 seconds)
2024-10-08 13:14:58 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 272 seconds)
2024-10-08 13:17:56 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef)
2024-10-08 13:19:46 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-08 13:21:39 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Client Quit)
2024-10-08 13:25:17 +0200srazkvt(~sarah@user/srazkvt) srazkvt
2024-10-08 13:33:37 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 248 seconds)
2024-10-08 13:39:01 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 13:40:49 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-08 13:50:23 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 245 seconds)
2024-10-08 13:52:48 +0200rosco(~rosco@175.136.22.30) rosco
2024-10-08 13:53:15 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-08 13:55:26 +0200rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2024-10-08 13:55:55 +0200rvalue(~rvalue@user/rvalue) rvalue
2024-10-08 14:01:58 +0200ash3en(~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 +0200ash3en(~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 +0200ash3en(~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 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 264 seconds)
2024-10-08 14:22:41 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-08 14:30:03 +0200ash3en(~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds)
2024-10-08 14:30:23 +0200ash3en(~Thunderbi@193.32.248.167) ash3en
2024-10-08 14:34:17 +0200CiaoSen(~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) CiaoSen
2024-10-08 14:38:11 +0200srazkvt(~sarah@user/srazkvt) (Quit: Konversation terminated!)
2024-10-08 14:40:17 +0200Lord_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 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 14:41:34 +0200identity(~identity@user/ZharMeny) identity
2024-10-08 14:45:52 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-08 14:51:33 +0200AlexZenon(~alzenon@178.34.151.120) (Quit: ;-)
2024-10-08 14:52:01 +0200AlexNoo(~AlexNoo@178.34.151.120) (Quit: Leaving)
2024-10-08 14:52:13 +0200Pixi`(~Pixi@user/pixi) Pixi
2024-10-08 14:55:13 +0200Pixi(~Pixi@user/pixi) (Ping timeout: 248 seconds)
2024-10-08 15:01:35 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-08 15:02:45 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-08 15:04:13 +0200ash3en(~Thunderbi@193.32.248.167) (Quit: ash3en)
2024-10-08 15:04:47 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-08 15:07:42 +0200Angelz(Angelz@user/angelz) (Ping timeout: 272 seconds)
2024-10-08 15:08:18 +0200zfnmxt(~zfnmxt@107.189.30.63) (Ping timeout: 245 seconds)
2024-10-08 15:12:19 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef)
2024-10-08 15:21:38 +0200alexherbo2(~alexherbo@2a02-8440-3202-2f93-5c9a-6ec5-11de-f4fb.rev.sfr.net) alexherbo2
2024-10-08 15:27:34 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds)
2024-10-08 15:28:22 +0200AlexNoo(~AlexNoo@178.34.151.120)
2024-10-08 15:30:33 +0200AlexZenon(~alzenon@178.34.151.120)
2024-10-08 15:31:06 +0200weary-traveler(~user@user/user363627) user363627
2024-10-08 15:54:17 +0200ash3en(~Thunderbi@193.32.248.167) ash3en
2024-10-08 16:00:49 +0200alp_(~alp@2001:861:e3d6:8f80:446d:e3f8:e9a4:2f3b) (Ping timeout: 260 seconds)
2024-10-08 16:01:29 +0200mari-estel(~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 244 seconds)
2024-10-08 16:02:14 +0200Lord_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 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 16:04:09 +0200ash3en(~Thunderbi@193.32.248.167) (Ping timeout: 276 seconds)
2024-10-08 16:06:31 +0200ash3en(~Thunderbi@193.32.248.167) ash3en
2024-10-08 16:09:53 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-10-08 16:09:59 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-10-08 16:10:07 +0200euleritian(~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de)
2024-10-08 16:10:30 +0200euleritian(~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-08 16:10:47 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 16:11:31 +0200ash3en(~Thunderbi@193.32.248.167) (Ping timeout: 264 seconds)
2024-10-08 16:13:15 +0200synchromesh(~john@2406:5a00:241a:5600:dc23:4239:fb04:33f4) (Ping timeout: 276 seconds)
2024-10-08 16:14:22 +0200Lord_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 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 16:15:56 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-10-08 16:16:27 +0200gorignak(~gorignak@user/gorignak) gorignak
2024-10-08 16:19:35 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-08 16:23:24 +0200biberao(~m@user/biberao) biberao
2024-10-08 16:23:26 +0200 <biberao> hi
2024-10-08 16:27:45 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-10-08 16:35:46 +0200gabiruh(~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in)
2024-10-08 16:35:53 +0200ash3en(~Thunderbi@193.32.248.167) ash3en
2024-10-08 16:36:10 +0200gabiruh(~gabiruh@vps19177.publiccloud.com.br) gabiruh
2024-10-08 16:43:35 +0200synchromesh(~john@180.148.124.74) synchromesh
2024-10-08 16:46:31 +0200ash3en(~Thunderbi@193.32.248.167) (Ping timeout: 252 seconds)
2024-10-08 16:49:02 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-08 16:53:46 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-08 16:55:41 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-08 17:00:09 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds)
2024-10-08 17:04:46 +0200alp_(~alp@2001:861:e3d6:8f80:1e84:aaa4:b350:85e4)
2024-10-08 17:07:35 +0200Lord_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 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 17:08:19 +0200CiaoSen(~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds)
2024-10-08 17:10:51 +0200ljdarj(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-08 17:11:11 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-08 17:16:33 +0200Lord_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 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 17:18:27 +0200jinsun(~jinsun@user/jinsun) jinsun
2024-10-08 17:20:36 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection)
2024-10-08 17:21:11 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 17:25:26 +0200alexherbo2(~alexherbo@2a02-8440-3202-2f93-5c9a-6ec5-11de-f4fb.rev.sfr.net) (Remote host closed the connection)
2024-10-08 17:31:44 +0200Lord_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 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-08 17:32:00 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
2024-10-08 17:32:15 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 17:35:31 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Client Quit)
2024-10-08 17:38:00 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-08 17:44:17 +0200rosco(~rosco@175.136.22.30) (Quit: Lost terminal)
2024-10-08 17:45:35 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-08 17:48:05 +0200alp_(~alp@2001:861:e3d6:8f80:1e84:aaa4:b350:85e4) (Ping timeout: 248 seconds)
2024-10-08 17:50:16 +0200califax(~califax@user/califx) (Ping timeout: 260 seconds)
2024-10-08 17:50:26 +0200vanishingideal(~vanishing@user/vanishingideal) (Read error: Connection reset by peer)
2024-10-08 17:50:54 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 17:51:36 +0200califax(~califax@user/califx) califx
2024-10-08 17:52:29 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-08 17:53:12 +0200Digitteknohippie(~user@user/digit) Digit
2024-10-08 17:53:41 +0200Digit(~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 +0200spew(~spew@201.141.99.170) spew
2024-10-08 17:57:53 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-10-08 17:58:11 +0200califax(~califax@user/califx) califx
2024-10-08 18:00:30 +0200berberman(~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in)
2024-10-08 18:00:57 +0200berberman(~berberman@user/berberman) berberman
2024-10-08 18:04:19 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
2024-10-08 18:04:56 +0200euleritian(~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de)
2024-10-08 18:08:21 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-08 18:09:09 +0200berberman(~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in)
2024-10-08 18:10:11 +0200berberman(~berberman@user/berberman) berberman
2024-10-08 18:12:41 +0200ljdarj(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-08 18:13:02 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-08 18:13:09 +0200petrichor(~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
2024-10-08 18:13:23 +0200petrichor(~znc-user@user/petrichor) petrichor
2024-10-08 18:13:26 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-08 18:17:22 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 244 seconds)
2024-10-08 18:18:33 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-10-08 18:18:41 +0200kuribas`(~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
2024-10-08 18:19:03 +0200DigitteknohippieDigit
2024-10-08 18:25:00 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-08 18:30:18 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 252 seconds)
2024-10-08 18:31:44 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
2024-10-08 18:34:22 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh
2024-10-08 18:34:28 +0200rvalue-(~rvalue@user/rvalue) rvalue
2024-10-08 18:35:11 +0200pavonia(~user@user/siracusa) siracusa
2024-10-08 18:35:29 +0200rvalue(~rvalue@user/rvalue) (Ping timeout: 248 seconds)
2024-10-08 18:35:30 +0200Pixi`Pixi
2024-10-08 18:37:00 +0200euleritian(~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-08 18:37:17 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 18:40:22 +0200rvalue-rvalue
2024-10-08 18:42:04 +0200alp_(~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 +0200ljdarj(~Thunderbi@user/ljdarj) (Quit: ljdarj)
2024-10-08 18:44:54 +0200cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-10-08 18:49:41 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-08 18:49:49 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-10-08 18:51:32 +0200EvanR(~EvanR@user/evanr) (Quit: Leaving)
2024-10-08 18:53:12 +0200chele(~chele@user/chele) (Remote host closed the connection)
2024-10-08 18:53:27 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
2024-10-08 18:53:37 +0200euleritian(~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de)
2024-10-08 18:56:14 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-08 18:57:23 +0200vanishingideal(~vanishing@user/vanishingideal) (Quit: Lost terminal)
2024-10-08 19:07:30 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!)
2024-10-08 19:08:00 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2024-10-08 19:09:10 +0200CiaoSen(~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) CiaoSen
2024-10-08 19:10:16 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 19:11:11 +0200euleritian(~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-08 19:11:29 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 19:12:11 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 19:17:14 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-08 19:23:06 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 252 seconds)
2024-10-08 19:23:06 +0200andrewboltachev(~andrey@178.141.244.27) (Quit: Leaving.)
2024-10-08 19:23:59 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-10-08 19:24:49 +0200wootehfoot(~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 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 19:29:56 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 19:30:43 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 265 seconds)
2024-10-08 19:31:17 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2024-10-08 19:31:59 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-08 19:33:06 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-08 19:35:20 +0200ss4(~wootehfoo@user/wootehfoot) wootehfoot
2024-10-08 19:37:29 +0200causal(~eric@50.35.88.207) causal
2024-10-08 19:38:05 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-10-08 19:38:13 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-08 19:39:09 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Ping timeout: 252 seconds)
2024-10-08 19:43:26 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-08 19:43:46 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 19:48:37 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-10-08 19:48:45 +0200kaskal(~kaskal@2001:4bb8:2af:db4a:8acd:a0ac:f117:1e24) (Quit: ZNC - https://znc.in)
2024-10-08 19:49:07 +0200kaskal(~kaskal@2001:4bb8:2af:db4a:8213:de4d:dd34:38f3) kaskal
2024-10-08 19:52:57 +0200ss4(~wootehfoo@user/wootehfoot) (Ping timeout: 246 seconds)
2024-10-08 19:55:37 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2024-10-08 19:55:40 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-10-08 19:56:11 +0200gorignak(~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 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 20:01:07 +0200Batzy_(~quassel@user/batzy) Batzy
2024-10-08 20:03:17 +0200Batzy(~quassel@user/batzy) (Ping timeout: 255 seconds)
2024-10-08 20:04:33 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-10-08 20:05:00 +0200ubert(~Thunderbi@178.165.187.120.wireless.dyn.drei.com) (Ping timeout: 252 seconds)
2024-10-08 20:08:13 +0200vanishingideal(~vanishing@user/vanishingideal) (Read error: Connection reset by peer)
2024-10-08 20:10:40 +0200mrtz(~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net)
2024-10-08 20:11:14 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 20:11:47 +0200samanklesaria(~samankles@68-168-167-245.fttp.usinternet.com)
2024-10-08 20:14:16 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 20:16:13 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-10-08 20:17:17 +0200briandaed(~root@185.234.210.211.r.toneticgroup.pl) (Remote host closed the connection)
2024-10-08 20:17:45 +0200lol_(~lol@2603:3016:1e01:b9e0:835:2698:e6f:bd82)
2024-10-08 20:19:19 +0200samanklesaria(~samankles@68-168-167-245.fttp.usinternet.com) (Remote host closed the connection)
2024-10-08 20:20:24 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds)
2024-10-08 20:20:51 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds)
2024-10-08 20:21:34 +0200jcarpenter2(~lol@2603:3016:1e01:b9e0:9c4e:1030:31bf:f76b) (Ping timeout: 260 seconds)
2024-10-08 20:24:22 +0200mrtz(~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) (Ping timeout: 265 seconds)
2024-10-08 20:27:01 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 20:35:24 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-10-08 20:38:57 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 20:43:55 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
2024-10-08 20:50:38 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-08 20:54:42 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 20:56:25 +0200Pixi(~Pixi@user/pixi) (Quit: Leaving)
2024-10-08 20:59:54 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-10-08 21:00:01 +0200caconym(~caconym@user/caconym) (Quit: bye)
2024-10-08 21:00:37 +0200caconym(~caconym@user/caconym) caconym
2024-10-08 21:01:51 +0200CiaoSen(~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds)
2024-10-08 21:07:43 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-10-08 21:08:14 +0200gorignak(~gorignak@user/gorignak) gorignak
2024-10-08 21:15:33 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 21:17:34 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds)
2024-10-08 21:17:55 +0200machinedgod(~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 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-10-08 21:20:40 +0200Pixi(~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 +0200tomsmedinghas 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 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 21:31:39 +0200supercode(~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 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 245 seconds)
2024-10-08 21:33:39 +0200mantraofpie(~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 +0200merijn(~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 +0200ubert(~Thunderbi@178.165.187.120.wireless.dyn.drei.com) ubert
2024-10-08 21:40:12 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 21:40:58 +0200causal(~eric@50.35.88.207) (Ping timeout: 252 seconds)
2024-10-08 21:41:22 +0200causal(~eric@50.35.88.207) causal
2024-10-08 21:48:00 +0200TimWolla(~timwolla@2a01:4f8:150:6153:beef::6667) (Quit: Bye)
2024-10-08 21:48:19 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 21:49:03 +0200supercode(~supercode@user/supercode) (Quit: Client closed)
2024-10-08 21:53:21 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-10-08 21:53:27 +0200zfnmxt(~zfnmxt@user/zfnmxt) zfnmxt
2024-10-08 21:55:29 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 248 seconds)
2024-10-08 21:57:12 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 21:58:46 +0200codaraxis(~codaraxis@user/codaraxis) Codaraxis
2024-10-08 21:59:27 +0200TimWolla(~timwolla@2a01:4f8:150:6153:beef::6667) TimWolla
2024-10-08 22:00:24 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-10-08 22:04:05 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 22:05:13 +0200alexherbo2(~alexherbo@2a02-8440-3215-f56e-1190-0b59-796f-612e.rev.sfr.net) alexherbo2
2024-10-08 22:05:44 +0200sourcetarius(~sourcetar@user/sourcetarius) (Quit: sourcetarius)
2024-10-08 22:08:49 +0200merijn(~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 +0200Angelz(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 +0200merijn(~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 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2024-10-08 22:17:28 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-10-08 22:21:29 +0200 <monochrom> IIRC the definition of algebraic effect includes a monad, it's a prerequisite. The monad is as free as the algebra.
2024-10-08 22:22:16 +0200 <tomsmeding> (disclaimer about weak CT-fu) can (algebraic) effects not be described merely as operations and equations, without reference to any monad?
2024-10-08 22:22:17 +0200 <monochrom> (Also I hate English. Officially, "prerequisite" is uncountable and my "a prerequisite" is illegal.)
2024-10-08 22:22:30 +0200 <tomsmeding> wait wat
2024-10-08 22:23:10 +0200 <tomsmeding> wiktionary does not agree https://en.wiktionary.org/wiki/prerequisite#Noun
2024-10-08 22:23:11 +0200 <monochrom> Yeah officially one has to say "a prerequisite requirement" so "a" belongs to "requirement" which is allowed to be countable. :)
2024-10-08 22:23:20 +0200 <tomsmeding> (phew)
2024-10-08 22:23:33 +0200 <tomsmeding> the adjectival use is also described
2024-10-08 22:23:41 +0200 <sam113101> https://paste.centos.org/view/raw/bf9a82a0
2024-10-08 22:23:43 +0200 <tomsmeding> but I don't see any uncountable definition
2024-10-08 22:23:45 +0200 <dolio> I bet the dictionaries are just lagging on that.
2024-10-08 22:23:58 +0200 <sam113101> I like how the information flows from left to right, sometimes that's clearer
2024-10-08 22:24:09 +0200 <sam113101> monochrom: what's a monad?
2024-10-08 22:24:19 +0200 <monochrom> In this case I think "the language keeps changing" applies. It was uncountable by the standard of old-school people.
2024-10-08 22:24:32 +0200 <monochrom> To be sure, I would be the first to welcome this change!
2024-10-08 22:24:41 +0200 <dolio> Algebraic effects are (slightly generalized) Lawvere theories.
2024-10-08 22:24:42 +0200 <TMA> isn't "a prerequisite requirement" a superfluous pleonasm?
2024-10-08 22:24:56 +0200 <monochrom> It's about time every English noun is made countable. I used to have a lot of hairs. There!
2024-10-08 22:25:17 +0200 <tomsmeding> "hair" is a countable noun _and_ an uncountable noun ;)
2024-10-08 22:25:23 +0200 <tomsmeding> I can definitely have three hairs in my hand
2024-10-08 22:25:30 +0200 <monochrom> Also, s/is made/was made/ . (I hate English. Let's get rid of tenses too.)
2024-10-08 22:26:15 +0200 <sam113101> nah I think "is" is the right one
2024-10-08 22:26:16 +0200 <monochrom> Generalized Wadler's Rule: English syntax is more discussed than Haskell semantics. >:)
2024-10-08 22:26:23 +0200 <sam113101> not an English expert though
2024-10-08 22:26:30 +0200 <dolio> But, the actual theories you can present in most programming scenarios do not have any equations.
2024-10-08 22:27:04 +0200 <tomsmeding> dolio: I have no clue what a Lawvere theory is :)
2024-10-08 22:27:33 +0200 <dolio> It's the categorical version of 'operations and equations' sorts of algebraic theories.
2024-10-08 22:27:40 +0200 <dolio> Finitary ones.
2024-10-08 22:27:40 +0200 <tomsmeding> I see
2024-10-08 22:27:41 +0200 <TMA> I vote for "It's about time every English noun be made countable."
2024-10-08 22:27:48 +0200 <tomsmeding> TMA++
2024-10-08 22:28:02 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 22:28:07 +0200 <tomsmeding> subjunctive is underused
2024-10-08 22:28:09 +0200 <TMA> we have the subjunctive so use it!
2024-10-08 22:28:14 +0200 <dolio> The papers on algebraic effects usually make them of countable arity rather than just finite.
2024-10-08 22:31:18 +0200 <sam113101> I remembering tyring to learn haskell
2024-10-08 22:32:29 +0200 <monochrom> sam113101: Consider [0..1000] & (filter (\x -> ...) >>> sum). >>> is from Control.Category, it looks general, but this one specializes to flip (.)
2024-10-08 22:32:36 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-10-08 22:32:58 +0200 <tomsmeding> also: [0..1000] & filter (\x -> ...) & sum
2024-10-08 22:34:19 +0200 <monochrom> I teach a Unix course so I prioritize "< input {filter | sum}". :)
2024-10-08 22:34:36 +0200moe_(~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net)
2024-10-08 22:34:37 +0200 <tomsmeding> what language is that lol
2024-10-08 22:34:52 +0200 <monochrom> plain bourne shell!
2024-10-08 22:35:06 +0200 <monochrom> And yes "<file cmd" is the same as "cmd <file"
2024-10-08 22:35:09 +0200 <tomsmeding> oh hah
2024-10-08 22:35:11 +0200 <tomsmeding> it is
2024-10-08 22:35:22 +0200 <geekosaur> yep, redirections can go anywhere in a command
2024-10-08 22:35:27 +0200 <tomsmeding> I knew that
2024-10-08 22:35:29 +0200 <monochrom> I actually read the bloody POSIX/OpenGroup docs to learn the detailed grammar!
2024-10-08 22:36:13 +0200 <tomsmeding> but the spacing (space after '<', no space after '{') and the ordering (what you say), combined with 'filter' and 'sum' not being the right commands here, made my brain not recognise it :p
2024-10-08 22:37:11 +0200 <monochrom> Also I know that students just google for solutions and hand in "sum <(filter < input)" which is the equiv of using (&) so I declare "no bash feature, only posix shell" to force them to learn pipelining.
2024-10-08 22:37:12 +0200 <geekosaur> I learned it from the old Bourne shell manual, although back then you needed extra semicolons (`{; filter | sum; }`)
2024-10-08 22:37:38 +0200 <monochrom> Oops I forgot the semicolon.
2024-10-08 22:37:51 +0200 <tomsmeding> ah right
2024-10-08 22:38:08 +0200 <monochrom> #1 source of mysterious syntax error messages
2024-10-08 22:38:18 +0200 <tomsmeding> if you insist on putting the redirection first, I would prefer "<input filter | sum" :p
2024-10-08 22:38:24 +0200 <tomsmeding> the {} being unnecessary
2024-10-08 22:41:27 +0200 <Lears> tomsmeding: The usual definition of algebraicity of an effect `op` is: 1. `op :: forall a. S (M a) -> M a` for some functor `S` and monad `M`; 2. `forall x, k. op x >>= k = op (x <&> (>>= k))`. Good luck extricating monad from that.
2024-10-08 22:41:46 +0200 <monochrom> From the grand unified CT POV I just teach one course: Kleisli categories. After symmetry breaking at low energies, it looks like I teach two courses: Unix, Haskell. >:)
2024-10-08 22:42:54 +0200 <tomsmeding> Lears: I'll have to pick the brain of the person who explained effects to me again :p
2024-10-08 22:43:49 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 22:44:00 +0200 <monochrom> Many effect languages (eg Koka) don't expose the underlying monads to the programmers. However, the monad is there in the math theory. You can always choose to upplay or downplay it though.
2024-10-08 22:44:45 +0200 <tomsmeding> Lears: but thanks for the concise and understandable (to my haskell brain) definition!
2024-10-08 22:45:10 +0200 <tomsmeding> (talking about English: "upplay" is a nice coinage)
2024-10-08 22:46:08 +0200 <monochrom> Did you know: When teaching computability, I pioneered renaming "not recognizable" to "unrecognizable". >:)
2024-10-08 22:46:14 +0200 <dolio> You probably replace the monad with 'models'.
2024-10-08 22:48:48 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-08 22:48:49 +0200zfnmxt(~zfnmxt@user/zfnmxt) (Ping timeout: 248 seconds)
2024-10-08 22:50:03 +0200Angelz(Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Ping timeout: 246 seconds)
2024-10-08 22:53:18 +0200moe_(~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) (Ping timeout: 252 seconds)
2024-10-08 22:54:23 +0200zfnmxt(~zfnmxt@user/zfnmxt) zfnmxt
2024-10-08 22:57:13 +0200 <biberao> monochrom: so you're a professor?
2024-10-08 22:59:35 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 23:01:13 +0200alexherbo2(~alexherbo@2a02-8440-3215-f56e-1190-0b59-796f-612e.rev.sfr.net) (Ping timeout: 256 seconds)
2024-10-08 23:01:14 +0200ubert(~Thunderbi@178.165.187.120.wireless.dyn.drei.com) (Ping timeout: 260 seconds)
2024-10-08 23:03:10 +0200 <dolio> I.E. that looks basically like, 'M is a family of S-models,' but why only consider S-models that can be assembled into a monad?
2024-10-08 23:05:14 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2024-10-08 23:06:09 +0200takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-10-08 23:08:59 +0200michalz(~michalz@185.246.207.222) (Remote host closed the connection)
2024-10-08 23:09:46 +0200weary-traveler(~user@user/user363627) user363627
2024-10-08 23:10:35 +0200 <monochrom> Because I write code like "foo x = { y <- op0 x; if | pred1 y -> op1 y | pred2 y -> op2 y | otherwise -> {z <- op3 y; foo z}}". That needs at least Selective+Arrow.
2024-10-08 23:11:13 +0200 <haskellbridge> <thirdofmay18081814goya> dolio: models for algebraic theories are given by monads
2024-10-08 23:13:04 +0200biberu(~biberu@user/biberu) (Read error: Connection reset by peer)
2024-10-08 23:15:22 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 23:15:26 +0200 <dolio> They don't have to be.
2024-10-08 23:17:12 +0200vanishingideal(~vanishing@user/vanishingideal) (Read error: Connection reset by peer)
2024-10-08 23:17:38 +0200 <haskellbridge> <thirdofmay18081814goya> ah right, strict statement is: the free models of an algebraic theory form a monad
2024-10-08 23:19:56 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 23:20:08 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-10-08 23:24:22 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 252 seconds)
2024-10-08 23:25:04 +0200biberao(~m@user/biberao) (Quit: WeeChat 3.8)
2024-10-08 23:25:17 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 23:25:49 +0200biberu(~biberu@user/biberu) biberu
2024-10-08 23:31:10 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 23:33:29 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 260 seconds)
2024-10-08 23:33:54 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-08 23:35:49 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-10-08 23:40:29 +0200alp_(~alp@2001:861:e3d6:8f80:cf3a:e88a:f2c8:6274) (Ping timeout: 252 seconds)
2024-10-08 23:42:48 +0200emmanuelux(~emmanuelu@user/emmanuelux) emmanuelux
2024-10-08 23:46:56 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-10-08 23:51:46 +0200merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)