Home liberachat/#haskell: Logs Calendar

Logs on 2025-04-27 (liberachat/#haskell)

00:04:33 × jespada_ quits (~jespada@r179-25-121-156.dialup.adsl.anteldata.net.uy) (Ping timeout: 244 seconds)
00:26:51 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
00:27:12 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
00:35:16 × pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 276 seconds)
00:39:09 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
00:39:10 × acidjnk_new quits (~acidjnk@p200300d6e71c4f09ad59765f396bb04f.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
00:41:34 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
00:42:25 × otto_s quits (~user@p5b044fbe.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
00:43:31 × mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Remote host closed the connection)
00:43:56 → otto_s joins (~user@p5de2f428.dip0.t-ipconnect.de)
00:47:40 → pabs3 joins (~pabs3@user/pabs3)
00:56:09 → mhatta joins (~mhatta@www21123ui.sakura.ne.jp)
01:02:42 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
01:14:33 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:17:16 → Feuermagier joins (~Feuermagi@user/feuermagier)
01:20:46 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
01:35:03 × notdabs quits (~Owner@2600:1700:69cf:9000:6cf1:9b1a:eb92:4847) (Read error: Connection reset by peer)
01:35:36 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
01:37:02 × Square2 quits (~Square@user/square) (Ping timeout: 272 seconds)
01:38:46 → j1n37 joins (~j1n37@user/j1n37)
01:42:49 → j1n37- joins (~j1n37@user/j1n37)
01:43:46 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
01:55:19 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
01:55:39 × __jmcantrell__ quits (~weechat@user/jmcantrell) (Ping timeout: 260 seconds)
02:04:16 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
02:04:43 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
02:05:05 × op_4 quits (~tslil@user/op-4/x-9116473) (Remote host closed the connection)
02:05:36 → op_4 joins (~tslil@user/op-4/x-9116473)
02:06:05 → __jmcantrell__ joins (~weechat@user/jmcantrell)
02:15:37 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
02:18:34 × j1n37- quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
02:18:59 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
02:19:47 × ddb quits (ddb@tilde.club) (Quit: WeeChat 4.5.2)
02:19:47 × anderson quits (anderson@user/anderson) (Quit: WeeChat 4.5.1)
02:22:31 × td_ quits (~td@i5387090C.versanet.de) (Ping timeout: 276 seconds)
02:23:16 → j1n37 joins (~j1n37@user/j1n37)
02:23:32 → td_ joins (~td@i5387092A.versanet.de)
02:25:45 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
02:28:49 → j1n37 joins (~j1n37@user/j1n37)
02:30:08 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:35:15 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
02:39:24 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
02:41:02 → infinity0 joins (~infinity0@pwned.gg)
02:45:40 × infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 252 seconds)
02:50:06 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:58:55 × xff0x quits (~xff0x@2405:6580:b080:900:a16e:31f3:ac48:6e3d) (Ping timeout: 276 seconds)
03:01:32 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
03:01:47 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
03:01:55 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
03:05:05 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
03:05:12 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
03:05:59 → j1n37 joins (~j1n37@user/j1n37)
03:12:25 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
03:13:27 × ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
03:14:27 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
03:17:05 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds)
03:17:13 → j1n37 joins (~j1n37@user/j1n37)
03:19:13 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
03:22:22 → j1n37 joins (~j1n37@user/j1n37)
03:24:15 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
03:26:13 × Typedfern quits (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 276 seconds)
03:31:12 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
03:31:45 → rvalue joins (~rvalue@user/rvalue)
03:44:40 → Typedfern joins (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net)
03:46:24 → j1n37 joins (~j1n37@user/j1n37)
03:53:56 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
03:57:28 todi1 is now known as todi
03:58:49 → fp joins (~Thunderbi@hof1.kyla.fi)
04:06:01 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:10:04 × Typedfern quits (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 252 seconds)
04:20:00 → j1n37- joins (~j1n37@user/j1n37)
04:20:01 × down200 quits (~down200@shell.lug.mtu.edu) (Quit: ZNC - https://znc.in)
04:21:17 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 265 seconds)
04:29:03 → Typedfern joins (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net)
04:32:32 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
04:34:30 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
04:35:52 → euleritian joins (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de)
04:41:41 × euleritian quits (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
04:42:09 → euleritian joins (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de)
04:42:28 × euleritian quits (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
04:42:46 → euleritian joins (~euleritia@77.23.248.47)
05:01:08 → LainIwakura joins (~LainIwaku@user/LainIwakura)
05:08:54 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
05:10:18 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
05:21:50 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:42:03 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
05:47:00 → wootehfoot joins (~wootehfoo@user/wootehfoot)
05:47:41 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Max SendQ exceeded)
05:48:26 → wootehfoot joins (~wootehfoo@user/wootehfoot)
06:11:40 → bitrot joins (~bitrot@2a09:bac5:3b4f:eaa::176:77)
06:18:14 × haritz quits (~hrtz@user/haritz) (Remote host closed the connection)
06:25:00 × xkuru quits (~xkuru@user/xkuru) (Read error: Connection reset by peer)
06:25:24 → xkuru joins (~xkuru@user/xkuru)
06:25:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
06:37:26 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:41:45 → CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
06:50:09 → tromp joins (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3)
06:50:49 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
07:00:02 × caconym7 quits (~caconym@user/caconym) (Quit: bye)
07:00:41 → caconym7 joins (~caconym@user/caconym)
07:12:35 → xff0x joins (~xff0x@2409:251:9040:2c00:ac74:2d0a:8f8e:3f83)
07:21:48 → Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
07:22:49 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds)
07:23:13 Lord_of_Life_ is now known as Lord_of_Life
07:29:24 × xff0x quits (~xff0x@2409:251:9040:2c00:ac74:2d0a:8f8e:3f83) (Ping timeout: 276 seconds)
07:35:49 × __jmcantrell__ quits (~weechat@user/jmcantrell) (Ping timeout: 276 seconds)
07:41:35 → acidjnk_new joins (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de)
07:44:35 → gmg joins (~user@user/gehmehgeh)
07:57:00 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds)
08:10:49 → mistivia_ joins (~mistivia@user/mistivia)
08:11:42 × mistivia quits (~mistivia@user/mistivia) (Ping timeout: 252 seconds)
08:12:25 × nckx quits (nckx@libera/staff/owl/nckx) (Ping timeout: 608 seconds)
08:15:44 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:27:49 × bitrot quits (~bitrot@2a09:bac5:3b4f:eaa::176:77) (Quit: Client closed)
08:29:40 × euleritian quits (~euleritia@77.23.248.47) (Ping timeout: 252 seconds)
08:30:11 → euleritian joins (~euleritia@dynamic-176-006-128-100.176.6.pool.telefonica.de)
08:30:36 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
08:33:01 × acidjnk_new quits (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
08:33:33 <[exa]> EvanR, int-e: btw re the ambiguity avoidance yesterday, wasn't there a proposal for that already? I recall I saw something
08:37:53 → euphores joins (~SASL_euph@user/euphores)
08:43:00 → sprotte24 joins (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de)
08:49:30 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
08:50:16 → gmg joins (~user@user/gehmehgeh)
08:50:44 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
08:53:14 × img_ quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
08:54:39 → img joins (~img@user/img)
08:55:57 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
08:58:31 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
09:19:47 × xkuru quits (~xkuru@user/xkuru) (Remote host closed the connection)
09:20:10 → xkuru joins (~xkuru@user/xkuru)
09:24:16 → lxsameer joins (~lxsameer@Serene/lxsameer)
09:25:02 × xkuru quits (~xkuru@user/xkuru) (Ping timeout: 252 seconds)
09:27:32 → __monty__ joins (~toonn@user/toonn)
09:41:55 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
09:53:05 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
09:55:29 → acidjnk_new joins (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de)
10:04:30 → ljdarj joins (~Thunderbi@user/ljdarj)
10:04:55 → j1n37 joins (~j1n37@user/j1n37)
10:05:19 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds)
10:06:42 × fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 276 seconds)
10:09:31 → fp joins (~Thunderbi@hof1.kyla.fi)
10:43:42 → j1n37- joins (~j1n37@user/j1n37)
10:43:45 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds)
10:45:31 → takuan joins (~takuan@d8D86B601.access.telenet.be)
10:59:21 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
11:01:49 → jespada joins (~jespada@r190-133-35-70.dialup.adsl.anteldata.net.uy)
11:05:15 → xff0x joins (~xff0x@2409:251:9040:2c00:9deb:37d0:5584:c159)
11:09:02 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
11:15:53 × euleritian quits (~euleritia@dynamic-176-006-128-100.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
11:16:05 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
11:16:15 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
11:27:30 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
11:32:33 × fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 248 seconds)
11:34:04 → vgtw_ joins (~vgtw@user/vgtw)
11:34:28 × vgtw quits (~vgtw@user/vgtw) (Ping timeout: 252 seconds)
11:48:40 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds)
11:54:44 <haskellbridge> <hellwolf> refactoring in Haskell is very satisfying... compiles -> works.
11:54:44 <haskellbridge> Why would I let LLM takes that fun away from me..
11:55:00 <haskellbridge> <hellwolf> Two day later: https://paste.tomsmeding.com/NxOWsZbb , I got rid of all the Rv/Uv decorators.
11:55:27 <haskellbridge> <hellwolf> the dilemma is to "dumb down" things by "type Var = Ur".
11:55:35 <haskellbridge> <hellwolf> *whether to
12:01:51 → nckx joins (nckx@libera/staff/owl/nckx)
12:03:36 <haskellbridge> <hellwolf> and it is a type error if I swap some lines: power of LinearTypes
12:03:51 <haskellbridge> <hellwolf> preventing temporal logic error using types.
12:17:00 → ljdarj joins (~Thunderbi@user/ljdarj)
12:20:26 → Square2 joins (~Square@user/square)
12:24:27 × tromp quits (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…)
12:28:58 × acidjnk_new quits (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
12:30:16 × adamCS quits (~adamCS@70.19.85.77) (Ping timeout: 276 seconds)
12:30:49 × cstml quits (~Thunderbi@user/cstml) (Remote host closed the connection)
12:31:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
12:34:15 → jespada_ joins (~jespada@r186-49-245-168.dialup.adsl.anteldata.net.uy)
12:34:43 × jespada quits (~jespada@r190-133-35-70.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
12:35:03 → acidjnk_new joins (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de)
12:40:44 → adamCS joins (~adamCS@70.19.85.77)
12:42:36 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
12:44:26 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Remote host closed the connection)
12:44:54 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
13:13:49 × Vajb quits (~Vajb@n83sqe30rcw6481fyv6-1.v6.elisa-mobile.fi) (Ping timeout: 252 seconds)
13:14:00 → Vajb joins (~Vajb@n70s1gw9rltp7nongp6-1.v6.elisa-mobile.fi)
13:14:36 <haskellbridge> <Liamzee> yo, EvanR, you here?
13:15:16 <haskellbridge> <Liamzee> https://paste.tomsmeding.com/mGHVraNc
13:15:16 <haskellbridge> <Liamzee> this solves my problem
13:15:31 <haskellbridge> <Liamzee> the one with chained error handling without ExceptT
13:15:36 × AlexZenon quits (~alzenon@178.34.151.238) (Ping timeout: 272 seconds)
13:15:49 <haskellbridge> <Liamzee> explicit use of monadic bind and traverse to engage the error type
13:21:47 × j1n37- quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
13:22:13 → AlexZenon joins (~alzenon@178.34.151.238)
13:22:34 × acidjnk_new quits (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
13:24:57 <haskellbridge> <Liamzee> hmmm, this actually doesn't work, ugh
13:25:01 <haskellbridge> <Liamzee> almost
13:26:36 → j1n37 joins (~j1n37@user/j1n37)
13:31:14 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
13:32:50 <haskellbridge> <Liamzee> ahhh
13:33:31 <haskellbridge> <Liamzee> either (pure . Left) v works, as does u >>= fmap join . traverse v
13:33:33 → j1n37 joins (~j1n37@user/j1n37)
13:37:03 <haskellbridge> <Liamzee> there was a guy telling me that Haskell is actually underappreciated for Crud
13:39:04 <haskellbridge> <Liamzee> and taking traverse / for_ as a way to propagate errors as an example
13:40:40 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
13:40:46 → tromp joins (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3)
13:43:06 → j1n37 joins (~j1n37@user/j1n37)
13:47:21 → ljdarj1 joins (~Thunderbi@user/ljdarj)
13:51:37 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
13:51:37 ljdarj1 is now known as ljdarj
13:58:36 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
14:01:37 → j1n37 joins (~j1n37@user/j1n37)
14:09:00 × Buliarous quits (~gypsydang@46.232.210.139) (Remote host closed the connection)
14:09:28 → Buliarous joins (~gypsydang@46.232.210.139)
14:19:15 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
14:20:34 × hidjgr quits (~hidjgr@user/hidjgr) (Ping timeout: 252 seconds)
14:30:06 × puke quits (~puke@user/puke) (Ping timeout: 252 seconds)
14:41:57 → puke joins (~puke@user/puke)
14:58:51 → machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
15:02:22 × xff0x quits (~xff0x@2409:251:9040:2c00:9deb:37d0:5584:c159) (Ping timeout: 276 seconds)
15:03:29 → j1n37- joins (~j1n37@user/j1n37)
15:03:46 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds)
15:13:04 → __jmcantrell__ joins (~weechat@user/jmcantrell)
15:13:41 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
15:25:45 × Buliarous quits (~gypsydang@46.232.210.139) (Remote host closed the connection)
15:26:13 → Buliarous joins (~gypsydang@46.232.210.139)
15:30:58 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 276 seconds)
15:33:04 × tromp quits (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…)
15:47:52 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
15:47:53 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
15:48:12 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
15:58:50 → srazkvt joins (~sarah@user/srazkvt)
15:59:57 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
16:07:44 → tromp joins (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3)
16:28:26 × j1n37- quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
16:31:24 → j1n37 joins (~j1n37@user/j1n37)
16:31:27 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
16:32:17 → gmg joins (~user@user/gehmehgeh)
16:36:46 → Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
16:37:11 → lxsameer joins (~lxsameer@Serene/lxsameer)
16:45:15 → acidjnk_new joins (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de)
16:49:51 → tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
16:51:34 → OftenFaded joins (~OftenFade@user/tisktisk)
16:54:48 × chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds)
16:59:55 × tromp quits (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:03:45 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
17:05:13 → alexherbo2 joins (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net)
17:08:04 × __jmcantrell__ quits (~weechat@user/jmcantrell) (Ping timeout: 244 seconds)
17:10:02 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
17:11:49 × cawfee quits (root@2001:19f0:4400:79a1::babe) (Quit: WeeChat 4.6.1)
17:12:29 → cawfee joins (root@2001:19f0:4400:79a1::babe)
17:26:58 → jacopovalanzano joins (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net)
17:27:40 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 265 seconds)
17:31:20 → tromp joins (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3)
17:33:44 <haskellbridge> <hellwolf> what is the lens library that works with non-hask types?
17:45:51 × srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!)
17:45:53 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds)
17:48:41 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
17:59:10 → weary-traveler joins (~user@user/user363627)
18:03:09 → ljdarj joins (~Thunderbi@user/ljdarj)
18:08:44 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
18:10:08 Square2 is now known as Square
18:11:03 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:15:06 × acidjnk_new quits (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Remote host closed the connection)
18:15:31 → acidjnk_new joins (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de)
18:25:28 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
18:25:50 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
18:37:11 → dhil joins (~dhil@5.151.29.141)
18:37:41 × xal quits (~xal@mx1.xal.systems) (Quit: bye)
18:38:10 → xal joins (~xal@mx1.xal.systems)
18:42:25 → LainIwakura joins (~LainIwaku@user/LainIwakura)
18:43:08 × alexherbo2 quits (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net) (Remote host closed the connection)
18:43:17 → alexherbo2 joins (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net)
18:46:15 × alexherbo2 quits (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net) (Remote host closed the connection)
18:49:49 → alexherbo2 joins (~alexherbo@2a02-8440-2507-890c-388b-fef0-359d-316c.rev.sfr.net)
18:51:55 → lxsameer joins (~lxsameer@Serene/lxsameer)
18:53:36 × alexherbo2 quits (~alexherbo@2a02-8440-2507-890c-388b-fef0-359d-316c.rev.sfr.net) (Remote host closed the connection)
18:54:51 × mulk quits (~mulk@pd95149c0.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
18:57:42 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
19:00:03 × caconym7 quits (~caconym@user/caconym) (Quit: bye)
19:00:48 → caconym7 joins (~caconym@user/caconym)
19:08:01 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds)
19:09:11 → mulk joins (~mulk@pd95149c0.dip0.t-ipconnect.de)
19:19:44 → chiselfuse joins (~chiselfus@user/chiselfuse)
19:21:07 → LainIwakura joins (~LainIwaku@user/LainIwakura)
19:27:25 → Sgeo joins (~Sgeo@user/sgeo)
19:35:24 → pavonia joins (~user@user/siracusa)
19:35:24 → JuanDaugherty joins (~juan@user/JuanDaugherty)
19:39:56 × OftenFaded quits (~OftenFade@user/tisktisk) (Ping timeout: 252 seconds)
19:53:57 × Digit quits (~user@user/digit) (Ping timeout: 248 seconds)
20:03:34 → Digit joins (~user@user/digit)
20:07:46 Digit is now known as digitteknohippie
20:10:37 → talismanick joins (~user@2601:644:937c:ed10::ae5)
20:13:32 digitteknohippie is now known as Digit
20:16:00 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
20:17:03 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
20:18:28 → j1n37 joins (~j1n37@user/j1n37)
20:19:02 → michalz joins (~michalz@185.246.207.193)
20:20:41 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
20:21:28 → xff0x joins (~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4)
20:23:42 → j1n37 joins (~j1n37@user/j1n37)
20:24:17 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
20:27:33 → j1n37 joins (~j1n37@user/j1n37)
20:28:07 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:34:21 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
20:35:40 → benin joins (~benin@80-108-89-247.cable.dynamic.surfer.at)
20:36:26 × benin quits (~benin@80-108-89-247.cable.dynamic.surfer.at) (Client Quit)
20:38:36 → j1n37 joins (~j1n37@user/j1n37)
20:52:18 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
20:57:17 → ljdarj1 joins (~Thunderbi@user/ljdarj)
21:00:31 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
21:01:06 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds)
21:01:07 ljdarj1 is now known as ljdarj
21:03:31 × takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection)
21:04:50 × michalz quits (~michalz@185.246.207.193) (Remote host closed the connection)
21:12:47 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
21:14:01 → notdabs joins (~Owner@2600:1700:69cf:9000:c531:a8cf:57a8:ee6f)
21:32:05 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
21:38:19 × dhil quits (~dhil@5.151.29.141) (Ping timeout: 245 seconds)
21:39:33 <EvanR> in dependent types world you sometimes hear about erasable types which helps compiled code not be as slowed down carrying proofs around that aren't actually used
21:40:27 <EvanR> but is there a way to use that information for optimization instead, instead of just "do no harm"
21:43:14 <ncf> what do you mean? erasure is a form of optimisation
21:43:18 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
21:43:40 <EvanR> ok
21:43:47 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:44:12 <EvanR> or the two steps forward that the dependent types added the two steps back for you earlier
21:44:35 <davean> And which cases can't occur drop which conditions you need to check, etc.
21:44:48 <EvanR> ok that's good
21:45:44 <davean> What you're erasing is why the code only does the things it does, not the other things it might have to do.
21:46:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:47:27 <EvanR> though you might imagine there is more there that can be exploited beyond the obvious
21:51:42 <EvanR> like in a context where an integer is known to be in a small range or is small in magnitude
21:54:12 <davean> Those simplications usually show up in the code because the fact we used them is how we ended up with the type in the first place. That said, when we start inlining more abstract functions, etc we get to simplify under these new constraints. This is part of the code of how to optimize in Haskell too.
21:54:18 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds)
21:56:18 → j1n37 joins (~j1n37@user/j1n37)
21:57:46 <davean> Which is to say the benefits of this very much is associated with specialization and inlining.
21:58:12 <davean> We get it in Haskell beyond just what is in the type because of conditionals use for other purposes that overlap, etc.
22:00:24 × j0lol quits (~j0lol@132.145.17.236) (Ping timeout: 276 seconds)
22:00:57 <davean> I think the dependent version lets you use information a bit further away than Haskell does.
22:01:46 <davean> since it sorta drags providence along with it.
22:02:17 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
22:02:47 <davean> I have no idea if anyone has done serious work on dragging that information along though ...
22:04:20 → j1n37- joins (~j1n37@user/j1n37)
22:05:40 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds)
22:07:43 × tromp quits (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…)
22:22:00 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
22:22:51 → euleritian joins (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
22:25:20 × acidjnk_new quits (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
22:34:46 × euleritian quits (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
22:35:05 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
22:44:31 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds)
22:47:07 → j1n37 joins (~j1n37@user/j1n37)
22:49:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
22:50:58 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
22:59:06 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
23:02:21 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:03:14 × koz quits (~koz@121.99.240.58) (Ping timeout: 244 seconds)
23:10:25 <haskellbridge> <loonycyborg> I still have no idea how can you have both pi types and type erasure in the same language.
23:12:49 → typedfern_ joins (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net)
23:16:04 × Typedfern quits (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 260 seconds)
23:16:37 <EvanR> if the code doesn't use the argument, be it a type or a value, then the body is effectively a constant
23:16:45 → j0lol joins (~j0lol@132.145.17.236)
23:18:01 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:19:29 <EvanR> any call site would need to be adjusted to stop trying to call it like a function
23:19:41 <EvanR> just discard the argument
23:21:18 <EvanR> sigma type is a bit more mysterious to me, how do you know someone won't want to use the 2nd component
23:24:43 → acidjnk_new joins (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de)
23:25:24 × sprotte24 quits (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) (Quit: Leaving)
23:29:14 <monochrom> Do you accept: Encode Σx:A. B(x) as ∀r. Πx:A. B(x) -> r so it is just pi types all over again? :)
23:32:13 <EvanR> ... not sure
23:32:36 <monochrom> Err, ∀r. (Πx:A. B(x) -> r) -> r
23:34:14 <EvanR> ok yes
23:34:21 <monochrom> :)
23:35:01 <haskellbridge> <loonycyborg> Even if you technically make this work not sure it would be a good language design. Like most types that aren't passed around are erased but some have to remain which kinda feels inconsistent.
23:35:56 <EvanR> if that's in the machine code then it only bothers somebody trying to disassemnle it
23:36:02 <monochrom> Maybe the programmer doesn't use that encoding, but the compiler does the translation.
23:36:08 <EvanR> typing with pinkies is hard
23:36:36 × fantom quits (~fantom@2.219.56.221) (Ping timeout: 244 seconds)
23:37:20 <EvanR> erasing types or proofs shouldn't change the "observable" behavior
23:38:16 <haskellbridge> <loonycyborg> still it requires operating on type level things that can't be erased
23:38:33 <haskellbridge> <loonycyborg> which probably will have different implementations at runtime and compile time
23:38:54 <EvanR> if it's purely at the type level then it wouldn't need to exist at runtime
23:39:22 <EvanR> because this isn't java
23:39:24 → mange joins (~user@user/mange)
23:39:32 <EvanR> (but I heard java erases it's types also)
23:39:50 <haskellbridge> <loonycyborg> I'm not so sure because of types that could be specified entirely at runtime
23:40:30 <EvanR> well then that's not purely at the type level definitely
23:41:46 <EvanR> accept keyboard input and append to an ongoing list of Types that you can then ask for a listing of, because they have nice Show instances
23:41:55 <EvanR> isn't a type level thing
23:42:33 <haskellbridge> <loonycyborg> to me type erasure seems like technical decision asserting that "compile type == type level; runtime == term level"
23:43:01 <EvanR> well that's not true is it
23:43:19 <EvanR> because e.g. constant folding at compile time etc
23:43:48 <haskellbridge> <loonycyborg> so to get proper dependent types in a compiled language would have to drop type erasure, perhaps replacing it by something else
23:44:54 <EvanR> once you get to a phase where the types aren't doing anything, then keeping them around can only waste resources
23:46:03 <haskellbridge> <loonycyborg> But still there is the case of reading of arbitrary type from stdin :P
23:46:18 <EvanR> you can remove them like a compiler is expected to remove terms that aren't doing anything
23:46:26 <haskellbridge> <loonycyborg> if you explicitly don't support it then it's unlikely that it's a localized case
23:46:28 <mange> Idris 2 lets you be precise about which types you expect to be erased from the program, using multiplicities: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html#erasure
23:46:41 <haskellbridge> <loonycyborg> like need to explicitly figure out what is supported and what isn't
23:47:01 × xff0x quits (~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4) (Ping timeout: 248 seconds)
23:47:33 <EvanR> I don't see how you would even erase a type that is generated at runtime
23:47:37 <EvanR> or why you would want to
23:50:39 → fantom joins (~fantom@2.219.56.221)
23:51:13 <haskellbridge> <loonycyborg> What I'm really wondering about are things like: if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it?
23:51:33 <haskellbridge> <loonycyborg> And if we can then how it works :P
23:52:54 <EvanR> if this is mainstreet dependent types you wouldn't have a separate type level Nat
23:53:17 <EvanR> and compile time arithmetic at runtime sounds like a contradiction
23:54:02 <EvanR> the Nat used at type level can be the same Nat used at value level
23:54:13 <EvanR> not a DataKind
23:55:26 <EvanR> -- oh, compile time arithmetic at runtime, that would be JIT
23:56:53 <mange> I've also seen https://dl.acm.org/doi/10.1145/3341692, which is kind of about deferring type checking until runtime. It's not exactly what you're looking for, but it feels in the same ballpark.
23:59:07 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
23:59:21 <haskellbridge> <loonycyborg> EvanR: ye I actually meant dependent type arithmetic :P

All times are in UTC on 2025-04-27.