2024/06/13

2024-06-13 00:06:14 +0200mei(~mei@user/mei) (Remote host closed the connection)
2024-06-13 00:08:40 +0200mei(~mei@user/mei)
2024-06-13 00:11:18 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-06-13 00:17:58 +0200tabemann(~tabemann@syn-074-135-160-243.res.spectrum.com)
2024-06-13 00:18:09 +0200esph(~weechat@user/esph)
2024-06-13 00:18:39 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2024-06-13 00:36:23 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 00:36:39 +0200 <rustisafungus> would it be too offtopic to ask whether folks here are using jax?
2024-06-13 00:37:16 +0200 <rustisafungus> on a related note i saw a differentiable renderer somewhere commenting about laziness helping with differentiability of the program, but the commentary was above my reading level,... how do the two relate...?
2024-06-13 00:38:59 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-06-13 00:52:13 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 00:56:26 +0200wagle(~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.)
2024-06-13 00:56:43 +0200wagle(~wagle@quassel.wagle.io)
2024-06-13 00:56:44 +0200wagle(~wagle@quassel.wagle.io) (Client Quit)
2024-06-13 00:57:34 +0200wagle(~wagle@quassel.wagle.io)
2024-06-13 00:59:48 +0200philopsos1(~caecilius@user/philopsos)
2024-06-13 01:01:56 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex)
2024-06-13 01:04:11 +0200tabemann(~tabemann@syn-074-135-160-243.res.spectrum.com) (Ping timeout: 264 seconds)
2024-06-13 01:05:35 +0200wagle(~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.)
2024-06-13 01:06:25 +0200wagle(~wagle@quassel.wagle.io)
2024-06-13 01:10:11 +0200mei(~mei@user/mei) (Ping timeout: 264 seconds)
2024-06-13 01:10:58 +0200mei(~mei@user/mei)
2024-06-13 01:12:51 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 264 seconds)
2024-06-13 01:17:51 +0200oo_miguel(~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 260 seconds)
2024-06-13 01:21:58 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-06-13 01:23:17 +0200TonyStone(~TonyStone@user/TonyStone) (Ping timeout: 240 seconds)
2024-06-13 01:30:53 +0200dysthesis(~dysthesis@user/dysthesis)
2024-06-13 01:36:21 +0200TonyStone(~TonyStone@user/TonyStone)
2024-06-13 01:39:13 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542)
2024-06-13 01:48:15 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 01:56:20 +0200sprout_(~quassel@2a02-a448-3a80-0-bd5b-db91-763e-cf24.fixed6.kpn.net)
2024-06-13 01:57:31 +0200sprout(~quassel@84-80-106-227.fixed.kpn.net) (Ping timeout: 260 seconds)
2024-06-13 01:58:29 +0200vizimajac(vizimajac@shell.xshellz.com) (Ping timeout: 240 seconds)
2024-06-13 02:10:54 +0200vizimajac(vizimajac@shell.xshellz.com)
2024-06-13 02:12:08 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915)
2024-06-13 02:12:51 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds)
2024-06-13 02:13:29 +0200Lord_of_Life_Lord_of_Life
2024-06-13 02:14:13 +0200dcoutts(~duncan@212.140.138.201)
2024-06-13 02:14:17 +0200dcoutts(~duncan@212.140.138.201) (Remote host closed the connection)
2024-06-13 02:17:07 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 02:19:45 +0200emmanuelux_(~emmanuelu@user/emmanuelux)
2024-06-13 02:19:51 +0200tabemann(~tabemann@2600:1700:7990:24e0:f01:e94f:2e5:5d5d)
2024-06-13 02:20:42 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Ping timeout: 255 seconds)
2024-06-13 02:23:03 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 02:28:32 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 02:38:23 +0200Square2(~Square4@user/square) (Ping timeout: 264 seconds)
2024-06-13 02:56:18 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-06-13 02:57:25 +0200califax(~califax@user/califx)
2024-06-13 03:11:23 +0200ystael(~ystael@user/ystael) (Ping timeout: 252 seconds)
2024-06-13 03:13:36 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:909:ef37:664d:c6a7)
2024-06-13 03:21:19 +0200dev2(~dev@2405:201:c062:801d:4d6f:d1e8:5a8c:26e3) (Quit: WeeChat 4.3.2)
2024-06-13 03:44:25 +0200xff0x(~xff0x@2405:6580:b080:900:611b:282b:7bc2:c44f) (Ping timeout: 255 seconds)
2024-06-13 03:55:11 +0200krei-se(~krei-se@p57af2529.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
2024-06-13 03:55:11 +0200krei-se-(~krei-se@p5085de1f.dip0.t-ipconnect.de)
2024-06-13 03:59:39 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
2024-06-13 04:07:26 +0200y04nn(~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds)
2024-06-13 04:21:11 +0200dysthesis(~dysthesis@user/dysthesis) (Quit: dysthesis)
2024-06-13 04:30:27 +0200wagle(~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.)
2024-06-13 04:31:23 +0200wagle(~wagle@quassel.wagle.io)
2024-06-13 04:33:02 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-13 04:55:27 +0200td_(~td@i5387092E.versanet.de) (Ping timeout: 264 seconds)
2024-06-13 04:56:46 +0200td_(~td@i53870929.versanet.de)
2024-06-13 04:57:49 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 268 seconds)
2024-06-13 05:00:54 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 05:14:50 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:909:ef37:664d:c6a7) (Quit: Leaving)
2024-06-13 05:16:37 +0200tabemann(~tabemann@2600:1700:7990:24e0:f01:e94f:2e5:5d5d) (Ping timeout: 268 seconds)
2024-06-13 05:18:15 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 05:25:14 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2024-06-13 05:25:30 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 05:33:17 +0200whatsupdoc(uid509081@id-509081.hampstead.irccloud.com)
2024-06-13 05:38:18 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer)
2024-06-13 05:40:22 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds)
2024-06-13 05:40:58 +0200michalz(~michalz@185.246.207.203)
2024-06-13 05:40:59 +0200euleritian(~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de)
2024-06-13 05:42:48 +0200michalz(~michalz@185.246.207.203) (Client Quit)
2024-06-13 05:45:36 +0200michalz(~michalz@185.246.207.201)
2024-06-13 05:45:41 +0200aforemny_(~aforemny@i59F516D7.versanet.de)
2024-06-13 05:46:48 +0200aforemny(~aforemny@2001:9e8:6cf6:d100:13b7:91e0:122d:7bf6) (Ping timeout: 255 seconds)
2024-06-13 05:48:57 +0200philopsos1(~caecilius@user/philopsos)
2024-06-13 05:51:23 +0200danse-nr3(~danse-nr3@151.37.247.23)
2024-06-13 05:57:43 +0200 <haskellbridge> <James> Hello
2024-06-13 06:04:35 +0200 <Axman6> Hello!
2024-06-13 06:09:06 +0200 <Axman6> rustisafungus: What is jax?
2024-06-13 06:09:34 +0200 <Axman6> rustisafungus: There's quite a few talks out there on implementing differentiation in Haskell, maybe they would be helpful?
2024-06-13 06:19:18 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-13 06:35:36 +0200y04nn(~username@2a03:1b20:8:f011::e10d)
2024-06-13 06:38:53 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 240 seconds)
2024-06-13 06:39:44 +0200euleritian(~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-13 06:40:01 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-13 06:40:53 +0200danse-nr3(~danse-nr3@151.37.247.23) (Ping timeout: 240 seconds)
2024-06-13 06:50:43 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Ping timeout: 255 seconds)
2024-06-13 06:54:03 +0200danse-nr3(~danse-nr3@151.37.247.23)
2024-06-13 06:54:39 +0200andrei_n(~andrei_n@2a02:a03f:c091:a800:2023:eb80:7e75:618b)
2024-06-13 06:54:39 +0200andrei_n(~andrei_n@2a02:a03f:c091:a800:2023:eb80:7e75:618b) (Changing host)
2024-06-13 06:54:39 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-13 06:54:57 +0200danse-nr3(~danse-nr3@151.37.247.23) (Remote host closed the connection)
2024-06-13 06:55:21 +0200danse-nr3(~danse-nr3@151.37.247.23)
2024-06-13 07:05:15 +0200alexherbo2(~alexherbo@2a02-8440-3301-9f46-013f-12cf-5855-af6b.rev.sfr.net)
2024-06-13 07:05:56 +0200 <rustisafungus> Axman6: jax is google's machine learning framework, like pytorch... although jax is python based it demands that you write pure functions
2024-06-13 07:08:12 +0200philopsos1(~caecilius@user/philopsos)
2024-06-13 07:11:11 +0200tomku(~tomku@user/tomku) (Ping timeout: 252 seconds)
2024-06-13 07:30:02 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-06-13 07:33:54 +0200TheCoffeMaker_(~TheCoffeM@200.114.213.75) (Ping timeout: 255 seconds)
2024-06-13 07:42:33 +0200TheCoffeMaker(~TheCoffeM@user/thecoffemaker)
2024-06-13 07:44:19 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds)
2024-06-13 07:45:08 +0200euleritian(~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de)
2024-06-13 07:46:31 +0200acidjnk(~acidjnk@p200300d6e714dc24101446769eacf81f.dip0.t-ipconnect.de)
2024-06-13 07:53:23 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 07:58:19 +0200rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2024-06-13 07:58:52 +0200rvalue(~rvalue@user/rvalue)
2024-06-13 08:20:42 +0200 <[exa]> Axman6: kinda like accelerate, but in python
2024-06-13 08:21:00 +0200jcarpenter2(~lol@96.78.87.198) (Ping timeout: 268 seconds)
2024-06-13 08:25:19 +0200poscat(~poscat@user/poscat) (Ping timeout: 260 seconds)
2024-06-13 08:26:20 +0200echoreply(~echoreply@2001:19f0:9002:1f3b:5400:ff:fe6f:8b8d) (Quit: WeeChat 2.8)
2024-06-13 08:27:39 +0200echoreply(~echoreply@45.32.163.16)
2024-06-13 08:35:23 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-13 08:37:04 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-13 08:41:45 +0200poscat(~poscat@user/poscat)
2024-06-13 08:42:26 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-13 08:44:18 +0200jcarpenter2(~lol@96.78.87.198)
2024-06-13 08:46:26 +0200causal(~eric@50.35.88.207) (Quit: WeeChat 4.3.1)
2024-06-13 08:49:02 +0200 <danse-nr3> kinda like pytorch, without side effects?
2024-06-13 08:50:32 +0200ft(~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving)
2024-06-13 08:54:40 +0200robobub(uid248673@id-248673.uxbridge.irccloud.com)
2024-06-13 08:56:26 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 256 seconds)
2024-06-13 09:10:58 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net)
2024-06-13 09:12:27 +0200euleritian(~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-13 09:12:44 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-13 09:15:45 +0200oo_miguel(~Thunderbi@78-11-181-16.static.ip.netia.com.pl)
2024-06-13 09:16:15 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-06-13 09:16:27 +0200danse-nr3(~danse-nr3@151.37.247.23) (Ping timeout: 264 seconds)
2024-06-13 09:17:07 +0200danse-nr3(~danse-nr3@151.35.245.71)
2024-06-13 09:17:26 +0200califax(~califax@user/califx)
2024-06-13 09:17:41 +0200mjacob(~mjacob@adrastea.uberspace.de) (Read error: Connection reset by peer)
2024-06-13 09:22:47 +0200mjacob(~mjacob@adrastea.uberspace.de)
2024-06-13 09:31:52 +0200CiaoSen(~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03)
2024-06-13 09:31:52 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-06-13 09:33:28 +0200califax(~califax@user/califx)
2024-06-13 09:48:00 +0200tomku(~tomku@syn-141-126-184-057.res.spectrum.com)
2024-06-13 09:48:11 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 09:53:09 +0200gmg(~user@user/gehmehgeh)
2024-06-13 09:54:12 +0200takuan(~takuan@178-116-218-225.access.telenet.be)
2024-06-13 09:58:22 +0200danse-nr3(~danse-nr3@151.35.245.71) (Ping timeout: 246 seconds)
2024-06-13 09:58:22 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-13 09:59:29 +0200notzmv(~daniel@user/notzmv) (Ping timeout: 272 seconds)
2024-06-13 10:00:06 +0200tomku(~tomku@syn-141-126-184-057.res.spectrum.com) (Remote host closed the connection)
2024-06-13 10:00:17 +0200danse-nr3(~danse-nr3@151.35.245.71)
2024-06-13 10:00:20 +0200tomku(~tomku@syn-141-126-184-057.res.spectrum.com)
2024-06-13 10:02:00 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be)
2024-06-13 10:04:27 +0200CiaoSen(~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) (Ping timeout: 264 seconds)
2024-06-13 10:05:03 +0200danse-nr3(~danse-nr3@151.35.245.71) (Ping timeout: 264 seconds)
2024-06-13 10:08:54 +0200sprout_sprout
2024-06-13 10:10:28 +0200danza(~francesco@151.35.245.71)
2024-06-13 10:12:53 +0200y04nn(~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds)
2024-06-13 10:20:00 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 10:20:32 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 10:25:34 +0200danza(~francesco@151.35.245.71) (Ping timeout: 268 seconds)
2024-06-13 10:27:27 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 10:37:11 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 10:37:53 +0200lxsameer(~lxsameer@Serene/lxsameer)
2024-06-13 10:43:53 +0200Guest19(~Guest76@49.245.75.147)
2024-06-13 10:45:53 +0200danse-nr3(~danse-nr3@151.35.245.71)
2024-06-13 10:51:46 +0200danse-nr3(~danse-nr3@151.35.245.71) (Remote host closed the connection)
2024-06-13 10:52:07 +0200danse-nr3(~danse-nr3@151.35.245.71)
2024-06-13 10:54:13 +0200danse-nr3(~danse-nr3@151.35.245.71) (Remote host closed the connection)
2024-06-13 10:54:38 +0200danse-nr3(~danse-nr3@151.35.245.71)
2024-06-13 10:56:04 +0200nickiminjaj(~nickiminj@188.146.127.82)
2024-06-13 10:56:04 +0200nickiminjaj(~nickiminj@188.146.127.82) (Changing host)
2024-06-13 10:56:04 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 11:02:49 +0200sawilagar(~sawilagar@user/sawilagar)
2024-06-13 11:04:41 +0200chele(~chele@user/chele)
2024-06-13 11:08:58 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 11:11:17 +0200destituion(~destituio@77.18.53.84.tmi.telenormobil.no) (Read error: Connection reset by peer)
2024-06-13 11:12:17 +0200destituion(~destituio@85.221.111.174)
2024-06-13 11:17:22 +0200seeg123456(~seeg12345@64.176.64.83) (Ping timeout: 268 seconds)
2024-06-13 11:18:06 +0200cfricke(~cfricke@user/cfricke)
2024-06-13 11:21:56 +0200CiaoSen(~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03)
2024-06-13 11:31:31 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Ping timeout: 255 seconds)
2024-06-13 11:31:53 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2024-06-13 11:41:40 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-13 11:44:33 +0200andrei_n(~andrei_n@2a02:a03f:c091:a800:4cc9:832b:d3d8:de1c)
2024-06-13 11:44:33 +0200andrei_n(~andrei_n@2a02:a03f:c091:a800:4cc9:832b:d3d8:de1c) (Changing host)
2024-06-13 11:44:33 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-13 11:44:44 +0200akegalj(~akegalj@141-138-29-155.dsl.iskon.hr)
2024-06-13 11:49:38 +0200MironZ3(~MironZ@nat-infra.ehlab.uk) (Quit: The Lounge - https://thelounge.chat)
2024-06-13 11:50:13 +0200MironZ3(~MironZ@nat-infra.ehlab.uk)
2024-06-13 11:55:29 +0200__monty__(~toonn@user/toonn)
2024-06-13 11:59:54 +0200akegalj(~akegalj@141-138-29-155.dsl.iskon.hr) (Quit: leaving)
2024-06-13 12:00:03 +0200nickiminjaj(~nickiminj@188.146.127.82)
2024-06-13 12:00:03 +0200nickiminjaj(~nickiminj@188.146.127.82) (Changing host)
2024-06-13 12:00:03 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 12:02:37 +0200Guest19(~Guest76@49.245.75.147) (Quit: Client closed)
2024-06-13 12:04:00 +0200econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-13 12:05:40 +0200 <kuribas> With types it's easy to verify that a field is used but doesn't exist.
2024-06-13 12:06:04 +0200 <kuribas> What about the opposite? For example you want to verify that a field that is passed to a REST api is actually used somewhere.
2024-06-13 12:09:48 +0200notzmv(~daniel@user/notzmv)
2024-06-13 12:15:51 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds)
2024-06-13 12:16:49 +0200absence(torgeihe@hildring.pvv.ntnu.no)
2024-06-13 12:17:43 +0200 <tomsmeding> kuribas: bind the individual fields to individual variables, and rely on an unused variable warning?
2024-06-13 12:18:35 +0200xdminsy(~xdminsy@117.147.70.212) (Quit: Konversation terminated!)
2024-06-13 12:18:55 +0200 <kuribas> tomsmeding: but you are not forced to put all fields in the record, no?
2024-06-13 12:20:13 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 12:21:21 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 272 seconds)
2024-06-13 12:22:58 +0200 <tomsmeding> ok I guess this depends on how you get the fields from the API
2024-06-13 12:23:20 +0200 <tomsmeding> at some point, in the beginning, there is a parser that gets all fields from the wire format
2024-06-13 12:23:40 +0200 <absence> I want to apply "f :: a -> m b" to an "a :: Maybe a" in a MaybeT context. Are there other options than "MaybeT (traverse f a)" or "lift . f =<< hoistMaybe a"? Both feel a bit finnicky, but maybe that can't be helped.
2024-06-13 12:24:57 +0200 <tomsmeding> absence: the "natural" thing would be 'f <$> a', of course, but that gives you a Maybe (m b) instead of an m (Maybe b)
2024-06-13 12:25:10 +0200 <tomsmeding> and monads cannot be commuted in general
2024-06-13 12:25:27 +0200alexherbo2(~alexherbo@2a02-8440-3301-9f46-013f-12cf-5855-af6b.rev.sfr.net) (Remote host closed the connection)
2024-06-13 12:25:32 +0200 <tomsmeding> specifically in the case of Maybe you can, but you have to use something Maybe-specific
2024-06-13 12:25:55 +0200 <tomsmeding> with your 'traverse' alternative, the Maybe-specific thing you're using is that Maybe is not only a Monad, but also Traversable
2024-06-13 12:26:03 +0200 <tomsmeding> with the second alternative, well, you're using hoistMaybe
2024-06-13 12:26:18 +0200 <tomsmeding> there will always be something
2024-06-13 12:28:52 +0200 <ncf> what's an "MaybeT context"?
2024-06-13 12:29:33 +0200 <absence> tomsmeding: Right. Since MaybeT is also Maybe specific, I was hoping there were other clever options, but possibly they would have to amount to something similar.
2024-06-13 12:30:20 +0200 <absence> ncf: The result of applying the function should be of type "MaybeT m b".
2024-06-13 12:30:38 +0200 <tomsmeding> ncf: presumably they're in a do-block in the 'MaybeT m' monad
2024-06-13 12:32:22 +0200 <ncf> hmm
2024-06-13 12:33:13 +0200 <ncf> i'd go with the hoistMaybe thing probably
2024-06-13 12:33:16 +0200 <tomsmeding> this also has the right type: MaybeT (return a) >>= MaybeT . fmap Just . f
2024-06-13 12:33:22 +0200 <tomsmeding> more verbose than all the other alternatives
2024-06-13 12:33:25 +0200 <tomsmeding> but I guess more principled?
2024-06-13 12:33:36 +0200 <ncf> meh, you've just inlined lift and hoistMaybe
2024-06-13 12:33:40 +0200 <tomsmeding> maybe :p
2024-06-13 12:44:29 +0200Square2(~Square4@user/square)
2024-06-13 12:50:03 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Ping timeout: 264 seconds)
2024-06-13 12:59:50 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-13 13:01:18 +0200 <lortabac> kuribas: import the fields explicitly instead of using the (..) syntax, so you get unused warnings
2024-06-13 13:05:34 +0200 <kuribas> lortabac: If I do Foo{bar}, I don't get a warning if I add "baz", no?
2024-06-13 13:06:12 +0200 <lortabac> ah I was thinking in the opposite sense
2024-06-13 13:07:15 +0200 <lortabac> I mean you already know all the fields, you just want to ensure that they are used in that module
2024-06-13 13:07:45 +0200 <tomsmeding> kuribas: don't use record syntax in the pattern match
2024-06-13 13:07:59 +0200 <tomsmeding> you lose labels but you get a name resolution error if the number of fields changes
2024-06-13 13:08:02 +0200 <kuribas> tomsmeding: positional? That sucks.
2024-06-13 13:08:06 +0200 <tomsmeding> fair
2024-06-13 13:08:13 +0200 <tomsmeding> haskell records suck :p
2024-06-13 13:08:17 +0200 <kuribas> true
2024-06-13 13:08:47 +0200 <lortabac> to be honest this looks like a simple warning to add
2024-06-13 13:09:39 +0200 <kuribas> like a pragma CompleteRecordFields?
2024-06-13 13:09:49 +0200 <lortabac> yes
2024-06-13 13:10:21 +0200 <tomsmeding> where would the pragma be added? On the record or on the match
2024-06-13 13:10:23 +0200 <tomsmeding> ?
2024-06-13 13:10:28 +0200 <kuribas> On the module?
2024-06-13 13:10:30 +0200 <lortabac> it's probably only useful in rare specific cases, so I wouldn't enable it in -Wall
2024-06-13 13:10:30 +0200 <tomsmeding> bad
2024-06-13 13:10:38 +0200 <kuribas> ok :)
2024-06-13 13:10:55 +0200 <tomsmeding> we need less of these things that apply gratuitously to everything once you want them for one particular case :p
2024-06-13 13:11:15 +0200 <tomsmeding> -Worphans, RebindableSyntax, Overloaded*
2024-06-13 13:11:29 +0200 <lortabac> tomsmeding: +1
2024-06-13 13:11:37 +0200 <Rembane> Worphans is the best word.
2024-06-13 13:11:46 +0200 <tomsmeding> :D
2024-06-13 13:11:51 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-13 13:12:06 +0200 <tomsmeding> I cannot read that as anything else than -W orphans, I guess I learned C before I learned English
2024-06-13 13:13:18 +0200danse-nr3(~danse-nr3@151.35.245.71) (Read error: Connection reset by peer)
2024-06-13 13:13:38 +0200danse-nr3(~danse-nr3@151.43.251.36)
2024-06-13 13:20:12 +0200xff0x(~xff0x@2405:6580:b080:900:1910:1409:8fe6:7f05)
2024-06-13 13:20:46 +0200 <Rembane> tomsmeding: There's a joke here involving &humor in C, but I can't spell it out.
2024-06-13 13:24:26 +0200 <int-e> I don't get the reference.
2024-06-13 13:24:58 +0200 <Rembane> It's probably not initialized. UB! :O
2024-06-13 13:25:18 +0200 <int-e> (C doesn't have references :-P)
2024-06-13 13:26:51 +0200 <Rembane> This is true, but isn't it possible to reference something using the ampersand?
2024-06-13 13:27:41 +0200 <int-e> You'd get a pointer.
2024-06-13 13:28:37 +0200 <Rembane> That's true, my joke totally failed. :D
2024-06-13 13:29:04 +0200 <Rembane> It's "dereferencing", so uh... yeah...
2024-06-13 13:42:10 +0200 <mauke> C lets you dereference without having references; Java can throw a NullPointerException without having pointers
2024-06-13 13:44:39 +0200danse-nr3(~danse-nr3@151.43.251.36) (Ping timeout: 264 seconds)
2024-06-13 13:46:01 +0200 <ncf> pointers are an implementation of references
2024-06-13 13:51:37 +0200 <Rembane> mauke: Programming languages are weird. It's the Saphire Worphan hypothesis all over again!
2024-06-13 13:54:32 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 14:01:48 +0200Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 255 seconds)
2024-06-13 14:04:42 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 14:09:22 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 14:13:28 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-13 14:14:18 +0200danse-nr3(~danse-nr3@151.43.251.36)
2024-06-13 14:15:16 +0200danse-nr3(~danse-nr3@151.43.251.36) (Remote host closed the connection)
2024-06-13 14:15:40 +0200danse-nr3(~danse-nr3@151.43.251.36)
2024-06-13 14:23:42 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2024-06-13 14:23:50 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 14:28:41 +0200Maxdamantus(~Maxdamant@user/maxdamantus)
2024-06-13 14:34:19 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 14:45:03 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
2024-06-13 14:47:41 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 14:48:07 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 14:50:07 +0200Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 268 seconds)
2024-06-13 14:58:38 +0200rosco(~rosco@175.136.155.137)
2024-06-13 15:00:15 +0200nickiminjaj_(~nickiminj@user-5-173-188-100.play-internet.pl)
2024-06-13 15:00:15 +0200nickiminjaj_(~nickiminj@user-5-173-188-100.play-internet.pl) (Changing host)
2024-06-13 15:00:15 +0200nickiminjaj_(~nickiminj@user/laxhh)
2024-06-13 15:04:27 +0200nickiminjaj(~nickiminj@user/laxhh) (Ping timeout: 264 seconds)
2024-06-13 15:08:37 +0200someone235(uid419897@id-419897.ilkley.irccloud.com)
2024-06-13 15:09:50 +0200nickiminjaj_(~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-06-13 15:11:50 +0200Maxdamantus(~Maxdamant@user/maxdamantus)
2024-06-13 15:22:40 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 15:24:35 +0200nickiminjaj(~nickiminj@user/laxhh) (Client Quit)
2024-06-13 15:25:42 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal)
2024-06-13 15:25:48 +0200ystael(~ystael@user/ystael)
2024-06-13 15:27:33 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Quit: Leaving)
2024-06-13 15:32:05 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 15:35:59 +0200nickiminjaj(~nickiminj@user/laxhh) (Client Quit)
2024-06-13 15:38:03 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 15:42:25 +0200 <danse-nr3> @hoogle Maybe (a -> Maybe b) -> a -> Maybe b
2024-06-13 15:42:26 +0200 <lambdabot> Util apMA :: Monad m => m (a -> m b) -> a -> m b
2024-06-13 15:43:44 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-06-13 15:44:06 +0200 <danse-nr3> doesn't seem to be a thing at https://hoogle.haskell.org/?hoogle=Maybe%20(a%20-%3E%20Maybe%20b)%20-%3E%20a%20-%3E%20Maybe%20b
2024-06-13 15:45:49 +0200TactfulCitrus(~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047)
2024-06-13 15:47:19 +0200brett48(~brett48@cpc91312-watf11-2-0-cust1213.15-2.cable.virginm.net)
2024-06-13 15:48:58 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
2024-06-13 15:49:40 +0200 <danse-nr3> so i am not sure from which package does that Util come
2024-06-13 15:50:50 +0200euleritian(~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de)
2024-06-13 15:50:55 +0200 <tomsmeding> danse-nr3: https://hackage.haskell.org/package/util-0.1.17.1/docs/Util.html
2024-06-13 15:51:08 +0200 <tomsmeding> the description of that package is "Deprecated"
2024-06-13 15:51:41 +0200 <danse-nr3> thanks tomsmeding!
2024-06-13 15:52:43 +0200 <danse-nr3> this signature is too weird anyways i hope to get to something simpler eventually
2024-06-13 15:53:55 +0200 <tomsmeding> :t (join .) . fmap . flip id
2024-06-13 15:53:56 +0200 <lambdabot> Monad m => b -> m (b -> m a) -> m a
2024-06-13 15:55:00 +0200gdl_(~gdl__@mob-5-91-23-178.net.vodafone.it)
2024-06-13 15:55:08 +0200 <danse-nr3> ^^; a bit of type-fu. Kind of spoiled the fun but still appreciated
2024-06-13 15:55:21 +0200 <gdl_> Hi all! Just updated to vscode 1.90 and HLS seems not to be working at all :(
2024-06-13 15:59:54 +0200euleritian(~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-13 16:00:13 +0200euleritian(~euleritia@77.22.252.56)
2024-06-13 16:04:09 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 16:04:19 +0200 <danse-nr3> not sure gdl_ not using neither vscode nor HLS
2024-06-13 16:04:27 +0200 <gdl_> manually downgrading to vscode 1.89 works as a quick fix... Any hint on where to report this?
2024-06-13 16:05:39 +0200Square2(~Square4@user/square) (Ping timeout: 264 seconds)
2024-06-13 16:05:39 +0200 <EvanR> maybe there is an HLS channel here
2024-06-13 16:05:56 +0200 <EvanR> yay breakage
2024-06-13 16:06:13 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-06-13 16:06:35 +0200nickiminjaj(~nickiminj@user/laxhh) (Client Quit)
2024-06-13 16:07:12 +0200euleritian(~euleritia@77.22.252.56) (Ping timeout: 268 seconds)
2024-06-13 16:07:49 +0200 <ncf> :t (=<<) . (&)
2024-06-13 16:07:51 +0200 <lambdabot> Monad m => a -> m (a -> m b) -> m b
2024-06-13 16:08:13 +0200TactfulCitrus(~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection)
2024-06-13 16:09:24 +0200TactfulCitrus(~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047)
2024-06-13 16:09:37 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 255 seconds)
2024-06-13 16:09:57 +0200califax(~califax@user/califx)
2024-06-13 16:10:32 +0200euleritian(~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de)
2024-06-13 16:10:54 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-13 16:11:07 +0200 <tomsmeding> #haskell-language-server
2024-06-13 16:11:25 +0200 <tomsmeding> gdl_: try there, but they may redirect you elsewhere again
2024-06-13 16:14:13 +0200 <gdl_> thank you :)
2024-06-13 16:17:14 +0200 <danse-nr3> ooh, the (=<<) . (&) solution looks more meaningful to me
2024-06-13 16:17:59 +0200 <danse-nr3> in fact it's kind of explaining the uncanny-valley feeling i had about that type
2024-06-13 16:18:33 +0200TactfulCitrus(~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection)
2024-06-13 16:21:26 +0200ChaiTRex(~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds)
2024-06-13 16:22:18 +0200TactfulCitrus(~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047)
2024-06-13 16:23:38 +0200ChaiTRex(~ChaiTRex@user/chaitrex)
2024-06-13 16:26:44 +0200eron(~eron@179.98.163.50)
2024-06-13 16:30:38 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds)
2024-06-13 16:38:13 +0200eron(~eron@179.98.163.50) (Ping timeout: 250 seconds)
2024-06-13 16:38:31 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 16:44:39 +0200destituion(~destituio@85.221.111.174) (Ping timeout: 264 seconds)
2024-06-13 16:49:22 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 16:51:14 +0200TactfulCitrus(~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection)
2024-06-13 16:53:00 +0200destituion(~destituio@2a02:2121:306:89fe:6583:236:fa09:18d5)
2024-06-13 16:55:11 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 16:55:29 +0200k_hachig(~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca)
2024-06-13 16:57:56 +0200nickiminjaj(~nickiminj@user/laxhh) (Quit: Textual IRC Client: www.textualapp.com)
2024-06-13 16:58:09 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 17:03:45 +0200nickiminjaj(~nickiminj@user/laxhh)
2024-06-13 17:06:46 +0200picnoir(~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Ping timeout: 255 seconds)
2024-06-13 17:07:10 +0200noctux(~noctux@user/noctux) (Read error: Connection reset by peer)
2024-06-13 17:11:03 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 264 seconds)
2024-06-13 17:11:56 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net)
2024-06-13 17:13:50 +0200weechatdminuoso
2024-06-13 17:15:21 +0200danse-nr3(~danse-nr3@151.43.251.36) (Read error: Connection reset by peer)
2024-06-13 17:15:39 +0200danse-nr3(~danse-nr3@151.47.241.29)
2024-06-13 17:17:16 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf)
2024-06-13 17:24:05 +0200noctux(~noctux@user/noctux)
2024-06-13 17:26:46 +0200mauke(~mauke@user/mauke) (Read error: Connection reset by peer)
2024-06-13 17:29:19 +0200ames(~amelia@offtopia/offtopian/amelia)
2024-06-13 17:32:25 +0200ames(~amelia@offtopia/offtopian/amelia) (Client Quit)
2024-06-13 17:32:33 +0200mauke(~mauke@user/mauke)
2024-06-13 17:32:34 +0200ames(~amelia@offtopia/offtopian/amelia)
2024-06-13 17:33:54 +0200ames(~amelia@offtopia/offtopian/amelia) (Client Quit)
2024-06-13 17:35:39 +0200ames(~amelia@offtopia/offtopian/amelia)
2024-06-13 17:42:38 +0200puke(~puke@user/puke)
2024-06-13 17:42:42 +0200Sgeo(~Sgeo@user/sgeo)
2024-06-13 17:42:57 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-13 17:48:11 +0200euleritian(~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-13 17:48:28 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-13 17:51:13 +0200cyphase(~cyphase@user/cyphase) (Ping timeout: 246 seconds)
2024-06-13 17:51:56 +0200chele(~chele@user/chele) (Remote host closed the connection)
2024-06-13 17:52:12 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 255 seconds)
2024-06-13 17:52:45 +0200picnoir(~picnoir@about/aquilenet/vodoo/NinjaTrappeur)
2024-06-13 17:58:59 +0200someone235(uid419897@id-419897.ilkley.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-13 18:01:54 +0200CiaoSen(~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds)
2024-06-13 18:03:02 +0200szkl(uid110435@id-110435.uxbridge.irccloud.com)
2024-06-13 18:03:15 +0200danse-nr3(~danse-nr3@151.47.241.29) (Ping timeout: 264 seconds)
2024-06-13 18:11:55 +0200yin(~yin@user/zero)
2024-06-13 18:12:01 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
2024-06-13 18:12:33 +0200haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
2024-06-13 18:14:26 +0200gdl_(~gdl__@mob-5-91-23-178.net.vodafone.it) (Remote host closed the connection)
2024-06-13 18:18:38 +0200haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com)
2024-06-13 18:18:38 +0200ChanServ+v haskellbridge
2024-06-13 18:19:50 +0200danse-nr3(~danse-nr3@151.47.241.29)
2024-06-13 18:22:43 +0200cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-06-13 18:23:26 +0200danse-nr3(~danse-nr3@151.47.241.29) (Remote host closed the connection)
2024-06-13 18:34:22 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-06-13 18:40:54 +0200califax(~califax@user/califx)
2024-06-13 18:47:07 +0200hueso(~root@user/hueso) (Ping timeout: 255 seconds)
2024-06-13 18:49:17 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-13 18:53:39 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
2024-06-13 18:54:59 +0200euleritian(~euleritia@dynamic-176-003-011-033.176.3.pool.telefonica.de)
2024-06-13 18:58:27 +0200rdcdr(~rdcdr@user/rdcdr) (Ping timeout: 264 seconds)
2024-06-13 18:58:54 +0200Me-me(~me-me@user/me-me) (Remote host closed the connection)
2024-06-13 18:59:21 +0200hueso(~root@user/hueso)
2024-06-13 18:59:28 +0200Me-me(~me-me@kc.randomserver.name)
2024-06-13 19:01:14 +0200euleritian(~euleritia@dynamic-176-003-011-033.176.3.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-13 19:01:31 +0200euleritian(~euleritia@77.22.252.56)
2024-06-13 19:01:47 +0200henry40408(~henry4040@175.182.111.183)
2024-06-13 19:04:07 +0200rdcdr(~rdcdr@user/rdcdr)
2024-06-13 19:14:36 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2024-06-13 19:15:14 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 19:16:36 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 19:17:50 +0200osogyian(~osogyian@2804:1b3:6603:6f0b:4dd2:8d4e:c6db:c6b7)
2024-06-13 19:19:53 +0200osogyian(~osogyian@2804:1b3:6603:6f0b:4dd2:8d4e:c6db:c6b7) ()
2024-06-13 19:22:27 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 19:28:17 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-06-13 19:39:17 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-13 19:42:51 +0200 <lxsameer> would it be possible to define a dependent type using type families?
2024-06-13 19:44:57 +0200 <EvanR> by promoting then reimplementing all the value level code for e.g. numbers, that is how you can go about getting dependentish types with type families
2024-06-13 19:45:02 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 19:45:39 +0200 <lxsameer> EvanR: got it. Thank you
2024-06-13 19:48:56 +0200ocra8(~ocra8@user/ocra8) (Read error: Connection reset by peer)
2024-06-13 19:53:47 +0200ocra8(~ocra8@user/ocra8)
2024-06-13 19:54:03 +0200 <haskellbridge> <sm> yikes, thanks for the heads up. Checking my VS Code updates are manual
2024-06-13 19:54:22 +0200ft(~ft@p3e9bcb39.dip0.t-ipconnect.de)
2024-06-13 19:59:41 +0200ocra8(~ocra8@user/ocra8) (Ping timeout: 240 seconds)
2024-06-13 20:00:59 +0200ocra8(~ocra8@user/ocra8)
2024-06-13 20:03:36 +0200brett48(~brett48@cpc91312-watf11-2-0-cust1213.15-2.cable.virginm.net) (Quit: brett48)
2024-06-13 20:05:35 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds)
2024-06-13 20:08:26 +0200califax_(~califax@user/califx)
2024-06-13 20:08:59 +0200Chai-T-Rex(~ChaiTRex@user/chaitrex)
2024-06-13 20:09:24 +0200gehmehgeh(~user@user/gehmehgeh)
2024-06-13 20:10:34 +0200califax(~califax@user/califx) (Ping timeout: 260 seconds)
2024-06-13 20:10:34 +0200gmg(~user@user/gehmehgeh) (Ping timeout: 260 seconds)
2024-06-13 20:10:35 +0200califax_califax
2024-06-13 20:11:02 +0200ChaiTRex(~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds)
2024-06-13 20:11:02 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds)
2024-06-13 20:12:29 +0200szkl(uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-13 20:12:53 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-13 20:15:32 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2024-06-13 20:17:41 +0200 <tomsmeding> lxsameer: aren't GADTs more the thing that you can get limited dependencies with?
2024-06-13 20:18:07 +0200 <tomsmeding> type families are restricted to the type level, and the "dependencies" of "dependent types" refer to types depending on terms
2024-06-13 20:18:58 +0200 <tomsmeding> with GADTs you can have types depend on GADT constructors, thus you do get actual _dependent_ types -- albeit limited to GADT constructors, not arbitrary values
2024-06-13 20:22:07 +0200 <lxsameer> got it. but in my understanding you can use type families that "depend" (loosly) on terms. right?
2024-06-13 20:22:50 +0200gehmehgehgmg
2024-06-13 20:22:54 +0200 <dolio> GADTs correspond to inductive families/indexed inductive types. But the indices are entirely at the type level for GADTs.
2024-06-13 20:23:46 +0200 <dolio> So they're not really like dependent types, still. You have to manually establish a correspondence between values and types.
2024-06-13 20:24:21 +0200 <EvanR> type families map types to types, but using DataKinds you can more conveniently clone value constructors to the type level to use for that
2024-06-13 20:24:42 +0200 <yin> what are the advantages of dependent types, performance-wise?
2024-06-13 20:24:49 +0200 <yin> if there are any
2024-06-13 20:24:58 +0200 <EvanR> at runtime there are no types, so none xD
2024-06-13 20:25:20 +0200 <dolio> In principle you have more detailed information for static analysis, but that is rarely actually realized.
2024-06-13 20:25:46 +0200 <yin> well, by using them the runtime will likely be different from when you don't use them, right?
2024-06-13 20:26:11 +0200 <EvanR> data families could have different runtime implementation at different indices
2024-06-13 20:26:12 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-06-13 20:26:23 +0200hueso(~root@user/hueso) (Ping timeout: 264 seconds)
2024-06-13 20:27:25 +0200 <EvanR> the main thing I've seen dependent types used for is guaranteeing properties and invariants before it all gets compiled away
2024-06-13 20:27:39 +0200 <yin> knowing your Int can only be < x must open the door to some memory management optimizations, i imagine
2024-06-13 20:28:09 +0200hueso(~root@user/hueso)
2024-06-13 20:28:20 +0200 <EvanR> using Fin X for numbers less than X (and greater than or equal to zero) likely performs WORSE, due to more naive implementation
2024-06-13 20:28:46 +0200 <EvanR> Int that is known to be within some range sounds more like liquid types
2024-06-13 20:29:02 +0200 <yin> well yeah bad example
2024-06-13 20:29:23 +0200 <dolio> I mean, you could detect and optimize.
2024-06-13 20:30:08 +0200 <dolio> Like, Agda's ℕ is in principle defined in unary, but it gets handled specially to use Haskell's Integer behind the scenes.
2024-06-13 20:31:17 +0200 <dolio> But, most dependently typed languages aren't in the business of doing stuff like that right now.
2024-06-13 20:33:24 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
2024-06-13 20:40:47 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 20:47:23 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 20:48:34 +0200rvalue(~rvalue@user/rvalue) (Remote host closed the connection)
2024-06-13 20:49:02 +0200rvalue(~rvalue@user/rvalue)
2024-06-13 20:52:02 +0200Square(~Square@user/square)
2024-06-13 21:03:00 +0200cyphase(~cyphase@user/cyphase)
2024-06-13 21:09:58 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 21:10:18 +0200Guest13(~Guest13@220.67.223.22)
2024-06-13 21:10:39 +0200foul_owl(~kerry@185.216.231.181) (Ping timeout: 255 seconds)
2024-06-13 21:10:50 +0200foul_owl(~kerry@174-21-146-130.tukw.qwest.net)
2024-06-13 21:11:02 +0200Guest13(~Guest13@220.67.223.22) (Client Quit)
2024-06-13 21:16:54 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 21:21:36 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds)
2024-06-13 21:23:51 +0200philopsos1(~caecilius@user/philopsos)
2024-06-13 21:25:01 +0200 <probie> Depending on your dependently typed language and how you "run" code, `Σ ℕ (λn → n < X)` may perform no worse than `ℕ` (e.g. in Coq with "run" meaning running code extracted to OCaml or Haskell), although I don't know of any where it performs better
2024-06-13 21:25:50 +0200noumenon(~noumenon@113.51-175-156.customer.lyse.net)
2024-06-13 21:29:44 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 252 seconds)
2024-06-13 21:30:01 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net)
2024-06-13 21:30:45 +0200 <probie> I think it'd be completely unexpected if a function with type `∀ {x y : ℕ} → x < y → Σ ℕ (λn → n < x) → Σ ℕ (λn → n < y)` were to change the representation of the first part of the pair if `y` was much bigger than `x`
2024-06-13 21:34:28 +0200target_i(~target_i@user/target-i/x-6023099)
2024-06-13 21:35:27 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 21:38:44 +0200 <tomsmeding> if one has evidence of the maximum value of a natural number, one might be able to eliminate bounds checks when using them as an index into arrays, for example
2024-06-13 21:38:51 +0200 <tomsmeding> thus they can improve performance in some cases
2024-06-13 21:39:33 +0200smalltalkman(uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-13 21:39:40 +0200 <tomsmeding> but that typically requires a careful setup, plus care that the proofs of those bounds (to satisfy the type checker that the bounds are indeed valid) do not require additional runtime code that more than negates the wins from eliminated bounds checks
2024-06-13 21:40:28 +0200 <dolio> I don't think it's that hard to see how it could effectively change the representation. Integer in GHC is either a word-sized thing or an arbitrary precision thing. So for small enough x, you can know that you will actually never have the arbitrary-precision thing.
2024-06-13 21:40:32 +0200 <tomsmeding> this can, I guess, be seen as a type theory implementation of what compiler writers (of languages with bounds checks) already do
2024-06-13 21:40:50 +0200 <dolio> Then you optimize everything with that type to only operate on word-sized things.
2024-06-13 21:42:34 +0200henry40408(~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds))
2024-06-13 21:42:59 +0200henry40408(~henry4040@175.182.111.183)
2024-06-13 21:43:04 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds)
2024-06-13 21:45:18 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-13 21:53:39 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds)
2024-06-13 21:59:22 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 22:06:26 +0200andrei_n(~andrei_n@user/andrei-n:62396)
2024-06-13 22:08:03 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-13 22:18:40 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 22:19:02 +0200mei(~mei@user/mei) (Remote host closed the connection)
2024-06-13 22:20:20 +0200hueso(~root@user/hueso) (Ping timeout: 252 seconds)
2024-06-13 22:20:47 +0200hueso(~root@user/hueso)
2024-06-13 22:21:28 +0200mei(~mei@user/mei)
2024-06-13 22:26:39 +0200andrei_n(~andrei_n@user/andrei-n:62396) (Ping timeout: 264 seconds)
2024-06-13 22:26:46 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds)
2024-06-13 22:38:10 +0200yin(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-13 22:38:55 +0200yin(~yin@user/zero)
2024-06-13 22:38:58 +0200causal(~eric@50.35.88.207)
2024-06-13 22:40:22 +0200k_hachig(~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca) (Ping timeout: 256 seconds)
2024-06-13 22:43:26 +0200yin(~yin@user/zero) (Ping timeout: 252 seconds)
2024-06-13 22:43:42 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-06-13 22:44:17 +0200yin(~yin@user/zero)
2024-06-13 22:44:39 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds)
2024-06-13 22:49:50 +0200rustisafungus(~segfaultf@23-93-189-95.fiber.dynamic.sonic.net)
2024-06-13 22:54:11 +0200k_hachig(~k_hachig@65.94.221.127)
2024-06-13 23:03:52 +0200michalz(~michalz@185.246.207.201) (Quit: ZNC 1.9.0 - https://znc.in)
2024-06-13 23:08:33 +0200opqdonut(opqdonut@pseudo.fixme.fi) (Ping timeout: 255 seconds)
2024-06-13 23:08:47 +0200Me-me(~me-me@kc.randomserver.name) (Changing host)
2024-06-13 23:08:47 +0200Me-me(~me-me@user/me-me)
2024-06-13 23:15:11 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-13 23:18:22 +0200sp1ff(~user@c-24-21-45-157.hsd1.wa.comcast.net) (Remote host closed the connection)
2024-06-13 23:21:18 +0200rvalue-(~rvalue@user/rvalue)
2024-06-13 23:22:01 +0200takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-06-13 23:22:34 +0200rvalue(~rvalue@user/rvalue) (Ping timeout: 268 seconds)
2024-06-13 23:25:17 +0200rvalue-rvalue
2024-06-13 23:28:26 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2024-06-13 23:35:32 +0200mei(~mei@user/mei) (Remote host closed the connection)
2024-06-13 23:37:54 +0200mei(~mei@user/mei)
2024-06-13 23:39:52 +0200sp1ff(~user@c-24-21-45-157.hsd1.wa.comcast.net)
2024-06-13 23:41:04 +0200euleritian(~euleritia@77.22.252.56) (Ping timeout: 268 seconds)
2024-06-13 23:41:29 +0200euleritian(~euleritia@dynamic-176-003-011-016.176.3.pool.telefonica.de)
2024-06-13 23:43:05 +0200k_hachig(~k_hachig@65.94.221.127) (Quit: WeeChat 4.3.2)
2024-06-13 23:44:13 +0200k_hachig(~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca)
2024-06-13 23:44:46 +0200AlexZenon(~alzenon@178.34.163.204) (Ping timeout: 268 seconds)
2024-06-13 23:44:54 +0200pavonia(~user@user/siracusa)
2024-06-13 23:53:37 +0200AlexZenon(~alzenon@178.34.163.204)
2024-06-13 23:55:09 +0200gabiruh_(~gabiruh@vps19177.publiccloud.com.br)
2024-06-13 23:56:02 +0200gabiruh(~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 252 seconds)