| 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 |