| 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…) |
| 2024-10-07 10:26:09 +0200 | rosco | (~rosco@175.136.23.101) (Read error: Connection reset by peer) |
| 2024-10-07 10:35:23 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-10-07 10:35:59 +0200 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-10-07 10:46:12 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 10:51:53 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-10-07 10:52:47 +0200 | <kuribas> | Anyone coming to munihac? |
| 2024-10-07 10:53:33 +0200 | chele | (~chele@user/chele) chele |
| 2024-10-07 10:55:20 +0200 | <lortabac> | I'm coming with a couple of colleagues |
| 2024-10-07 10:57:55 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 11:02:04 +0200 | ZLima12_ | ZLima12 |
| 2024-10-07 11:08:04 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2024-10-07 11:09:50 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
| 2024-10-07 11:09:56 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 11:10:03 +0200 | onliner10 | (~onliner10@user/onliner10) (Remote host closed the connection) |
| 2024-10-07 11:10:03 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-07 11:10:20 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2024-10-07 11:13:23 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 2024-10-07 11:14:56 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 11:16:33 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2024-10-07 11:24:12 +0200 | <kuribas> | lortabac: You have a project? |
| 2024-10-07 11:24:27 +0200 | <lortabac> | yes |
| 2024-10-07 11:24:44 +0200 | <lortabac> | more like a GHC proposal |
| 2024-10-07 11:26:39 +0200 | [exa] | curious |
| 2024-10-07 11:27:33 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-07 11:28:02 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 11:29:07 +0200 | <lortabac> | I've written a library to "fix" implicit parameters via a hack + a GHC plugin |
| 2024-10-07 11:30:05 +0200 | <lortabac> | but it's a proof of concept, a proper implementation would require modifying GHC |
| 2024-10-07 11:31:00 +0200 | <lortabac> | I have various options between "not doing nothing and keep using the hack" and "make a full-fledged GHC proposal to implement this exactly as I have it in mind" |
| 2024-10-07 11:31:08 +0200 | <lortabac> | *not doing anything |
| 2024-10-07 11:33:18 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-07 11:34:42 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 11:40:15 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 11:40:40 +0200 | caubert_ | (~caubert@user/caubert) (Quit: WeeChat 4.3.3) |
| 2024-10-07 11:40:55 +0200 | caubert | (~caubert@user/caubert) caubert |
| 2024-10-07 11:40:59 +0200 | hsw__ | (~hsw@112-104-11-250.adsl.dynamic.seed.net.tw) (Quit: Leaving) |
| 2024-10-07 11:41:14 +0200 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) hsw |
| 2024-10-07 11:45:25 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-10-07 11:46:23 +0200 | <famubu> | jle`: Thanks. Let me try that. |
| 2024-10-07 11:47:11 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 11:53:18 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 12:00:04 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-07 12:00:17 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-10-07 12:04:45 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 2024-10-07 12:05:13 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 12:06:16 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-07 12:09:57 +0200 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) jespada |
| 2024-10-07 12:10:10 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 12:10:28 +0200 | arahael | (~arahael@user/arahael) arahael |
| 2024-10-07 12:10:29 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds) |
| 2024-10-07 12:21:34 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 2024-10-07 12:22:20 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 12:39:52 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-10-07 12:41:39 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 12:49:16 +0200 | identity | (~identity@user/ZharMeny) identity |
| 2024-10-07 12:52:39 +0200 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-10-07 12:53:14 +0200 | Digit | (~user@user/digit) (Ping timeout: 272 seconds) |
| 2024-10-07 12:53:48 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds) |
| 2024-10-07 12:59:06 +0200 | Digitteknohippie | Digit |
| 2024-10-07 13:01:43 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 13:02:05 +0200 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 13:03:34 +0200 | rosco | (~rosco@175.136.22.30) rosco |
| 2024-10-07 13:04:36 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2024-10-07 13:11:14 +0200 | xff0x | (~xff0x@2405:6580:b080:900:31d8:fed5:6c70:b7b9) |
| 2024-10-07 13:17:33 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 13:20:11 +0200 | identity | (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60)) |
| 2024-10-07 13:21:16 +0200 | identity | (~identity@user/ZharMeny) identity |
| 2024-10-07 13:21:42 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-07 13:23:04 +0200 | tdammers_ | tdammers |
| 2024-10-07 13:24:34 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 13:24:54 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) (Ping timeout: 246 seconds) |
| 2024-10-07 13:25:53 +0200 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-10-07 13:26:13 +0200 | Digit | (~user@user/digit) (Ping timeout: 248 seconds) |
| 2024-10-07 13:26:32 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 13:31:45 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 13:32:12 +0200 | Digitteknohippie | Digit |
| 2024-10-07 13:33:44 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-10-07 13:38:34 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 13:43:21 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 276 seconds) |
| 2024-10-07 13:48:21 +0200 | <hc> | Hi all, I'm curious, I'm sure in this channel are some people who are developing commercial projects with haskell |
| 2024-10-07 13:48:49 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Read error: Connection reset by peer) |
| 2024-10-07 13:48:52 +0200 | <hc> | When it comes to security, do you use a static code analysis tool to scan for errors in your haskell code? Or are your customers convinced that haskell's typesystem itself is protection enough? |
| 2024-10-07 13:53:12 +0200 | <tdammers> | hc: neither. The type system helps, but ultimately, you should use all reasonable tools at your disposal, and security-aware design, security-focused code reviews, and, where appropriate, penetration testing, cannot easily be replaced with just static analysis. |
| 2024-10-07 13:54:32 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) (Quit: WeeChat 4.4.2) |
| 2024-10-07 13:54:46 +0200 | <hc> | tdammers: When you say neither you mean you're not using a static analysis tool? Or you are using one? |
| 2024-10-07 13:54:56 +0200 | <hc> | But not as an only measure? |
| 2024-10-07 13:55:00 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) m1dnight |
| 2024-10-07 13:55:38 +0200 | <tdammers> | I am not using any static analysis tools; I'm not even sure whether there's anything good out there for Haskell. But I'm not trying to convince any clients that Haskell's type system is enough to prevent any and all security issues, because that would be reckless. |
| 2024-10-07 13:56:16 +0200 | <kuribas> | This. Haskell typesystem is great for making robust software, but it hasn't been designed with security in mind. |
| 2024-10-07 13:56:17 +0200 | <hc> | Okay, I think my question was misleading |
| 2024-10-07 13:56:22 +0200 | <tdammers> | In a way, Haskell's type system *is* a static analysis tool though, and you can use it, to some extent, to find or prevent typical security issues. |
| 2024-10-07 13:56:25 +0200 | <kuribas> | Neither is the ghc runtime I think. |
| 2024-10-07 13:56:31 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) (Client Quit) |
| 2024-10-07 13:56:42 +0200 | <hc> | I didn't mean to ask whether the type system prevents security issues, but whether it makes the use of a(n external) static analysis tool superfluous |
| 2024-10-07 13:56:47 +0200 | m1dnight | (~christoph@d8D861908.access.telenet.be) m1dnight |
| 2024-10-07 13:57:33 +0200 | <tdammers> | I wouldn't say superfluous, no, but the reason external tools are popular in many other languages is because they don't have an existing type system that you could hook into for that |
| 2024-10-07 13:57:39 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-10-07 13:58:01 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 13:58:07 +0200 | <hc> | okok, because yeah, like you said, is there even an analysis tool out there that supports haskell? Or rust for that matter? |
| 2024-10-07 13:58:46 +0200 | <tdammers> | I'm not aware of any, but I'm sure some companies out there that use Haskell (or Rust) for Very Serious Applications will have some kind of in-house solution for that |
| 2024-10-07 13:59:18 +0200 | <hc> | Could be, and there's ivory and tower for niche applications |
| 2024-10-07 13:59:28 +0200 | <hc> | But that's not really "standard" haskell anymore %} |
| 2024-10-07 13:59:39 +0200 | <tdammers> | but anyway, I guess my point is that for many of the things that would require an external tool in, say, Python or PHP, you can get similar results in Haskell by leveraging the type system |
| 2024-10-07 14:00:11 +0200 | <hc> | Okay, yeah, I have a similar view on this and you're basically confirming it, thanks :-) |
| 2024-10-07 14:00:16 +0200 | dlock23 | (~dlock23@78.red-81-40-75.staticip.rima-tde.net) |
| 2024-10-07 14:00:17 +0200 | <hc> | Always good to get a 2nd opinion |
| 2024-10-07 14:00:29 +0200 | <tdammers> | e.g., you can prevent and flag incorrect HTML encoding errors (which pave the way for SQLi vulnerabilities) in Haskell by using separate HTML and plaintext types, and forcing all HTML construction from plaintext to go through a small handful of "blessed" conversion functions |
| 2024-10-07 14:01:00 +0200 | <hc> | Yeah, and there's a special "static text only" string type for SQL queries |
| 2024-10-07 14:01:26 +0200 | <tdammers> | yeah, stuff like that. it's not perfect, but static code analysis tools aren't either |
| 2024-10-07 14:02:02 +0200 | <hc> | Yeah; my feeling is that they're eliminating a bit the deficiencies of languages with type systems that are less expressive than haskell's, rust's or similar languages' |
| 2024-10-07 14:02:44 +0200 | <hc> | So may I ask, if you code commercial software in haskell, you do pentests and internal reviews of the code and otherwise rely on the type system? Or is there a step that I missed? |
| 2024-10-07 14:02:50 +0200 | <hc> | s/step/measure/ |
| 2024-10-07 14:05:18 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 14:06:48 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 14:07:19 +0200 | ystael | (~ystael@user/ystael) ystael |
| 2024-10-07 14:08:34 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 14:11:49 +0200 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 14:12:15 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 14:13:00 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds) |
| 2024-10-07 14:15:22 +0200 | Leonard26 | (~Leonard26@49.236.8.9) |
| 2024-10-07 14:17:16 +0200 | <Leonard26> | Hello! How are you today? :] I was wondering if there was a way to have a variable that increases over time whenever a function gets called in Haskell? Sort of like a for loop in JavaScript |
| 2024-10-07 14:19:13 +0200 | <__monty__> | Leonard26: Recursive functions sometimes have an accumulator argument. Which is usually used as the result when a stop condition is reached. |
| 2024-10-07 14:19:43 +0200 | <__monty__> | The pattern is usually expressed as a fold, left/right/monoidal. |
| 2024-10-07 14:19:53 +0200 | <__monty__> | So check out `foldr`. |
| 2024-10-07 14:22:49 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) alexherbo2 |
| 2024-10-07 14:23:29 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 14:23:29 +0200 | <Leonard26> | Thank you, I will check it out now |
| 2024-10-07 14:24:14 +0200 | <Lears> | :t \n -> for_ [0..n] |
| 2024-10-07 14:24:15 +0200 | <lambdabot> | (Applicative f, Num a, Enum a) => a -> (a -> f b) -> f () |
| 2024-10-07 14:25:03 +0200 | <Leonard26> | (y) |
| 2024-10-07 14:25:23 +0200 | diod | (~diod@142.188.102.4) sonny |
| 2024-10-07 14:25:50 +0200 | malte | (~malte@mal.tc) (Ping timeout: 252 seconds) |
| 2024-10-07 14:26:09 +0200 | <diod> | in object oriented and others classes/libraries are organized in hierarchy, what happens in haskell? |
| 2024-10-07 14:26:23 +0200 | <tdammers> | hc: pentests and external audits if there's enough of an incentive, and the client is paying for them. reviews (both of the design and the code), always. I'll also do some informal self-pen-testing usually, taking my code and approaching it with a hacker mindset, trying to break it. |
| 2024-10-07 14:27:17 +0200 | <tdammers> | diod: just because they're not classes doesn't mean you can't have organizational hierarchies. Haskell has a decent module system, and it is commonly used for this exact purpose. Libraries and packages work pretty much like in any other language that has them. |
| 2024-10-07 14:27:53 +0200 | <diod> | ah ok, interesting |
| 2024-10-07 14:27:57 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 2024-10-07 14:28:18 +0200 | <diod> | I was thinking functions are independent so hierarchy wouldn't be needed |
| 2024-10-07 14:28:41 +0200 | <tdammers> | it's not technically needed, but it's still useful as a code organization strategy |
| 2024-10-07 14:29:10 +0200 | <tdammers> | also, you can have dependencies between functions too |
| 2024-10-07 14:29:32 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-07 14:29:52 +0200 | <diod> | ok, ty |
| 2024-10-07 14:29:56 +0200 | malte | (~malte@mal.tc) malte |
| 2024-10-07 14:35:14 +0200 | <Leonard26> | I have read what foldr does, I'm not sure it is what I was looking for. I have a list of values that I want to give a variable to in order. So when the function gets called the first time the first value is set for the variable, when the function gets called for the second time the second value is set, the third call sets the third value and so on |
| 2024-10-07 14:35:14 +0200 | <Leonard26> | and on until the last value when it stops. How could this be achieved? =L |
| 2024-10-07 14:35:15 +0200 | <Leonard26> | Say I have these values for example [0.00,0.05,0.10,0.15,0.20,0.25,0.30,0.35,0.40,0.45,0.50] |
| 2024-10-07 14:36:18 +0200 | <__monty__> | What's your expected output? |
| 2024-10-07 14:37:53 +0200 | <hc> | tdammers: kk, thanks, that makes sense :-) |
| 2024-10-07 14:39:46 +0200 | <Leonard26> | I am working with Gstreamer, I have a video stream that needs to fade out, the values I am talking about are the opacity property of the video. |
| 2024-10-07 14:41:10 +0200 | <Leonard26> | I have a function that gets called every 1s, that's why the variable must change each time |
| 2024-10-07 14:42:29 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2024-10-07 14:44:13 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 14:46:52 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-07 14:46:53 +0200 | <kuribas> | > foldr (+) [a, b, c, d] e |
| 2024-10-07 14:46:54 +0200 | <lambdabot> | error: |
| 2024-10-07 14:46:54 +0200 | <lambdabot> | • Couldn't match expected type ‘t0 [Expr]’ with actual type ‘Expr’ |
| 2024-10-07 14:46:54 +0200 | <lambdabot> | • In the third argument of ‘foldr’, namely ‘e’ |
| 2024-10-07 14:47:07 +0200 | <kuribas> | > foldr (+) e [a, b, c, d] |
| 2024-10-07 14:47:08 +0200 | <lambdabot> | a + (b + (c + (d + e))) |
| 2024-10-07 14:47:16 +0200 | <kuribas> | > foldl (+) e [a, b, c, d] |
| 2024-10-07 14:47:17 +0200 | <lambdabot> | e + a + b + c + d |
| 2024-10-07 14:47:37 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 14:49:05 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-10-07 14:49:29 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-10-07 14:53:42 +0200 | dyniec | (~dyniec@dybiec.info) dyniec |
| 2024-10-07 14:56:49 +0200 | Typedfern | (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) (Ping timeout: 265 seconds) |
| 2024-10-07 15:00:23 +0200 | cfricke | (~cfricke@user/cfricke) (Remote host closed the connection) |
| 2024-10-07 15:00:34 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:00:40 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 15:00:48 +0200 | cfricke | (~cfricke@user/cfricke) (Remote host closed the connection) |
| 2024-10-07 15:01:03 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 15:01:54 +0200 | Duste3 | (~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816) |
| 2024-10-07 15:03:19 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 15:03:23 +0200 | <Duste3> | Are Kinds the same thing as Type 1 universe level in a theorem prover like Lean? |
| 2024-10-07 15:05:54 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-10-07 15:06:33 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:06:57 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2024-10-07 15:07:29 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-07 15:08:30 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 2024-10-07 15:09:11 +0200 | Typedfern | (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) |
| 2024-10-07 15:13:03 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-10-07 15:14:49 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 15:16:36 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 15:16:42 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 15:18:21 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:20:19 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.4.2) |
| 2024-10-07 15:20:26 +0200 | <tomsmeding> | Duste3: values have types, and types have kinds |
| 2024-10-07 15:20:47 +0200 | <tomsmeding> | not sure about the precise numbering of the universe levels, but it indeed corresponds to one universe level higher than types |
| 2024-10-07 15:21:54 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) NinjaTrappeur |
| 2024-10-07 15:22:05 +0200 | <tomsmeding> | but do note that Haskell is inconsistent when viewed as a theorem prover, because Type \in Type (where Type is the kind of types that can hold values, sometimes written *) |
| 2024-10-07 15:22:30 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-10-07 15:22:52 +0200 | <tomsmeding> | (it's also inconsistent as a theorem prover for a bunch of other reasons) |
| 2024-10-07 15:27:20 +0200 | <Duste3> | Ok thanks |
| 2024-10-07 15:29:33 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 2024-10-07 15:29:37 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-07 15:29:59 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 15:37:34 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-07 15:39:52 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-07 15:40:11 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) alexherbo2 |
| 2024-10-07 15:40:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 15:40:57 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-10-07 15:52:34 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 15:54:52 +0200 | mari-estel | (~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) |
| 2024-10-07 15:55:22 +0200 | <EvanR> | Char :: Type |
| 2024-10-07 15:55:29 +0200 | <EvanR> | but also |
| 2024-10-07 15:55:31 +0200 | <EvanR> | Type :: Type |
| 2024-10-07 15:55:43 +0200 | <EvanR> | there's no Type 1 |
| 2024-10-07 15:57:45 +0200 | <EvanR> | the question seemed to be if "Kinds" as a conversational category of things "is the same thing" as "Type 1" which is a type, and has type Type 2 |
| 2024-10-07 15:57:54 +0200 | <EvanR> | so by definition they seem to be different |
| 2024-10-07 16:00:52 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 2024-10-07 16:05:56 +0200 | mari-estel | (~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) (Ping timeout: 265 seconds) |
| 2024-10-07 16:07:33 +0200 | Leonard26 | (~Leonard26@49.236.8.9) (Quit: Client closed) |
| 2024-10-07 16:10:38 +0200 | <Duste3> | Since Type :: Type then Haskell would be considered Impredicative? (and so its inconsistent as a theorem prover) |
| 2024-10-07 16:11:31 +0200 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 264 seconds) |
| 2024-10-07 16:12:03 +0200 | <dolio> | Type :: Type is more than impredicative. It's is outright inconsistent. |
| 2024-10-07 16:12:25 +0200 | <dolio> | Like having a set of all sets. |
| 2024-10-07 16:12:45 +0200 | <dolio> | (And not being New Foundations, I suppose.) |
| 2024-10-07 16:12:46 +0200 | synchromesh | (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) (Read error: Connection reset by peer) |
| 2024-10-07 16:13:11 +0200 | <haskellbridge> | <Bowuigi> Haskell already was inconsistent because you have access to general recursion and to undefined (bottom) |
| 2024-10-07 16:13:18 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-07 16:13:49 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-07 16:14:13 +0200 | synchromesh | (~john@2406:5a00:241a:5600:1537:bb1c:ebe9:2fdf) synchromesh |
| 2024-10-07 16:15:44 +0200 | <dolio> | GHC is impredicative in the type theory sense once you allow data types that have `forall` in the types of fields. |
| 2024-10-07 16:15:48 +0200 | <fr33domlover> | o/ Given some type `a`, is there a way to get a unique `(s :: Symbol)` that represents type `a`? Kind of like a type-level Show/Unique |
| 2024-10-07 16:16:18 +0200 | <dolio> | (Despite that not being the thing that ImpredicativeTypes enables.) |
| 2024-10-07 16:17:30 +0200 | <EvanR> | what a mess |
| 2024-10-07 16:19:14 +0200 | diod | (~diod@142.188.102.4) () |
| 2024-10-07 16:21:16 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 16:21:22 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 16:22:23 +0200 | <haskellbridge> | <Bowuigi> Duste3 /dolio Yeah there are two kinds of impredicativity. One is having an "impredicative universe" (which is the case with Type) and the other is being able to instance type variables to types with foralls |
| 2024-10-07 16:23:05 +0200 | <dolio> | It's not really two different things. GHC just divides them up strangely. |
| 2024-10-07 16:24:56 +0200 | <dolio> | The impredicativity is that `forall a. ...` has kind Type despite quantifying over Type. However, by default, GHC does this weird thing where even though that quantified type supposedly has kind Type, you can't use it everywhere something of kind Type is expected. |
| 2024-10-07 16:25:06 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2024-10-07 16:25:07 +0200 | ljdarj1 | ljdarj |
| 2024-10-07 16:25:19 +0200 | <haskellbridge> | <Bowuigi> Impredicativity just means "something that contains itself" so that checks out I guess |
| 2024-10-07 16:26:21 +0200 | <dolio> | There's sort of a similar situation, where type families/aliases are reported to have some kind, but you can't use them everywhere things of that kind are expected. |
| 2024-10-07 16:26:57 +0200 | <haskellbridge> | <Bowuigi> Also type inference (ala HM, inferring type applications and abstractions) in impredicative system F is undecidable IIRC, it makes sense that GHC is a bit conservative just in casd |
| 2024-10-07 16:27:59 +0200 | <dolio> | Yeah. I don't think you can even manually instantiate without ImpredicativeTypes, though. |