| 2024-06-13 00:06:14 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-06-13 00:08:40 +0200 | mei | (~mei@user/mei) |
| 2024-06-13 00:11:18 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-06-13 00:17:58 +0200 | tabemann | (~tabemann@syn-074-135-160-243.res.spectrum.com) |
| 2024-06-13 00:18:09 +0200 | esph | (~weechat@user/esph) |
| 2024-06-13 00:18:39 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-06-13 00:36:23 +0200 | rustisafungus | (~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 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-06-13 00:52:13 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 00:56:26 +0200 | wagle | (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-06-13 00:56:43 +0200 | wagle | (~wagle@quassel.wagle.io) |
| 2024-06-13 00:56:44 +0200 | wagle | (~wagle@quassel.wagle.io) (Client Quit) |
| 2024-06-13 00:57:34 +0200 | wagle | (~wagle@quassel.wagle.io) |
| 2024-06-13 00:59:48 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-13 01:01:56 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-06-13 01:04:11 +0200 | tabemann | (~tabemann@syn-074-135-160-243.res.spectrum.com) (Ping timeout: 264 seconds) |
| 2024-06-13 01:05:35 +0200 | wagle | (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-06-13 01:06:25 +0200 | wagle | (~wagle@quassel.wagle.io) |
| 2024-06-13 01:10:11 +0200 | mei | (~mei@user/mei) (Ping timeout: 264 seconds) |
| 2024-06-13 01:10:58 +0200 | mei | (~mei@user/mei) |
| 2024-06-13 01:12:51 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 264 seconds) |
| 2024-06-13 01:17:51 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 260 seconds) |
| 2024-06-13 01:21:58 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-06-13 01:23:17 +0200 | TonyStone | (~TonyStone@user/TonyStone) (Ping timeout: 240 seconds) |
| 2024-06-13 01:30:53 +0200 | dysthesis | (~dysthesis@user/dysthesis) |
| 2024-06-13 01:36:21 +0200 | TonyStone | (~TonyStone@user/TonyStone) |
| 2024-06-13 01:39:13 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2024-06-13 01:48:15 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 01:56:20 +0200 | sprout_ | (~quassel@2a02-a448-3a80-0-bd5b-db91-763e-cf24.fixed6.kpn.net) |
| 2024-06-13 01:57:31 +0200 | sprout | (~quassel@84-80-106-227.fixed.kpn.net) (Ping timeout: 260 seconds) |
| 2024-06-13 01:58:29 +0200 | vizimajac | (vizimajac@shell.xshellz.com) (Ping timeout: 240 seconds) |
| 2024-06-13 02:10:54 +0200 | vizimajac | (vizimajac@shell.xshellz.com) |
| 2024-06-13 02:12:08 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-06-13 02:12:51 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 2024-06-13 02:13:29 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2024-06-13 02:14:13 +0200 | dcoutts | (~duncan@212.140.138.201) |
| 2024-06-13 02:14:17 +0200 | dcoutts | (~duncan@212.140.138.201) (Remote host closed the connection) |
| 2024-06-13 02:17:07 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 02:19:45 +0200 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
| 2024-06-13 02:19:51 +0200 | tabemann | (~tabemann@2600:1700:7990:24e0:f01:e94f:2e5:5d5d) |
| 2024-06-13 02:20:42 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 255 seconds) |
| 2024-06-13 02:23:03 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 02:28:32 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 02:38:23 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 264 seconds) |
| 2024-06-13 02:56:18 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-06-13 02:57:25 +0200 | califax | (~califax@user/califx) |
| 2024-06-13 03:11:23 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2024-06-13 03:13:36 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:909:ef37:664d:c6a7) |
| 2024-06-13 03:21:19 +0200 | dev2 | (~dev@2405:201:c062:801d:4d6f:d1e8:5a8c:26e3) (Quit: WeeChat 4.3.2) |
| 2024-06-13 03:44:25 +0200 | xff0x | (~xff0x@2405:6580:b080:900:611b:282b:7bc2:c44f) (Ping timeout: 255 seconds) |
| 2024-06-13 03:55:11 +0200 | krei-se | (~krei-se@p57af2529.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-06-13 03:55:11 +0200 | krei-se- | (~krei-se@p5085de1f.dip0.t-ipconnect.de) |
| 2024-06-13 03:59:39 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 2024-06-13 04:07:26 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 2024-06-13 04:21:11 +0200 | dysthesis | (~dysthesis@user/dysthesis) (Quit: dysthesis) |
| 2024-06-13 04:30:27 +0200 | wagle | (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-06-13 04:31:23 +0200 | wagle | (~wagle@quassel.wagle.io) |
| 2024-06-13 04:33:02 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-06-13 04:55:27 +0200 | td_ | (~td@i5387092E.versanet.de) (Ping timeout: 264 seconds) |
| 2024-06-13 04:56:46 +0200 | td_ | (~td@i53870929.versanet.de) |
| 2024-06-13 04:57:49 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 268 seconds) |
| 2024-06-13 05:00:54 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 05:14:50 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:909:ef37:664d:c6a7) (Quit: Leaving) |
| 2024-06-13 05:16:37 +0200 | tabemann | (~tabemann@2600:1700:7990:24e0:f01:e94f:2e5:5d5d) (Ping timeout: 268 seconds) |
| 2024-06-13 05:18:15 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 05:25:14 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-06-13 05:25:30 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 05:33:17 +0200 | whatsupdoc | (uid509081@id-509081.hampstead.irccloud.com) |
| 2024-06-13 05:38:18 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer) |
| 2024-06-13 05:40:22 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-06-13 05:40:58 +0200 | michalz | (~michalz@185.246.207.203) |
| 2024-06-13 05:40:59 +0200 | euleritian | (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) |
| 2024-06-13 05:42:48 +0200 | michalz | (~michalz@185.246.207.203) (Client Quit) |
| 2024-06-13 05:45:36 +0200 | michalz | (~michalz@185.246.207.201) |
| 2024-06-13 05:45:41 +0200 | aforemny_ | (~aforemny@i59F516D7.versanet.de) |
| 2024-06-13 05:46:48 +0200 | aforemny | (~aforemny@2001:9e8:6cf6:d100:13b7:91e0:122d:7bf6) (Ping timeout: 255 seconds) |
| 2024-06-13 05:48:57 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-13 05:51:23 +0200 | danse-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 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) |
| 2024-06-13 06:35:36 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
| 2024-06-13 06:38:53 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 2024-06-13 06:39:44 +0200 | euleritian | (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-13 06:40:01 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-13 06:40:53 +0200 | danse-nr3 | (~danse-nr3@151.37.247.23) (Ping timeout: 240 seconds) |
| 2024-06-13 06:50:43 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Ping timeout: 255 seconds) |
| 2024-06-13 06:54:03 +0200 | danse-nr3 | (~danse-nr3@151.37.247.23) |
| 2024-06-13 06:54:39 +0200 | andrei_n | (~andrei_n@2a02:a03f:c091:a800:2023:eb80:7e75:618b) |
| 2024-06-13 06:54:39 +0200 | andrei_n | (~andrei_n@2a02:a03f:c091:a800:2023:eb80:7e75:618b) (Changing host) |
| 2024-06-13 06:54:39 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) |
| 2024-06-13 06:54:57 +0200 | danse-nr3 | (~danse-nr3@151.37.247.23) (Remote host closed the connection) |
| 2024-06-13 06:55:21 +0200 | danse-nr3 | (~danse-nr3@151.37.247.23) |
| 2024-06-13 07:05:15 +0200 | alexherbo2 | (~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 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-13 07:11:11 +0200 | tomku | (~tomku@user/tomku) (Ping timeout: 252 seconds) |
| 2024-06-13 07:30:02 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-06-13 07:33:54 +0200 | TheCoffeMaker_ | (~TheCoffeM@200.114.213.75) (Ping timeout: 255 seconds) |
| 2024-06-13 07:42:33 +0200 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) |
| 2024-06-13 07:44:19 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-06-13 07:45:08 +0200 | euleritian | (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) |
| 2024-06-13 07:46:31 +0200 | acidjnk | (~acidjnk@p200300d6e714dc24101446769eacf81f.dip0.t-ipconnect.de) |
| 2024-06-13 07:53:23 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 07:58:19 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-06-13 07:58:52 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-06-13 08:20:42 +0200 | <[exa]> | Axman6: kinda like accelerate, but in python |
| 2024-06-13 08:21:00 +0200 | jcarpenter2 | (~lol@96.78.87.198) (Ping timeout: 268 seconds) |
| 2024-06-13 08:25:19 +0200 | poscat | (~poscat@user/poscat) (Ping timeout: 260 seconds) |
| 2024-06-13 08:26:20 +0200 | echoreply | (~echoreply@2001:19f0:9002:1f3b:5400:ff:fe6f:8b8d) (Quit: WeeChat 2.8) |
| 2024-06-13 08:27:39 +0200 | echoreply | (~echoreply@45.32.163.16) |
| 2024-06-13 08:35:23 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-06-13 08:37:04 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-06-13 08:41:45 +0200 | poscat | (~poscat@user/poscat) |
| 2024-06-13 08:42:26 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-13 08:44:18 +0200 | jcarpenter2 | (~lol@96.78.87.198) |
| 2024-06-13 08:46:26 +0200 | causal | (~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 +0200 | ft | (~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-06-13 08:54:40 +0200 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) |
| 2024-06-13 08:56:26 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 256 seconds) |
| 2024-06-13 09:10:58 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-06-13 09:12:27 +0200 | euleritian | (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-13 09:12:44 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-13 09:15:45 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 2024-06-13 09:16:15 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-06-13 09:16:27 +0200 | danse-nr3 | (~danse-nr3@151.37.247.23) (Ping timeout: 264 seconds) |
| 2024-06-13 09:17:07 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) |
| 2024-06-13 09:17:26 +0200 | califax | (~califax@user/califx) |
| 2024-06-13 09:17:41 +0200 | mjacob | (~mjacob@adrastea.uberspace.de) (Read error: Connection reset by peer) |
| 2024-06-13 09:22:47 +0200 | mjacob | (~mjacob@adrastea.uberspace.de) |
| 2024-06-13 09:31:52 +0200 | CiaoSen | (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) |
| 2024-06-13 09:31:52 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-06-13 09:33:28 +0200 | califax | (~califax@user/califx) |
| 2024-06-13 09:48:00 +0200 | tomku | (~tomku@syn-141-126-184-057.res.spectrum.com) |
| 2024-06-13 09:48:11 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 09:53:09 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-13 09:54:12 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-06-13 09:58:22 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) (Ping timeout: 246 seconds) |
| 2024-06-13 09:58:22 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-13 09:59:29 +0200 | notzmv | (~daniel@user/notzmv) (Ping timeout: 272 seconds) |
| 2024-06-13 10:00:06 +0200 | tomku | (~tomku@syn-141-126-184-057.res.spectrum.com) (Remote host closed the connection) |
| 2024-06-13 10:00:17 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) |
| 2024-06-13 10:00:20 +0200 | tomku | (~tomku@syn-141-126-184-057.res.spectrum.com) |
| 2024-06-13 10:02:00 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-06-13 10:04:27 +0200 | CiaoSen | (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) (Ping timeout: 264 seconds) |
| 2024-06-13 10:05:03 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) (Ping timeout: 264 seconds) |
| 2024-06-13 10:08:54 +0200 | sprout_ | sprout |
| 2024-06-13 10:10:28 +0200 | danza | (~francesco@151.35.245.71) |
| 2024-06-13 10:12:53 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 2024-06-13 10:20:00 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 10:20:32 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 10:25:34 +0200 | danza | (~francesco@151.35.245.71) (Ping timeout: 268 seconds) |
| 2024-06-13 10:27:27 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 10:37:11 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 10:37:53 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-13 10:43:53 +0200 | Guest19 | (~Guest76@49.245.75.147) |
| 2024-06-13 10:45:53 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) |
| 2024-06-13 10:51:46 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) (Remote host closed the connection) |
| 2024-06-13 10:52:07 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) |
| 2024-06-13 10:54:13 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) (Remote host closed the connection) |
| 2024-06-13 10:54:38 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) |
| 2024-06-13 10:56:04 +0200 | nickiminjaj | (~nickiminj@188.146.127.82) |
| 2024-06-13 10:56:04 +0200 | nickiminjaj | (~nickiminj@188.146.127.82) (Changing host) |
| 2024-06-13 10:56:04 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 11:02:49 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-06-13 11:04:41 +0200 | chele | (~chele@user/chele) |
| 2024-06-13 11:08:58 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 11:11:17 +0200 | destituion | (~destituio@77.18.53.84.tmi.telenormobil.no) (Read error: Connection reset by peer) |
| 2024-06-13 11:12:17 +0200 | destituion | (~destituio@85.221.111.174) |
| 2024-06-13 11:17:22 +0200 | seeg123456 | (~seeg12345@64.176.64.83) (Ping timeout: 268 seconds) |
| 2024-06-13 11:18:06 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-13 11:21:56 +0200 | CiaoSen | (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) |
| 2024-06-13 11:31:31 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Ping timeout: 255 seconds) |
| 2024-06-13 11:31:53 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-06-13 11:41:40 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-13 11:44:33 +0200 | andrei_n | (~andrei_n@2a02:a03f:c091:a800:4cc9:832b:d3d8:de1c) |
| 2024-06-13 11:44:33 +0200 | andrei_n | (~andrei_n@2a02:a03f:c091:a800:4cc9:832b:d3d8:de1c) (Changing host) |
| 2024-06-13 11:44:33 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) |
| 2024-06-13 11:44:44 +0200 | akegalj | (~akegalj@141-138-29-155.dsl.iskon.hr) |
| 2024-06-13 11:49:38 +0200 | MironZ3 | (~MironZ@nat-infra.ehlab.uk) (Quit: The Lounge - https://thelounge.chat) |
| 2024-06-13 11:50:13 +0200 | MironZ3 | (~MironZ@nat-infra.ehlab.uk) |
| 2024-06-13 11:55:29 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-06-13 11:59:54 +0200 | akegalj | (~akegalj@141-138-29-155.dsl.iskon.hr) (Quit: leaving) |
| 2024-06-13 12:00:03 +0200 | nickiminjaj | (~nickiminj@188.146.127.82) |
| 2024-06-13 12:00:03 +0200 | nickiminjaj | (~nickiminj@188.146.127.82) (Changing host) |
| 2024-06-13 12:00:03 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 12:02:37 +0200 | Guest19 | (~Guest76@49.245.75.147) (Quit: Client closed) |
| 2024-06-13 12:04:00 +0200 | econo_ | (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 +0200 | notzmv | (~daniel@user/notzmv) |
| 2024-06-13 12:15:51 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds) |
| 2024-06-13 12:16:49 +0200 | absence | (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 +0200 | xdminsy | (~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 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 12:21:21 +0200 | lortabac | (~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 +0200 | alexherbo2 | (~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 +0200 | Square2 | (~Square4@user/square) |
| 2024-06-13 12:50:03 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Ping timeout: 264 seconds) |
| 2024-06-13 12:59:50 +0200 | lortabac | (~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 +0200 | andrei_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 +0200 | danse-nr3 | (~danse-nr3@151.35.245.71) (Read error: Connection reset by peer) |
| 2024-06-13 13:13:38 +0200 | danse-nr3 | (~danse-nr3@151.43.251.36) |
| 2024-06-13 13:20:12 +0200 | xff0x | (~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 +0200 | danse-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 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 14:01:48 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 255 seconds) |
| 2024-06-13 14:04:42 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 14:09:22 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 14:13:28 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-13 14:14:18 +0200 | danse-nr3 | (~danse-nr3@151.43.251.36) |
| 2024-06-13 14:15:16 +0200 | danse-nr3 | (~danse-nr3@151.43.251.36) (Remote host closed the connection) |
| 2024-06-13 14:15:40 +0200 | danse-nr3 | (~danse-nr3@151.43.251.36) |
| 2024-06-13 14:23:42 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-06-13 14:23:50 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 14:28:41 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2024-06-13 14:34:19 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 14:45:03 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-06-13 14:47:41 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 14:48:07 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 14:50:07 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 268 seconds) |
| 2024-06-13 14:58:38 +0200 | rosco | (~rosco@175.136.155.137) |
| 2024-06-13 15:00:15 +0200 | nickiminjaj_ | (~nickiminj@user-5-173-188-100.play-internet.pl) |
| 2024-06-13 15:00:15 +0200 | nickiminjaj_ | (~nickiminj@user-5-173-188-100.play-internet.pl) (Changing host) |
| 2024-06-13 15:00:15 +0200 | nickiminjaj_ | (~nickiminj@user/laxhh) |
| 2024-06-13 15:04:27 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Ping timeout: 264 seconds) |
| 2024-06-13 15:08:37 +0200 | someone235 | (uid419897@id-419897.ilkley.irccloud.com) |
| 2024-06-13 15:09:50 +0200 | nickiminjaj_ | (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-13 15:11:50 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2024-06-13 15:22:40 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 15:24:35 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Client Quit) |
| 2024-06-13 15:25:42 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal) |
| 2024-06-13 15:25:48 +0200 | ystael | (~ystael@user/ystael) |
| 2024-06-13 15:27:33 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Quit: Leaving) |
| 2024-06-13 15:32:05 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 15:35:59 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Client Quit) |
| 2024-06-13 15:38:03 +0200 | rustisafungus | (~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 +0200 | lortabac | (~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 +0200 | TactfulCitrus | (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) |
| 2024-06-13 15:47:19 +0200 | brett48 | (~brett48@cpc91312-watf11-2-0-cust1213.15-2.cable.virginm.net) |
| 2024-06-13 15:48:58 +0200 | euleritian | (~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 +0200 | euleritian | (~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 +0200 | gdl_ | (~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 +0200 | euleritian | (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-13 16:00:13 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-06-13 16:04:09 +0200 | nickiminjaj | (~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 +0200 | Square2 | (~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 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-06-13 16:06:35 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Client Quit) |
| 2024-06-13 16:07:12 +0200 | euleritian | (~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 +0200 | TactfulCitrus | (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection) |
| 2024-06-13 16:09:24 +0200 | TactfulCitrus | (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) |
| 2024-06-13 16:09:37 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 255 seconds) |
| 2024-06-13 16:09:57 +0200 | califax | (~califax@user/califx) |
| 2024-06-13 16:10:32 +0200 | euleritian | (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) |
| 2024-06-13 16:10:54 +0200 | waleee | (~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 +0200 | TactfulCitrus | (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection) |
| 2024-06-13 16:21:26 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 2024-06-13 16:22:18 +0200 | TactfulCitrus | (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) |
| 2024-06-13 16:23:38 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-06-13 16:26:44 +0200 | eron | (~eron@179.98.163.50) |
| 2024-06-13 16:30:38 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 2024-06-13 16:38:13 +0200 | eron | (~eron@179.98.163.50) (Ping timeout: 250 seconds) |
| 2024-06-13 16:38:31 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 16:44:39 +0200 | destituion | (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 2024-06-13 16:49:22 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 16:51:14 +0200 | TactfulCitrus | (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection) |
| 2024-06-13 16:53:00 +0200 | destituion | (~destituio@2a02:2121:306:89fe:6583:236:fa09:18d5) |
| 2024-06-13 16:55:11 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 16:55:29 +0200 | k_hachig | (~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca) |
| 2024-06-13 16:57:56 +0200 | nickiminjaj | (~nickiminj@user/laxhh) (Quit: Textual IRC Client: www.textualapp.com) |
| 2024-06-13 16:58:09 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 17:03:45 +0200 | nickiminjaj | (~nickiminj@user/laxhh) |
| 2024-06-13 17:06:46 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Ping timeout: 255 seconds) |
| 2024-06-13 17:07:10 +0200 | noctux | (~noctux@user/noctux) (Read error: Connection reset by peer) |
| 2024-06-13 17:11:03 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 264 seconds) |
| 2024-06-13 17:11:56 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-06-13 17:13:50 +0200 | weechat | dminuoso |
| 2024-06-13 17:15:21 +0200 | danse-nr3 | (~danse-nr3@151.43.251.36) (Read error: Connection reset by peer) |
| 2024-06-13 17:15:39 +0200 | danse-nr3 | (~danse-nr3@151.47.241.29) |
| 2024-06-13 17:17:16 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-06-13 17:24:05 +0200 | noctux | (~noctux@user/noctux) |
| 2024-06-13 17:26:46 +0200 | mauke | (~mauke@user/mauke) (Read error: Connection reset by peer) |
| 2024-06-13 17:29:19 +0200 | ames | (~amelia@offtopia/offtopian/amelia) |
| 2024-06-13 17:32:25 +0200 | ames | (~amelia@offtopia/offtopian/amelia) (Client Quit) |
| 2024-06-13 17:32:33 +0200 | mauke | (~mauke@user/mauke) |
| 2024-06-13 17:32:34 +0200 | ames | (~amelia@offtopia/offtopian/amelia) |
| 2024-06-13 17:33:54 +0200 | ames | (~amelia@offtopia/offtopian/amelia) (Client Quit) |
| 2024-06-13 17:35:39 +0200 | ames | (~amelia@offtopia/offtopian/amelia) |
| 2024-06-13 17:42:38 +0200 | puke | (~puke@user/puke) |
| 2024-06-13 17:42:42 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-06-13 17:42:57 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-13 17:48:11 +0200 | euleritian | (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-13 17:48:28 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-13 17:51:13 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 246 seconds) |
| 2024-06-13 17:51:56 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-06-13 17:52:12 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 255 seconds) |
| 2024-06-13 17:52:45 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) |
| 2024-06-13 17:58:59 +0200 | someone235 | (uid419897@id-419897.ilkley.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-13 18:01:54 +0200 | CiaoSen | (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 2024-06-13 18:03:02 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-06-13 18:03:15 +0200 | danse-nr3 | (~danse-nr3@151.47.241.29) (Ping timeout: 264 seconds) |
| 2024-06-13 18:11:55 +0200 | yin | (~yin@user/zero) |
| 2024-06-13 18:12:01 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-06-13 18:12:33 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2024-06-13 18:14:26 +0200 | gdl_ | (~gdl__@mob-5-91-23-178.net.vodafone.it) (Remote host closed the connection) |
| 2024-06-13 18:18:38 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 2024-06-13 18:18:38 +0200 | ChanServ | +v haskellbridge |
| 2024-06-13 18:19:50 +0200 | danse-nr3 | (~danse-nr3@151.47.241.29) |
| 2024-06-13 18:22:43 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-06-13 18:23:26 +0200 | danse-nr3 | (~danse-nr3@151.47.241.29) (Remote host closed the connection) |
| 2024-06-13 18:34:22 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-06-13 18:40:54 +0200 | califax | (~califax@user/califx) |
| 2024-06-13 18:47:07 +0200 | hueso | (~root@user/hueso) (Ping timeout: 255 seconds) |
| 2024-06-13 18:49:17 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-06-13 18:53:39 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2024-06-13 18:54:59 +0200 | euleritian | (~euleritia@dynamic-176-003-011-033.176.3.pool.telefonica.de) |
| 2024-06-13 18:58:27 +0200 | rdcdr | (~rdcdr@user/rdcdr) (Ping timeout: 264 seconds) |
| 2024-06-13 18:58:54 +0200 | Me-me | (~me-me@user/me-me) (Remote host closed the connection) |
| 2024-06-13 18:59:21 +0200 | hueso | (~root@user/hueso) |
| 2024-06-13 18:59:28 +0200 | Me-me | (~me-me@kc.randomserver.name) |
| 2024-06-13 19:01:14 +0200 | euleritian | (~euleritia@dynamic-176-003-011-033.176.3.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-13 19:01:31 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-06-13 19:01:47 +0200 | henry40408 | (~henry4040@175.182.111.183) |
| 2024-06-13 19:04:07 +0200 | rdcdr | (~rdcdr@user/rdcdr) |
| 2024-06-13 19:14:36 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-06-13 19:15:14 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 19:16:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 19:17:50 +0200 | osogyian | (~osogyian@2804:1b3:6603:6f0b:4dd2:8d4e:c6db:c6b7) |
| 2024-06-13 19:19:53 +0200 | osogyian | (~osogyian@2804:1b3:6603:6f0b:4dd2:8d4e:c6db:c6b7) () |
| 2024-06-13 19:22:27 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 19:28:17 +0200 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-06-13 19:39:17 +0200 | tromp | (~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 +0200 | rustisafungus | (~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 +0200 | ocra8 | (~ocra8@user/ocra8) (Read error: Connection reset by peer) |
| 2024-06-13 19:53:47 +0200 | ocra8 | (~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 +0200 | ft | (~ft@p3e9bcb39.dip0.t-ipconnect.de) |
| 2024-06-13 19:59:41 +0200 | ocra8 | (~ocra8@user/ocra8) (Ping timeout: 240 seconds) |
| 2024-06-13 20:00:59 +0200 | ocra8 | (~ocra8@user/ocra8) |
| 2024-06-13 20:03:36 +0200 | brett48 | (~brett48@cpc91312-watf11-2-0-cust1213.15-2.cable.virginm.net) (Quit: brett48) |
| 2024-06-13 20:05:35 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 2024-06-13 20:08:26 +0200 | califax_ | (~califax@user/califx) |
| 2024-06-13 20:08:59 +0200 | Chai-T-Rex | (~ChaiTRex@user/chaitrex) |
| 2024-06-13 20:09:24 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-06-13 20:10:34 +0200 | califax | (~califax@user/califx) (Ping timeout: 260 seconds) |
| 2024-06-13 20:10:34 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-06-13 20:10:35 +0200 | califax_ | califax |
| 2024-06-13 20:11:02 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 2024-06-13 20:11:02 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
| 2024-06-13 20:12:29 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-13 20:12:53 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-06-13 20:15:32 +0200 | tzh | (~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 +0200 | gehmehgeh | gmg |
| 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 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-06-13 20:26:23 +0200 | hueso | (~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 +0200 | hueso | (~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 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-06-13 20:40:47 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 20:47:23 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 20:48:34 +0200 | rvalue | (~rvalue@user/rvalue) (Remote host closed the connection) |
| 2024-06-13 20:49:02 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-06-13 20:52:02 +0200 | Square | (~Square@user/square) |
| 2024-06-13 21:03:00 +0200 | cyphase | (~cyphase@user/cyphase) |
| 2024-06-13 21:09:58 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 21:10:18 +0200 | Guest13 | (~Guest13@220.67.223.22) |
| 2024-06-13 21:10:39 +0200 | foul_owl | (~kerry@185.216.231.181) (Ping timeout: 255 seconds) |
| 2024-06-13 21:10:50 +0200 | foul_owl | (~kerry@174-21-146-130.tukw.qwest.net) |
| 2024-06-13 21:11:02 +0200 | Guest13 | (~Guest13@220.67.223.22) (Client Quit) |
| 2024-06-13 21:16:54 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 21:21:36 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds) |
| 2024-06-13 21:23:51 +0200 | philopsos1 | (~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 +0200 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) |
| 2024-06-13 21:29:44 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 252 seconds) |
| 2024-06-13 21:30:01 +0200 | dsrt^ | (~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 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-06-13 21:35:27 +0200 | rustisafungus | (~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 +0200 | smalltalkman | (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 +0200 | henry40408 | (~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds)) |
| 2024-06-13 21:42:59 +0200 | henry40408 | (~henry4040@175.182.111.183) |
| 2024-06-13 21:43:04 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2024-06-13 21:45:18 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-13 21:53:39 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 2024-06-13 21:59:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 22:06:26 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) |
| 2024-06-13 22:08:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-13 22:18:40 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 22:19:02 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-06-13 22:20:20 +0200 | hueso | (~root@user/hueso) (Ping timeout: 252 seconds) |
| 2024-06-13 22:20:47 +0200 | hueso | (~root@user/hueso) |
| 2024-06-13 22:21:28 +0200 | mei | (~mei@user/mei) |
| 2024-06-13 22:26:39 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Ping timeout: 264 seconds) |
| 2024-06-13 22:26:46 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds) |
| 2024-06-13 22:38:10 +0200 | yin | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-06-13 22:38:55 +0200 | yin | (~yin@user/zero) |
| 2024-06-13 22:38:58 +0200 | causal | (~eric@50.35.88.207) |
| 2024-06-13 22:40:22 +0200 | k_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 +0200 | yin | (~yin@user/zero) (Ping timeout: 252 seconds) |
| 2024-06-13 22:43:42 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-06-13 22:44:17 +0200 | yin | (~yin@user/zero) |
| 2024-06-13 22:44:39 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 2024-06-13 22:49:50 +0200 | rustisafungus | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 2024-06-13 22:54:11 +0200 | k_hachig | (~k_hachig@65.94.221.127) |
| 2024-06-13 23:03:52 +0200 | michalz | (~michalz@185.246.207.201) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2024-06-13 23:08:33 +0200 | opqdonut | (opqdonut@pseudo.fixme.fi) (Ping timeout: 255 seconds) |
| 2024-06-13 23:08:47 +0200 | Me-me | (~me-me@kc.randomserver.name) (Changing host) |
| 2024-06-13 23:08:47 +0200 | Me-me | (~me-me@user/me-me) |
| 2024-06-13 23:15:11 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-13 23:18:22 +0200 | sp1ff | (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 2024-06-13 23:21:18 +0200 | rvalue- | (~rvalue@user/rvalue) |
| 2024-06-13 23:22:01 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-06-13 23:22:34 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 2024-06-13 23:25:17 +0200 | rvalue- | rvalue |
| 2024-06-13 23:28:26 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-06-13 23:35:32 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-06-13 23:37:54 +0200 | mei | (~mei@user/mei) |
| 2024-06-13 23:39:52 +0200 | sp1ff | (~user@c-24-21-45-157.hsd1.wa.comcast.net) |
| 2024-06-13 23:41:04 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 2024-06-13 23:41:29 +0200 | euleritian | (~euleritia@dynamic-176-003-011-016.176.3.pool.telefonica.de) |
| 2024-06-13 23:43:05 +0200 | k_hachig | (~k_hachig@65.94.221.127) (Quit: WeeChat 4.3.2) |
| 2024-06-13 23:44:13 +0200 | k_hachig | (~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca) |
| 2024-06-13 23:44:46 +0200 | AlexZenon | (~alzenon@178.34.163.204) (Ping timeout: 268 seconds) |
| 2024-06-13 23:44:54 +0200 | pavonia | (~user@user/siracusa) |
| 2024-06-13 23:53:37 +0200 | AlexZenon | (~alzenon@178.34.163.204) |
| 2024-06-13 23:55:09 +0200 | gabiruh_ | (~gabiruh@vps19177.publiccloud.com.br) |
| 2024-06-13 23:56:02 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 252 seconds) |