| 2024-10-07 00:04:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-10-07 00:05:13 +0200 | artu | (artu@2600:3c01::f03c:92ff:fecc:1d32) |
| 2024-10-07 00:06:03 +0200 | gawen | (~gawen@user/gawen) (Quit: cya) |
| 2024-10-07 00:08:51 +0200 | neuroevolutus | (~neuroevol@146.70.211.110) (Ping timeout: 256 seconds) |
| 2024-10-07 00:10:35 +0200 | artu | (artu@2600:3c01::f03c:92ff:fecc:1d32) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2024-10-07 00:14:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 00:18:43 +0200 | artu | (artu@2600:3c01::f03c:92ff:fecc:1d32) |
| 2024-10-07 00:19:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 00:30:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 00:33:04 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 260 seconds) |
| 2024-10-07 00:34:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 00:37:29 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-10-07 00:41:30 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-10-07 00:45:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 00:46:12 +0200 | artu | (artu@2600:3c01::f03c:92ff:fecc:1d32) (Remote host closed the connection) |
| 2024-10-07 00:47:04 +0200 | artu | (artu@2600:3c01::f03c:92ff:fecc:1d32) artu |
| 2024-10-07 00:50:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-10-07 00:51:49 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb9628aff41673680d4c.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-10-07 01:01:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 01:03:33 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 2024-10-07 01:05:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 01:12:30 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-07 01:16:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 01:17:27 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-07 01:21:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 01:24:28 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-07 01:27:09 +0200 | <L29Ah> | are there weights-available LLMs that can do haskell programming? |
| 2024-10-07 01:30:05 +0200 | myxokephale | (~myxos@syn-065-028-251-121.res.spectrum.com) (Quit: myxokephale) |
| 2024-10-07 01:32:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 01:32:08 +0200 | <Inst> | afaik ChatGPT haskell programming is primitive, and apparently studies show that AI-assisted programming is net negative for productivity as of now |
| 2024-10-07 01:34:09 +0200 | <monochrom> | You can raise or lower the bar on "can". >:) |
| 2024-10-07 01:34:33 +0200 | <monochrom> | But public LLMs are going to be a bit better than most beginners. |
| 2024-10-07 01:35:06 +0200 | <monochrom> | That just relies on the definition of "beginner" cf. the Dunning-Kruger effect. |
| 2024-10-07 01:36:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-10-07 01:43:35 +0200 | <L29Ah> | Inst: yeah i know, i was mildly curious on whether one can make it produce complete (a little over ACME quality) libraries with cabal packages with some scripting and prompting |
| 2024-10-07 01:44:06 +0200 | <Inst> | why would it be more likely to be able to do this for Haskell than it would be able to do this for Rust, C+=, or for that matter, Python? |
| 2024-10-07 01:44:48 +0200 | <L29Ah> | it's not about likelyhood, it's about my desire to do haskell things instead of the sloppy languages |
| 2024-10-07 01:45:08 +0200 | L29Ah | hides |
| 2024-10-07 01:46:59 +0200 | <L29Ah> | with haskell there can be a more sensible generate-compile-run-prompt loop as it's harder to produce running-yet-broken code |
| 2024-10-07 01:47:15 +0200 | <Inst> | also type information, and iirc work on Agda2hs program derivation |
| 2024-10-07 01:47:27 +0200 | <L29Ah> | and one can pester llm to produce test cases too to catch all the stupid errors programmatically |
| 2024-10-07 01:47:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 01:48:03 +0200 | <Inst> | i'm wondering if LLM would have an easier time converting a domain into Agda types, then using Agda facilities to pound out a Haskell program |
| 2024-10-07 01:48:11 +0200 | <Inst> | but afaik Haskell generated by Agda is unreadable |
| 2024-10-07 01:48:12 +0200 | <L29Ah> | so ideally one converts a PC into a heater that hopefully produces working libraries once in a while :> |
| 2024-10-07 01:48:38 +0200 | <L29Ah> | true programming laziness |
| 2024-10-07 01:49:17 +0200 | <L29Ah> | implying llms can utilize boring things like file format specs |
| 2024-10-07 01:51:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 01:57:51 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale |
| 2024-10-07 02:03:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 02:07:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-10-07 02:14:50 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-10-07 02:18:00 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 272 seconds) |
| 2024-10-07 02:18:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 02:21:41 +0200 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2024-10-07 02:22:42 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-07 02:22:57 +0200 | fmira | (~user@user/fmira) (Remote host closed the connection) |
| 2024-10-07 02:23:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 02:23:22 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-07 02:30:44 +0200 | Inst | (~Inst@user/Inst) (Ping timeout: 255 seconds) |
| 2024-10-07 02:31:43 +0200 | Inst | (~Inst@user/Inst) Inst |
| 2024-10-07 02:32:40 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 2024-10-07 02:33:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 02:36:21 +0200 | Inst | (~Inst@user/Inst) (Ping timeout: 246 seconds) |
| 2024-10-07 02:38:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 02:46:44 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-10-07 02:47:04 +0200 | xff0x | (~xff0x@2405:6580:b080:900:16eb:2432:285b:7ea6) (Ping timeout: 260 seconds) |
| 2024-10-07 02:49:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 02:53:32 +0200 | EvanR_ | EvanR |
| 2024-10-07 02:53:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 02:58:09 +0200 | <yin> | what am i looking at here? https://hackage.haskell.org/package/ghc-prim-0.11.0/docs/src/GHC.Prim.html#readTVar%23 |
| 2024-10-07 02:58:50 +0200 | <yin> | what does it mean for a function# to be defined as itself? |
| 2024-10-07 02:59:24 +0200 | <yin> | is it just "magic" and we need the definition for the type signature? |
| 2024-10-07 02:59:33 +0200 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 248 seconds) |
| 2024-10-07 03:00:46 +0200 | <geekosaur> | everything in ghc-prim is "defined as itself", yes. it's just for documentation |
| 2024-10-07 03:00:58 +0200 | <geekosaur> | the actual definitions are baked into the compiler or backend |
| 2024-10-07 03:01:09 +0200 | <geekosaur> | necessarily |
| 2024-10-07 03:01:10 +0200 | <yin> | ok great, thanks |
| 2024-10-07 03:02:10 +0200 | <yin> | i wish all code was haskell all the way down to binary |
| 2024-10-07 03:02:11 +0200 | fmira | (~user@user/fmira) (Ping timeout: 260 seconds) |
| 2024-10-07 03:03:16 +0200 | <yin> | hits the magic way too soon |
| 2024-10-07 03:04:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 03:04:57 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-10-07 03:06:37 +0200 | <geekosaur> | how exactly do you write the platform's add instruction in haskell code? |
| 2024-10-07 03:06:45 +0200 | spew | (~spew@201.141.99.170) spew |
| 2024-10-07 03:07:02 +0200 | <geekosaur> | (the answer is: `+#` and the backend emits the actual instruction) |
| 2024-10-07 03:07:13 +0200 | <geekosaur> | the ones that aren;t that are mostly cmm code |
| 2024-10-07 03:09:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 03:15:56 +0200 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 2024-10-07 03:20:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 03:23:24 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-10-07 03:25:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 03:33:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 03:36:19 +0200 | <EvanR> | if the library was implemented in stuff that is eventually implemented in "haskell looking" assembly language, that would probably make optimizations harder. Because we only care about the high level semantics, not the exact sequence of instructions used |
| 2024-10-07 03:36:50 +0200 | <EvanR> | it's harder for the compiler to know another sequence of asm computes the same high level values |
| 2024-10-07 03:37:41 +0200 | <EvanR> | and if it can, and will rewrite it all, what was the point |
| 2024-10-07 03:37:45 +0200 | <EvanR> | of writing a bunch of asm |
| 2024-10-07 03:38:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 03:39:01 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-07 03:41:58 +0200 | <monochrom> | As Dennis Ritchie pointed out half a century ago, library source code means nothing if the compiler contains code to overrule it. |
| 2024-10-07 03:43:14 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 03:44:55 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-10-07 03:45:47 +0200 | <monochrom> | Not to mention that in the 1980s commercial compilers recognized popular benchmarking code and cheated. |
| 2024-10-07 03:46:56 +0200 | <monochrom> | (Probably part of why the benchmarks had to change every year.) |
| 2024-10-07 03:47:53 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2024-10-07 03:49:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 03:52:18 +0200 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 246 seconds) |
| 2024-10-07 03:53:31 +0200 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 2024-10-07 03:53:47 +0200 | qhong | (~qhong@DN200outg.stanford.edu) (Remote host closed the connection) |
| 2024-10-07 03:54:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-10-07 04:03:25 +0200 | Inst | (~Inst@user/Inst) Inst |
| 2024-10-07 04:04:36 +0200 | identity | (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60)) |
| 2024-10-07 04:04:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:09:12 +0200 | Inst | (~Inst@user/Inst) (Ping timeout: 252 seconds) |
| 2024-10-07 04:09:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-10-07 04:13:52 +0200 | td_ | (~td@i5387093A.versanet.de) (Ping timeout: 252 seconds) |
| 2024-10-07 04:15:52 +0200 | td_ | (~td@i5387091A.versanet.de) td_ |
| 2024-10-07 04:15:54 +0200 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 260 seconds) |
| 2024-10-07 04:16:24 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 04:18:22 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2024-10-07 04:18:38 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) tcard |
| 2024-10-07 04:20:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:23:08 +0200 | <haskellbridge> | <Bowuigi> L29Ah wouldn't recommend an LLM but rather something trained with Reinforcement Learning with the help of types, should get way better result and make zero type errors |
| 2024-10-07 04:25:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-07 04:29:14 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-07 04:32:47 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Read error: Connection timed out) |
| 2024-10-07 04:35:09 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 04:36:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:41:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-10-07 04:52:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:52:07 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-10-07 04:56:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:00:46 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2024-10-07 05:04:19 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-10-07 05:07:19 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-07 05:07:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:07:55 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) () |
| 2024-10-07 05:08:39 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 05:08:45 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2024-10-07 05:12:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:19:23 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-07 05:22:41 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-07 05:23:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:27:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-10-07 05:38:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:43:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:46:16 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2024-10-07 05:46:46 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 05:51:24 +0200 | synchromesh | (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) synchromesh |
| 2024-10-07 05:54:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:56:25 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a restriction on w-types that would get us all w-types that are traversable in a finite number of operations? |
| 2024-10-07 05:59:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-10-07 05:59:37 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-10-07 06:08:40 +0200 | <haskellbridge> | <Bowuigi> According to https://ncatlab.org/nlab/show/W-type every W type should be traversable in a finite number of steps |
| 2024-10-07 06:10:29 +0200 | <haskellbridge> | <Bowuigi> I mean, they represent well orders constructively |
| 2024-10-07 06:10:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:12:13 +0200 | <haskellbridge> | <Bowuigi> Every well ordered set has a least element and thus induction over the well order always terminates (assuming strong normalization outside of the W types) |
| 2024-10-07 06:12:34 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 2024-10-07 06:12:54 +0200 | <haskellbridge> | <Bowuigi> Inducting in the direction of the least element of course, like induction on the natural numbers |
| 2024-10-07 06:15:21 +0200 | <haskellbridge> | <Bowuigi> M types are the coinductive (thus possibly infinite) ones |
| 2024-10-07 06:15:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-10-07 06:20:56 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: hm issue is well-ordered trees can have infinite branches |
| 2024-10-07 06:21:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:21:46 +0200 | <haskellbridge> | <Bowuigi> Oh yeah forgot about that |
| 2024-10-07 06:22:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> so it works for induction but i'm trying to get at computable traversal |
| 2024-10-07 06:22:19 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Quit: Client closed) |
| 2024-10-07 06:23:04 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-10-07 06:23:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> uh i meant wellfounded |
| 2024-10-07 06:24:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> i'm not 100% how this translates to wellfoundedness |
| 2024-10-07 06:25:43 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah wellordered trees are less structured than wellfounded trees, only the latter must have finite chains |
| 2024-10-07 06:25:48 +0200 | <haskellbridge> | <Bowuigi> Not sure why can the trees be infinitely wide if the relation is a total order with a minimum element |
| 2024-10-07 06:26:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:26:33 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: totally ordered tree is just N |
| 2024-10-07 06:27:51 +0200 | michalz | (~michalz@185.246.207.217) |
| 2024-10-07 06:28:28 +0200 | <haskellbridge> | <Bowuigi> https://ncatlab.org/nlab/show/well-order assumes classical reasoning a lot lmao |
| 2024-10-07 06:30:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 06:31:43 +0200 | <haskellbridge> | <Bowuigi> So W-types are supposed to be a constructive counterpart to sets with a well founded irreflexive total order |
| 2024-10-07 06:32:55 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm i think we do not want well-order |
| 2024-10-07 06:33:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> because that make the tree = N |
| 2024-10-07 06:33:16 +0200 | <haskellbridge> | <thirdofmay18081814goya> or a subset |
| 2024-10-07 06:33:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> we want wellfoundedness |
| 2024-10-07 06:34:29 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 2024-10-07 06:35:01 +0200 | user4561 | myNameIs |
| 2024-10-07 06:35:23 +0200 | <haskellbridge> | <Bowuigi> The "constructiveness" is what seems to make the trees possibly infinitely wide |
| 2024-10-07 06:35:44 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: even in classical logic i think we get that wellfounded trees can be infinitely wide |
| 2024-10-07 06:36:29 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:f5b0:cd1b:e895:cf8a) (Ping timeout: 252 seconds) |
| 2024-10-07 06:36:50 +0200 | <haskellbridge> | <Bowuigi> I do not understand this topic enough yet lol, lemme learn how this works first |
| 2024-10-07 06:37:03 +0200 | <haskellbridge> | <Bowuigi> Btw this question is probably suitable for the HoTT Zulip |
| 2024-10-07 06:37:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> concretely wellfounded tree only implies that, given any chain of elements, that chain terminates. but it doesn't state anything about how many chains there can be |
| 2024-10-07 06:37:48 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: ah good point, ty |
| 2024-10-07 06:37:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> i haven't gone on there yet did not know it existed |
| 2024-10-07 06:40:39 +0200 | <haskellbridge> | <Bowuigi> Yeah, lots of smart people there. Had a question about positivity and negativity of universes, they solved it fairly quickly and directed everyone with a similar question to other stuff that I yet don't understand |
| 2024-10-07 06:40:54 +0200 | <haskellbridge> | <Bowuigi> Oh wait the HoTT book may say something about W types lemme check |
| 2024-10-07 06:41:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:42:44 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 06:44:56 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:45:39 +0200 | myNameIs | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Changing host) |
| 2024-10-07 06:45:39 +0200 | myNameIs | (~user4561@user/myNameIs) myNameIs |
| 2024-10-07 06:46:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-10-07 06:53:21 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 06:54:50 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:57:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:57:25 +0200 | myNameIs | (~user4561@user/myNameIs) (Ping timeout: 256 seconds) |
| 2024-10-07 06:57:31 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 06:59:00 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:01:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 07:03:33 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2024-10-07 07:03:35 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:05:03 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:05:15 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-07 07:07:51 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:09:19 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:12:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 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:17:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 07:17:21 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 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:18:02 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) |
| 2024-10-07 07:19:50 +0200 | <haskellbridge> | <thirdofmay18081814goya> am reading |
| 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:23:47 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:25:53 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:28:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 07:30:06 +0200 | andrewboltachev | (~andrey@178.141.123.3) andrewboltachev |
| 2024-10-07 07:30:11 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 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:32:49 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:32:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 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:34:28 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:34:30 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-07 07:36:43 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-10-07 07:37:19 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:37:26 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:39:12 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 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:40:18 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:41:53 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:46:19 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2024-10-07 07:46:26 +0200 | ZLima12_ | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2024-10-07 07:49:41 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:51:17 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:51:41 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:53:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:53:19 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-07 08:05:35 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-07 08:05:43 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-10-07 08:05:48 +0200 | cptaffe | (~cptaffe@user/cptaffe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-10-07 08:13:55 +0200 | xacktm | (xacktm@user/xacktm) (Ping timeout: 264 seconds) |
| 2024-10-07 08:16:49 +0200 | cptaffe | (~cptaffe@user/cptaffe) cptaffe |
| 2024-10-07 08:18:35 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 08:20:10 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 08:21:10 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 08:22:42 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 08:24:21 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 2024-10-07 08:26:28 +0200 | xff0x | (~xff0x@182.169.73.28) |
| 2024-10-07 08:28:26 +0200 | Fischmiep | (~Fischmiep@user/Fischmiep) (Remote host closed the connection) |
| 2024-10-07 08:29:05 +0200 | Fischmiep | (~Fischmiep@user/Fischmiep) Fischmiep |
| 2024-10-07 08:34:35 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 08:34:59 +0200 | xff0x | (~xff0x@182.169.73.28) (Ping timeout: 265 seconds) |
| 2024-10-07 08:36:06 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 08:36:40 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-07 08:37:00 +0200 | xacktm | (xacktm@user/xacktm) xacktm |
| 2024-10-07 08:37:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-07 08:37:49 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 08:41:24 +0200 | Digit | (~user@user/digit) (Ping timeout: 246 seconds) |
| 2024-10-07 08:41:26 +0200 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-10-07 08:43:42 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-10-07 08:48:34 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 08:49:38 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2024-10-07 08:50:08 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 08:52:53 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 08:54:26 +0200 | rosco | (~rosco@175.136.23.101) rosco |
| 2024-10-07 08:55:55 +0200 | madhavanmiui | (~madhavanm@2409:40f4:101b:c402:7962:1b32:f43c:cd72) |
| 2024-10-07 08:56:50 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) (Ping timeout: 244 seconds) |
| 2024-10-07 08:57:19 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-10-07 08:57:54 +0200 | madhavanmiui | (~madhavanm@2409:40f4:101b:c402:7962:1b32:f43c:cd72) (Client Quit) |
| 2024-10-07 08:59:15 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) m1dnight |
| 2024-10-07 09:00:03 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-10-07 09:00:08 +0200 | rosco | (~rosco@175.136.23.101) (Read error: Connection reset by peer) |
| 2024-10-07 09:00:41 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2024-10-07 09:00:58 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 09:01:56 +0200 | ft | (~ft@p4fc2a216.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-10-07 09:04:03 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 09:05:23 +0200 | rosco | (~rosco@175.136.23.101) rosco |
| 2024-10-07 09:09:30 +0200 | kuribas | (~user@ptr-17d51em3rhcvuvotah6.18120a2.ip6.access.telenet.be) |
| 2024-10-07 09:09:53 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2024-10-07 09:15:22 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 09:16:00 +0200 | Digitteknohippie | Digit |
| 2024-10-07 09:16:26 +0200 | gawen | (~gawen@user/gawen) gawen |
| 2024-10-07 09:17:50 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2024-10-07 09:21:46 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 09:22:58 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2024-10-07 09:23:00 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) m1dnight |
| 2024-10-07 09:24:54 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-07 09:25:24 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb09b827840f1f57a57d.dip0.t-ipconnect.de) acidjnk |
| 2024-10-07 09:36:47 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 09:40:51 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Client Quit) |
| 2024-10-07 09:41:09 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 09:42:41 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 09:46:58 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 09:52:48 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) (Ping timeout: 265 seconds) |
| 2024-10-07 09:53:23 +0200 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2024-10-07 09:54:46 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2024-10-07 10:00:54 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) m1dnight |
| 2024-10-07 10:03:06 +0200 | famubu | (~julinuser@14.139.174.50) famubu |
| 2024-10-07 10:03:06 +0200 | famubu | (~julinuser@14.139.174.50) (Changing host) |
| 2024-10-07 10:03:06 +0200 | famubu | (~julinuser@user/famubu) famubu |
| 2024-10-07 10:04:17 +0200 | <famubu> | Hi. In hedgehog, is there a way to generate n unqiue samples? We can use `Gen.sample` to get one sample. But using it repeatedly could give non-uniques samples. |
| 2024-10-07 10:04:20 +0200 | <famubu> | https://hackage.haskell.org/package/hedgehog-1.5/docs/Hedgehog-Gen.html#v:sample |
| 2024-10-07 10:05:50 +0200 | <jle`> | famubu: i wonder if you can use the Set generator |
| 2024-10-07 10:06:16 +0200 | <jle`> | it doesn't do anything smart afaict |
| 2024-10-07 10:07:20 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-10-07 10:08:36 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-10-07 10:09:26 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 10:12:39 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 10:19:05 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |