| 2024-06-03 00:00:04 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) |
| 2024-06-03 00:01:26 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-06-03 00:04:17 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-06-03 00:32:48 +0200 | myme | (~myme@2a01:799:d5c:5f00:69d5:8c7b:dd4d:cbe8) (Quit: WeeChat 4.2.2) |
| 2024-06-03 00:33:29 +0200 | acidjnk | (~acidjnk@p200300d6e714dc176c976a8b55dd22bd.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2024-06-03 00:36:16 +0200 | <yin> | mauke: which haskell doesn't do, right? |
| 2024-06-03 00:39:56 +0200 | <geekosaur> | polymorphic typeclass recursion can |
| 2024-06-03 00:40:58 +0200 | <yin> | geekosaur: at *runtime* ? |
| 2024-06-03 00:41:16 +0200 | <geekosaur> | not only can it create new types, it can create them from types that aren't even known at compile time but come from instances defined by some package that didn't even exist when you wrote your code |
| 2024-06-03 00:41:28 +0200 | <geekosaur> | yes, at runtime |
| 2024-06-03 00:41:40 +0200 | <yin> | can you point me to a simple example? |
| 2024-06-03 00:41:48 +0200 | <yin> | this is new to me |
| 2024-06-03 00:42:43 +0200 | <geekosaur> | considering what I just said, code that uses `SomeTypeclass m => m a` may find itself with an `m a` that can'tg possibly be known at compile time |
| 2024-06-03 00:43:26 +0200 | <geekosaur> | all it knows is a passed-in instance dictionary |
| 2024-06-03 00:43:28 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-06-03 00:44:15 +0200 | <geekosaur> | normally this isn't aa problem, but with polymorphic recursion in a typeclass method you end up with methods that can't be completely resolved at compile time even with WPC |
| 2024-06-03 00:45:06 +0200 | <geekosaur> | this isn't what you normally think of with "types defined at runtime", but it behaves like that |
| 2024-06-03 00:45:44 +0200 | <yin> | i see. thanks |
| 2024-06-03 00:50:02 +0200 | <geekosaur> | I'm not sure of this but I think it may also verge on dependent types? since the type it constructs is defined by an instance record. but the compiler restricts it so much that you need hacks like IfCxt to actually explore that direction? |
| 2024-06-03 00:50:17 +0200 | <geekosaur> | maybe I should say "type" in scare quotes |
| 2024-06-03 00:59:27 +0200 | Square | (~Square@user/square) |
| 2024-06-03 00:59:35 +0200 | TMA | (tma@twin.jikos.cz) |
| 2024-06-03 01:05:23 +0200 | troojg | (~troojg@99.36.5.199) (Quit: leaving) |
| 2024-06-03 01:15:00 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-06-03 01:15:41 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-06-03 01:19:41 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 240 seconds) |
| 2024-06-03 01:20:36 +0200 | <geekosaur> | there was a practical example in here a couple months ago where, given [()] and a polymorphically recursive call, it generated [[()]] then [[[()]]] and so on which were never specified at compile time but generated on the fly by recursing on the typeclass method |
| 2024-06-03 01:21:34 +0200 | <geekosaur> | because all of those types can be captured by a typeclass method that turns `a` into `[a]`, fed back into itself |
| 2024-06-03 01:22:44 +0200 | <int-e> | > read "[[[[[[[()]]]]]]]" :: [[[[[[[()]]]]]]] |
| 2024-06-03 01:22:46 +0200 | <lambdabot> | [[[[[[[()]]]]]]] |
| 2024-06-03 01:24:40 +0200 | rdcdr | (~rdcdr@user/rdcdr) (Ping timeout: 256 seconds) |
| 2024-06-03 01:24:44 +0200 | rdcdr_ | (~rdcdr@97-113-199-193.tukw.qwest.net) |
| 2024-06-03 01:29:45 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2024-06-03 01:55:10 +0200 | <yin> | for a moment there i thought this was #lisp |
| 2024-06-03 01:59:29 +0200 | ystael | (~ystael@user/ystael) |
| 2024-06-03 01:59:47 +0200 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-03 02:03:47 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-03 02:07:55 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-06-03 02:08:19 +0200 | <int-e> | yin: it just occurred to me that `read` fits the description geekosaur gave |
| 2024-06-03 02:08:52 +0200 | <int-e> | even though I expect that the actual code was quite different |
| 2024-06-03 02:09:23 +0200 | <geekosaur> | that type is specified at compile time via an ascription, no? |
| 2024-06-03 02:12:10 +0200 | <int-e> | yeah which is kind of necessary because the value is actually returned rather than hidden in a recursive call. |
| 2024-06-03 02:12:21 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-03 02:13:35 +0200 | <geekosaur> | here's the original discussion from my logs https://paste.tomsmeding.com/cGswS9X2 |
| 2024-06-03 02:14:18 +0200 | <int-e> | the recursion part of this doesn't even require type classes. You can have data BalancedTree a = Leaf a | Nest (BalancedTree (a,a)) and generate a tree of depth n with foo :: Int -> a -> BalancedTree a; foo 0 a = Leaf a; foo n a = Nest (foo (n-1) a) |
| 2024-06-03 02:15:22 +0200 | <int-e> | Ah that example is similar. |
| 2024-06-03 02:15:27 +0200 | <geekosaur> | right, there's a distinction to be made between recursive types and recursive typeclass instances |
| 2024-06-03 02:15:49 +0200 | <int-e> | (the Show type class is involved but not essential) |
| 2024-06-03 02:16:56 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-06-03 02:17:07 +0200 | <int-e> | Okay if the point was to point out that type classes are different from C++ templates then it is essential. |
| 2024-06-03 02:21:20 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-03 02:23:33 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 2024-06-03 02:24:16 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-06-03 02:37:00 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-06-03 02:44:12 +0200 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-06-03 02:46:30 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-03 02:49:45 +0200 | gentauro | (~gentauro@user/gentauro) |
| 2024-06-03 02:53:09 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 268 seconds) |
| 2024-06-03 02:54:44 +0200 | <dmj`> | mauke: intensional type analysis is a way around the polymorphic recursion inlining problem, Oleg explains |
| 2024-06-03 02:54:54 +0200 | <dmj`> | rust still has this problem |
| 2024-06-03 02:55:34 +0200 | <dmj`> | yin: it works by making a small interpreter from the recursive type language at compile time |
| 2024-06-03 03:00:33 +0200 | troydm | (~troydm@user/troydm) (Ping timeout: 268 seconds) |
| 2024-06-03 03:09:30 +0200 | euleritian | (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 2024-06-03 03:10:08 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-06-03 03:18:58 +0200 | yin | (~yin@user/zero) (Ping timeout: 246 seconds) |
| 2024-06-03 03:25:49 +0200 | yin | (~yin@user/zero) |
| 2024-06-03 03:31:44 +0200 | pavonia | (~user@user/siracusa) |
| 2024-06-03 04:25:01 +0200 | joeyadams | (~joeyadams@38.48.105.67) |
| 2024-06-03 04:35:52 +0200 | gastus_ | (~gastus@185.6.123.144) |
| 2024-06-03 04:39:13 +0200 | gastus | (~gastus@185.6.123.201) (Ping timeout: 268 seconds) |
| 2024-06-03 04:49:37 +0200 | td_ | (~td@i53870901.versanet.de) (Ping timeout: 246 seconds) |
| 2024-06-03 04:51:45 +0200 | td_ | (~td@i53870924.versanet.de) |
| 2024-06-03 05:04:56 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 260 seconds) |
| 2024-06-03 05:38:07 +0200 | JimL | (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-06-03 05:41:09 +0200 | JimL | (~quassel@89.162.16.26) |
| 2024-06-03 05:55:52 +0200 | aforemny_ | (~aforemny@2001:9e8:6ced:6800:13d6:de3b:fcd:8fe6) |
| 2024-06-03 05:56:23 +0200 | aforemny | (~aforemny@i59F516FA.versanet.de) (Ping timeout: 264 seconds) |
| 2024-06-03 06:01:41 +0200 | joeyadams | (~joeyadams@38.48.105.67) (Quit: Leaving) |
| 2024-06-03 06:03:47 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 2024-06-03 06:13:12 +0200 | euleritian | (~euleritia@77.22.252.56) (Remote host closed the connection) |
| 2024-06-03 06:13:42 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-03 06:14:56 +0200 | fryguybob | (~fryguybob@syn-024-094-050-022.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-06-03 06:14:59 +0200 | TonyStone | (~TonyStone@user/TonyStone) (Ping timeout: 252 seconds) |
| 2024-06-03 06:15:30 +0200 | michalz | (~michalz@185.246.207.222) |
| 2024-06-03 06:21:38 +0200 | fryguybob | (~fryguybob@syn-024-094-050-022.res.spectrum.com) |
| 2024-06-03 06:28:12 +0200 | TonyStone | (~TonyStone@user/TonyStone) |
| 2024-06-03 06:35:16 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-03 06:41:16 +0200 | michalz | (~michalz@185.246.207.222) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2024-06-03 06:41:25 +0200 | ak-1 | (~ak-1@149.50.189.146) |
| 2024-06-03 06:43:59 +0200 | michalz | (~michalz@185.246.207.197) |
| 2024-06-03 06:56:23 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-06-03 07:03:50 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-06-03 07:22:18 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-06-03 07:22:38 +0200 | yin | (~yin@user/zero) (Ping timeout: 252 seconds) |
| 2024-06-03 07:29:03 +0200 | ak-1 | (~ak-1@149.50.189.146) (Quit: ak-1) |
| 2024-06-03 07:29:34 +0200 | yin | (~yin@user/zero) |
| 2024-06-03 07:30:05 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-06-03 07:30:45 +0200 | ak-1 | (~ak-1@149.50.189.146) |
| 2024-06-03 07:32:32 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-06-03 07:32:54 +0200 | euleritian | (~euleritia@dynamic-176-006-189-105.176.6.pool.telefonica.de) |
| 2024-06-03 07:40:28 +0200 | acidjnk | (~acidjnk@p200300d6e714dc88f58a1eda715be1ae.dip0.t-ipconnect.de) |
| 2024-06-03 08:00:04 +0200 | rvalue- | (~rvalue@user/rvalue) |
| 2024-06-03 08:01:08 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 2024-06-03 08:04:11 +0200 | rvalue- | rvalue |
| 2024-06-03 08:13:31 +0200 | yin | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-06-03 08:13:55 +0200 | xdminsy | (~xdminsy@117.147.70.212) (Quit: Konversation terminated!) |
| 2024-06-03 08:14:19 +0200 | xdminsy | (~xdminsy@117.147.70.212) |
| 2024-06-03 08:37:17 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 2024-06-03 08:39:23 +0200 | andrei_n | (~andrei_n@2a02:a03f:c091:a800:1c16:40cf:83b1:6f42) |
| 2024-06-03 08:42:41 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-06-03 08:43:33 +0200 | euleritian | (~euleritia@dynamic-176-006-189-105.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-03 08:43:51 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-03 08:47:15 +0200 | dmj` | (sid72307@id-72307.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-03 08:54:52 +0200 | myme | (~myme@2a01:799:d5c:5f00:69d5:8c7b:dd4d:cbe8) |
| 2024-06-03 09:13:47 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-06-03 09:16:42 +0200 | sroso | (~sroso@user/SrOso) |
| 2024-06-03 09:17:09 +0200 | sroso | (~sroso@user/SrOso) (Max SendQ exceeded) |
| 2024-06-03 09:21:02 +0200 | mei | (~mei@user/mei) (Ping timeout: 268 seconds) |
| 2024-06-03 09:22:58 +0200 | sroso | (~sroso@user/SrOso) |
| 2024-06-03 09:27:15 +0200 | rosco | (~rosco@90.58.221.226) |
| 2024-06-03 09:43:31 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-03 09:57:55 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-03 10:05:59 +0200 | kmein | (~weechat@user/kmein) (Ping timeout: 264 seconds) |
| 2024-06-03 10:13:01 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-06-03 10:24:34 +0200 | gastus_ | (~gastus@185.6.123.144) (Ping timeout: 246 seconds) |
| 2024-06-03 10:25:28 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-03 10:28:15 +0200 | andrei_n | (~andrei_n@2a02:a03f:c091:a800:1c16:40cf:83b1:6f42) (Ping timeout: 268 seconds) |
| 2024-06-03 10:28:44 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-06-03 10:30:38 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-06-03 10:35:17 +0200 | rosco | (~rosco@90.58.221.226) (Quit: Lost terminal) |
| 2024-06-03 10:49:33 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-03 10:50:41 +0200 | danse-nr3 | (~danse-nr3@151.43.217.1) |
| 2024-06-03 10:56:28 +0200 | rosco | (~rosco@90.58.221.226) |
| 2024-06-03 10:59:18 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-03 10:59:30 +0200 | andrei_n | (~andrei_n@2001:6a8:3081:6f02:1146:7cf9:6058:140d) |
| 2024-06-03 11:03:35 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-06-03 11:04:17 +0200 | Rodney_ | (~Rodney@176.254.244.83) (Ping timeout: 252 seconds) |
| 2024-06-03 11:05:06 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:cea1:c36c:9ead:da4e) |
| 2024-06-03 11:11:19 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-06-03 11:13:32 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 2024-06-03 11:15:23 +0200 | vadparaszt | (~Rodney@176.254.244.83) |
| 2024-06-03 11:16:21 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-03 11:21:16 +0200 | benjaminl | (~benjaminl@user/benjaminl) (Ping timeout: 246 seconds) |
| 2024-06-03 11:21:24 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-06-03 11:22:09 +0200 | andrei_n | (~andrei_n@2001:6a8:3081:6f02:1146:7cf9:6058:140d) (Quit: Leaving) |
| 2024-06-03 11:24:45 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
| 2024-06-03 11:25:00 +0200 | ft | (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-06-03 11:25:50 +0200 | Square2 | (~Square4@user/square) |
| 2024-06-03 11:29:42 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-03 11:29:51 +0200 | kmein | (~weechat@user/kmein) |
| 2024-06-03 11:31:04 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-03 11:38:13 +0200 | Square2 | (~Square4@user/square) (Remote host closed the connection) |
| 2024-06-03 11:38:50 +0200 | Square2 | (~Square4@user/square) |
| 2024-06-03 11:43:11 +0200 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Read error: Connection reset by peer) |
| 2024-06-03 11:43:36 +0200 | chele | (~chele@user/chele) |
| 2024-06-03 11:49:30 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 255 seconds) |
| 2024-06-03 11:56:25 +0200 | benjaminl | (~benjaminl@user/benjaminl) |
| 2024-06-03 12:02:21 +0200 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 2024-06-03 12:08:18 +0200 | Square2 | (~Square4@user/square) |
| 2024-06-03 12:13:02 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2024-06-03 12:15:33 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 272 seconds) |
| 2024-06-03 12:16:17 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 2024-06-03 12:16:58 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-06-03 12:18:14 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-03 12:18:35 +0200 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-06-03 12:25:44 +0200 | hc | (~hc@mail.hce.li) |
| 2024-06-03 12:25:49 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-03 12:30:16 +0200 | ak-1_ | (~ak-1@149.50.189.44) |
| 2024-06-03 12:31:19 +0200 | ak-1 | (~ak-1@149.50.189.146) (Ping timeout: 260 seconds) |
| 2024-06-03 12:34:53 +0200 | ak-1_ | (~ak-1@149.50.189.44) (Client Quit) |
| 2024-06-03 12:35:07 +0200 | ak-1 | (~ak-1@149.50.189.44) |
| 2024-06-03 12:44:50 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
| 2024-06-03 12:46:56 +0200 | michalz | (~michalz@185.246.207.197) (Ping timeout: 256 seconds) |
| 2024-06-03 12:47:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-03 12:47:33 +0200 | michalz | (~michalz@185.246.207.221) |
| 2024-06-03 12:48:41 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-06-03 12:55:29 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-06-03 12:58:23 +0200 | myme | (~myme@2a01:799:d5c:5f00:69d5:8c7b:dd4d:cbe8) (Ping timeout: 260 seconds) |
| 2024-06-03 12:59:10 +0200 | myme | (~myme@2a01:799:d5c:5f00:afc2:43bf:76e1:e67c) |
| 2024-06-03 13:01:00 +0200 | bontaq | (~user@ool-45779c03.dyn.optonline.net) |
| 2024-06-03 13:02:43 +0200 | CiaoSen | (~Jura@2a05:5800:21b:6a00:e6b9:7aff:fe80:3d03) |
| 2024-06-03 13:18:58 +0200 | ncf | (~n@monade.li) (Quit: Fairfarren.) |
| 2024-06-03 13:18:58 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-06-03 13:19:18 +0200 | ncf | (~n@monade.li) |
| 2024-06-03 13:19:38 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-03 13:22:50 +0200 | puke | (~puke@user/puke) |
| 2024-06-03 13:30:04 +0200 | billchenchina | (~billchenc@103.152.35.21) |
| 2024-06-03 13:33:43 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-06-03 13:34:04 +0200 | srk | (~sorki@user/srk) (Read error: Connection reset by peer) |
| 2024-06-03 13:35:18 +0200 | srk | (~sorki@user/srk) |
| 2024-06-03 13:38:04 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-06-03 13:41:51 +0200 | yin | (~yin@user/zero) |
| 2024-06-03 13:48:20 +0200 | poscat0x04 | (~poscat@user/poscat) (Quit: Bye) |
| 2024-06-03 13:58:42 +0200 | poscat | (~poscat@user/poscat) |
| 2024-06-03 14:03:10 +0200 | danza | (~francesco@151.43.217.1) |
| 2024-06-03 14:09:46 +0200 | danza | (~francesco@151.43.217.1) (Read error: Connection reset by peer) |
| 2024-06-03 14:10:04 +0200 | danse-nr3 | (~danse-nr3@151.43.217.1) (Read error: Connection reset by peer) |
| 2024-06-03 14:29:35 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-06-03 14:37:48 +0200 | reki | (~halloy704@broadband-5-228-80-43.ip.moscow.rt.ru) |
| 2024-06-03 14:40:27 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-03 14:41:49 +0200 | yin | (~yin@user/zero) (Ping timeout: 246 seconds) |
| 2024-06-03 14:47:41 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2024-06-03 14:48:40 +0200 | yin | (~yin@user/zero) |
| 2024-06-03 14:51:31 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-06-03 14:54:35 +0200 | dmj` | (uid72307@id-72307.hampstead.irccloud.com) |
| 2024-06-03 15:00:43 +0200 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 246 seconds) |
| 2024-06-03 15:06:33 +0200 | yin | (~yin@user/zero) (Ping timeout: 272 seconds) |
| 2024-06-03 15:07:18 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-06-03 15:07:59 +0200 | yin | (~yin@user/zero) |
| 2024-06-03 15:08:32 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-03 15:14:39 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-03 15:17:10 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-06-03 15:17:16 +0200 | ystael | (~ystael@user/ystael) |
| 2024-06-03 15:22:19 +0200 | joeyadams | (~joeyadams@38.48.105.67) |
| 2024-06-03 15:35:59 +0200 | euleritian | (~euleritia@dynamic-176-006-193-029.176.6.pool.telefonica.de) |
| 2024-06-03 15:36:24 +0200 | rosco | (~rosco@90.58.221.226) (Quit: Lost terminal) |
| 2024-06-03 15:39:17 +0200 | hueso | (~root@user/hueso) (Ping timeout: 252 seconds) |
| 2024-06-03 15:41:11 +0200 | hueso | (~root@user/hueso) |
| 2024-06-03 15:48:18 +0200 | AlexZenon | (~alzenon@178.34.150.84) (Ping timeout: 268 seconds) |
| 2024-06-03 15:49:10 +0200 | thailigur | (~thailigur@151.240.196.165) |
| 2024-06-03 15:51:10 +0200 | thailigur | (~thailigur@151.240.196.165) (Client Quit) |
| 2024-06-03 15:54:54 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-06-03 15:56:32 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-03 15:56:35 +0200 | AlexZenon | (~alzenon@178.34.150.84) |
| 2024-06-03 16:05:16 +0200 | danse-nr3 | (~danse-nr3@151.43.168.146) |
| 2024-06-03 16:05:59 +0200 | danse-nr3 | (~danse-nr3@151.43.168.146) (Max SendQ exceeded) |
| 2024-06-03 16:10:04 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2024-06-03 16:11:43 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-06-03 16:13:57 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-06-03 16:15:00 +0200 | danse-nr3 | (~danse-nr3@151.43.168.146) |
| 2024-06-03 16:17:31 +0200 | tinjamin2 | (~tinjamin@banshee.h4x0r.space) |
| 2024-06-03 16:17:51 +0200 | rosco | (~rosco@2a01cb058a492200bdaee9401e243ca0.ipv6.abo.wanadoo.fr) |
| 2024-06-03 16:20:31 +0200 | tinjamin | (~tinjamin@banshee.h4x0r.space) (Ping timeout: 256 seconds) |
| 2024-06-03 16:20:32 +0200 | tinjamin2 | tinjamin |
| 2024-06-03 16:24:56 +0200 | euleritian | (~euleritia@dynamic-176-006-193-029.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-03 16:26:08 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-03 16:27:42 +0200 | Core6585 | (~rosco@2a02-8440-7155-0678-fd99-c8d7-f5f1-3f14.rev.sfr.net) |
| 2024-06-03 16:30:19 +0200 | rosco | (~rosco@2a01cb058a492200bdaee9401e243ca0.ipv6.abo.wanadoo.fr) (Ping timeout: 246 seconds) |
| 2024-06-03 16:30:28 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-06-03 16:31:25 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-06-03 16:32:56 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-06-03 16:33:17 +0200 | euleritian | (~euleritia@dynamic-176-006-193-029.176.6.pool.telefonica.de) |
| 2024-06-03 16:36:14 +0200 | califax | (~califax@user/califx) |
| 2024-06-03 16:49:48 +0200 | Guest9783 | (~user@72.2.12.179) |
| 2024-06-03 16:53:39 +0200 | reki | (~halloy704@broadband-5-228-80-43.ip.moscow.rt.ru) (Remote host closed the connection) |
| 2024-06-03 16:54:25 +0200 | halloy7049 | (~halloy704@broadband-5-228-80-43.ip.moscow.rt.ru) |
| 2024-06-03 16:54:29 +0200 | halloy7049 | reki |
| 2024-06-03 16:57:36 +0200 | ocra8 | (ocra8@user/ocra8) (Quit: WeeChat 4.2.2) |
| 2024-06-03 17:00:36 +0200 | ocra8 | (ocra8@user/ocra8) |
| 2024-06-03 17:02:59 +0200 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2024-06-03 17:04:00 +0200 | dmj` | (uid72307@id-72307.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-03 17:04:58 +0200 | CiaoSen | (~Jura@2a05:5800:21b:6a00:e6b9:7aff:fe80:3d03) (Ping timeout: 246 seconds) |
| 2024-06-03 17:07:57 +0200 | vladl | (~vladl@24.35.90.183) |
| 2024-06-03 17:16:38 +0200 | joeyadams | (~joeyadams@38.48.105.67) (Quit: Leaving) |
| 2024-06-03 17:24:42 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-06-03 17:37:11 +0200 | euleritian | (~euleritia@dynamic-176-006-193-029.176.6.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 2024-06-03 17:43:58 +0200 | euleritian | (~euleritia@dynamic-176-000-200-168.176.0.pool.telefonica.de) |
| 2024-06-03 17:54:57 +0200 | causal | (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 2024-06-03 17:58:55 +0200 | dmj` | (uid72307@id-72307.hampstead.irccloud.com) |
| 2024-06-03 18:00:04 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-03 18:07:03 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:cea1:c36c:9ead:da4e) (Remote host closed the connection) |
| 2024-06-03 18:08:53 +0200 | danse-nr3 | (~danse-nr3@151.43.168.146) (Ping timeout: 252 seconds) |
| 2024-06-03 18:11:49 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
| 2024-06-03 18:12:58 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
| 2024-06-03 18:16:12 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-03 18:17:18 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 256 seconds) |
| 2024-06-03 18:20:30 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-06-03 18:20:41 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-03 18:23:19 +0200 | falafel | (~falafel@211.248.248.50) |
| 2024-06-03 18:27:45 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-06-03 18:28:38 +0200 | reki | (~halloy704@broadband-5-228-80-43.ip.moscow.rt.ru) (Ping timeout: 256 seconds) |
| 2024-06-03 18:31:26 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-06-03 18:31:58 +0200 | <tomsmeding> | I'm writing a test suite with Hedgehog (quickcheck-lookalike); in a property, I first generate a length (from {0,...,8}), then generate a bunch of that length. The length==0 case should be tested, but results in just a single test case (everything is empty), yet of course the generator generates a whole bunch of zeros. Is there a way to reduce the amount of redundant 0 tests here? |
| 2024-06-03 18:32:45 +0200 | <tomsmeding> | can I e.g. assume that, like with quickcheck, the Size parameter is 0 at least once (and probably not very often after that) while testing? |
| 2024-06-03 18:35:37 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-06-03 18:38:22 +0200 | <jackdk> | tomsmeding: Hedgehog.Gen.frequency will at least allow you to change the relative frequency of zero vs. nonzero generators. I'm also interested to know if there's an easy way to generate exactly one "zero case", otherwise you could write a unit test for empty lists and a property test for nonempty lists? |
| 2024-06-03 18:39:07 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 268 seconds) |
| 2024-06-03 18:44:30 +0200 | <tomsmeding> | jackdk: unit test + property test is indeed one way to go, but that doesn't feel very nice :p |
| 2024-06-03 18:45:37 +0200 | Guest76 | (~Guest76@119.34.172.187) |
| 2024-06-03 18:46:40 +0200 | <tomsmeding> | I'll probably just reduce the probability of zero with frequency, indeed |
| 2024-06-03 18:52:46 +0200 | <tomsmeding> | geekosaur: isn't a much easier example `withSomeSNat` or similar? https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-TypeNats.html#v:withSomeSNat |
| 2024-06-03 18:53:19 +0200 | <tomsmeding> | index a type class on a type-level natural, parse a value-level Natural to a type-level one, and invoke the type class on that type |
| 2024-06-03 18:53:29 +0200 | <tomsmeding> | there's an infinite number of types that could be |
| 2024-06-03 18:53:56 +0200 | <tomsmeding> | (2^(number of bits in the maximum haskell heap size your machine will support) is not infinite, but close enough) |
| 2024-06-03 18:56:50 +0200 | <EvanR> | please turn in your ultrafinitist card and weapon |
| 2024-06-03 18:57:09 +0200 | ocra8 | (ocra8@user/ocra8) (Quit: WeeChat 4.2.2) |
| 2024-06-03 18:58:49 +0200 | <tomsmeding> | ( reads up on ultrafinitism on wikipedia) surely the point of mathematics is to be able to talk about structures without needing to construct them? |
| 2024-06-03 18:59:24 +0200 | <tomsmeding> | in order to understand the structures abstractly so that you can formulate and prove theorems that hold for all constructible instances |
| 2024-06-03 18:59:45 +0200 | <tomsmeding> | _all_ constructible instances, even if someone builds a larger computer at some point |
| 2024-06-03 19:00:11 +0200 | <tomsmeding> | why do ultrafinitists consider mathematics useful at all |
| 2024-06-03 19:02:15 +0200 | <tomsmeding> | the article gives an example that noone has calculated the natural number floor(exp(exp(exp(79)))), which is probably true, but surely we can compute digits of it |
| 2024-06-03 19:02:46 +0200 | <mauke> | > floor(exp(exp(exp(79)))) |
| 2024-06-03 19:02:47 +0200 | <lambdabot> | 1797693134862315907729305190789024733617976978942306572734300811577326758055... |
| 2024-06-03 19:02:50 +0200 | <tomsmeding> | it's a bit rash to consider a thing not a natural number despite being able to calculate digits of it! |
| 2024-06-03 19:03:06 +0200 | <mauke> | why does math have to be useful? |
| 2024-06-03 19:03:29 +0200 | <tomsmeding> | mauke: that's not the value of that expression ;) |
| 2024-06-03 19:03:34 +0200 | <tomsmeding> | > exp(exp(79)) |
| 2024-06-03 19:03:35 +0200 | <lambdabot> | Infinity |
| 2024-06-03 19:04:08 +0200 | <tomsmeding> | mauke: if math is completely useless, then surely we should stop doing it |
| 2024-06-03 19:04:13 +0200 | <mauke> | why? |
| 2024-06-03 19:04:24 +0200 | <tomsmeding> | okay fair point |
| 2024-06-03 19:04:26 +0200 | Guest76 | (~Guest76@119.34.172.187) (Quit: Client closed) |
| 2024-06-03 19:04:32 +0200 | <mauke> | some things are just for fun |
| 2024-06-03 19:04:35 +0200 | <tomsmeding> | at least we should stop funding it as scientific research |
| 2024-06-03 19:04:49 +0200 | <geekosaur> | define "useful". "because it's there" is "useful" enough for some |
| 2024-06-03 19:04:52 +0200 | <mauke> | practical applications are for physicists |
| 2024-06-03 19:04:56 +0200 | <tomsmeding> | I would be the last person to say that we shouldn't do useless fun things |
| 2024-06-03 19:05:21 +0200 | <tomsmeding> | math has been useful in physics |
| 2024-06-03 19:05:28 +0200 | <tomsmeding> | surely pi is useful! Have you ever written down pi? |
| 2024-06-03 19:05:56 +0200 | <EvanR> | ultrafinitism is an interpretation of mathematics, not a formulation, then falls under philosophy not science xD |
| 2024-06-03 19:06:23 +0200 | <tomsmeding> | not only am I apparently not an ultrafinitist, I furthermore don't understand why ultrafinitists think their philosophy is a useful one :p |
| 2024-06-03 19:06:39 +0200 | <monochrom> | Yes, I have written down pi. |
| 2024-06-03 19:06:40 +0200 | <monochrom> | pi |
| 2024-06-03 19:06:46 +0200 | <monochrom> | There, I wrote it again. >:) |
| 2024-06-03 19:06:59 +0200 | <tomsmeding> | I could decide that my philosophy is that natural numbers don't exist at all, but that's not a useful philosophy to live by |
| 2024-06-03 19:07:04 +0200 | <monochrom> | I could write a longer form that uses integration if you want. :) |
| 2024-06-03 19:07:09 +0200 | <tomsmeding> | monochrom: convince an ultrafinitist :p |
| 2024-06-03 19:07:13 +0200 | <mauke> | "A mathematician, like a painter or poet, is a maker of patterns. If his patterns are more permanent than theirs, it is because they are made with ideas. [...] The mathematician's patterns, like the painter's or the poet's must be beautiful; the ideas like the colours or the words, must fit together in a harmonious way. Beauty is the first test: there is no permanent place in the world for ugly |
| 2024-06-03 19:07:19 +0200 | <mauke> | mathematics." |
| 2024-06-03 19:07:20 +0200 | <geekosaur> | 1.0 (written in a system based on pi 😈 ) |
| 2024-06-03 19:07:30 +0200 | <monochrom> | I have only written a finite-length formula so it's ultrafinite. |
| 2024-06-03 19:08:07 +0200 | erty | (~user@user/aeroplane) |
| 2024-06-03 19:08:22 +0200 | <tomsmeding> | monochrom: that contradicts this page https://en.wikipedia.org/wiki/Ultrafinitism which claims that apparently (?) ultrafinitists refrain from accepting the existence of large numbers such as floor(exp(exp(exp(79)))) -- despite this being a finite-length formulate for precisely that number! |
| 2024-06-03 19:08:25 +0200 | <monochrom> | I wonder if some conspiracy theories can also be described as patterns made with ideas. |
| 2024-06-03 19:08:39 +0200 | <tomsmeding> | *formula |
| 2024-06-03 19:08:57 +0200 | <EvanR> | even though the subject matter is not even related, you get the same vibes from ultrafinitism as from flat earth |
| 2024-06-03 19:09:27 +0200 | <mauke> | "I have never done anything 'useful'. [...] Judged by all practical standards, the value of my mathematical life is nil; and outside mathematics it is trivial anyhow. I have just one chance of escaping a verdict of complete triviality, that I may be judged to have created something worth creating." |
| 2024-06-03 19:09:40 +0200 | <geekosaur> | monochrom, mathematics at least strives for consistency, even if it can't achieve it (thanks, Gödel); most conspiracy theories don't |
| 2024-06-03 19:09:44 +0200 | <monochrom> | Yeah I was role-playing misunderstanding ultrafinitism :) |
| 2024-06-03 19:11:23 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Ping timeout: 264 seconds) |
| 2024-06-03 19:12:32 +0200 | <monochrom> | Dijkstra had an accidental argument against ultrafinitism. He was just arguing for reasoning about programs, but the same argument applies to ultrafinitism. |
| 2024-06-03 19:12:49 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) |
| 2024-06-03 19:13:25 +0200 | <monochrom> | So suppose someone asks you to write code for, say, summing up a finite list of numbers. |
| 2024-06-03 19:14:16 +0200 | <monochrom> | If you knew up front all the actual inputs from users, ever (and we know that's finite), then you just have to hardcode those cases and their answers. Nothing to prove correct. |
| 2024-06-03 19:14:36 +0200 | <monochrom> | But of course you don't know upfront, so now you have to write general code and a general proof. |
| 2024-06-03 19:15:02 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 2024-06-03 19:15:05 +0200 | <mauke> | it doesn't have to be fully general |
| 2024-06-03 19:15:16 +0200 | <monochrom> | So ultrafinitism can be right but impractically, intractibly untenable. |
| 2024-06-03 19:15:17 +0200 | <mauke> | e.g. I often limit myself to 64-bit integers |
| 2024-06-03 19:15:53 +0200 | <EvanR> | what's the formula to sum a list of 64-bit integers (correctly) |
| 2024-06-03 19:16:02 +0200 | <monochrom> | Even if you also know the length is less than 2^64, you don't actually code up 64^(2^64) cases, do you? |
| 2024-06-03 19:16:30 +0200 | <mauke> | no, that would take me too long |
| 2024-06-03 19:16:39 +0200 | <mauke> | I write a script that generates the cases |
| 2024-06-03 19:16:45 +0200 | <tomsmeding> | I don't even agree with "Nothing to prove correct" |
| 2024-06-03 19:16:49 +0200 | <monochrom> | hahaha |
| 2024-06-03 19:17:14 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-06-03 19:17:53 +0200 | <tomsmeding> | if your code is "here's a list of 1000 cases and that's everything", even if that happens to actually _be_ everything, just giving that to me doesn't at all convince me that it's correct |
| 2024-06-03 19:18:10 +0200 | <tomsmeding> | in fact, I'd consider it very likely that the function is wrong |
| 2024-06-03 19:18:29 +0200 | <tomsmeding> | so you still have to prove correctness, you just made it more difficult for yourself |
| 2024-06-03 19:18:38 +0200 | <monochrom> | Yeah, but you don't write an induction proof or loop invariant proof. |
| 2024-06-03 19:19:02 +0200 | <tomsmeding> | well, how does the proof look then? |
| 2024-06-03 19:19:04 +0200 | <tomsmeding> | 1000 cases? |
| 2024-06-03 19:19:06 +0200 | <tomsmeding> | that doesn't help |
| 2024-06-03 19:19:34 +0200 | <monochrom> | A lot of people actually fear induction and invariants. They actual would rather, OK, so far I've only heard they write out 50 cases. |
| 2024-06-03 19:25:05 +0200 | halloy7049 | (~halloy704@broadband-5-228-80-43.ip.moscow.rt.ru) |
| 2024-06-03 19:25:16 +0200 | halloy7049 | reki |
| 2024-06-03 19:25:58 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-06-03 19:28:40 +0200 | billchenchina | (~billchenc@103.152.35.21) (Quit: Leaving) |
| 2024-06-03 19:29:16 +0200 | falafel | (~falafel@211.248.248.50) (Ping timeout: 256 seconds) |
| 2024-06-03 19:30:32 +0200 | <tomsmeding> | (I started with writing "50", then thought "wait, there might actually be people who prefer that, let's increase it") |
| 2024-06-03 19:32:29 +0200 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-06-03 19:36:01 +0200 | <monochrom> | :) |