Newest at the top
| 2024-10-07 08:28:26 +0200 | Fischmiep | (~Fischmiep@user/Fischmiep) (Remote host closed the connection) |
| 2024-10-07 08:26:28 +0200 | xff0x | (~xff0x@182.169.73.28) |
| 2024-10-07 08:24:21 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 2024-10-07 08:22:42 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 08:21:10 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 08:20:10 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 08:18:35 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 08:16:49 +0200 | cptaffe | (~cptaffe@user/cptaffe) cptaffe |
| 2024-10-07 08:13:55 +0200 | xacktm | (xacktm@user/xacktm) (Ping timeout: 264 seconds) |
| 2024-10-07 08:05:48 +0200 | cptaffe | (~cptaffe@user/cptaffe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-10-07 08:05:43 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-10-07 08:05:35 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-07 07:53:19 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-07 07:53:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:51:41 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:51:17 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:49:41 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:46:26 +0200 | ZLima12_ | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2024-10-07 07:46:19 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2024-10-07 07:41:53 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:40:18 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:39:16 +0200 | <haskellbridge> | <Bowuigi> F omega would allow me to introduce recursion with a type level size via some magic and cool interactions between features, as well as an effect system based on the Van Laarhoven Free Monad (similar to https://aaronlevin.ca/post/136494428283/extensible-effects-in-the-van-laarhoven-free-monad) |
| 2024-10-07 07:39:12 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:37:26 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:37:19 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:36:43 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-10-07 07:34:30 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-07 07:34:28 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:34:07 +0200 | <haskellbridge> | <Bowuigi> Maybe the overhead of switching from System F to System F omega on the interpreter is not as high as I expected. After all, smalltt has an even more powerful base yet is super fast |
| 2024-10-07 07:32:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 07:32:49 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:32:47 +0200 | <haskellbridge> | <Bowuigi> This also makes me think, is directly going for recursion schemes a good way to do recursion on my language's design? Maybe I should try some other concepts before getting into adding potentially unnecessary features to it |
| 2024-10-07 07:30:11 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-10-07 07:30:06 +0200 | andrewboltachev | (~andrey@178.141.123.3) andrewboltachev |
| 2024-10-07 07:28:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 07:25:53 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:23:47 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:20:25 +0200 | <haskellbridge> | <Bowuigi> So if every "B(a)" corresponds to a type with a finite amount of constructors (like an n-Set or "Fin n"), every node must have a finite amount of branches, thus becoming finitely wide and fully traversable in a finite amount of steps |
| 2024-10-07 07:19:50 +0200 | <haskellbridge> | <thirdofmay18081814goya> am reading |
| 2024-10-07 07:18:02 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) |
| 2024-10-07 07:17:55 +0200 | <haskellbridge> | <Bowuigi> Quoting, "The W type "W (a : A) B(a)" can thus be thought of as the type of well-founded trees, where nodes are labeled by elements of "A" and each node labeled by "a : A" has "B(a)"-many branches" |
| 2024-10-07 07:17:21 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-10-07 07:17:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 07:15:34 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya It has an entire section on them (5.3), short answer, if you have a W type "W (a : A) B(a)" you just have to make every result of "B(a)" a finite type |
| 2024-10-07 07:12:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 07:09:19 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:07:51 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:05:15 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-07 07:05:03 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:03:35 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |