Logs on 2024-10-08 (liberachat/#haskell)
| 00:05:08 | → | gentauro joins (~gentauro@user/gentauro) |
| 00:26:42 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 00:27:02 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 00:34:07 | → | TonyStone joins (~TonyStone@user/TonyStone) |
| 00:35:20 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 00:37:41 | × | alp_ quits (~alp@2001:861:e3d6:8f80:e06c:ffe4:c8a0:d22b) (Ping timeout: 248 seconds) |
| 00:39:25 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 00:39:57 | → | morb joins (~morb@108.41.100.120) |
| 00:44:39 | → | hgolden__ joins (~hgolden@23.162.40.28) |
| 00:47:20 | × | hgolden_ quits (~hgolden@146.70.173.37) (Ping timeout: 272 seconds) |
| 00:48:04 | × | xff0x quits (~xff0x@2405:6580:b080:900:8633:3fd0:abbc:825) (Ping timeout: 260 seconds) |
| 00:52:05 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 248 seconds) |
| 00:54:24 | × | morb quits (~morb@108.41.100.120) (Remote host closed the connection) |
| 01:12:56 | × | spew quits (~spew@201.141.99.170) (Quit: spew) |
| 01:23:30 | × | krei-se quits (~krei-se@p57af2362.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 01:24:12 | → | krei-se joins (~krei-se@p5085d9ca.dip0.t-ipconnect.de) |
| 01:24:13 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 01:24:22 | → | ethantwardy joins (user@user/ethantwardy) |
| 01:25:26 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 01:28:54 | <haskellbridge> | <thirdofmay18081814goya> what are some useful coinductive types? |
| 01:29:09 | → | troojg joins (~troojg@user/troojg) |
| 01:29:17 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 01:29:43 | <monochrom> | Infinite lists. Infinite free monads. |
| 01:30:14 | <haskellbridge> | <thirdofmay18081814goya> hm right i see ty |
| 01:31:06 | <talismanick> | infinite (nonempty) lists are often referred to in literature as streams |
| 01:31:13 | <talismanick> | you can even do calculus on them: https://www.cs.ox.ac.uk/people/ralf.hinze/publications/CSC.pdf |
| 01:32:01 | <haskellbridge> | <thirdofmay18081814goya> are these the streams you usually encounter in programming? |
| 01:33:35 | <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? |
| 01:34:17 | <EvanR> | object oriented programming via copatterns |
| 01:34:18 | <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. |
| 01:34:33 | <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..]]) |
| 01:35:05 | <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) |
| 01:35:14 | <EvanR> | chalk up remote host closed connection to "thread died" xD |
| 01:35:26 | <EvanR> | thread's code itself has no idea |
| 01:35:44 | <EvanR> | it never observed the end of the stream so it's still infinite xD |
| 01:35:57 | <talismanick> | https://hackage.haskell.org/package/comonad-5.0.8/ shows 164 reverse dependencies and 8416 indirect |
| 01:36:15 | <talismanick> | so there are few cases :D |
| 01:36:31 | <haskellbridge> | <thirdofmay18081814goya> i see thanks for comments! |
| 01:37:12 | <geekosaur> | fwiw what I am aiming for is "the size isn't defined statically by your program, but by something synamic / outside of it" |
| 01:37:45 | <geekosaur> | *dynamic |
| 01:38:58 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 01:39:07 | <EvanR> | the basic haskell list type really is a conundrum for ultrafinitists right |
| 01:39:09 | <monochrom> | It is the same as "unbounded" Integer where there is a bound but it's outside of your model. |
| 01:39:23 | <EvanR> | if all haskell lists are "really" finite, then what is the answer to length (repeat ()) |
| 01:39:54 | <EvanR> | or is the length function broken |
| 01:40:11 | <geekosaur> | ⊥ because `length` breaks when it hits `maxBound :: Int` |
| 01:40:28 | <EvanR> | >_< |
| 01:41:35 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 01:41:58 | <haskellbridge> | <thirdofmay18081814goya> hm can we not do induction on coinductive structures or does coinduction capture something completely different? |
| 01:42:12 | <haskellbridge> | <thirdofmay18081814goya> (is coinduction the type eliminator for coinductive types?) |
| 01:43:42 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 01:45:53 | geekosaur | is wondering if it would be a type introducer |
| 01:46:34 | <geekosaur> | (or "co-eliminator", whatever that works out to be) |
| 01:48:24 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 01:51:04 | <EvanR> | the only reason you can do induction on an inductive type is because it comes with an induction rule |
| 01:51:59 | <EvanR> | unless you can figure out how to synthesize one as a theorem |
| 01:52:09 | <haskellbridge> | <thirdofmay18081814goya> yeah the induction rule associated to a particular inductive type is the elimination rule for that type |
| 01:54:08 | <monochrom> | induction rule is part of what "inductive type" means. What does "coinductive type" mean? Perhaps it contains the coinduction rule. |
| 01:54:31 | <EvanR> | you can probably come up with a coinductive type which it is possible to derive a synthetic induction rule |
| 01:54:35 | <EvanR> | for |
| 01:54:56 | <EvanR> | like one that doesn't lead to infinite data |
| 01:56:22 | <EvanR> | but if you look at another example, the potentially infinite natural number type... you can see how induction would fail |
| 01:57:38 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 01:57:59 | <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 |
| 01:58:04 | <EvanR> | no |
| 01:59:20 | <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 |
| 01:59:47 | <EvanR> | specifically define the potentially infinite natural numbers using the coinductive style |
| 01:59:59 | <EvanR> | not set theory |
| 01:59:59 | <haskellbridge> | <thirdofmay18081814goya> oh |
| 02:00:08 | <haskellbridge> | <thirdofmay18081814goya> ok i see |
| 02:00:28 | <EvanR> | though I'm not sure set theory would fix it |
| 02:01:09 | <monochrom> | You can do it in set theory. It is just not called "the natural numbers" there. |
| 02:01:26 | <EvanR> | ordinals? xD |
| 02:01:40 | <EvanR> | that comes with its own induction rule |
| 02:01:57 | <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. |
| 02:02:39 | <monochrom> | We also say "make a Xerox copy" and then go on to use a Konica photocopier. |
| 02:02:59 | <EvanR> | thirdofmayyaddayaddagoya: if you do classic induction to prove something, you proved it for all finite natural numbers, and that's it |
| 02:03:01 | <monochrom> | so I guess "infinite natural" and even "uncountable natural" can be legit names. |
| 02:03:31 | <EvanR> | it misses something |
| 02:05:08 | <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 |
| 02:05:34 | <EvanR> | it's illogical! |
| 02:06:54 | <monochrom> | It's even the same phenomenon. The termination proof assumes induction, so it only covers what induction reaches. |
| 02:07:01 | <haskellbridge> | <thirdofmay18081814goya> hm looks like coalgebras sort disassemble things |
| 02:07:09 | <haskellbridge> | <thirdofmay18081814goya> sort of disassemble things |
| 02:08:29 | <haskellbridge> | <thirdofmay18081814goya> hm so then in a sense the final coalgebra gives you a canonical way to disassemble a thing |
| 02:08:41 | <monochrom> | On recent exams I became careful to write "Prove by induction: For all finite lists xs, ..." :) |
| 02:12:37 | <EvanR> | is final coalgebra the categorical wonkery for coinductive types? |
| 02:12:40 | <monochrom> | Hagino says "co-natural number" instead of "infinite natural number". :) |
| 02:12:54 | <haskellbridge> | <thirdofmay18081814goya> EvanR: yes |
| 02:13:33 | × | td_ quits (~td@i5387091A.versanet.de) (Ping timeout: 246 seconds) |
| 02:13:58 | <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.) |
| 02:14:45 | <haskellbridge> | <thirdofmay18081814goya> monochrom: was planning to return to his thesis after foray into coinduction |
| 02:14:56 | <EvanR> | disassemble might give you the wrong idea |
| 02:15:11 | <haskellbridge> | <thirdofmay18081814goya> monochrom: by any chance do you know how Hagino's type formation through adjunction works? |
| 02:15:17 | <monochrom> | And if that is not enough, look for "Bart Jacobs coalgebra". He's the coalgebra guy. |
| 02:15:28 | <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 |
| 02:15:36 | <monochrom> | I don't, I didn't really read it. |
| 02:15:39 | → | td_ joins (~td@i5387092D.versanet.de) |
| 02:16:02 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 02:16:30 | <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 |
| 02:17:41 | <EvanR> | and in the case of infinite data, assembling from the ground up is impossible |
| 02:18:52 | <EvanR> | but maybe that's just prejudice leaking through from "a monad is this thing you wrap like a burrito" PTSD |
| 02:19:25 | <dolio> | To build codata, you say what happens for all the ways of observing it, corecursively. |
| 02:21:28 | <dolio> | Like unfoldr, but that only has one thing to observe. |
| 02:26:10 | <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. |
| 02:27:08 | <haskellbridge> | <thirdofmay18081814goya> ty for comments helpful stuff |
| 02:29:21 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 02:31:07 | × | identity quits (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.91)) |
| 02:36:59 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 02:39:49 | × | motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 248 seconds) |
| 02:52:19 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 260 seconds) |
| 02:52:51 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 02:59:04 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 03:01:04 | × | sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 03:09:12 | × | zlqrvx_ quits (~zlqrvx@101.175.150.247) (Ping timeout: 272 seconds) |
| 03:22:21 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 03:27:37 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 03:27:37 | × | ethantwardy quits (user@user/ethantwardy) (Read error: Connection reset by peer) |
| 03:29:52 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 03:31:20 | → | ethantwardy joins (user@user/ethantwardy) |
| 03:43:38 | × | floyza quits (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 03:43:57 | → | floyza joins (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) |
| 03:44:40 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 272 seconds) |
| 03:46:59 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 03:49:41 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 04:04:53 | → | infinity0 joins (~infinity0@pwned.gg) |
| 04:07:51 | × | talismanick quits (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 04:08:05 | → | talismanick joins (~user@2601:644:937c:ed10::ae5) |
| 04:15:45 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 04:19:30 | × | _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 265 seconds) |
| 04:24:28 | → | _d0t joins (~{-d0t-}@user/-d0t-/x-7915216) |
| 04:34:45 | <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 |
| 04:39:57 | × | simendsjo quits (~user@84.211.91.108) (Ping timeout: 276 seconds) |
| 04:45:50 | <jackdk> | Axman6: Is this about how finger trees use polymorphic recursion? |
| 04:45:56 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 04:55:47 | <mauke> | Axman6: non-regular? nested type? |
| 04:57:53 | → | michalz joins (~michalz@185.246.207.222) |
| 05:03:41 | astra | is now known as amish |
| 05:03:44 | × | amish quits (sid289983@id-289983.hampstead.irccloud.com) (Changing host) |
| 05:03:44 | → | amish joins (sid289983@user/amish) |
| 05:04:04 | amish | is now known as astra |
| 05:08:47 | → | st_aldini1 joins (~Thunderbi@136.48.22.91) |
| 05:09:05 | → | euphores joins (~SASL_euph@user/euphores) |
| 05:10:13 | × | st_aldini quits (~Thunderbi@136.48.22.91) (Ping timeout: 248 seconds) |
| 05:10:13 | st_aldini1 | is now known as st_aldini |
| 05:12:38 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:21:51 | × | dtman34 quits (~dtman34@2601:447:d080:1a3c:e9e9:5bc8:51:a5ea) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 05:22:12 | → | dtman34 joins (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) |
| 05:23:01 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 248 seconds) |
| 05:32:01 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 05:38:13 | <Axman6> | yeah I think both of those work |
| 05:53:12 | → | acidjnk joins (~acidjnk@p200300d6e72cfb34519e9ca14c5ce943.dip0.t-ipconnect.de) |
| 05:57:33 | → | ubert joins (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) |
| 06:04:00 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 06:08:25 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 06:08:38 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:09:11 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 06:09:33 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:10:24 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 06:10:57 | → | mari-estel joins (~mari-este@185.238.219.10) |
| 06:11:38 | → | mari77696 joins (~mari-este@185.238.219.10) |
| 06:14:05 | × | foul_owl quits (~kerry@185.219.141.162) (Ping timeout: 255 seconds) |
| 06:17:16 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:32:05 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 06:32:17 | × | mari77696 quits (~mari-este@185.238.219.10) (Ping timeout: 248 seconds) |
| 06:32:49 | × | mari-estel quits (~mari-este@185.238.219.10) (Ping timeout: 248 seconds) |
| 06:42:16 | → | rosco joins (~rosco@175.136.22.30) |
| 06:44:10 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:57:37 | → | foul_owl joins (~kerry@185.219.141.162) |
| 07:00:00 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:37 | → | caconym joins (~caconym@user/caconym) |
| 07:01:40 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:05:21 | <yin> | Axman6: regular |
| 07:13:21 | × | myxos quits (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 276 seconds) |
| 07:13:36 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:13:53 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 07:14:09 | → | gorignak joins (~gorignak@user/gorignak) |
| 07:16:47 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 07:24:55 | → | zlqrvx joins (~zlqrvx@user/zlqrvx) |
| 07:24:57 | → | alp_ joins (~alp@2001:861:e3d6:8f80:9869:a17b:401:f55) |
| 07:29:19 | <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 |
| 07:32:13 | → | mari68681 joins (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 07:32:13 | → | mari-estel joins (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 07:32:41 | → | briandaed joins (~root@185.234.210.211.r.toneticgroup.pl) |
| 07:37:30 | <tomsmeding> | yay normal channels :) |
| 07:38:28 | × | rosco quits (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 07:40:07 | <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 |
| 07:40:36 | <Athas> | tomsmeding: meaningless inconsistency. I suppose I can never decided whether eta-reduction would confuse my students. |
| 07:40:42 | <Athas> | Today I feel like it won't, so I will fix it. |
| 07:41:11 | <tomsmeding> | I can relate to that sentiment, even s/my students/myself/ |
| 07:42:46 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 244 seconds) |
| 07:43:03 | <tomsmeding> | only tangentially related: I often find myself writing code like this: https://github.com/tomsmeding/ad-dualrev-th/blob/17b758dbb3966de66394a756b708dae6ab57687e/src/Language/Haskell/ReverseAD/TH.hs#L901 (older example because this is the first I found in public code) |
| 07:43:34 | <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 |
| 07:43:45 | <tomsmeding> | because I want to reuse those same names in the 'where' block |
| 07:44:09 | <tomsmeding> | it feels awkward to write code this way; are there better ways? |
| 07:45:09 | × | mari68681 quits (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 252 seconds) |
| 07:45:09 | × | mari-estel quits (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 252 seconds) |
| 07:45:21 | × | floyza quits (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 07:45:56 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 07:47:02 | → | myxos joins (~myxos@syn-065-028-251-121.res.spectrum.com) |
| 07:53:29 | → | chele joins (~chele@user/chele) |
| 07:58:08 | → | sourcetarius joins (~sourcetar@user/sourcetarius) |
| 07:58:36 | <briandaed> | maybe making go function top-level (with more verbose name) and just not exporting it from module |
| 07:58:57 | <tomsmeding> | that is indeed an option |
| 07:59:01 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 07:59:29 | <briandaed> | ddrType just process result from 'meat' produced by 'go' |
| 07:59:57 | <briandaed> | but it's a matter of taste only |
| 08:00:16 | <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 |
| 08:00:25 | → | merijn joins (~merijn@77.242.116.146) |
| 08:00:36 | <Lears> | tomsmeding: `ddrType (go &&& show -> (ebr, showty)) = case ebr of ...` >:) |
| 08:00:54 | <tomsmeding> | Lears: I mean, sure, you can always make code more pointless :p |
| 08:01:37 | <tomsmeding> | I don't think that's any less awkward ;) |
| 08:02:05 | <Lears> | The lambda is fine, really; I do the same thing. |
| 08:02:36 | <Lears> | Or give the top-level (usually single-use) variable a 0 suffix. |
| 08:02:39 | <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 |
| 08:02:44 | <tomsmeding> | right |
| 08:02:53 | × | myxos quits (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 245 seconds) |
| 08:03:43 | raym_ | is now known as raym |
| 08:07:25 | <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 |
| 08:07:27 | <tomsmeding> | the open, and they want to prevent that by construction (instead of instructing those teachers to do a better job) |
| 08:08:15 | <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 |
| 08:10:46 | → | kuribas joins (~user@2a02:1808:7:f56b:d4a9:b96f:9d61:d1a7) |
| 08:12:08 | → | cfricke joins (~cfricke@user/cfricke) |
| 08:20:53 | → | myxos joins (~myxos@syn-065-028-251-121.res.spectrum.com) |
| 08:22:46 | → | CiaoSen joins (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) |
| 08:24:12 | × | raym quits (~ray@user/raym) (Ping timeout: 252 seconds) |
| 08:25:52 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:30:26 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 08:33:15 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 08:33:29 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Client Quit) |
| 08:33:38 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 08:37:13 | → | euphores joins (~SASL_euph@user/euphores) |
| 08:40:24 | × | myxos quits (~myxos@syn-065-028-251-121.res.spectrum.com) (Remote host closed the connection) |
| 08:40:59 | → | raym joins (~ray@user/raym) |
| 08:41:07 | → | myxos joins (~myxos@syn-065-028-251-121.res.spectrum.com) |
| 08:42:54 | → | kuribas` joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 08:44:33 | × | kuribas quits (~user@2a02:1808:7:f56b:d4a9:b96f:9d61:d1a7) (Ping timeout: 248 seconds) |
| 08:52:35 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 08:54:10 | × | synchromesh quits (~john@2406:5a00:241a:5600:1537:bb1c:ebe9:2fdf) (Read error: Connection reset by peer) |
| 08:54:33 | → | merijn joins (~merijn@77.242.116.146) |
| 08:55:10 | → | synchromesh joins (~john@2406:5a00:241a:5600:dc23:4239:fb04:33f4) |
| 08:55:18 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 09:01:04 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 09:03:34 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 09:04:04 | × | gorignak quits (~gorignak@user/gorignak) (Ping timeout: 252 seconds) |
| 09:04:30 | → | gorignak joins (~gorignak@user/gorignak) |
| 09:10:26 | × | fmira quits (~user@user/fmira) (Quit: fmira) |
| 09:17:25 | → | rosco joins (~rosco@175.136.22.30) |
| 09:17:59 | → | supercode joins (~supercode@user/supercode) |
| 09:22:26 | × | arahael quits (~arahael@user/arahael) (Remote host closed the connection) |
| 09:22:29 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 09:27:40 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 09:30:47 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 09:31:00 | → | merijn joins (~merijn@77.242.116.146) |
| 09:32:17 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 09:36:42 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 09:36:55 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 09:37:37 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 09:42:04 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 09:44:31 | → | merijn joins (~merijn@77.242.116.146) |
| 09:48:47 | → | Guest41 joins (~Guest41@ip-38-9-3-83.internet.url.net.au) |
| 09:49:13 | × | Guest41 quits (~Guest41@ip-38-9-3-83.internet.url.net.au) (Client Quit) |
| 09:52:45 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:55:01 | × | alp_ quits (~alp@2001:861:e3d6:8f80:9869:a17b:401:f55) (Ping timeout: 252 seconds) |
| 10:08:58 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 10:15:29 | → | andrewboltachev joins (~andrey@178.141.244.27) |
| 10:18:34 | → | aforemny joins (~aforemny@2001:9e8:6cd9:9400:c5f2:6987:2beb:3640) |
| 10:19:09 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 10:19:22 | → | euleritian joins (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) |
| 10:21:07 | → | __monty__ joins (~toonn@user/toonn) |
| 10:28:44 | × | CiaoSen quits (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 10:31:21 | × | supercode quits (~supercode@user/supercode) (Killed (NickServ (GHOST command used by supercode63))) |
| 10:31:23 | × | euleritian quits (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:31:40 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 10:35:26 | → | comerijn joins (~merijn@77.242.116.146) |
| 10:38:26 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 10:39:21 | → | alp_ joins (~alp@2001:861:e3d6:8f80:446d:e3f8:e9a4:2f3b) |
| 10:40:59 | → | mari-estel joins (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 10:42:42 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 10:42:58 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 10:47:44 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 10:48:49 | → | euleritian joins (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) |
| 10:51:31 | × | euleritian quits (~euleritia@dynamic-176-006-134-097.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:51:48 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 10:58:31 | × | rosco quits (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 11:00:05 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 11:02:34 | → | caconym joins (~caconym@user/caconym) |
| 11:05:28 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:10:26 | → | xff0x joins (~xff0x@2405:6580:b080:900:da07:5be8:5f56:f410) |
| 11:12:14 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 11:14:58 | × | mari-estel quits (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 272 seconds) |
| 11:17:56 | → | mari-estel joins (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 11:19:46 | → | merijn joins (~merijn@77.242.116.146) |
| 11:21:39 | × | mari-estel quits (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Client Quit) |
| 11:25:17 | → | srazkvt joins (~sarah@user/srazkvt) |
| 11:33:37 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 11:39:01 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 11:40:49 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:50:23 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 11:52:48 | → | rosco joins (~rosco@175.136.22.30) |
| 11:53:15 | → | merijn joins (~merijn@77.242.116.146) |
| 11:55:26 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 11:55:55 | → | rvalue joins (~rvalue@user/rvalue) |
| 12:01:58 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 12:04:04 | <haskellbridge> | <thirdofmay18081814goya> what's a mental picture to use when structuring a program through algebraic effects and handlers? |
| 12:06:41 | <probie> | <bad joke>A burrito</bad joke> |
| 12:07:40 | <Rembane> | I'm usually thinking about it as building a very small EDSL |
| 12:08:41 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 255 seconds) |
| 12:08:41 | <haskellbridge> | <thirdofmay18081814goya> Rembane: hm I see, each effect/handler pair a fragment? |
| 12:09:36 | <Rembane> | Are you using a particular library? Something to make this more concrete. |
| 12:13:54 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 12:13:58 | <haskellbridge> | <thirdofmay18081814goya> hm no particular library atm, maybe it would make more sense to use one |
| 12:15:08 | <Rembane> | Or create a datatype for effects and then create an interpreter for it |
| 12:15:43 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 264 seconds) |
| 12:22:41 | → | merijn joins (~merijn@77.242.116.146) |
| 12:30:03 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds) |
| 12:30:23 | → | ash3en joins (~Thunderbi@193.32.248.167) |
| 12:34:17 | → | CiaoSen joins (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) |
| 12:38:11 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 12:40:17 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 12:41:08 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 12:41:34 | → | identity joins (~identity@user/ZharMeny) |
| 12:45:52 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 12:51:33 | × | AlexZenon quits (~alzenon@178.34.151.120) (Quit: ;-) |
| 12:52:01 | × | AlexNoo quits (~AlexNoo@178.34.151.120) (Quit: Leaving) |
| 12:52:13 | → | Pixi` joins (~Pixi@user/pixi) |
| 12:55:13 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 248 seconds) |
| 13:01:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:02:45 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 13:04:13 | × | ash3en quits (~Thunderbi@193.32.248.167) (Quit: ash3en) |
| 13:04:47 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 13:07:42 | × | Angelz quits (Angelz@user/angelz) (Ping timeout: 272 seconds) |
| 13:08:18 | × | zfnmxt quits (~zfnmxt@107.189.30.63) (Ping timeout: 245 seconds) |
| 13:12:19 | → | mari-estel joins (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) |
| 13:21:38 | → | alexherbo2 joins (~alexherbo@2a02-8440-3202-2f93-5c9a-6ec5-11de-f4fb.rev.sfr.net) |
| 13:27:34 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 13:28:22 | → | AlexNoo joins (~AlexNoo@178.34.151.120) |
| 13:30:33 | → | AlexZenon joins (~alzenon@178.34.151.120) |
| 13:31:06 | → | weary-traveler joins (~user@user/user363627) |
| 13:54:17 | → | ash3en joins (~Thunderbi@193.32.248.167) |
| 14:00:49 | × | alp_ quits (~alp@2001:861:e3d6:8f80:446d:e3f8:e9a4:2f3b) (Ping timeout: 260 seconds) |
| 14:01:29 | × | mari-estel quits (~mari-este@2a02:3032:307:1a8e:216:3eff:fe65:4eef) (Ping timeout: 244 seconds) |
| 14:02:14 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 14:02:34 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 14:04:09 | × | ash3en quits (~Thunderbi@193.32.248.167) (Ping timeout: 276 seconds) |
| 14:06:31 | → | ash3en joins (~Thunderbi@193.32.248.167) |
| 14:09:53 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 14:09:59 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 14:10:07 | → | euleritian joins (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) |
| 14:10:30 | × | euleritian quits (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 14:10:47 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 14:11:31 | × | ash3en quits (~Thunderbi@193.32.248.167) (Ping timeout: 264 seconds) |
| 14:13:15 | × | synchromesh quits (~john@2406:5a00:241a:5600:dc23:4239:fb04:33f4) (Ping timeout: 276 seconds) |
| 14:14:22 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 14:14:49 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 14:15:56 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 14:16:27 | → | gorignak joins (~gorignak@user/gorignak) |
| 14:19:35 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 14:23:24 | → | biberao joins (~m@user/biberao) |
| 14:23:26 | <biberao> | hi |
| 14:27:45 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 14:35:46 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 14:35:53 | → | ash3en joins (~Thunderbi@193.32.248.167) |
| 14:36:10 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 14:43:35 | → | synchromesh joins (~john@180.148.124.74) |
| 14:46:31 | × | ash3en quits (~Thunderbi@193.32.248.167) (Ping timeout: 252 seconds) |
| 14:49:02 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 14:53:46 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 14:55:41 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 15:00:09 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 15:04:46 | → | alp_ joins (~alp@2001:861:e3d6:8f80:1e84:aaa4:b350:85e4) |
| 15:07:35 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 15:08:05 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 15:08:19 | × | CiaoSen quits (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 15:10:51 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 15:11:11 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 15:16:33 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 15:16:58 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 15:18:27 | → | jinsun joins (~jinsun@user/jinsun) |
| 15:20:36 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 15:21:11 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 15:25:26 | × | alexherbo2 quits (~alexherbo@2a02-8440-3202-2f93-5c9a-6ec5-11de-f4fb.rev.sfr.net) (Remote host closed the connection) |
| 15:31:44 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 15:31:51 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 15:32:00 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 15:32:15 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 15:35:31 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 15:38:00 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 15:44:17 | × | rosco quits (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 15:45:35 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 15:48:05 | × | alp_ quits (~alp@2001:861:e3d6:8f80:1e84:aaa4:b350:85e4) (Ping timeout: 248 seconds) |
| 15:50:16 | × | califax quits (~califax@user/califx) (Ping timeout: 260 seconds) |
| 15:50:26 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 15:50:54 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 15:51:36 | → | califax joins (~califax@user/califx) |
| 15:52:29 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 15:53:12 | → | Digitteknohippie joins (~user@user/digit) |
| 15:53:41 | × | Digit quits (~user@user/digit) (Ping timeout: 255 seconds) |
| 15:55:32 | <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. |
| 15:57:01 | <haskellbridge> | <thirdofmay18081814goya> hm i see |
| 15:57:44 | → | spew joins (~spew@201.141.99.170) |
| 15:57:53 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 15:58:11 | → | califax joins (~califax@user/califx) |
| 16:00:30 | × | berberman quits (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:00:57 | → | berberman joins (~berberman@user/berberman) |
| 16:04:19 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 16:04:56 | → | euleritian joins (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) |
| 16:08:21 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:09:09 | × | berberman quits (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:10:11 | → | berberman joins (~berberman@user/berberman) |
| 16:12:41 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 16:13:02 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 16:13:09 | × | petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:13:23 | → | petrichor joins (~znc-user@user/petrichor) |
| 16:13:26 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 16:17:22 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 244 seconds) |
| 16:18:33 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 16:18:41 | × | kuribas` quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 16:19:03 | Digitteknohippie | is now known as Digit |
| 16:25:00 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:30:18 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 16:31:44 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 16:34:22 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 16:34:28 | → | rvalue- joins (~rvalue@user/rvalue) |
| 16:35:11 | → | pavonia joins (~user@user/siracusa) |
| 16:35:29 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 16:35:30 | Pixi` | is now known as Pixi |
| 16:37:00 | × | euleritian quits (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:37:17 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:40:22 | rvalue- | is now known as rvalue |
| 16:42:04 | → | alp_ joins (~alp@2001:861:e3d6:8f80:cf3a:e88a:f2c8:6274) |
| 16:42:59 | <haskellbridge> | <thirdofmay18081814goya> i just need a free monad to model algebraic effect rights? |
| 16:44:39 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 16:44:54 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 16:49:41 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:49:49 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 16:51:32 | × | EvanR quits (~EvanR@user/evanr) (Quit: Leaving) |
| 16:53:12 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 16:53:27 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 16:53:37 | → | euleritian joins (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) |
| 16:56:14 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 16:57:23 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Quit: Lost terminal) |
| 17:07:30 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 17:08:00 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:09:10 | → | CiaoSen joins (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) |
| 17:10:16 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 17:11:11 | × | euleritian quits (~euleritia@dynamic-176-006-129-122.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:11:29 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:12:11 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:17:14 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 17:23:06 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 17:23:06 | × | andrewboltachev quits (~andrey@178.141.244.27) (Quit: Leaving.) |
| 17:23:59 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 17:24:49 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Ping timeout: 260 seconds) |
| 17:27:29 | <haskellbridge> | <thirdofmay18081814goya> hm yeah only if the effect actually is algebraic |
| 17:27:59 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:29:56 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 17:30:43 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 265 seconds) |
| 17:31:17 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:31:59 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 17:33:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 17:35:20 | → | ss4 joins (~wootehfoo@user/wootehfoot) |
| 17:37:29 | → | causal joins (~eric@50.35.88.207) |
| 17:38:05 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 17:38:13 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:39:09 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Ping timeout: 252 seconds) |
| 17:43:26 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:43:46 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:48:37 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 17:48:45 | × | kaskal quits (~kaskal@2001:4bb8:2af:db4a:8acd:a0ac:f117:1e24) (Quit: ZNC - https://znc.in) |
| 17:49:07 | → | kaskal joins (~kaskal@2001:4bb8:2af:db4a:8213:de4d:dd34:38f3) |
| 17:52:57 | × | ss4 quits (~wootehfoo@user/wootehfoot) (Ping timeout: 246 seconds) |
| 17:55:37 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 17:55:40 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 17:56:11 | → | gorignak joins (~gorignak@user/gorignak) |
| 17:59:27 | <haskellbridge> | <thirdofmay18081814goya> nvm i don't know what i'm talking about |
| 17:59:33 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:01:07 | → | Batzy_ joins (~quassel@user/batzy) |
| 18:03:17 | × | Batzy quits (~quassel@user/batzy) (Ping timeout: 255 seconds) |
| 18:04:33 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 18:05:00 | × | ubert quits (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 18:08:13 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 18:10:40 | → | mrtz joins (~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) |
| 18:11:14 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:11:47 | → | samanklesaria joins (~samankles@68-168-167-245.fttp.usinternet.com) |
| 18:14:16 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 18:16:13 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 18:17:17 | × | briandaed quits (~root@185.234.210.211.r.toneticgroup.pl) (Remote host closed the connection) |
| 18:17:45 | → | lol_ joins (~lol@2603:3016:1e01:b9e0:835:2698:e6f:bd82) |
| 18:19:19 | × | samanklesaria quits (~samankles@68-168-167-245.fttp.usinternet.com) (Remote host closed the connection) |
| 18:20:24 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 18:20:51 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds) |
| 18:21:34 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b9e0:9c4e:1030:31bf:f76b) (Ping timeout: 260 seconds) |
| 18:24:22 | × | mrtz quits (~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) (Ping timeout: 265 seconds) |
| 18:27:01 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:35:24 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 18:38:57 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:43:55 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 18:50:38 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 18:54:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:56:25 | × | Pixi quits (~Pixi@user/pixi) (Quit: Leaving) |
| 18:59:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 19:00:01 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:37 | → | caconym joins (~caconym@user/caconym) |
| 19:01:51 | × | CiaoSen quits (~Jura@2a05:5800:225:700:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 19:07:43 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 19:08:14 | → | gorignak joins (~gorignak@user/gorignak) |
| 19:15:33 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:17:34 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 19:17:55 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 19:18:32 | <tomsmeding> | goya: You don't _need_ a free monad to model algebraic effects; free monads _can be used_ to model algebraic effects |
| 19:18:49 | <tomsmeding> | and they are traditional vehicle in haskell, but not all effects libraries use them |
| 19:19:18 | <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 |
| 19:20:04 | <tomsmeding> | https://hackage.haskell.org/package/effectful-core-2.3.1.0/docs/src/Effectful.Internal.Monad.html#Eff |
| 19:20:06 | <tomsmeding> | for example |
| 19:20:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 19:20:40 | → | Pixi joins (~Pixi@user/pixi) |
| 19:21:42 | <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 |
| 19:21:56 | <tomsmeding> | there's also 'eff' based on delimited continuations |
| 19:24:50 | <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. |
| 19:25:03 | <dolio> | E.G. they cannot do state. |
| 19:25:46 | tomsmeding | has difficulty parsing that |
| 19:26:16 | <dolio> | They can do get/put |
| 19:26:39 | <dolio> | And it's up to the handler whether that satisfies the expected equations for state or not. |
| 19:26:59 | <tomsmeding> | I would not call that "giving rise to free monads" |
| 19:27:06 | <tomsmeding> | sure, free monads are one way to implement that semantics |
| 19:27:29 | <tomsmeding> | as in: you don't need to actually reify the computation as a data type |
| 19:27:33 | <tomsmeding> | which is what "free monad" means to me |
| 19:27:51 | <haskellbridge> | <thirdofmay18081814goya> aren't free monads their canonical abstract implementation-independent representation |
| 19:27:59 | <tomsmeding> | perhaps |
| 19:28:07 | <tomsmeding> | but "need" is too strong, I think |
| 19:28:25 | <haskellbridge> | <thirdofmay18081814goya> hm right |
| 19:28:59 | <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 |
| 19:29:12 | <tomsmeding> | and there are actually other data types, such as Bag, that are better in certain circumstances |
| 19:30:15 | <Franciman> | dolio: can you also define equations in those effect systems? |
| 19:30:15 | <tomsmeding> | (data Bag a = Empty | Single a | Many (Bag a) (Bag a)) |
| 19:30:29 | <dolio> | Franciman: No. That's why they're free. |
| 19:30:46 | <Franciman> | can't you do the presentation of a struct? |
| 19:31:00 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:31:39 | → | supercode joins (~supercode@user/supercode) |
| 19:32:05 | <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. |
| 19:32:07 | <Franciman> | of a set of equation* |
| 19:32:23 | <Franciman> | t looks interesting |
| 19:33:18 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 19:33:39 | → | mantraofpie joins (~mantraofp@user/mantraofpie) |
| 19:34:08 | <dolio> | Anyhow, 'free' doesn't mean data type. That's something from the category end that hasn't really trickled into Haskell so much. |
| 19:34:38 | <tomsmeding> | I see |
| 19:34:38 | <Franciman> | free is not about categories |
| 19:34:44 | <Franciman> | it has a wider meaning |
| 19:34:58 | <tomsmeding> | s/category end/category theory end/ |
| 19:35:39 | <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. |
| 19:35:52 | <tomsmeding> | right, that makes sense |
| 19:35:58 | <tomsmeding> | (with my limited CT knowledge) |
| 19:36:11 | <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. |
| 19:36:15 | <tomsmeding> | okay in that case, "free monad" is indeed appropriate, I guess |
| 19:36:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 19:38:12 | <haskellbridge> | <thirdofmay18081814goya> Franciman: warning free adjunct |
| 19:38:19 | <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. |
| 19:39:11 | <haskellbridge> | <thirdofmay18081814goya> x is not about categories is in general inaccurate |
| 19:39:16 | → | ubert joins (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) |
| 19:40:12 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 19:40:58 | × | causal quits (~eric@50.35.88.207) (Ping timeout: 252 seconds) |
| 19:41:22 | → | causal joins (~eric@50.35.88.207) |
| 19:48:00 | × | TimWolla quits (~timwolla@2a01:4f8:150:6153:beef::6667) (Quit: Bye) |
| 19:48:19 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:49:03 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 19:53:21 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 19:53:27 | → | zfnmxt joins (~zfnmxt@user/zfnmxt) |
| 19:55:29 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 19:57:12 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 19:58:46 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 19:59:27 | → | TimWolla joins (~timwolla@2a01:4f8:150:6153:beef::6667) |
| 20:00:24 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 20:04:05 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:05:13 | → | alexherbo2 joins (~alexherbo@2a02-8440-3215-f56e-1190-0b59-796f-612e.rev.sfr.net) |
| 20:05:44 | × | sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 20:08:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:09:30 | <sam113101> | does haskell have something like the pipe operator (|>) in elixir? |
| 20:10:04 | <tomsmeding> | :t (&) |
| 20:10:05 | <lambdabot> | a -> (a -> b) -> b |
| 20:10:10 | <tomsmeding> | :t ($) |
| 20:10:10 | <lambdabot> | (a -> b) -> a -> b |
| 20:10:27 | <tomsmeding> | > map toUpper "hello" |
| 20:10:28 | <lambdabot> | "HELLO" |
| 20:10:34 | <tomsmeding> | > hello & map toUpper |
| 20:10:36 | <lambdabot> | error: Variable not in scope: hello :: [Char] |
| 20:10:39 | <tomsmeding> | > "hello" & map toUpper |
| 20:10:40 | <lambdabot> | "HELLO" |
| 20:10:50 | <tomsmeding> | sam113101: is that what you're looking for? (&) is in Data.Function |
| 20:11:10 | <sam113101> | I think yes |
| 20:11:24 | <sam113101> | what's $ |
| 20:11:33 | <tomsmeding> | normal function application :) |
| 20:11:38 | <tomsmeding> | > map toUpper $ "hello" |
| 20:11:39 | <lambdabot> | "HELLO" |
| 20:11:50 | → | Angelz joins (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) |
| 20:12:04 | <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 |
| 20:12:16 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:12:22 | <tomsmeding> | there are various ways to do that: |
| 20:12:40 | <tomsmeding> | > map toUpper (reverse (show (Just 42))) |
| 20:12:42 | <lambdabot> | "24 TSUJ" |
| 20:12:49 | <tomsmeding> | > map toUpper $ reverse $ show $ Just 42 |
| 20:12:50 | <lambdabot> | "24 TSUJ" |
| 20:12:56 | <tomsmeding> | > map toUpper . reverse . show $ Just 42 |
| 20:12:57 | <lambdabot> | "24 TSUJ" |
| 20:13:09 | <tomsmeding> | the first version you should be able to read: that's just applying functions as usual |
| 20:13:38 | <sam113101> | yeah |
| 20:13:41 | <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 |
| 20:14:11 | <tomsmeding> | in the third version, I'm using (.) to _compose_ three functions, then applying the whole composition at once to the argument (Just 42) |
| 20:14:16 | <tomsmeding> | :t (.) |
| 20:14:17 | <lambdabot> | (b -> c) -> (a -> b) -> a -> c |
| 20:15:24 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 20:17:28 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 20:21:29 | <monochrom> | IIRC the definition of algebraic effect includes a monad, it's a prerequisite. The monad is as free as the algebra. |
| 20:22:16 | <tomsmeding> | (disclaimer about weak CT-fu) can (algebraic) effects not be described merely as operations and equations, without reference to any monad? |
| 20:22:17 | <monochrom> | (Also I hate English. Officially, "prerequisite" is uncountable and my "a prerequisite" is illegal.) |
| 20:22:30 | <tomsmeding> | wait wat |
| 20:23:10 | <tomsmeding> | wiktionary does not agree https://en.wiktionary.org/wiki/prerequisite#Noun |
| 20:23:11 | <monochrom> | Yeah officially one has to say "a prerequisite requirement" so "a" belongs to "requirement" which is allowed to be countable. :) |
| 20:23:20 | <tomsmeding> | (phew) |
| 20:23:33 | <tomsmeding> | the adjectival use is also described |
| 20:23:41 | <sam113101> | https://paste.centos.org/view/raw/bf9a82a0 |
| 20:23:43 | <tomsmeding> | but I don't see any uncountable definition |
| 20:23:45 | <dolio> | I bet the dictionaries are just lagging on that. |
| 20:23:58 | <sam113101> | I like how the information flows from left to right, sometimes that's clearer |
| 20:24:09 | <sam113101> | monochrom: what's a monad? |
| 20:24:19 | <monochrom> | In this case I think "the language keeps changing" applies. It was uncountable by the standard of old-school people. |
| 20:24:32 | <monochrom> | To be sure, I would be the first to welcome this change! |
| 20:24:41 | <dolio> | Algebraic effects are (slightly generalized) Lawvere theories. |
| 20:24:42 | <TMA> | isn't "a prerequisite requirement" a superfluous pleonasm? |
| 20:24:56 | <monochrom> | It's about time every English noun is made countable. I used to have a lot of hairs. There! |
| 20:25:17 | <tomsmeding> | "hair" is a countable noun _and_ an uncountable noun ;) |
| 20:25:23 | <tomsmeding> | I can definitely have three hairs in my hand |
| 20:25:30 | <monochrom> | Also, s/is made/was made/ . (I hate English. Let's get rid of tenses too.) |
| 20:26:15 | <sam113101> | nah I think "is" is the right one |
| 20:26:16 | <monochrom> | Generalized Wadler's Rule: English syntax is more discussed than Haskell semantics. >:) |
| 20:26:23 | <sam113101> | not an English expert though |
| 20:26:30 | <dolio> | But, the actual theories you can present in most programming scenarios do not have any equations. |
| 20:27:04 | <tomsmeding> | dolio: I have no clue what a Lawvere theory is :) |
| 20:27:33 | <dolio> | It's the categorical version of 'operations and equations' sorts of algebraic theories. |
| 20:27:40 | <dolio> | Finitary ones. |
| 20:27:40 | <tomsmeding> | I see |
| 20:27:41 | <TMA> | I vote for "It's about time every English noun be made countable." |
| 20:27:48 | <tomsmeding> | TMA++ |
| 20:28:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:28:07 | <tomsmeding> | subjunctive is underused |
| 20:28:09 | <TMA> | we have the subjunctive so use it! |
| 20:28:14 | <dolio> | The papers on algebraic effects usually make them of countable arity rather than just finite. |
| 20:31:18 | <sam113101> | I remembering tyring to learn haskell |
| 20:32:29 | <monochrom> | sam113101: Consider [0..1000] & (filter (\x -> ...) >>> sum). >>> is from Control.Category, it looks general, but this one specializes to flip (.) |
| 20:32:36 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 20:32:58 | <tomsmeding> | also: [0..1000] & filter (\x -> ...) & sum |
| 20:34:19 | <monochrom> | I teach a Unix course so I prioritize "< input {filter | sum}". :) |
| 20:34:36 | → | moe_ joins (~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) |
| 20:34:37 | <tomsmeding> | what language is that lol |
| 20:34:52 | <monochrom> | plain bourne shell! |
| 20:35:06 | <monochrom> | And yes "<file cmd" is the same as "cmd <file" |
| 20:35:09 | <tomsmeding> | oh hah |
| 20:35:11 | <tomsmeding> | it is |
| 20:35:22 | <geekosaur> | yep, redirections can go anywhere in a command |
| 20:35:27 | <tomsmeding> | I knew that |
| 20:35:29 | <monochrom> | I actually read the bloody POSIX/OpenGroup docs to learn the detailed grammar! |
| 20:36:13 | <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 |
| 20:37:11 | <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. |
| 20:37:12 | <geekosaur> | I learned it from the old Bourne shell manual, although back then you needed extra semicolons (`{; filter | sum; }`) |
| 20:37:38 | <monochrom> | Oops I forgot the semicolon. |
| 20:37:51 | <tomsmeding> | ah right |
| 20:38:08 | <monochrom> | #1 source of mysterious syntax error messages |
| 20:38:18 | <tomsmeding> | if you insist on putting the redirection first, I would prefer "<input filter | sum" :p |
| 20:38:24 | <tomsmeding> | the {} being unnecessary |
| 20:41:27 | <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. |
| 20:41:46 | <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. >:) |
| 20:42:54 | <tomsmeding> | Lears: I'll have to pick the brain of the person who explained effects to me again :p |
| 20:43:49 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:44:00 | <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. |
| 20:44:45 | <tomsmeding> | Lears: but thanks for the concise and understandable (to my haskell brain) definition! |
| 20:45:10 | <tomsmeding> | (talking about English: "upplay" is a nice coinage) |
| 20:46:08 | <monochrom> | Did you know: When teaching computability, I pioneered renaming "not recognizable" to "unrecognizable". >:) |
| 20:46:14 | <dolio> | You probably replace the monad with 'models'. |
| 20:48:48 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:48:49 | × | zfnmxt quits (~zfnmxt@user/zfnmxt) (Ping timeout: 248 seconds) |
| 20:50:03 | × | Angelz quits (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Ping timeout: 246 seconds) |
| 20:53:18 | × | moe_ quits (~moe@lewi-19-b2-v4wan-169604-cust1264.vm4.cable.virginm.net) (Ping timeout: 252 seconds) |
| 20:54:23 | → | zfnmxt joins (~zfnmxt@user/zfnmxt) |
| 20:57:13 | <biberao> | monochrom: so you're a professor? |
| 20:59:35 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:01:13 | × | alexherbo2 quits (~alexherbo@2a02-8440-3215-f56e-1190-0b59-796f-612e.rev.sfr.net) (Ping timeout: 256 seconds) |
| 21:01:14 | × | ubert quits (~Thunderbi@178.165.187.120.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 21:03:10 | <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? |
| 21:05:14 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 21:06:09 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:08:59 | × | michalz quits (~michalz@185.246.207.222) (Remote host closed the connection) |
| 21:09:46 | → | weary-traveler joins (~user@user/user363627) |
| 21:10:35 | <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. |
| 21:11:13 | <haskellbridge> | <thirdofmay18081814goya> dolio: models for algebraic theories are given by monads |
| 21:13:04 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 21:15:22 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:15:26 | <dolio> | They don't have to be. |
| 21:17:12 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 21:17:38 | <haskellbridge> | <thirdofmay18081814goya> ah right, strict statement is: the free models of an algebraic theory form a monad |
| 21:19:56 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 21:20:08 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 21:24:22 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 21:25:04 | × | biberao quits (~m@user/biberao) (Quit: WeeChat 3.8) |
| 21:25:17 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 21:25:49 | → | biberu joins (~biberu@user/biberu) |
| 21:31:10 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:33:29 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 260 seconds) |
| 21:33:54 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 21:35:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 21:40:29 | × | alp_ quits (~alp@2001:861:e3d6:8f80:cf3a:e88a:f2c8:6274) (Ping timeout: 252 seconds) |
| 21:42:48 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:46:56 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:51:46 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 22:02:44 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:04:16 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 22:06:12 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:07:38 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 22:11:27 | → | arahael joins (~arahael@user/arahael) |
| 22:11:57 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:12:31 | → | Angelz joins (Angelz@Angelz.oddprotocol.org) |
| 22:12:51 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:18:31 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:23:31 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 22:23:41 | × | lbseale quits (~quassel@user/ep1ctetus) (Ping timeout: 244 seconds) |
| 22:29:15 | × | acidjnk quits (~acidjnk@p200300d6e72cfb34519e9ca14c5ce943.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 22:29:56 | × | mantraofpie quits (~mantraofp@user/mantraofpie) (Quit: Leaving) |
| 22:30:37 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 22:33:28 | → | thelounge6036 joins (~thelounge@ip4d14fa4d.dynamic.kabel-deutschland.de) |
| 22:34:18 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:39:11 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 22:41:26 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 22:46:05 | × | thelounge6036 quits (~thelounge@ip4d14fa4d.dynamic.kabel-deutschland.de) (Quit: The Lounge - https://thelounge.chat) |
| 22:50:05 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:54:51 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:05:52 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 23:05:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:10:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 23:19:48 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 23:20:22 | → | rvalue joins (~rvalue@user/rvalue) |
| 23:21:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:26:28 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:28:59 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 23:31:05 | → | weary-traveler joins (~user@user/user363627) |
| 23:31:39 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 23:37:27 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:42:56 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 23:47:36 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 23:52:52 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 23:53:14 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:54:37 | → | hgolden_ joins (~hgolden@146.70.174.37) |
| 23:57:09 | × | hgolden__ quits (~hgolden@23.162.40.28) (Ping timeout: 248 seconds) |
| 23:58:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
All times are in UTC on 2024-10-08.