2024/06/20

2024-06-20 00:17:55 +0200Midjak(~MarciZ@82.66.147.146) (Quit: Leaving)
2024-06-20 00:22:46 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 00:30:03 +0200 <dolio> I'm not particularly convinced that you're showing that 'dependent types are overkill' when you list multiple features that people want to use dependent types for, and have to be separately grafted onto other languages.
2024-06-20 00:31:09 +0200 <geekosaur> that you can use feature X to do thing Y doesn't mean it's the best way to do thing Y
2024-06-20 00:31:59 +0200 <monochrom> Good points, both of you. :)
2024-06-20 00:32:01 +0200Sgeo(~Sgeo@user/sgeo)
2024-06-20 00:32:07 +0200 <dolio> Well, I didn't make the examples.
2024-06-20 00:34:17 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-06-20 00:35:40 +0200Eoco(~ian@128.101.131.218) (Quit: WeeChat 4.1.1)
2024-06-20 00:41:33 +0200acidjnk_new3(~acidjnk@p200300d6e714dc52cdce3fd1d2726986.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
2024-06-20 00:43:04 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua) (Read error: Connection reset by peer)
2024-06-20 00:43:34 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua)
2024-06-20 00:44:21 +0200danse-nr3(~danse-nr3@151.35.139.58) (Read error: Connection reset by peer)
2024-06-20 00:45:24 +0200danse-nr3(~danse-nr3@151.37.122.33)
2024-06-20 00:46:47 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
2024-06-20 00:48:57 +0200euleritian(~euleritia@dynamic-176-001-131-134.176.1.pool.telefonica.de)
2024-06-20 00:53:57 +0200ystael(~ystael@user/ystael) (Ping timeout: 268 seconds)
2024-06-20 00:54:15 +0200glguy(g@libera/staff/glguy) (Quit: Quit)
2024-06-20 00:56:40 +0200glguy(g@libera/staff/glguy)
2024-06-20 00:57:50 +0200Square2(~Square4@user/square)
2024-06-20 00:58:53 +0200mud(~mud@user/kadoban) (Ping timeout: 268 seconds)
2024-06-20 01:01:03 +0200Square(~Square@user/square) (Ping timeout: 255 seconds)
2024-06-20 01:02:02 +0200glguy(g@libera/staff/glguy) (Remote host closed the connection)
2024-06-20 01:03:16 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2024-06-20 01:03:30 +0200glguy(g@libera/staff/glguy)
2024-06-20 01:03:35 +0200danse-nr3(~danse-nr3@151.37.122.33) (Ping timeout: 264 seconds)
2024-06-20 01:03:38 +0200danza(~francesco@151.37.122.33)
2024-06-20 01:04:52 +0200mud(~mud@user/kadoban)
2024-06-20 01:08:09 +0200talismanick(~user@2601:644:937c:ed10::ae5)
2024-06-20 01:08:45 +0200danza(~francesco@151.37.122.33) (Ping timeout: 268 seconds)
2024-06-20 01:19:39 +0200talismanick(~user@2601:644:937c:ed10::ae5) (Remote host closed the connection)
2024-06-20 01:24:04 +0200talismanick(~user@2601:644:937c:ed10::ae5)
2024-06-20 01:25:04 +0200danza(~francesco@151.37.122.33)
2024-06-20 01:25:24 +0200 <talismanick> Is suppressing the "type inference for inner bindings fragile" warning with MonoLocalBinds generally safe?
2024-06-20 01:26:08 +0200 <talismanick> or, more precisely, intent- and correctness-preserving
2024-06-20 01:38:16 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:be5c:bfac:9926:c006)
2024-06-20 01:52:14 +0200johnw(~johnw@69.62.242.138) (Ping timeout: 268 seconds)
2024-06-20 01:52:22 +0200johnw_(~johnw@69.62.242.138)
2024-06-20 01:56:29 +0200sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 240 seconds)
2024-06-20 01:59:32 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-06-20 02:00:20 +0200hgolden_(~hgolden@syn-172-251-233-141.res.spectrum.com) (Remote host closed the connection)
2024-06-20 02:09:38 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
2024-06-20 02:10:01 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-06-20 02:10:11 +0200euleritian(~euleritia@dynamic-176-001-131-134.176.1.pool.telefonica.de) (Ping timeout: 252 seconds)
2024-06-20 02:12:19 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit)
2024-06-20 02:12:42 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-06-20 02:15:37 +0200euleritian(~euleritia@dynamic-176-002-140-016.176.2.pool.telefonica.de)
2024-06-20 02:22:44 +0200whatsupdoc(uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-20 02:23:41 +0200falafel(~falafel@2a0c:5a87:3103:ec01::62b8) (Ping timeout: 240 seconds)
2024-06-20 02:24:44 +0200euleritian(~euleritia@dynamic-176-002-140-016.176.2.pool.telefonica.de) (Ping timeout: 256 seconds)
2024-06-20 02:26:01 +0200euleritian(~euleritia@dynamic-176-000-200-205.176.0.pool.telefonica.de)
2024-06-20 02:37:47 +0200henry40408(~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds))
2024-06-20 02:38:15 +0200henry40408(~henry4040@175.182.111.183)
2024-06-20 02:38:33 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal)
2024-06-20 02:38:53 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-20 02:42:35 +0200euleritian(~euleritia@dynamic-176-000-200-205.176.0.pool.telefonica.de) (Ping timeout: 264 seconds)
2024-06-20 02:43:29 +0200CrunchyFlakes(~CrunchyFl@146.52.130.128) (Read error: Connection reset by peer)
2024-06-20 02:44:36 +0200euleritian(~euleritia@dynamic-176-006-000-101.176.6.pool.telefonica.de)
2024-06-20 02:45:51 +0200CrunchyFlakes(~CrunchyFl@146.52.130.128)
2024-06-20 02:47:10 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 246 seconds)
2024-06-20 02:50:10 +0200segfaultfizzbuzz(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Remote host closed the connection)
2024-06-20 02:53:28 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua)
2024-06-20 03:00:03 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds)
2024-06-20 03:05:39 +0200euleritian(~euleritia@dynamic-176-006-000-101.176.6.pool.telefonica.de) (Ping timeout: 260 seconds)
2024-06-20 03:07:02 +0200euleritian(~euleritia@dynamic-176-006-011-015.176.6.pool.telefonica.de)
2024-06-20 03:09:40 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
2024-06-20 03:14:16 +0200bionade24(~quassel@2a03:4000:33:45b::1) (Remote host closed the connection)
2024-06-20 03:15:25 +0200bionade24(~quassel@2a03:4000:33:45b::1)
2024-06-20 03:23:39 +0200danza(~francesco@151.37.122.33) (Ping timeout: 264 seconds)
2024-06-20 03:26:54 +0200talismanick(~user@2601:644:937c:ed10::ae5) (Remote host closed the connection)
2024-06-20 03:32:47 +0200ChaiTRex(~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2024-06-20 03:36:10 +0200hgolden(~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9)
2024-06-20 03:41:01 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::)
2024-06-20 03:42:31 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::) (Client Quit)
2024-06-20 03:50:59 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 264 seconds)
2024-06-20 03:51:30 +0200talismanick(~user@2601:644:937c:ed10::ae5)
2024-06-20 03:53:11 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Quit: au revoir)
2024-06-20 03:53:56 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua)
2024-06-20 04:01:41 +0200euleritian(~euleritia@dynamic-176-006-011-015.176.6.pool.telefonica.de) (Ping timeout: 240 seconds)
2024-06-20 04:02:06 +0200petrichor(~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
2024-06-20 04:03:29 +0200petrichor(~znc-user@user/petrichor)
2024-06-20 04:04:11 +0200xff0x(~xff0x@ai068022.d.east.v6connect.net) (Ping timeout: 264 seconds)
2024-06-20 04:06:31 +0200euleritian(~euleritia@dynamic-176-007-145-030.176.7.pool.telefonica.de)
2024-06-20 04:12:22 +0200 <monochrom> Intent requires true AI (not even today's LLM). But if type checking succeeds, it's sound, i.e., as correct as the type system can tell.
2024-06-20 04:13:47 +0200 <geekosaur> right, that warning says that you may get unexpected type checking failures because type inference might not work
2024-06-20 04:13:59 +0200 <geekosaur> but if it does typecheck, you're fine
2024-06-20 04:14:15 +0200 <geekosaur> (or you can just give everything explicit types)
2024-06-20 04:25:10 +0200zzz(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-20 04:29:48 +0200 <probie> Re give everything explicit types: I sometimes wish I had some way to say "should be inferred as having type [α-equivalent to] τ"
2024-06-20 04:33:08 +0200 <probie> That way I could write something like `stutter ::[inferred] [a] -> [a]; stutter = foldr (\x xs -> x:x:xs) []` and the compiler can warn me that I've picked a type more specific than what would have been inferred
2024-06-20 04:38:33 +0200causal(~eric@50.35.88.207)
2024-06-20 04:44:53 +0200euleritian(~euleritia@dynamic-176-007-145-030.176.7.pool.telefonica.de) (Ping timeout: 240 seconds)
2024-06-20 04:46:07 +0200euleritian(~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de)
2024-06-20 04:53:43 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-20 04:56:00 +0200td_(~td@i53870921.versanet.de) (Ping timeout: 268 seconds)
2024-06-20 04:57:43 +0200td_(~td@i5387090C.versanet.de)
2024-06-20 04:58:53 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex)
2024-06-20 05:02:10 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-06-20 05:08:59 +0200sam113101(~sam@24.157.253.231) (Remote host closed the connection)
2024-06-20 05:15:38 +0200xdminsy(~xdminsy@117.147.70.231) (Quit: Konversation terminated!)
2024-06-20 05:33:40 +0200sam113101(~sam@24.157.253.231)
2024-06-20 05:43:17 +0200aforemny_(~aforemny@i59F516D3.versanet.de)
2024-06-20 05:44:39 +0200aforemny(~aforemny@2001:9e8:6cc0:df00:949a:33df:9d68:3e31) (Ping timeout: 264 seconds)
2024-06-20 06:07:21 +0200Square2(~Square4@user/square) (Read error: Connection reset by peer)
2024-06-20 06:08:23 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
2024-06-20 06:09:07 +0200iqubic(~sophia@2601:602:9502:c70:f6b8:a053:cf21:deda) (Ping timeout: 246 seconds)
2024-06-20 06:27:49 +0200philopsos1(~caecilius@user/philopsos)
2024-06-20 06:31:42 +0200sam113101(~sam@24.157.253.231) (Remote host closed the connection)
2024-06-20 06:34:27 +0200sam113101(~sam@24.157.253.231)
2024-06-20 06:42:57 +0200michalz(~michalz@185.246.207.221)
2024-06-20 06:45:10 +0200euleritian(~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-20 06:45:27 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-20 06:50:50 +0200xdminsy(~xdminsy@117.147.70.231)
2024-06-20 06:51:56 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Ping timeout: 268 seconds)
2024-06-20 06:58:17 +0200wlhn(~wenzel@dl46fx8hbfttwvhb-h1ly-3.rev.dnainternet.fi)
2024-06-20 07:00:32 +0200darmario(~MrFox___@user/darmario)
2024-06-20 07:07:49 +0200rosco(~rosco@175.136.155.137)
2024-06-20 07:09:58 +0200takuan(~takuan@178-116-218-225.access.telenet.be)
2024-06-20 07:12:45 +0200riatre(~quassel@2001:310:6000:f::5198:1) (Quit: http://quassel-irc.org)
2024-06-20 07:13:04 +0200darmario(~MrFox___@user/darmario) (Quit: Leaving)
2024-06-20 07:21:18 +0200simendsjo(~user@84.209.170.3) (Ping timeout: 255 seconds)
2024-06-20 07:34:32 +0200michalz(~michalz@185.246.207.221) (Quit: ZNC 1.9.0 - https://znc.in)
2024-06-20 07:37:17 +0200michalz(~michalz@185.246.207.218)
2024-06-20 07:44:37 +0200acidjnk_new3(~acidjnk@p200300d6e714dc085da20c6dea9e24be.dip0.t-ipconnect.de)
2024-06-20 07:45:16 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-20 07:46:05 +0200euleritian(~euleritia@77.22.252.56)
2024-06-20 07:51:08 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 268 seconds)
2024-06-20 08:16:31 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::)
2024-06-20 08:18:03 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::) (Client Quit)
2024-06-20 08:18:53 +0200iqubic(~sophia@2601:602:9502:c70:6afe:7af5:5891:b32f)
2024-06-20 08:22:02 +0200riatre(~quassel@2001:310:6000:f::5198:1)
2024-06-20 08:27:16 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:be5c:bfac:9926:c006) (Quit: Leaving)
2024-06-20 08:32:03 +0200rvalue(~rvalue@user/rvalue) (Ping timeout: 264 seconds)
2024-06-20 08:32:03 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-20 08:33:52 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-20 08:36:27 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 08:38:33 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-06-20 08:40:13 +0200rvalue(~rvalue@user/rvalue)
2024-06-20 08:40:29 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-20 08:43:13 +0200euleritian(~euleritia@77.22.252.56) (Ping timeout: 256 seconds)
2024-06-20 08:45:38 +0200euleritian(~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de)
2024-06-20 08:46:02 +0200euleritian(~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-20 08:46:04 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::)
2024-06-20 08:47:46 +0200euleritian(~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de)
2024-06-20 08:49:47 +0200euleritian(~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-20 08:50:05 +0200euleritian(~euleritia@77.22.252.56)
2024-06-20 08:52:11 +0200ft(~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving)
2024-06-20 08:54:26 +0200euleritian(~euleritia@77.22.252.56) (Ping timeout: 252 seconds)
2024-06-20 08:55:05 +0200euleritian(~euleritia@77.22.252.56)
2024-06-20 09:08:31 +0200jle`(~jle`@2603:8001:3b02:84d4:309b:a5ab:1320:adb2) (Ping timeout: 268 seconds)
2024-06-20 09:09:54 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 256 seconds)
2024-06-20 09:09:55 +0200jle`(~jle`@2603:8001:3b02:84d4:89e:9b05:41f1:3af8)
2024-06-20 09:13:43 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua)
2024-06-20 09:15:18 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::) (Quit: Quit)
2024-06-20 09:30:02 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 09:38:40 +0200danse-nr3(~danse-nr3@151.57.10.250)
2024-06-20 09:44:00 +0200manwithluck(manwithluc@gateway/vpn/protonvpn/manwithluck)
2024-06-20 09:48:00 +0200dcoutts__(~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 255 seconds)
2024-06-20 09:52:11 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542)
2024-06-20 09:55:59 +0200 <tomsmeding> a tag to check that this is not only a valid type, but is actually a _most general_ type for the definition?
2024-06-20 09:56:01 +0200 <tomsmeding> interesting
2024-06-20 09:58:47 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-20 10:02:28 +0200cfricke(~cfricke@user/cfricke)
2024-06-20 10:04:43 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-06-20 10:12:33 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-06-20 10:16:21 +0200lxsameer(~lxsameer@Serene/lxsameer)
2024-06-20 10:17:21 +0200 <dminuoso> That seems a bit weird. Isn't the goal of Damas Milner type inference to already give you "the most general type"?
2024-06-20 10:17:59 +0200Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) (Ping timeout: 264 seconds)
2024-06-20 10:18:16 +0200rosco(~rosco@175.136.155.137)
2024-06-20 10:18:31 +0200 <dminuoso> How would the type checker know of "a more general type" to begin with?
2024-06-20 10:19:00 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Quit: Leaving)
2024-06-20 10:19:28 +0200 <dminuoso> I mean "should be inferred as having type [α-equivalent to] τ" can be stated by `x :: τ`
2024-06-20 10:20:24 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net)
2024-06-20 10:21:15 +0200 <dminuoso> Ohh I think as I was writing about it, I understood.
2024-06-20 10:22:21 +0200 <dminuoso> So a kind of `x :: τ; x :: _` as if it were?
2024-06-20 10:22:28 +0200 <ncf> they want an synthesized-then-checked type ascription, presumably
2024-06-20 10:22:53 +0200__monty__(~toonn@user/toonn)
2024-06-20 10:24:01 +0200Luj(~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5)
2024-06-20 10:24:50 +0200Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no)
2024-06-20 10:24:56 +0200 <ncf> Γ ⊢ x => τ Γ ⊢ x <= τ
2024-06-20 10:24:57 +0200 <ncf> ----------------- as opposed to -----------------
2024-06-20 10:24:58 +0200 <ncf> Γ ⊢ (x :: τ) => τ Γ ⊢ (x :: τ) => τ
2024-06-20 10:26:48 +0200 <ChrisTrac> hi, I'm playing with GHC.Exts.withDict and am wondering if there's a way to instantiate a class with multiple methods? I'm using QuickCheck, and want to define `Gen a` values rather than instantiating `Arbitrary`; but lots of existing generators have `Arbitrary a` constraints that I can't satisfy.
2024-06-20 10:29:09 +0200 <ChrisTrac> (the usual alternative is to define a load of newtypes, but I've got LOTS of nested datatypes that makes that a pain; but they're Generic so I can auto-generate a lot of Gen values easily)
2024-06-20 10:30:28 +0200 <tomsmeding> dminuoso: they want that `x ::[inferred] Int ; x = 42` would fail because that's less general than `x :: Num a => a`
2024-06-20 10:31:06 +0200 <tomsmeding> ChrisTrac: have you considered using hedgehog instead? :)
2024-06-20 10:31:28 +0200 <tomsmeding> it's designed around providing explicit generators, instead of relying on an Arbitrary type class
2024-06-20 10:32:17 +0200 <ChrisTrac> heh, I'm actually more of a fan of falsify; this project already uses QuickCheck in parts, so I'm after a path of least-resistance
2024-06-20 10:32:44 +0200 <tomsmeding> generating type class evidence out of thin air is always a dangerous endeavour
2024-06-20 10:33:17 +0200 <ChrisTrac> yeah, unsafeCoerce can do it; but that's worse than just writing a mountain of instances IMHO
2024-06-20 10:33:23 +0200 <tomsmeding> I don't think there's a supported way apart from withDict
2024-06-20 10:33:33 +0200 <tomsmeding> (which only works for single-method classes)
2024-06-20 10:33:55 +0200 <tomsmeding> (and even withDict is not meant to be used lightly)
2024-06-20 10:34:53 +0200 <ChrisTrac> I tried making my own single-method `class Arb a where arb :: Gen a`, which works fine for withDict; but I can't use that to satisfy an existing Arbitrary constraint :(
2024-06-20 10:36:45 +0200euleritian(~euleritia@77.22.252.56) (Read error: Connection reset by peer)
2024-06-20 10:37:08 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-20 10:39:31 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-20 10:40:01 +0200 <Leary> ChrisTrac: You can if you get nasty. If you write `newtype FromArb a = FromArb a; instance Arb a => Arbitrary (FromArb a)`, then you can turn `Gen a ->` into `Arb a =>` with `withDict`, which gives you `Arbitrary (FromArb a)`, which you can capture with `data Dict c = c => Dict`, and safely `unsafeCoerce` to `Dict (Arbitrary a)`.
2024-06-20 10:40:21 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-20 10:40:59 +0200 <danse-nr3> hmm "safely unsafeCoerce"
2024-06-20 10:41:44 +0200 <ChrisTrac> Leary: Yeah, it seems like there's inevitably an `unsafeCoerce` (whether directly, or indirectly via a library like `constraints`)
2024-06-20 10:42:33 +0200 <Leary> In my opinion, `withDict` is actually more dangerous than `unsafeCoerce` where you know the representation matches.
2024-06-20 10:44:09 +0200 <tomsmeding> and how do we all know that ghc will pick the Arbitrary constraint we're trying to pass, and not some other floating around?
2024-06-20 10:44:11 +0200 <ChrisTrac> Leary: how so? I thought withDict just fails to find an instance (a compile error), whilst unsafeCoerce can cause segfaults, etc.
2024-06-20 10:44:47 +0200dcoutts__(~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net)
2024-06-20 10:45:27 +0200 <ChrisTrac> tomsmeding: in this case it's "morally coherent", in that I don't care which is picked (I just want one, any one)
2024-06-20 10:46:54 +0200 <Leary> I'll re-emphasise: /where you know the representation matches/
2024-06-20 10:47:43 +0200 <danse-nr3> `withDict` seems an advanced function indeed, was not familiar with it
2024-06-20 10:47:57 +0200 <Leary> Using it to erase a newtype obviously cannot cause a segfault; it's more like reaching for internals that weren't exposed.
2024-06-20 10:48:58 +0200 <tomsmeding> and "knowing that the representation matches" is not? :p
2024-06-20 10:49:52 +0200 <tomsmeding> (I'm not saying that you can't do what you're suggesting -- I'm just saying that depending on knowledge about internal representation, for which you can't even explicitly tell the compiler that you're depending on it, is dangerous)
2024-06-20 10:52:43 +0200 <Leary> `newtype`s are language-guaranteed to share the same representation as the type they wrap?
2024-06-20 10:52:46 +0200 <ChrisTrac> I think coercing between representational types (e.g. newtype wrappers) is fine; coercing between GHC's current dictionary representations is where it gets hairy (i.e. where we're depending on the Core structure)
2024-06-20 10:53:47 +0200 <danse-nr3> but then... whey would you coerce between newtype wrappers?
2024-06-20 10:53:51 +0200 <danse-nr3> *why
2024-06-20 10:54:13 +0200sawilagar(~sawilagar@user/sawilagar)
2024-06-20 10:54:18 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2024-06-20 10:54:50 +0200 <ChrisTrac> danse-nr3: classic examples are Monoid instances for `Sum Int`, `Product Int`, `Min Int`, `Max Int`, etc. (where all those wrappers are newtypes)
2024-06-20 10:56:42 +0200 <Leary> ChrisTrac: What I'm suggesting is only `unsafeCoerce :: Dict (Arbitrary (FromArb a)) -> Dict (Arbitrary a)`. This doesn't depend on anything the language doesn't guarantee; it's only a threat to coherence, same as `withDict`.
2024-06-20 10:56:52 +0200 <danse-nr3> i get it can be handy, i guess i would prefer to find a way that plays well with the type system
2024-06-20 10:57:54 +0200 <tomsmeding> Leary: hm, I guess -- as long as you know that all methods of Arbitrary use the type variable at most representationally
2024-06-20 10:59:03 +0200 <tomsmeding> how do I get ghci to print roles for a newtype again?
2024-06-20 10:59:04 +0200 <Leary> Right, that's a point worthy of note.
2024-06-20 10:59:42 +0200 <ChrisTrac> danse-nr3: say you `getSum (mappend (map Sum myBigListOfInts))`, the `Sum` and `getSum` are no-ops, so zero-overhead; but we might end up running `map` over the list, wasting resources (depends on optimisations; even if lists get optimised away, more complicated structures might not). We can replace the `map Sum` with coerce to ensure it's
2024-06-20 10:59:43 +0200 <ChrisTrac> definitely a no-op (and the type-checker will ensure it's safe)
2024-06-20 11:00:00 +0200AlexNoo_AlexNoo
2024-06-20 11:00:01 +0200 <tomsmeding> but that's _coerce_, not _unsafeCoerce_
2024-06-20 11:00:14 +0200 <tomsmeding> with unsafeCoerce it's up to you to check that there is indeed representational equality
2024-06-20 11:00:29 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2024-06-20 11:00:29 +0200 <tomsmeding> the language does not, really, guarantee anything about the representation of dictionaries in something like the Dict type
2024-06-20 11:00:38 +0200chele(~chele@user/chele)
2024-06-20 11:01:25 +0200 <tomsmeding> so with the Leary's unsafeCoerce trick we're still depending on the fact that whatever that runtime representation of type class evidence is, this representation is the same for representationally equal type parameters
2024-06-20 11:01:33 +0200 <tomsmeding> Haskell2010 does not guarantee that
2024-06-20 11:01:43 +0200 <tomsmeding> it's _true_ in GHC
2024-06-20 11:03:27 +0200 <tomsmeding> and the fact that I can't think of a different, still sensible implementation notwithstanding :p
2024-06-20 11:05:37 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Ping timeout: 250 seconds)
2024-06-20 11:15:47 +0200 <danse-nr3> interesting. `coerce` does not even feel that coercing :)
2024-06-20 11:15:58 +0200danse-nr3wonders whether a `cast` exists
2024-06-20 11:16:01 +0200 <danse-nr3> @hoogle cast
2024-06-20 11:16:02 +0200 <lambdabot> Data.Typeable cast :: forall a b . (Typeable a, Typeable b) => a -> Maybe b
2024-06-20 11:16:02 +0200 <lambdabot> Protolude cast :: (Typeable a, Typeable b) => a -> Maybe b
2024-06-20 11:16:02 +0200 <lambdabot> BasePrelude cast :: (Typeable a, Typeable b) => a -> Maybe b
2024-06-20 11:16:19 +0200 <danse-nr3> @hoogle coerce
2024-06-20 11:16:20 +0200 <lambdabot> Data.Coerce coerce :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) . Coercible a b => a -> b
2024-06-20 11:16:20 +0200 <lambdabot> GHC.Exts coerce :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) . Coercible a b => a -> b
2024-06-20 11:16:20 +0200 <lambdabot> Control.Lens.Internal.Coerce coerce :: Coercible a b => a -> b
2024-06-20 11:19:32 +0200 <mauke> @hoogle reify
2024-06-20 11:19:33 +0200 <lambdabot> Language.Haskell.TH reify :: Name -> Q Info
2024-06-20 11:19:33 +0200 <lambdabot> Language.Haskell.TH.Syntax reify :: Name -> Q Info
2024-06-20 11:19:33 +0200 <lambdabot> Hedgehog.Internal.State reify :: HTraversable t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
2024-06-20 11:19:37 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net)
2024-06-20 11:23:51 +0200 <tomsmeding> @hoogle reflect
2024-06-20 11:23:52 +0200 <lambdabot> Pipes.Core reflect :: Functor m => Proxy a' a b' b m r -> Proxy b b' a a' m r
2024-06-20 11:23:52 +0200 <lambdabot> Data.Reflection reflect :: Reifies s a => proxy s -> a
2024-06-20 11:23:52 +0200 <lambdabot> Control.Monad.Logic.Class reflect :: MonadLogic m => Maybe (a, m a) -> m a
2024-06-20 11:24:17 +0200danse-nr3raises eyebrow
2024-06-20 11:24:31 +0200 <tomsmeding> ¯\_(ツ)_/¯
2024-06-20 11:24:37 +0200 <danse-nr3> =D
2024-06-20 11:27:45 +0200kuribas(~user@ptr-17d51emfywuvjswcfv8.18120a2.ip6.access.telenet.be)
2024-06-20 11:28:39 +0200gawen(~gawen@user/gawen) (Quit: cya)
2024-06-20 11:34:42 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Quit: Client closed)
2024-06-20 11:36:20 +0200gawen(~gawen@user/gawen)
2024-06-20 11:42:37 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-06-20 11:43:36 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net)
2024-06-20 11:43:38 +0200 <mreh> I'm rather inspired by servant and beam to create some kind of depently typed eDSL to generate (limited for now) OpenGL pipelines.
2024-06-20 11:44:04 +0200 <mreh> The amount of boilerplate I have to write doing OpenGL currently.
2024-06-20 11:45:06 +0200gehmehgeh(~user@user/gehmehgeh)
2024-06-20 11:45:21 +0200gehmehgehgmg
2024-06-20 11:46:24 +0200gmg(~user@user/gehmehgeh) (Client Quit)
2024-06-20 11:49:18 +0200L29Ah(~L29Ah@wikipedia/L29Ah)
2024-06-20 11:52:03 +0200TonyStone(~TonyStone@user/TonyStone) (Ping timeout: 260 seconds)
2024-06-20 11:57:25 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::)
2024-06-20 11:59:58 +0200dequbed(~dequbed@banana-new.kilobyte22.de)
2024-06-20 12:01:09 +0200madhavanmiui(~madhavanm@2409:40f4:ae:dd09:8000::) (Client Quit)
2024-06-20 12:03:32 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-20 12:04:40 +0200TonyStone(~TonyStone@user/TonyStone)
2024-06-20 12:05:20 +0200 <danse-nr3> does nothing like that already exist mreh?
2024-06-20 12:05:33 +0200gehmehgeh(~user@user/gehmehgeh)
2024-06-20 12:06:36 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds)
2024-06-20 12:06:38 +0200gehmehgehgmg
2024-06-20 12:06:41 +0200gawen(~gawen@user/gawen) (Quit: cya)
2024-06-20 12:10:27 +0200 <mreh> danse-nr3: There are DSLs and eDSLs, but I don't think they can exclude many runtime errors, say for example I don't have a vertex buffer object bound with the right kind of data in it with the right attribute pointer for my vertex shader.
2024-06-20 12:11:38 +0200 <danse-nr3> oh had overlooked the "dependently typed" part. Good luck then
2024-06-20 12:12:12 +0200 <mreh> The eDSLs I've found are also not well documented. Lambdacube looks good, but I didn't fancy it since it's its own language with its own toolchain.
2024-06-20 12:13:01 +0200 <danse-nr3> i assume good doc is also a matter of how much collaboration one can get on their project
2024-06-20 12:13:15 +0200acidjnk_new3(~acidjnk@p200300d6e714dc085da20c6dea9e24be.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2024-06-20 12:13:59 +0200 <mreh> danse-nr3: probably. They're also mostly all around 10 years old and dependent types and OpenGL have come along a lot since then.
2024-06-20 12:14:23 +0200gawen(~gawen@user/gawen)
2024-06-20 12:14:28 +0200 <danse-nr3> but we've got "fearless refactoring"
2024-06-20 12:14:44 +0200danse-nr3is not trying to get mreh collaborating on an existing project at all
2024-06-20 12:14:51 +0200ChrisTrac91(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net)
2024-06-20 12:15:00 +0200 <mreh> danse-nr3: go on :)
2024-06-20 12:15:05 +0200 <danse-nr3> :P
2024-06-20 12:15:28 +0200 <mreh> do you have something of your own in mind?
2024-06-20 12:15:54 +0200 <danse-nr3> nope, i just saw a lot of projects start, get no traction and eventually be abandoned
2024-06-20 12:16:45 +0200 <mreh> yeah, I know right. I'm going to be the primary user of it
2024-06-20 12:17:04 +0200 <mreh> so there will be an enthusiastic development team behind it
2024-06-20 12:17:59 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Ping timeout: 250 seconds)
2024-06-20 12:18:33 +0200 <mreh> lack of traction in the case of the others is probably because of no doc and incompleteness
2024-06-20 12:18:47 +0200 <danse-nr3> an enthusiastic team of 1 you mean? (:
2024-06-20 12:18:55 +0200 <mreh> danse-nr3: damn right
2024-06-20 12:19:07 +0200 <mreh> even lambdacube is hard to get into
2024-06-20 12:19:51 +0200 <danse-nr3> enthusiastic & a bit lonely. Not uncommon in haskell land but also not necessarily the only way
2024-06-20 12:21:12 +0200 <mreh> there seems to be a bit of a haskell boom going on right now
2024-06-20 12:21:28 +0200ChrisTrac91(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Ping timeout: 250 seconds)
2024-06-20 12:21:28 +0200 <danse-nr3> "a bit of a boom"?
2024-06-20 12:22:22 +0200 <mreh> I see lots of mainstream influencers talking about it
2024-06-20 12:28:12 +0200cfricke(~cfricke@user/cfricke) (Ping timeout: 255 seconds)
2024-06-20 12:30:51 +0200noumenon(~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving)
2024-06-20 12:34:29 +0200danse-nr3(~danse-nr3@151.57.10.250) (Ping timeout: 268 seconds)
2024-06-20 12:35:06 +0200sprout(~quassel@2a02-a448-3a80-0-758a-35d7-4890-aab6.fixed6.kpn.net) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
2024-06-20 12:35:29 +0200sprout(~quassel@2a02-a448-3a80-0-d1d9-fee0-140e-a81b.fixed6.kpn.net)
2024-06-20 12:41:53 +0200cfricke(~cfricke@user/cfricke)
2024-06-20 12:53:42 +0200ubert(~Thunderbi@2a02:8109:ab8a:5a00:b0fb:c3f5:4666:ad2f)
2024-06-20 12:55:15 +0200piele_(~piele@tbonesteak.creativeserver.net) (Remote host closed the connection)
2024-06-20 12:56:28 +0200piele(~piele@tbonesteak.creativeserver.net)
2024-06-20 13:04:44 +0200xff0x(~xff0x@ai068022.d.east.v6connect.net)
2024-06-20 13:07:05 +0200mmohammadi9812(~mohammad@85.185.34.203)
2024-06-20 13:09:31 +0200danza(~francesco@151.43.26.19)
2024-06-20 13:22:58 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net)
2024-06-20 13:24:56 +0200CiaoSen(~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03)
2024-06-20 13:26:53 +0200danza(~francesco@151.43.26.19) (Ping timeout: 240 seconds)
2024-06-20 13:28:34 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-06-20 13:33:19 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-06-20 13:34:21 +0200ChrisTrac(~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Quit: Client closed)
2024-06-20 13:40:28 +0200CiaoSen(~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds)
2024-06-20 13:45:33 +0200andrewboltachev(~andrey@178.141.121.180)
2024-06-20 13:46:16 +0200 <andrewboltachev> Hi. Do I understand correctly that `mtl` is much more recommended to use than `trnasformers`?
2024-06-20 13:46:44 +0200danse-nr3(~danse-nr3@151.43.38.52)
2024-06-20 13:47:47 +0200 <andrewboltachev> I have a challenge of adding one more monad to here (StateT): https://github.com/andrewboltachev/matcher/blob/master/src/Logicore/Matcher/Core.hs#L468 so will transition to MTL make such things easier?
2024-06-20 13:54:58 +0200dcoutts__(~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 268 seconds)
2024-06-20 13:57:33 +0200 <mreh> transformers is a dependency of mtl
2024-06-20 13:58:08 +0200 <mreh> andrewboltachev: ^
2024-06-20 13:59:53 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer)
2024-06-20 14:00:32 +0200 <mreh> you have to use transformers if you need to write Haskell98, otherwise mtl has some nice features
2024-06-20 14:01:12 +0200 <mreh> since mtl uses some Language extensions, it's GHC only I believe
2024-06-20 14:01:55 +0200L29Ah(~L29Ah@wikipedia/L29Ah)
2024-06-20 14:04:34 +0200dcoutts__(~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net)
2024-06-20 14:06:49 +0200acidjnk_new3(~acidjnk@p200300d6e714dc085da20c6dea9e24be.dip0.t-ipconnect.de)
2024-06-20 14:07:34 +0200 <mreh> simply put, mtl doesn't require you to litter your code with `lift` when using transformer stacks
2024-06-20 14:10:12 +0200 <andrewboltachev> mreh: yes, this seems clear. I have things like that when I need to "ask" (so, not even lift): https://github.com/andrewboltachev/matcher/blob/master/src/Logicore/Matcher/Core.hs#L946
2024-06-20 14:12:21 +0200 <mreh> yeah, so MatchStatusT could derive the class MonadReader if you were using mtl
2024-06-20 14:12:37 +0200 <mreh> you could make MatchStatusT a type synonym and get that for free
2024-06-20 14:13:10 +0200 <mreh> or use newtype deriving
2024-06-20 14:14:09 +0200 <mreh> that would also apply to the other typeclasses, like Monad, Functor, Applicative...
2024-06-20 14:15:20 +0200 <mreh> nothing to do with mtl in the latter case, but something I noticed about the code
2024-06-20 14:16:19 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-20 14:21:17 +0200Buggys(Buggys@shelltalk.net) (Quit: IRCNow and Forever!)
2024-06-20 14:26:35 +0200gmg(~user@user/gehmehgeh)
2024-06-20 14:31:35 +0200Pixi(~Pixi@user/pixi) (Ping timeout: 252 seconds)
2024-06-20 14:32:29 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Quit: Lost terminal)
2024-06-20 14:35:40 +0200mmohammadi9812(~mohammad@85.185.34.203) (Ping timeout: 268 seconds)
2024-06-20 14:37:13 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2024-06-20 14:38:49 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua)
2024-06-20 14:45:47 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-06-20 14:50:57 +0200 <andrewboltachev> mreh: I guess this one is also should be called MatchStatusM (by convention)?
2024-06-20 14:51:09 +0200 <andrewboltachev> the type synonym
2024-06-20 14:51:46 +0200Pixi(~Pixi@user/pixi)
2024-06-20 14:52:27 +0200 <mreh> andrewboltachev: not sure I follow you
2024-06-20 14:53:40 +0200 <andrewboltachev> you said above: you could make MatchStatusT a type synonym and get that for free
2024-06-20 14:54:21 +0200 <andrewboltachev> I know that sonetimes that "top-level monads" are defined as type synonyms and also called like AppM, ResponderM etc
2024-06-20 14:55:18 +0200 <andrewboltachev> I always thought that that "M" means sth special
2024-06-20 14:55:34 +0200 <mreh> oh right yeah, it just means Monad usually!
2024-06-20 14:57:05 +0200 <andrewboltachev> well I think I've got the idea of what mtl is now
2024-06-20 14:57:49 +0200 <mreh> why not call it something like `Match`?
2024-06-20 14:58:43 +0200 <andrewboltachev> might be
2024-06-20 14:59:32 +0200 <edwardk> andrewboltachev: 'transformers' is the base upon which 'mtl' is built. if you dont want to use mtl, but want to use some other mechanism, like, say, the ill-advised monads-tf package or whatever, or some effect system that might just use the mtl to write out the code of a handler or two, then this lets you share the base transformers, while retaining the option of dispatching classes in a different way.
2024-06-20 15:00:23 +0200 <edwardk> the main scenario where this split is useful is that you might import only transformers if you want to provide instances for your own class for its data types, rather than import all of mtl.
2024-06-20 15:00:31 +0200 <edwardk> but this is pretty much a tiny wibble
2024-06-20 15:01:20 +0200 <andrewboltachev> so the idea is that I shouldn't implement MatchStatusT's MonadTrans instance?
2024-06-20 15:01:36 +0200 <edwardk> no. you should implement all the things
2024-06-20 15:02:41 +0200 <edwardk> let's look at that type for a sec.
2024-06-20 15:02:45 +0200 <edwardk> newtype MatchStatusT m a = MatchStatusT { runMatchStatusT :: ReaderT MatcherEnv m (MatchStatus a) }
2024-06-20 15:03:10 +0200 <edwardk> ok, so you have a readerT, and some match status thing. i've literally never read this code before so give me a sec.
2024-06-20 15:03:42 +0200 <edwardk> data MatchStatus a = MatchSuccess a| MatchFailure T.Text| NoMatch T.Text deriving (Eq, Show)
2024-06-20 15:04:28 +0200 <edwardk> ok, so that is purely an error type. so this is basicaly ReaderT MatcherEnv (EitherT MatchFailure m) a
2024-06-20 15:04:38 +0200 <edwardk> for some notion of match failure that covers the two cases in matchstatus
2024-06-20 15:05:07 +0200 <andrewboltachev> so, yes. it's like Either but with extra state
2024-06-20 15:05:33 +0200 <mreh> did you intend MatchStatus to be at the bottom of the stack?
2024-06-20 15:05:36 +0200 <edwardk> now you have a couple of options. if you want the _user_ to be reaching into that MatcherEnv using ask/asks you can implement MonadReader for MatchStatusT. if you want the _user_ to be responding to failures and extracting that information you can implement MonadError
2024-06-20 15:06:29 +0200 <edwardk> and mreh has a good point. MatchStatus = MatchStatusT Identity is what one would expect, but you used it for the MatchResult type more or less
2024-06-20 15:07:45 +0200 <edwardk> if the stuff in the MatcherEnv is for 'you' and you expect it to be tricky for users to maintain its invariants it may make sense not to implement the MonadReader instance for it. because then you can implement MonadReader e (MatchStatusT m) for whatever m offers!
2024-06-20 15:07:49 +0200 <andrewboltachev> mreh: I'm not even sure
2024-06-20 15:08:19 +0200 <edwardk> the user can then ask/asks/local that rather than get tripped up by the fact that you have some administrative environmental stuff out in MatchStatusT
2024-06-20 15:08:50 +0200 <mreh> also should MatchStatusT even be a transformer? another question I would ask myself
2024-06-20 15:09:03 +0200 <mreh> you might already know the answer
2024-06-20 15:09:11 +0200 <edwardk> do you want users 'matching with monadic side-effects?'
2024-06-20 15:09:12 +0200 <mreh> (just asking :)
2024-06-20 15:09:28 +0200 <edwardk> e.g. running IO-actions that might launch missiles while you haven't even resolved the match
2024-06-20 15:09:51 +0200 <edwardk> what is the semantics you want to assign to matching, basically
2024-06-20 15:09:51 +0200 <andrewboltachev> print :-)
2024-06-20 15:10:03 +0200 <mreh> "my JSON doesn't match, time to turn on the coffee machine"
2024-06-20 15:10:10 +0200 <andrewboltachev> so btw
2024-06-20 15:10:17 +0200 <edwardk> you can include that in the mix, just be warned you're loading a footgun
2024-06-20 15:11:10 +0200 <andrewboltachev> https://www.dropbox.com/scl/fi/iyutvisq8v6arlj5ppuf8/2024-06-20-16-10-33.png?rlkey=ej84tfvumvfoh3w…
2024-06-20 15:11:47 +0200 <andrewboltachev> this is a "python code schema" that I made encoded as python code to match python code and extract patterns from it
2024-06-20 15:12:33 +0200 <edwardk> looks like you're building up a 'bigger and bigger' stuck term for all the elimination forms being applied to some initial stuck object, like one does in a normalization by evaluation interpreter
2024-06-20 15:13:15 +0200 <andrewboltachev> I also dealt with Figma files for example (yet the type is clear so there's not so much to match) but just as an example of big data structure (100s of MB) - I read/write some preliminary results into Redis for example
2024-06-20 15:13:28 +0200 <edwardk> want to see what a lambda does? pass this sort of thing in as an argument and see what the lambda does to the argument.
2024-06-20 15:13:58 +0200 <andrewboltachev> uhm
2024-06-20 15:15:05 +0200 <edwardk> andrewboltachev: https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf is a walkthrough of building something kind of similar for a simple lambda calculus implemented in haskell
2024-06-20 15:16:34 +0200 <andrewboltachev> interesting. I still thought that I'm building more like a... lens
2024-06-20 15:17:19 +0200 <mreh> you're talking to the right man
2024-06-20 15:18:39 +0200 <edwardk> if what you wrote is what i think you wrote, its like a big sticky ball of tar that any attempt to invoke it as a function gets turned into a bigger ball of tar that represents 'hey this is the result of calling that previous thing with this argument' or invoking && on it captures 'hey this is the result of calling && with some other argument on that base thing'. so if it gets returned as part of the result of a function it 'traces' what
2024-06-20 15:18:39 +0200 <edwardk> was done relative to the input to the function.
2024-06-20 15:19:14 +0200 <edwardk> chuck the ball of tar in, see what comes out stuck to it
2024-06-20 15:19:28 +0200 <edwardk> this is the essence of NBE ;)
2024-06-20 15:20:03 +0200 <edwardk> mreh: hah
2024-06-20 15:20:14 +0200 <andrewboltachev> aha. but the trick is, there's always some more theory
2024-06-20 15:20:59 +0200 <andrewboltachev> I'm in my spare time going through "Elementary categories elementary toposes" book and it doesn't seem to end very soon. 287 pages but ~500 theorems or so
2024-06-20 15:21:48 +0200 <edwardk> andrewboltachev: that's the good part. without more theory you are stuck inventing it all from scratch and you can miss good stuff! ;)
2024-06-20 15:22:25 +0200 <andrewboltachev> well, thanks :-) I'll keep that
2024-06-20 15:23:31 +0200 <andrewboltachev> pretty much the biggest theoretical discovery I made is that: (MatchStringExact "abc") (i.e. the "type" that only has one object) is a final object
2024-06-20 15:24:13 +0200 <edwardk> what are your morphisms?
2024-06-20 15:24:43 +0200 <andrewboltachev> well that's just like in Set
2024-06-20 15:25:03 +0200 <edwardk> so these are functions that take sets of strings to sets of strings?
2024-06-20 15:25:57 +0200 <andrewboltachev> Say, all the types of JSON (Aeson)
2024-06-20 15:26:14 +0200Pixi`(~Pixi@user/pixi)
2024-06-20 15:26:15 +0200 <andrewboltachev> (MatchStringExact "abc") is a set of one string
2024-06-20 15:27:04 +0200 <edwardk> or do you have something like a 'is more specific than' thing where a -> b shows json objet that would parse into 'a' should parse in 'b', which behaves kind of like set^op.
2024-06-20 15:27:46 +0200 <edwardk> the ltter is more like a powerset, which pushes you contravariant, and then breaks your current intution
2024-06-20 15:27:46 +0200 <andrewboltachev> this function that I have: https://github.com/andrewboltachev/matcher/blob/master/src/Logicore/Matcher/Core.hs#L1766 given a grammar (MatchPattern) is meant to eliminate the "static" part of that grammar...
2024-06-20 15:28:08 +0200 <andrewboltachev> static part of data*
2024-06-20 15:28:23 +0200Pixi`(~Pixi@user/pixi) (Read error: Connection reset by peer)
2024-06-20 15:28:48 +0200Pixi`(~Pixi@user/pixi)
2024-06-20 15:29:03 +0200Pixi(~Pixi@user/pixi) (Ping timeout: 260 seconds)
2024-06-20 15:29:25 +0200 <andrewboltachev> https://dpaste.com/DWWJLDHCC#wrap
2024-06-20 15:29:42 +0200 <andrewboltachev> that "w" aka whitespace is eliminated
2024-06-20 15:30:31 +0200Pixi__(~Pixi@user/pixi)
2024-06-20 15:32:30 +0200 <andrewboltachev> ah, sorry, this is the correct example: https://dpaste.com/4FPGJMZ7J#wrap
2024-06-20 15:34:17 +0200Pixi`(~Pixi@user/pixi) (Ping timeout: 252 seconds)
2024-06-20 15:34:29 +0200 <andrewboltachev> idea is that "b" is already "terminal object", so we can throw it away, and deal with "a" (provide another value for it) and then re-create the whole structure. the whitespace-like stuff is another beast I'm trying to support
2024-06-20 15:35:46 +0200 <andrewboltachev> so product of terminal objects is itself a terminal object ('cause when you multiply by 1 you got the same number)
2024-06-20 15:36:37 +0200 <andrewboltachev> and that's exactly what I have to eliminate (to write this function called `matchResultToThinValueFAlgebra` correctly)
2024-06-20 15:37:30 +0200 <andrewboltachev> thanks for help and support mreh edwardk :-)
2024-06-20 15:39:42 +0200caubert_(~caubert@user/caubert) (Read error: Connection reset by peer)
2024-06-20 15:40:02 +0200caubert(~caubert@user/caubert)
2024-06-20 15:49:33 +0200ocra8(~ocra8@user/ocra8)
2024-06-20 16:00:13 +0200ystael(~ystael@user/ystael)
2024-06-20 16:07:43 +0200 <mreh> andrewboltachev: np
2024-06-20 16:14:25 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
2024-06-20 16:18:13 +0200andrewboltachev(~andrey@178.141.121.180) (Quit: Leaving.)
2024-06-20 16:19:26 +0200euleritian(~euleritia@dynamic-176-007-169-090.176.7.pool.telefonica.de)
2024-06-20 16:22:03 +0200Sgeo(~Sgeo@user/sgeo)
2024-06-20 16:35:15 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds)
2024-06-20 16:41:44 +0200enoq(~enoq@2a05:1141:1e6:3b00:c958:a45e:c4e0:3650)
2024-06-20 16:42:30 +0200 <enoq> hi, so I was watching a Kotlin talk recently where they've mentioned that sum types have undecidability problems; is this inherent to sum types or just related to how OO languages design their type hyrarchies?
2024-06-20 16:45:18 +0200euleritian(~euleritia@dynamic-176-007-169-090.176.7.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-20 16:45:32 +0200mmohammadi9812(~mohammad@85.185.34.203)
2024-06-20 16:45:34 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-20 16:47:16 +0200soverysour(~soverysou@188.27.2.34)
2024-06-20 16:47:16 +0200soverysour(~soverysou@188.27.2.34) (Changing host)
2024-06-20 16:47:16 +0200soverysour(~soverysou@user/soverysour)
2024-06-20 16:49:54 +0200 <danse-nr3> sounds to me something related more to object-oriented hierarchies, but it's difficult to tell without more detail
2024-06-20 16:51:37 +0200 <dolio> Undecidability of what?
2024-06-20 16:51:52 +0200 <tomsmeding> haskell has no problems with sum types, but then haskell is not an OO language
2024-06-20 16:56:43 +0200 <sprout> most interesting type systems are undecidable
2024-06-20 16:56:50 +0200sproutlooks at system f
2024-06-20 16:57:12 +0200yin(~yin@user/zero)
2024-06-20 17:06:35 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2024-06-20 17:08:49 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-06-20 17:08:54 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Ping timeout: 268 seconds)
2024-06-20 17:09:56 +0200Pixi__(~Pixi@user/pixi) (Quit: Leaving)
2024-06-20 17:13:53 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2024-06-20 17:14:48 +0200chiselfuse(~chiselfus@user/chiselfuse)
2024-06-20 17:16:26 +0200 <drdo> enoq: decidability of what exactly?
2024-06-20 17:17:23 +0200 <enoq> I think they've mentioned something about polynomial runtime
2024-06-20 17:19:33 +0200 <EvanR> kotlin conf 2024 brochure says this apparently to elaborate on what "kotlin's type system is undecdiable" means: we can reliably cause the type-checker to stack overflow
2024-06-20 17:20:01 +0200 <EvanR> and it is unsound because "we can trick it into thinking a String is an Int"
2024-06-20 17:20:15 +0200 <dolio> That's a bit non-standard.
2024-06-20 17:21:01 +0200EvanRloads up some isomorphic javascript and escapes through it
2024-06-20 17:22:19 +0200Pixi(~Pixi@user/pixi)
2024-06-20 17:24:28 +0200cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-06-20 17:25:10 +0200danse-nr3(~danse-nr3@151.43.38.52) (Read error: Connection reset by peer)
2024-06-20 17:25:23 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 17:25:24 +0200 <EvanR> if something can be decided in polynomial time, that's highly non-undecidable
2024-06-20 17:26:23 +0200danse-nr3(~danse-nr3@151.43.0.225)
2024-06-20 17:26:37 +0200L29Ah(~L29Ah@wikipedia/L29Ah)
2024-06-20 17:27:51 +0200 <drdo> EvanR: did you throw that double negative in to confuse the intuitionists?
2024-06-20 17:29:19 +0200 <dolio> Intuitionists are the ones who aren't confused about double negatives. :)
2024-06-20 17:33:29 +0200 <EvanR> let the rhetorical purpose there be a free construction of the mind
2024-06-20 17:37:57 +0200 <dminuoso> Regarding type safety, if we take the TaPL definition, then "safety = progress + preservation", and confusing a String for an Int probably is a preservation violation
2024-06-20 17:39:11 +0200 <danse-nr3> resorting to the definition probably unnecessary in order to consider that unsafe
2024-06-20 17:39:25 +0200 <danse-nr3> well to /a/ definition
2024-06-20 17:40:26 +0200 <dminuoso> Well, I think to state "x is unsafe" requires some definition of what we mean by "unsafe" really.
2024-06-20 17:40:55 +0200 <danse-nr3> then i'll say "x is frown upon". Even works better these days
2024-06-20 17:41:10 +0200 <danse-nr3> *frowned
2024-06-20 17:42:47 +0200 <EvanR> they say it's unsound, which sounds like a logic thing not a programming thing
2024-06-20 17:43:12 +0200 <EvanR> like unsafe
2024-06-20 17:43:58 +0200 <dminuoso> EvanR: Again according to TaPL at least, soundness is in some circles a synonym for safety
2024-06-20 17:44:05 +0200 <EvanR> but I can imagine using suitable logic you can use the assumption that String = Int to prove 0 = 1 or False
2024-06-20 17:45:38 +0200igghibu(~igghibu@193.19.202.131)
2024-06-20 17:46:23 +0200igghibu(~igghibu@193.19.202.131) (Remote host closed the connection)
2024-06-20 17:46:52 +0200 <dolio> Type soundness is a programming thing.
2024-06-20 17:48:51 +0200 <dolio> In GHC, getting a String where you're expecting Ints might causes a segfault or something. In Kotlin it probably only causes some kind of runtime exception, but it's probably harder to debug than most errors.
2024-06-20 17:49:24 +0200 <dolio> It might not even be obvious where the problem is.
2024-06-20 17:50:09 +0200 <dolio> Segfault is if you're lucky in GHC, I guess. It might just do something wrong and leave you wondering why.
2024-06-20 17:55:59 +0200 <dminuoso> Bugs like Pentium FDIV make you wonder how many subtle errors are left in silicon, microcode, kernel code, or compilers that have not been detected but keep influencing your programs, perhaps especially in case of FDIV in ways that are hard to even notice.
2024-06-20 17:57:03 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-06-20 17:57:17 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 240 seconds)
2024-06-20 18:00:03 +0200Buggys(Buggys@shelltalk.net)
2024-06-20 18:01:12 +0200 <johnw_> what if FDIV results in Zombies being harder to kill in Left for Dead, so we simply evolved to become better zombie killers...
2024-06-20 18:08:29 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 240 seconds)
2024-06-20 18:09:17 +0200soverysour(~soverysou@user/soverysour)
2024-06-20 18:10:39 +0200lxsameer(lxsameer@Serene/lxsameer)
2024-06-20 18:15:57 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
2024-06-20 18:16:40 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-20 18:17:51 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 255 seconds)
2024-06-20 18:18:48 +0200Buggys(Buggys@shelltalk.net) (Quit: IRCNow and Forever!)
2024-06-20 18:19:15 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2024-06-20 18:20:08 +0200kyborg2011(~kyborg201@host-176-36-215-61.b024.la.net.ua)
2024-06-20 18:21:00 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643)
2024-06-20 18:24:07 +0200lxsameer(lxsameer@Serene/lxsameer) (Ping timeout: 246 seconds)
2024-06-20 18:24:41 +0200igghibu(~igghibu@193.19.202.131)
2024-06-20 18:25:48 +0200danse-nr3(~danse-nr3@151.43.0.225) (Ping timeout: 256 seconds)
2024-06-20 18:25:57 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 18:26:08 +0200chele(~chele@user/chele) (Remote host closed the connection)
2024-06-20 18:26:09 +0200lxsameer(~lxsameer@Serene/lxsameer)
2024-06-20 18:26:11 +0200CiaoSen(~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03)
2024-06-20 18:29:03 +0200igghibu(~igghibu@193.19.202.131) (Remote host closed the connection)
2024-06-20 18:30:02 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2024-06-20 18:30:22 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643)
2024-06-20 18:30:51 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 18:30:54 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2024-06-20 18:35:22 +0200danse-nr3(~danse-nr3@151.43.0.225)
2024-06-20 18:39:31 +0200dcoutts__(~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 246 seconds)
2024-06-20 18:40:51 +0200CiaoSen(~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03) (Ping timeout: 260 seconds)
2024-06-20 18:41:17 +0200madhavanmiui(~madhavanm@2409:40f4:28:9c68:8000::)
2024-06-20 18:41:24 +0200igghibu(~igghibu@146.70.225.113)
2024-06-20 18:42:15 +0200mmohammadi9812(~mohammad@85.185.34.203) (Ping timeout: 260 seconds)
2024-06-20 18:43:15 +0200yin(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-20 18:43:23 +0200igghibu(~igghibu@146.70.225.113) (Remote host closed the connection)
2024-06-20 18:43:40 +0200igghibu(~igghibu@146.70.225.113)
2024-06-20 18:43:44 +0200madhavanmiui(~madhavanm@2409:40f4:28:9c68:8000::) (Client Quit)
2024-06-20 18:47:30 +0200ubert(~Thunderbi@2a02:8109:ab8a:5a00:b0fb:c3f5:4666:ad2f) (Remote host closed the connection)
2024-06-20 18:47:40 +0200bontaq(~user@ool-45779c03.dyn.optonline.net)
2024-06-20 18:55:51 +0200yin(~yin@user/zero)
2024-06-20 19:02:56 +0200ft(~ft@p3e9bcb39.dip0.t-ipconnect.de)
2024-06-20 19:03:52 +0200igghibu(~igghibu@146.70.225.113) (Remote host closed the connection)
2024-06-20 19:08:50 +0200wootehfoot(~wootehfoo@user/wootehfoot)
2024-06-20 19:10:19 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 246 seconds)
2024-06-20 19:13:24 +0200Square(~Square@user/square)
2024-06-20 19:14:05 +0200yin(~yin@user/zero) (Remote host closed the connection)
2024-06-20 19:15:29 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 19:15:44 +0200enoq(~enoq@2a05:1141:1e6:3b00:c958:a45e:c4e0:3650) (Quit: Leaving)
2024-06-20 19:29:30 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-20 19:31:57 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-20 19:32:37 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 19:43:36 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 19:46:12 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2024-06-20 19:47:27 +0200simendsjo(~user@84.209.170.3)
2024-06-20 19:49:37 +0200philopsos1(~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net)
2024-06-20 19:52:32 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 19:52:33 +0200danse-nr3(~danse-nr3@151.43.0.225) (Quit: Leaving)
2024-06-20 19:53:14 +0200philopsos1(~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Client Quit)
2024-06-20 19:58:09 +0200philopsos1(~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net)
2024-06-20 20:01:02 +0200philopsos1(~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Client Quit)
2024-06-20 20:01:29 +0200philopsos1(~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net)
2024-06-20 20:02:10 +0200philopsos1(~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Changing host)
2024-06-20 20:02:10 +0200philopsos1(~caecilius@user/philopsos)
2024-06-20 20:02:49 +0200philopsos1(~caecilius@user/philopsos) (Client Quit)
2024-06-20 20:03:25 +0200philopsos1(~caecilius@user/philopsos)
2024-06-20 20:08:29 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915)
2024-06-20 20:10:09 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 272 seconds)
2024-06-20 20:11:26 +0200Lord_of_Life_Lord_of_Life
2024-06-20 20:13:57 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Quit: Lost terminal)
2024-06-20 20:14:32 +0200philopsos(~caecilius@user/philopsos) (Quit: Lost terminal)
2024-06-20 20:15:10 +0200soverysour(~soverysou@188.27.2.34)
2024-06-20 20:15:10 +0200soverysour(~soverysou@188.27.2.34) (Changing host)
2024-06-20 20:15:10 +0200soverysour(~soverysou@user/soverysour)
2024-06-20 20:17:40 +0200L29Ah(~L29Ah@wikipedia/L29Ah)
2024-06-20 20:19:00 +0200mmohammadi9812(~mohammad@85.185.34.203)
2024-06-20 20:19:48 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 20:21:23 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 252 seconds)
2024-06-20 20:23:46 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 20:31:19 +0200ocra8(~ocra8@user/ocra8) (Quit: WeeChat 4.3.2)
2024-06-20 20:40:25 +0200jrm(~jrm@user/jrm) (Ping timeout: 268 seconds)
2024-06-20 20:42:12 +0200target_i(~target_i@user/target-i/x-6023099)
2024-06-20 20:42:29 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-20 20:43:30 +0200jrm(~jrm@user/jrm)
2024-06-20 20:44:27 +0200wlhn(~wenzel@dl46fx8hbfttwvhb-h1ly-3.rev.dnainternet.fi) (Quit: Leaving)
2024-06-20 20:48:36 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 255 seconds)
2024-06-20 21:06:35 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds)
2024-06-20 21:08:34 +0200lxsameer(lxsameer@Serene/lxsameer)
2024-06-20 21:17:01 +0200lxsameer(lxsameer@Serene/lxsameer) (Ping timeout: 256 seconds)
2024-06-20 21:18:59 +0200lxsameer(~lxsameer@Serene/lxsameer)
2024-06-20 21:19:16 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds)
2024-06-20 21:20:24 +0200 <hadronized> I have a silly question; is there a range (expected range?) of the time a typicall GC collection can take?
2024-06-20 21:20:30 +0200 <hadronized> is there a upper boundary?
2024-06-20 21:21:00 +0200 <hadronized> like, if there are tons of free objects, is the GC interruptable to prevent having stopping the world for too long? and if not, is there a way to know the average-worst performance?
2024-06-20 21:21:08 +0200 <hadronized> is it within 1ms? 10ms? 100ms?
2024-06-20 21:22:53 +0200 <EvanR> there is --copying-gc and --nonmoving-gc which will get different latency characteristics
2024-06-20 21:23:31 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-20 21:23:41 +0200 <EvanR> the default copying gc will worst case take time proportional to how many live objects there are
2024-06-20 21:24:20 +0200 <EvanR> use profiling to see how much the time actually is
2024-06-20 21:27:42 +0200 <tomsmeding> also consider using the `+RTS -S` rts flag; it prints statistics about GC runtime when the process exits
2024-06-20 21:27:47 +0200 <hadronized> I just wanted to have a rough idea of what to expect
2024-06-20 21:28:14 +0200 <EvanR> write a program and tell us how it goes xD
2024-06-20 21:28:15 +0200 <tomsmeding> hadronized: it depends completely on the size of your heap
2024-06-20 21:28:30 +0200 <tomsmeding> if you never have more than 100 KB of data alive at a time, GC will be trivial
2024-06-20 21:28:51 +0200 <tomsmeding> if you have 30 GB of live data, GC will be very expensive, see if you can use compact regions or similar to alleviate trouble
2024-06-20 21:29:12 +0200 <hadronized> yeah
2024-06-20 21:29:26 +0200 <tomsmeding> (that is, live data that the GC has to traverse; a huge ByteString doesn't count because the GC sees "ok, here's a ByteString" and moves on)
2024-06-20 21:29:27 +0200 <hadronized> I’m trying to think whether it would be usable to make some graphics code to make a video game etc.
2024-06-20 21:29:35 +0200 <hadronized> since I really want to go back to what I used to do ~years ago (luminance)o
2024-06-20 21:29:36 +0200 <hadronized> -o
2024-06-20 21:30:35 +0200 <tomsmeding> the nonmoving GC would be better for that because it tries to keep GC latency low, at the expense of throughput (i.e. total amount of time spent in GC is higher, but most of it happens in parallel with your code)
2024-06-20 21:30:48 +0200 <EvanR> video games are possible, check out #haskell-game xD
2024-06-20 21:31:00 +0200 <hadronized> is lambdacube still a thing?
2024-06-20 21:31:03 +0200 <EvanR> intense CPU based graphics code, might be possible for very low rez framebuffer
2024-06-20 21:31:23 +0200 <tomsmeding> if you want to make a game with large amounts of data in-memory and a consistent, high frame rate, perhaps haskell is not the optimal language to make that in
2024-06-20 21:32:21 +0200 <tomsmeding> GC can easily take 10ms if you have GBs of data
2024-06-20 21:32:34 +0200andrewboltachev(~andrey@178.141.121.180)
2024-06-20 21:32:39 +0200 <tomsmeding> probably more
2024-06-20 21:32:41 +0200 <EvanR> there are ECS engines... I heard good things about Apecs
2024-06-20 21:32:51 +0200 <EvanR> probably overkill for your first attempt at a haskell game
2024-06-20 21:33:25 +0200 <EvanR> GB of truly dynamic data seems a bit nuts, usually games have huge amounts of static stuff loaded once
2024-06-20 21:33:34 +0200 <EvanR> triple A games
2024-06-20 21:33:43 +0200 <hadronized> yeah that sounds like a lot of data
2024-06-20 21:34:15 +0200 <hadronized> but if you have memory that sticks around (not garbage), even with tons of it, the GC shouldn’t have too much problem with that, right?
2024-06-20 21:34:17 +0200 <EvanR> I think performance isn't going to be first hurdle to writing games
2024-06-20 21:34:20 +0200 <EvanR> in haskell
2024-06-20 21:36:33 +0200 <tomsmeding> hadronized: the GC is going to traverse all that data every time, except if 1. it's memory of which the GC knows that it doesn't contain pointers, such as a ByteString, or 2. it's in a compact region (https://hackage.haskell.org/package/compact)
2024-06-20 21:37:04 +0200 <tomsmeding> if you use the (default) copying GC, (1.) has the further side condition that that memory must be pinned, otherwise it'll be copied anyway; a ByteString is pinned, but a Vector is not, for example
2024-06-20 21:37:46 +0200 <talismanick> Can `data Tree a = Tip a | Bin (Tree a) (Tree a)` be reformulated to avoid proving typeclass laws by cases + induction? Something to do with recursion schemes?
2024-06-20 21:38:38 +0200 <tomsmeding> which type classes?
2024-06-20 21:38:58 +0200 <EvanR> hadronized, for each ton of non garbage, the major collection cycle requires 1 millisecond per ton of time xD
2024-06-20 21:38:59 +0200 <talismanick> tomsmeding: Applicative thus far, but also Monad
2024-06-20 21:39:29 +0200 <talismanick> I wrote `(Tip f) <*> t = f <$> t` and `(Bin l r) <*> t = Bin (l <*> t) (r <*> t)`
2024-06-20 21:39:52 +0200 <tomsmeding> that's correct, I think
2024-06-20 21:40:11 +0200 <talismanick> proving interchange was easy enough with induction, but composition is a doozy
2024-06-20 21:40:12 +0200 <tomsmeding> general advice with this is: write pure (easy) and (>>=) (harder, but less chance of making mistakes), then define (<*>) = ap
2024-06-20 21:40:47 +0200 <talismanick> bind was `Tip x >>= f = f x` and `Bin l r >>= f = Bin (l >>= f) (r >>= f)`
2024-06-20 21:40:47 +0200 <tomsmeding> you'll find that there's really only one way to write (>>=) for your Tree
2024-06-20 21:40:54 +0200 <tomsmeding> indeed
2024-06-20 21:41:38 +0200 <tomsmeding> if you expand the definition of 'ap' and the calls to your (>>=) that it contains, you'll find out that it's equivalent to the (<*>) that you wrote
2024-06-20 21:42:00 +0200 <talismanick> so just prove the monad laws and leave it at that?
2024-06-20 21:42:27 +0200 <tomsmeding> there's no "standard" way to generate Monad instances for general tree-like data types (this is why there is no -XDeriveMonad), so it'll be hard to find some general construction that makes it come "for free"
2024-06-20 21:42:39 +0200 <tomsmeding> but this particular data type is very standard; you might be able to find it in a library
2024-06-20 21:42:41 +0200 <hadronized> it’s a bit discouraging :(
2024-06-20 21:42:59 +0200 <EvanR> hadronized, are you imagining bad gc performance for some reason?
2024-06-20 21:43:01 +0200 <EvanR> that's not healthy
2024-06-20 21:43:03 +0200 <tomsmeding> talismanick: yes, I'd just prove the monad laws for your (>>=); they imply the applicative laws
2024-06-20 21:43:07 +0200 <hadronized> EvanR: yeah
2024-06-20 21:43:11 +0200 <EvanR> lol
2024-06-20 21:43:16 +0200 <talismanick> tomsmeding: I don't mean a way to derive Monad (because that depends on Applicative, which depends on a choice of monoid)
2024-06-20 21:43:23 +0200 <hadronized> I mean, a decent video game today has to run at the v-sync of your screen
2024-06-20 21:43:25 +0200 <EvanR> that's like people can't write any C code because they thing malloc will be too slow
2024-06-20 21:43:26 +0200 <talismanick> I mean a way to factor out recursion/induction when proving laws
2024-06-20 21:43:29 +0200 <hadronized> my screen, for instance, runs at 165Hz
2024-06-20 21:43:52 +0200 <hadronized> so a whole frame has to be rendered in less than 6ms
2024-06-20 21:44:00 +0200 <hadronized> if a GC pause can take 10ms, that’s already done
2024-06-20 21:44:02 +0200 <EvanR> I recommend using opengl somehow so you utilize the GPU for graphics
2024-06-20 21:44:24 +0200 <EvanR> esp at 165 fps
2024-06-20 21:44:28 +0200 <hadronized> EvanR: I wrote luminance in Haskell years ago, and luminance in Rust using OpenGL, WebGL, Vulkan, etc.
2024-06-20 21:44:40 +0200 <hadronized> so yeah, I’m not saying the problem will be due to graphics technology
2024-06-20 21:44:41 +0200 <tomsmeding> talismanick: I mean, you can factor your data type as `newtype Fix f = In (f (Fix f)); data TreeF a r = TipF a | BinF r r; type Tree a = Fix (TreeF a)`
2024-06-20 21:44:44 +0200 <hadronized> but everything that revolve around it
2024-06-20 21:44:52 +0200 <talismanick> although it would be nice to be able to write "given this monoid, derive the corresponding Applicative/Monad instances"
2024-06-20 21:45:08 +0200 <tomsmeding> talismanick: what monoid do you mean? `join`?
2024-06-20 21:45:27 +0200 <tomsmeding> there are sometimes less valid Monad instances than there are valid Applicative instances for a type
2024-06-20 21:45:32 +0200m5zs7k(aquares@web10.mydevil.net) (Ping timeout: 252 seconds)
2024-06-20 21:45:33 +0200 <tomsmeding> so bunching them together like that doesn't sound right
2024-06-20 21:45:38 +0200 <tomsmeding> (to wit: [a])
2024-06-20 21:45:57 +0200 <talismanick> yeah, zipping is applicative but not monadic
2024-06-20 21:46:22 +0200 <talismanick> but I thought every monad instance depends on some underlying applicative, which itself depends on some underlying choice of monoid
2024-06-20 21:46:24 +0200 <EvanR> hadronized, yeah a hypothetical unsubstantiated data point was 10ms for a major collection because you have gigabytes of live heap for some reason
2024-06-20 21:46:42 +0200 <tomsmeding> talismanick: what monoid are you talking about there? (My category-fu is limited)
2024-06-20 21:46:42 +0200 <EvanR> note that most collections aren't major collections
2024-06-20 21:47:02 +0200 <EvanR> you can also time major collections yourself if there's a convenient place to do it, e.g. between levels
2024-06-20 21:47:20 +0200 <tomsmeding> if that happens often enough
2024-06-20 21:47:29 +0200 <talismanick> www.staff.city.ac.uk/~ross/papers/Applicative.pdf
2024-06-20 21:47:46 +0200m5zs7k(aquares@web10.mydevil.net)
2024-06-20 21:47:52 +0200 <ncf> starting to understand why Escardó says the Applicative => Monad thing was a pedagogical disaster...
2024-06-20 21:47:54 +0200 <EvanR> sure you just wouldn't want to switch levels then wait until sometime into the next level for a major GC "pause" (if there is one)
2024-06-20 21:47:59 +0200 <talismanick> see section 4, "Monoids are phantom Applicative functors"
2024-06-20 21:48:56 +0200 <ncf> a monad does not "depend" on a choice of underlying applicative; every Monad induces two Applicative structures, and there is a law that says that if a type implements Monad then it also has to implement Applicative with the first of those induced structures
2024-06-20 21:49:06 +0200 <tomsmeding> talismanick: doesn't that say that every Monoid induces an Applicative, not that every Applicative is based on a Monoid?
2024-06-20 21:49:28 +0200 <ncf> that section is just explaining the Monoid m => Applicative (Const m) instance
2024-06-20 21:49:41 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 240 seconds)
2024-06-20 21:49:57 +0200 <ncf> every monoid gives rise to an applicative this way (and to a monad via Writer), but that does not mean that every applicative (or monad) has an underlying Monoid
2024-06-20 21:50:10 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 21:50:10 +0200 <ncf> (it does have an underlying monoid object in some monoidal category but that's another story)
2024-06-20 21:50:16 +0200 <talismanick> isn't every applicative isomorphic to a monoidal functor?
2024-06-20 21:50:19 +0200 <ncf> yes
2024-06-20 21:50:27 +0200 <tomsmeding> that's a different monoid, though
2024-06-20 21:50:32 +0200 <talismanick> ah, I see
2024-06-20 21:50:33 +0200 <tomsmeding> that's `join`
2024-06-20 21:50:38 +0200 <tomsmeding> :t join
2024-06-20 21:50:39 +0200 <lambdabot> Monad m => m (m a) -> m a
2024-06-20 21:50:48 +0200 <ncf> join has little to do with monoidal functors
2024-06-20 21:50:52 +0200 <tomsmeding> oh oops
2024-06-20 21:51:22 +0200tomsmedingwill refrain from saying further falsehoods about category theory :p
2024-06-20 21:51:50 +0200 <EvanR> hadronized, you could also try existing commercial computer games that were written in haskell and see if run at 165 fps, if you're still skeptical
2024-06-20 21:52:10 +0200 <hadronized> is there any?!
2024-06-20 21:52:15 +0200 <EvanR> lol
2024-06-20 21:53:03 +0200 <EvanR> hmm https://magiccookies2.haskell.games/
2024-06-20 21:53:38 +0200 <talismanick> https://keera.co.uk/posts/2014/10/15/from-60-fps-to-500/
2024-06-20 21:54:38 +0200talismanicksees reference to gamedev in Haskell, greps chat log for references to FRP
2024-06-20 21:56:16 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 22:00:13 +0200va10323(~v324@2802:8010:a008:4700:4e6a:6189:b174:1928)
2024-06-20 22:00:58 +0200_xor(~xor@ip-208-102-243-175.dynamic.fuse.net) (Quit: Ping timeout (120 seconds))
2024-06-20 22:01:12 +0200_xor(~xor@ip-208-102-243-175.dynamic.fuse.net)
2024-06-20 22:04:59 +0200va10323(~v324@2802:8010:a008:4700:4e6a:6189:b174:1928) (Quit: Leaving)
2024-06-20 22:13:49 +0200 <cheater> i wish codex was up to date
2024-06-20 22:13:53 +0200 <cheater> cuz it's really good actually
2024-06-20 22:21:23 +0200rlj(~rlj@194-218-34-180.customer.telia.com)
2024-06-20 22:22:12 +0200rlj(~rlj@194-218-34-180.customer.telia.com) (Client Quit)
2024-06-20 22:25:39 +0200Guest|39(~Guest|39@160.178.51.69)
2024-06-20 22:27:10 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-20 22:37:59 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving)
2024-06-20 22:39:24 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-20 22:40:25 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303)
2024-06-20 22:46:38 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-06-20 22:46:57 +0200ystael(~ystael@user/ystael) (Quit: Lost terminal)
2024-06-20 22:50:23 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds)
2024-06-20 22:52:27 +0200simendsjo(~user@84.209.170.3) (Ping timeout: 264 seconds)
2024-06-20 22:53:05 +0200philopsos1(~caecilius@user/philopsos)
2024-06-20 22:53:47 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2024-06-20 22:55:29 +0200Guest|39(~Guest|39@160.178.51.69) (Ping timeout: 256 seconds)
2024-06-20 22:58:33 +0200Guest|86(~Guest|86@161.230.86.113)
2024-06-20 22:59:36 +0200ystael(~ystael@user/ystael)
2024-06-20 23:01:55 +0200Guest|86(~Guest|86@161.230.86.113) (Client Quit)
2024-06-20 23:02:33 +0200Guest|86(~Guest|86@161.230.86.113)
2024-06-20 23:02:39 +0200AlexZenon(~alzenon@178.34.162.224) (Ping timeout: 260 seconds)
2024-06-20 23:03:41 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2024-06-20 23:05:53 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-20 23:07:39 +0200mmohammadi9812(~mohammad@85.185.34.203) (Ping timeout: 255 seconds)
2024-06-20 23:08:03 +0200AlexZenon(~alzenon@178.34.162.224)
2024-06-20 23:10:54 +0200saus(~saus@pool-98-114-45-229.phlapa.fios.verizon.net)
2024-06-20 23:12:23 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Quit: Leaving)
2024-06-20 23:13:23 +0200AlexZenon(~alzenon@178.34.162.224) (Ping timeout: 260 seconds)
2024-06-20 23:14:04 +0200takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-06-20 23:17:48 +0200AlexZenon(~alzenon@178.34.162.224)
2024-06-20 23:23:08 +0200philopsos1(~caecilius@user/philopsos) (Quit: Lost terminal)
2024-06-20 23:23:27 +0200michalz(~michalz@185.246.207.218) (Quit: ZNC 1.9.0 - https://znc.in)
2024-06-20 23:24:05 +0200philopsos1(~caecilius@user/philopsos)
2024-06-20 23:24:13 +0200emmanuelux(~emmanuelu@user/emmanuelux)
2024-06-20 23:24:27 +0200Guest|86(~Guest|86@161.230.86.113) (Quit: Connection closed)
2024-06-20 23:24:43 +0200philopsos1(~caecilius@user/philopsos) (Client Quit)
2024-06-20 23:26:06 +0200philopsos1(~caecilius@user/philopsos)
2024-06-20 23:28:00 +0200EvanR(~EvanR@user/evanr) (Quit: Leaving)
2024-06-20 23:32:30 +0200EvanR(~EvanR@user/evanr)
2024-06-20 23:34:54 +0200saus(~saus@pool-98-114-45-229.phlapa.fios.verizon.net) (Quit: Client closed)
2024-06-20 23:46:42 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2024-06-20 23:55:58 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)