2024/10/07

2024-10-07 00:04:06 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-10-07 00:05:13 +0200artu(artu@2600:3c01::f03c:92ff:fecc:1d32)
2024-10-07 00:06:03 +0200gawen(~gawen@user/gawen) (Quit: cya)
2024-10-07 00:08:51 +0200neuroevolutus(~neuroevol@146.70.211.110) (Ping timeout: 256 seconds)
2024-10-07 00:10:35 +0200artu(artu@2600:3c01::f03c:92ff:fecc:1d32) (Quit: ZNC 1.7.2+deb3 - https://znc.in)
2024-10-07 00:14:40 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 00:18:43 +0200artu(artu@2600:3c01::f03c:92ff:fecc:1d32)
2024-10-07 00:19:12 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 00:30:06 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 00:33:04 +0200troojg(~troojg@user/troojg) (Ping timeout: 260 seconds)
2024-10-07 00:34:58 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 00:37:29 +0200peterbecich(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 00:46:12 +0200artu(artu@2600:3c01::f03c:92ff:fecc:1d32) (Remote host closed the connection)
2024-10-07 00:47:04 +0200artu(artu@2600:3c01::f03c:92ff:fecc:1d32) artu
2024-10-07 00:50:24 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-10-07 00:51:49 +0200acidjnk(~acidjnk@p200300d6e72cfb9628aff41673680d4c.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2024-10-07 01:01:09 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 01:03:33 +0200sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 252 seconds)
2024-10-07 01:05:46 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 01:12:30 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-10-07 01:16:34 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 01:17:27 +0200euphores(~SASL_euph@user/euphores) euphores
2024-10-07 01:21:27 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 01:24:28 +0200LukeHoersten(~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 +0200myxokephale(~myxos@syn-065-028-251-121.res.spectrum.com) (Quit: myxokephale)
2024-10-07 01:32:00 +0200merijn(~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 +0200merijn(~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 +0200L29Ahhides
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 +0200merijn(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 01:57:51 +0200myxos(~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale
2024-10-07 02:03:03 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 02:07:59 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-10-07 02:14:50 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod
2024-10-07 02:18:00 +0200ystael(~ystael@user/ystael) (Ping timeout: 272 seconds)
2024-10-07 02:18:33 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 02:21:41 +0200supercode(~supercode@user/supercode) (Quit: Client closed)
2024-10-07 02:22:42 +0200fmira(~user@user/fmira) fmira
2024-10-07 02:22:57 +0200fmira(~user@user/fmira) (Remote host closed the connection)
2024-10-07 02:23:03 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 02:23:22 +0200fmira(~user@user/fmira) fmira
2024-10-07 02:30:44 +0200Inst(~Inst@user/Inst) (Ping timeout: 255 seconds)
2024-10-07 02:31:43 +0200Inst(~Inst@user/Inst) Inst
2024-10-07 02:32:40 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection)
2024-10-07 02:33:58 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 02:36:21 +0200Inst(~Inst@user/Inst) (Ping timeout: 246 seconds)
2024-10-07 02:38:32 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 02:46:44 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2024-10-07 02:47:04 +0200xff0x(~xff0x@2405:6580:b080:900:16eb:2432:285b:7ea6) (Ping timeout: 260 seconds)
2024-10-07 02:49:24 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 02:53:32 +0200EvanR_EvanR
2024-10-07 02:53:56 +0200merijn(~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 +0200ethantwardy(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 +0200fmira(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 03:04:57 +0200weary-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 +0200spew(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 03:15:56 +0200ethantwardy(user@user/ethantwardy) ethantwardy
2024-10-07 03:20:21 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 03:23:24 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-10-07 03:25:06 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 03:33:54 +0200merijn(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 03:39:01 +0200xff0x(~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 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-07 03:44:55 +0200athan(~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 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 265 seconds)
2024-10-07 03:49:19 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 03:52:18 +0200ethantwardy(user@user/ethantwardy) (Ping timeout: 246 seconds)
2024-10-07 03:53:31 +0200ethantwardy(user@user/ethantwardy) ethantwardy
2024-10-07 03:53:47 +0200qhong(~qhong@DN200outg.stanford.edu) (Remote host closed the connection)
2024-10-07 03:54:10 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-10-07 04:03:25 +0200Inst(~Inst@user/Inst) Inst
2024-10-07 04:04:36 +0200identity(~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60))
2024-10-07 04:04:45 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 04:09:12 +0200Inst(~Inst@user/Inst) (Ping timeout: 252 seconds)
2024-10-07 04:09:54 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-10-07 04:13:52 +0200td_(~td@i5387093A.versanet.de) (Ping timeout: 252 seconds)
2024-10-07 04:15:52 +0200td_(~td@i5387091A.versanet.de) td_
2024-10-07 04:15:54 +0200ethantwardy(user@user/ethantwardy) (Ping timeout: 260 seconds)
2024-10-07 04:16:24 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-07 04:18:22 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection)
2024-10-07 04:18:38 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) tcard
2024-10-07 04:20:29 +0200merijn(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-10-07 04:29:14 +0200weary-traveler(~user@user/user363627) user363627
2024-10-07 04:32:47 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Read error: Connection timed out)
2024-10-07 04:35:09 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-07 04:36:17 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 04:41:05 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-10-07 04:52:04 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 04:52:07 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2024-10-07 04:56:46 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 05:00:46 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 272 seconds)
2024-10-07 05:04:19 +0200spew(~spew@201.141.99.170) (Quit: spew)
2024-10-07 05:07:19 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-07 05:07:35 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 05:07:55 +0200ZLima12(~zlima12@user/meow/ZLima12) ()
2024-10-07 05:08:39 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-10-07 05:08:45 +0200ZLima12(~zlima12@user/meow/ZLima12) ZLima12
2024-10-07 05:12:10 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 05:19:23 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection)
2024-10-07 05:22:41 +0200fmira(~user@user/fmira) fmira
2024-10-07 05:23:01 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 05:27:51 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-10-07 05:38:29 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 05:43:20 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 05:46:16 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
2024-10-07 05:46:46 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-07 05:51:24 +0200synchromesh(~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) synchromesh
2024-10-07 05:54:03 +0200merijn(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds)
2024-10-07 05:59:37 +0200weary-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 +0200merijn(~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 +0200user4561(~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 +0200merijn(~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 +0200youthlic(~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 +0200user4561(~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Quit: Client closed)
2024-10-07 06:23:04 +0200machinedgod(~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 +0200merijn(~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 +0200michalz(~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 +0200merijn(~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 +0200user4561(~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98)
2024-10-07 06:35:01 +0200user4561myNameIs
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 +0200alp_(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 06:42:44 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 06:44:56 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 06:45:39 +0200myNameIs(~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Changing host)
2024-10-07 06:45:39 +0200myNameIs(~user4561@user/myNameIs) myNameIs
2024-10-07 06:46:32 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2024-10-07 06:53:21 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 06:54:50 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 06:57:09 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 06:57:25 +0200myNameIs(~user4561@user/myNameIs) (Ping timeout: 256 seconds)
2024-10-07 06:57:31 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 06:59:00 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:01:47 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 07:03:33 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
2024-10-07 07:03:35 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 07:05:03 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:05:15 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2024-10-07 07:07:51 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 07:09:19 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:12:34 +0200merijn(~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 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 07:17:21 +0200takuan(~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 +0200alp_(~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 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 07:25:53 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:28:04 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 07:30:06 +0200andrewboltachev(~andrey@178.141.123.3) andrewboltachev
2024-10-07 07:30:11 +0200Sgeo(~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 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 07:32:58 +0200merijn(~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 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:34:30 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-07 07:36:43 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2024-10-07 07:37:19 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:37:26 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 07:39:12 +0200youthlic(~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 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 07:41:53 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:46:19 +0200ZLima12(~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds)
2024-10-07 07:46:26 +0200ZLima12_(~zlima12@user/meow/ZLima12) ZLima12
2024-10-07 07:49:41 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 07:51:17 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:51:41 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 07:53:13 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 07:53:19 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-10-07 08:05:35 +0200euphores(~SASL_euph@user/euphores) euphores
2024-10-07 08:05:43 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod
2024-10-07 08:05:48 +0200cptaffe(~cptaffe@user/cptaffe) (Quit: ZNC 1.8.2 - https://znc.in)
2024-10-07 08:13:55 +0200xacktm(xacktm@user/xacktm) (Ping timeout: 264 seconds)
2024-10-07 08:16:49 +0200cptaffe(~cptaffe@user/cptaffe) cptaffe
2024-10-07 08:18:35 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 08:20:10 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 08:21:10 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 08:22:42 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 08:24:21 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds)
2024-10-07 08:26:28 +0200xff0x(~xff0x@182.169.73.28)
2024-10-07 08:28:26 +0200Fischmiep(~Fischmiep@user/Fischmiep) (Remote host closed the connection)
2024-10-07 08:29:05 +0200Fischmiep(~Fischmiep@user/Fischmiep) Fischmiep
2024-10-07 08:34:35 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 08:34:59 +0200xff0x(~xff0x@182.169.73.28) (Ping timeout: 265 seconds)
2024-10-07 08:36:06 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 08:36:40 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2024-10-07 08:37:00 +0200xacktm(xacktm@user/xacktm) xacktm
2024-10-07 08:37:03 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 08:37:49 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 08:41:24 +0200Digit(~user@user/digit) (Ping timeout: 246 seconds)
2024-10-07 08:41:26 +0200Digitteknohippie(~user@user/digit) Digit
2024-10-07 08:43:42 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 272 seconds)
2024-10-07 08:48:34 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 08:49:38 +0200sord937(~sord937@gateway/tor-sasl/sord937) sord937
2024-10-07 08:50:08 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 08:52:53 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 08:54:26 +0200rosco(~rosco@175.136.23.101) rosco
2024-10-07 08:55:55 +0200madhavanmiui(~madhavanm@2409:40f4:101b:c402:7962:1b32:f43c:cd72)
2024-10-07 08:56:50 +0200m1dnight(~christoph@d8D861908.access.telenet.be) (Ping timeout: 244 seconds)
2024-10-07 08:57:19 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-10-07 08:57:54 +0200madhavanmiui(~madhavanm@2409:40f4:101b:c402:7962:1b32:f43c:cd72) (Client Quit)
2024-10-07 08:59:15 +0200m1dnight(~christoph@d8D861908.access.telenet.be) m1dnight
2024-10-07 09:00:03 +0200caconym(~caconym@user/caconym) (Quit: bye)
2024-10-07 09:00:08 +0200rosco(~rosco@175.136.23.101) (Read error: Connection reset by peer)
2024-10-07 09:00:41 +0200caconym(~caconym@user/caconym) caconym
2024-10-07 09:00:58 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 09:01:56 +0200ft(~ft@p4fc2a216.dip0.t-ipconnect.de) (Quit: leaving)
2024-10-07 09:04:03 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 09:05:23 +0200rosco(~rosco@175.136.23.101) rosco
2024-10-07 09:09:30 +0200kuribas(~user@ptr-17d51em3rhcvuvotah6.18120a2.ip6.access.telenet.be)
2024-10-07 09:09:53 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 255 seconds)
2024-10-07 09:15:22 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-07 09:16:00 +0200DigitteknohippieDigit
2024-10-07 09:16:26 +0200gawen(~gawen@user/gawen) gawen
2024-10-07 09:17:50 +0200m1dnight(~christoph@d8D861908.access.telenet.be) (Ping timeout: 252 seconds)
2024-10-07 09:21:46 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 09:22:58 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
2024-10-07 09:23:00 +0200m1dnight(~christoph@d8D861908.access.telenet.be) m1dnight
2024-10-07 09:24:54 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2024-10-07 09:25:24 +0200acidjnk(~acidjnk@p200300d6e72cfb09b827840f1f57a57d.dip0.t-ipconnect.de) acidjnk
2024-10-07 09:36:47 +0200ash3en(~Thunderbi@89.246.174.164) ash3en
2024-10-07 09:40:51 +0200ash3en(~Thunderbi@89.246.174.164) (Client Quit)
2024-10-07 09:41:09 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 09:42:41 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 09:46:58 +0200ash3en(~Thunderbi@89.246.174.164) ash3en
2024-10-07 09:52:48 +0200m1dnight(~christoph@d8D861908.access.telenet.be) (Ping timeout: 265 seconds)
2024-10-07 09:53:23 +0200sawilagar(~sawilagar@user/sawilagar) sawilagar
2024-10-07 09:54:46 +0200__monty__(~toonn@user/toonn) toonn
2024-10-07 10:00:54 +0200m1dnight(~christoph@d8D861908.access.telenet.be) m1dnight
2024-10-07 10:03:06 +0200famubu(~julinuser@14.139.174.50) famubu
2024-10-07 10:03:06 +0200famubu(~julinuser@14.139.174.50) (Changing host)
2024-10-07 10:03:06 +0200famubu(~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 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2024-10-07 10:08:36 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-10-07 10:09:26 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 10:12:39 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 10:19:05 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-07 10:26:09 +0200rosco(~rosco@175.136.23.101) (Read error: Connection reset by peer)
2024-10-07 10:35:23 +0200rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2024-10-07 10:35:59 +0200rvalue(~rvalue@user/rvalue) rvalue
2024-10-07 10:46:12 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 10:51:53 +0200Smiles(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 +0200chele(~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 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 11:02:04 +0200ZLima12_ZLima12
2024-10-07 11:08:04 +0200JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2024-10-07 11:09:50 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer)
2024-10-07 11:09:56 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-07 11:10:03 +0200onliner10(~onliner10@user/onliner10) (Remote host closed the connection)
2024-10-07 11:10:03 +0200CiaoSen(~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) CiaoSen
2024-10-07 11:10:20 +0200Lord_of_Life_Lord_of_Life
2024-10-07 11:13:23 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Client Quit)
2024-10-07 11:14:56 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-07 11:16:33 +0200xff0x(~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 +0200Lord_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 +0200Lord_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 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 11:34:42 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 11:40:15 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 11:40:40 +0200caubert_(~caubert@user/caubert) (Quit: WeeChat 4.3.3)
2024-10-07 11:40:55 +0200caubert(~caubert@user/caubert) caubert
2024-10-07 11:40:59 +0200hsw__(~hsw@112-104-11-250.adsl.dynamic.seed.net.tw) (Quit: Leaving)
2024-10-07 11:41:14 +0200hsw(~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) hsw
2024-10-07 11:45:25 +0200merijn(~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 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 11:53:18 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 12:00:04 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-07 12:00:17 +0200cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-10-07 12:04:45 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 265 seconds)
2024-10-07 12:05:13 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 12:06:16 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-07 12:09:57 +0200jespada(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) jespada
2024-10-07 12:10:10 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 12:10:28 +0200arahael(~arahael@user/arahael) arahael
2024-10-07 12:10:29 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds)
2024-10-07 12:21:34 +0200CiaoSen(~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds)
2024-10-07 12:22:20 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 12:39:52 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2024-10-07 12:41:39 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 12:49:16 +0200identity(~identity@user/ZharMeny) identity
2024-10-07 12:52:39 +0200Digitteknohippie(~user@user/digit) Digit
2024-10-07 12:53:14 +0200Digit(~user@user/digit) (Ping timeout: 272 seconds)
2024-10-07 12:53:48 +0200ash3en(~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds)
2024-10-07 12:59:06 +0200DigitteknohippieDigit
2024-10-07 13:01:43 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 13:02:05 +0200comerijn(~merijn@77.242.116.146) merijn
2024-10-07 13:03:34 +0200rosco(~rosco@175.136.22.30) rosco
2024-10-07 13:04:36 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 246 seconds)
2024-10-07 13:11:14 +0200xff0x(~xff0x@2405:6580:b080:900:31d8:fed5:6c70:b7b9)
2024-10-07 13:17:33 +0200comerijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 13:20:11 +0200identity(~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60))
2024-10-07 13:21:16 +0200identity(~identity@user/ZharMeny) identity
2024-10-07 13:21:42 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-10-07 13:23:04 +0200tdammers_tdammers
2024-10-07 13:24:34 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 13:24:54 +0200alp_(~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) (Ping timeout: 246 seconds)
2024-10-07 13:25:53 +0200Digitteknohippie(~user@user/digit) Digit
2024-10-07 13:26:13 +0200Digit(~user@user/digit) (Ping timeout: 248 seconds)
2024-10-07 13:26:32 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-07 13:31:45 +0200ash3en(~Thunderbi@89.246.174.164) ash3en
2024-10-07 13:32:12 +0200DigitteknohippieDigit
2024-10-07 13:33:44 +0200cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-10-07 13:38:34 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-07 13:43:21 +0200ash3en(~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 +0200hiecaq(~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 +0200m1dnight(~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 +0200m1dnight(~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 +0200m1dnight(~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 +0200m1dnight(~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 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 276 seconds)
2024-10-07 13:58:01 +0200merijn(~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 +0200dlock23(~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 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 14:06:48 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 14:07:19 +0200ystael(~ystael@user/ystael) ystael
2024-10-07 14:08:34 +0200ash3en(~Thunderbi@89.246.174.164) ash3en
2024-10-07 14:11:49 +0200comerijn(~merijn@77.242.116.146) merijn
2024-10-07 14:12:15 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 14:13:00 +0200ash3en(~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds)
2024-10-07 14:15:22 +0200Leonard26(~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 +0200alexherbo2(~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) alexherbo2
2024-10-07 14:23:29 +0200morb(~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 +0200diod(~diod@142.188.102.4) sonny
2024-10-07 14:25:50 +0200malte(~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 +0200morb(~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 +0200CiaoSen(~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 +0200malte(~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 +0200comerijn(~merijn@77.242.116.146) (Ping timeout: 248 seconds)
2024-10-07 14:44:13 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 14:46:52 +0200Lord_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 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-07 14:49:05 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 265 seconds)
2024-10-07 14:49:29 +0200sourcetarius(~sourcetar@user/sourcetarius) (Quit: sourcetarius)
2024-10-07 14:53:42 +0200dyniec(~dyniec@dybiec.info) dyniec
2024-10-07 14:56:49 +0200Typedfern(~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) (Ping timeout: 265 seconds)
2024-10-07 15:00:23 +0200cfricke(~cfricke@user/cfricke) (Remote host closed the connection)
2024-10-07 15:00:34 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 15:00:40 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-07 15:00:48 +0200cfricke(~cfricke@user/cfricke) (Remote host closed the connection)
2024-10-07 15:01:03 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-07 15:01:54 +0200Duste3(~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816)
2024-10-07 15:03:19 +0200morb(~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 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 276 seconds)
2024-10-07 15:06:33 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 15:06:57 +0200CiaoSen(~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds)
2024-10-07 15:07:29 +0200weary-traveler(~user@user/user363627) user363627
2024-10-07 15:08:30 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds)
2024-10-07 15:09:11 +0200Typedfern(~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net)
2024-10-07 15:13:03 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 276 seconds)
2024-10-07 15:14:49 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 15:16:36 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 15:16:42 +0200ash3en(~Thunderbi@89.246.174.164) ash3en
2024-10-07 15:18:21 +0200merijn(~merijn@77.242.116.146) merijn
2024-10-07 15:20:19 +0200picnoir(~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 +0200picnoir(~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 +0200JuanDaugherty(~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 +0200ash3en(~Thunderbi@89.246.174.164) (Quit: ash3en)
2024-10-07 15:29:37 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-07 15:29:59 +0200ash3en(~Thunderbi@89.246.174.164) ash3en
2024-10-07 15:37:34 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-07 15:39:52 +0200alexherbo2(~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection)
2024-10-07 15:40:11 +0200alexherbo2(~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) alexherbo2
2024-10-07 15:40:13 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 15:40:57 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2024-10-07 15:52:34 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 15:54:52 +0200mari-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 +0200ash3en(~Thunderbi@89.246.174.164) (Quit: ash3en)
2024-10-07 16:05:56 +0200mari-estel(~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) (Ping timeout: 265 seconds)
2024-10-07 16:07:33 +0200Leonard26(~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 +0200cfricke(~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 +0200synchromesh(~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 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-10-07 16:13:49 +0200gorignak(~gorignak@user/gorignak) gorignak
2024-10-07 16:14:13 +0200synchromesh(~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 +0200diod(~diod@142.188.102.4) ()
2024-10-07 16:21:16 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-10-07 16:21:22 +0200ljdarj1(~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 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
2024-10-07 16:25:07 +0200ljdarj1ljdarj
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.
2024-10-07 16:29:51 +0200 <haskellbridge> <Bowuigi> Perhaps a bit too conservative there
2024-10-07 16:31:02 +0200 <haskellbridge> <Bowuigi> The type family/type alias issue happens because they are supposed to be fully saturated (exceptions exist) as to avoid going to System F omega and further complicating GHC
2024-10-07 16:31:49 +0200ljdarj(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-07 16:32:08 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 16:34:30 +0200spew(~spew@201.141.99.170) spew
2024-10-07 16:37:05 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2024-10-07 16:41:00 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-07 16:41:57 +0200euphores(~SASL_euph@user/euphores) euphores
2024-10-07 16:44:23 +0200 <lortabac> fr33domlover: can I ask you what your goal is?
2024-10-07 16:46:34 +0200 <lortabac> maybe you can use the qualified type name as a Symbol with TemplateHaskell
2024-10-07 16:47:05 +0200 <lortabac> but depending on what you are trying to achieve you may not actually need this
2024-10-07 16:48:33 +0200Pixi`(~Pixi@user/pixi) Pixi
2024-10-07 16:50:06 +0200Pixi(~Pixi@user/pixi) (Ping timeout: 244 seconds)
2024-10-07 16:50:29 +0200mari-estel(~mari-este@185.238.219.77)
2024-10-07 16:57:59 +0200benjaminl(~benjaminl@user/benjaminl) (Ping timeout: 252 seconds)
2024-10-07 16:58:23 +0200benjaminl(~benjaminl@user/benjaminl) benjaminl
2024-10-07 16:59:47 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-10-07 17:00:06 +0200Duste3(~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816) (Remote host closed the connection)
2024-10-07 17:02:10 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-10-07 17:12:09 +0200mari-estel(~mari-este@185.238.219.77) ()
2024-10-07 17:12:49 +0200Pixi`Pixi
2024-10-07 17:12:49 +0200cfricke(~cfricke@user/cfricke) cfricke
2024-10-07 17:14:08 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2024-10-07 17:14:37 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-07 17:16:51 +0200alexherbo2(~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection)
2024-10-07 17:17:34 +0200alexherbo2(~alexherbo@2a02-8440-3313-f515-a060-99c7-e89f-be85.rev.sfr.net) alexherbo2
2024-10-07 17:19:28 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Client Quit)
2024-10-07 17:21:23 +0200alexherbo2(~alexherbo@2a02-8440-3313-f515-a060-99c7-e89f-be85.rev.sfr.net) (Remote host closed the connection)
2024-10-07 17:24:12 +0200alp_(~alp@2001:861:e3d6:8f80:e06c:ffe4:c8a0:d22b)
2024-10-07 17:34:52 +0200__monty_1(~toonn@user/toonn) toonn
2024-10-07 17:35:02 +0200__monty__(~toonn@user/toonn) (Ping timeout: 252 seconds)
2024-10-07 17:35:05 +0200__monty_1__monty__
2024-10-07 17:36:11 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2024-10-07 17:43:33 +0200fmira(~user@user/fmira) (Remote host closed the connection)
2024-10-07 17:43:56 +0200fmira(~user@user/fmira) fmira
2024-10-07 17:52:27 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-07 17:56:42 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine)
2024-10-07 17:57:59 +0200rosco(~rosco@175.136.22.30) (Quit: Lost terminal)
2024-10-07 17:58:08 +0200m1dnight(~christoph@d8D861908.access.telenet.be) (Ping timeout: 252 seconds)
2024-10-07 17:58:53 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-07 18:00:05 +0200EvanR(~EvanR@user/evanr) (Quit: Leaving)
2024-10-07 18:04:42 +0200briandaed(~root@185.234.210.211.r.toneticgroup.pl)
2024-10-07 18:06:20 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-10-07 18:10:47 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 255 seconds)
2024-10-07 18:10:57 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2024-10-07 18:12:01 +0200LukeHoersten(~LukeHoers@user/lukehoersten) LukeHoersten
2024-10-07 18:23:13 +0200fmira(~user@user/fmira) (Remote host closed the connection)
2024-10-07 18:23:36 +0200fmira(~user@user/fmira) fmira
2024-10-07 18:27:03 +0200ljdarj(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-07 18:27:22 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 18:29:56 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 18:32:28 +0200m1dnight(~christoph@d8D861908.access.telenet.be) m1dnight
2024-10-07 18:35:14 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2024-10-07 18:36:36 +0200ft(~ft@p4fc2a216.dip0.t-ipconnect.de) ft
2024-10-07 18:39:00 +0200jespada_(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) jespada
2024-10-07 18:39:29 +0200jespada(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Read error: Connection reset by peer)
2024-10-07 18:45:13 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2024-10-07 18:45:20 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 18:47:42 +0200jespada_(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com)
2024-10-07 18:48:12 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 276 seconds)
2024-10-07 18:49:42 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds)
2024-10-07 18:50:12 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 18:53:15 +0200jespada(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) jespada
2024-10-07 18:53:26 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-10-07 18:59:54 +0200ljdarj(~Thunderbi@user/ljdarj) (Quit: ljdarj)
2024-10-07 19:00:13 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 19:00:43 +0200pavonia(~user@user/siracusa) siracusa
2024-10-07 19:00:53 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 19:00:59 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 19:05:48 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-10-07 19:08:10 +0200sawilagar(~sawilagar@user/sawilagar) (Remote host closed the connection)
2024-10-07 19:09:59 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds)
2024-10-07 19:11:56 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 19:14:55 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2024-10-07 19:15:19 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-07 19:17:27 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-10-07 19:18:58 +0200petrichor(~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
2024-10-07 19:19:24 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-07 19:25:07 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod
2024-10-07 19:25:54 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-10-07 19:27:31 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 19:32:19 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-10-07 19:34:26 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2024-10-07 19:35:14 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
2024-10-07 19:35:40 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de)
2024-10-07 19:42:56 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 19:47:24 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-10-07 19:48:37 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 248 seconds)
2024-10-07 19:48:48 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-10-07 19:49:38 +0200ash3en(~Thunderbi@146.70.124.222) ash3en
2024-10-07 19:53:25 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 19:53:44 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-10-07 19:54:00 +0200ash3en(~Thunderbi@146.70.124.222) (Ping timeout: 252 seconds)
2024-10-07 19:54:06 +0200ash3en1(~Thunderbi@2a02:8108:2810:ab00::1f3e) ash3en
2024-10-07 19:56:23 +0200ash3en1ash3en
2024-10-07 20:08:34 +0200petrichor(~znc-user@user/petrichor) petrichor
2024-10-07 20:09:23 +0200ash3en(~Thunderbi@2a02:8108:2810:ab00::1f3e) (Ping timeout: 252 seconds)
2024-10-07 20:09:44 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh
2024-10-07 20:10:57 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2024-10-07 20:15:04 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!)
2024-10-07 20:24:57 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2024-10-07 20:25:15 +0200dlock23(~dlock23@78.red-81-40-75.staticip.rima-tde.net) (Quit: Leaving)
2024-10-07 20:27:44 +0200cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-10-07 20:28:45 +0200kuribas(~user@ptr-17d51em3rhcvuvotah6.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
2024-10-07 20:35:37 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2024-10-07 20:36:19 +0200mari-estel(~mari-este@2a02:3032:311:fd82:216:3eff:fe65:4eef)
2024-10-07 20:40:08 +0200hgolden_(~hgolden@146.70.173.37) hgolden
2024-10-07 20:40:38 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-10-07 20:40:56 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 252 seconds)
2024-10-07 20:41:07 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-07 20:41:25 +0200euleritian(~euleritia@ip5f5ad3f6.dynamic.kabel-deutschland.de)
2024-10-07 20:42:53 +0200hgolden__(~hgolden@169.150.203.23) (Ping timeout: 265 seconds)
2024-10-07 20:43:11 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2024-10-07 20:49:50 +0200mari-estel(~mari-este@2a02:3032:311:fd82:216:3eff:fe65:4eef) (Ping timeout: 244 seconds)
2024-10-07 20:51:52 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2024-10-07 21:00:02 +0200caconym(~caconym@user/caconym) (Quit: bye)
2024-10-07 21:00:38 +0200caconym(~caconym@user/caconym) caconym
2024-10-07 21:01:52 +0200briandaed(~root@185.234.210.211.r.toneticgroup.pl) (Remote host closed the connection)
2024-10-07 21:02:04 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-07 21:05:23 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-10-07 21:05:30 +0200bearen(~bearen@user/bearen) bearen
2024-10-07 21:07:52 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 21:08:26 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit)
2024-10-07 21:08:38 +0200bearen(~bearen@user/bearen) (Client Quit)
2024-10-07 21:08:44 +0200simendsjo(~user@84.211.91.108) simendsjo
2024-10-07 21:09:35 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 21:14:12 +0200mari-estel(~mari-este@185.238.219.66)
2024-10-07 21:16:43 +0200ljdarj(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-07 21:17:02 +0200target_i(~target_i@user/target-i/x-6023099) target_i
2024-10-07 21:20:38 +0200youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-10-07 21:22:08 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 21:22:46 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-07 21:24:12 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds)
2024-10-07 21:25:28 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 21:37:00 +0200youthlic(~Thunderbi@user/youthlic) (Remote host closed the connection)
2024-10-07 21:39:46 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-10-07 21:40:33 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod
2024-10-07 21:41:54 +0200youthlic(~Thunderbi@user/youthlic) (Client Quit)
2024-10-07 21:42:01 +0200ljdarj(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-07 21:42:20 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 21:42:43 +0200mantraofpie(~mantraofp@user/mantraofpie) mantraofpie
2024-10-07 21:48:02 +0200mari-estel(~mari-este@185.238.219.66) (Ping timeout: 252 seconds)
2024-10-07 21:48:23 +0200EvanR(~EvanR@user/evanr) EvanR
2024-10-07 21:53:18 +0200weary-traveler(~user@user/user363627) user363627
2024-10-07 21:56:53 +0200floyza(~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown
2024-10-07 21:58:39 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds)
2024-10-07 21:58:58 +0200 <yin> is there any logical reason why we can't use bound variables (with `<-` in do blocks) inside where clauses?
2024-10-07 21:59:26 +0200 <yin> s/can't/wouldn't be able to
2024-10-07 21:59:29 +0200 <ncf> huh?
2024-10-07 22:00:48 +0200 <int-e> yin: yes, they're not in scope outside of the do block (they're only in scope for any subsequent statements inside the do block)
2024-10-07 22:00:49 +0200 <monochrom> It is because do-block is an expression but "where" is for definitions and pattern matching, so do-block is neither.
2024-10-07 22:01:14 +0200 <c_wraith> well, it introduces the obvious question of *when* they would be bound. Usually names defined in a where block are evaluated on demand. That would be ugly for <- bindings
2024-10-07 22:01:15 +0200 <int-e> @undo do x <- a; b
2024-10-07 22:01:15 +0200 <lambdabot> a >>= \ x -> b
2024-10-07 22:02:16 +0200 <int-e> (after desugaring, the x is not in scope outside of that lambda)
2024-10-07 22:02:25 +0200 <monochrom> "f x = y+1 where y = x" the "where" belongs to "f x =", not to "y+1". "case xs of x:xt -> y+1 where y = x" the "where" belongs to "x:xt ->", not to "y+1".
2024-10-07 22:04:01 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 22:04:39 +0200 <monochrom> To be sure, Landin would have (actually did) "where" belonging to an expression, so meh, it's a personal taste, you can design a language to look whatever you like.
2024-10-07 22:04:40 +0200 <EvanR> maybe you want to use a recursive do
2024-10-07 22:04:51 +0200 <EvanR> </clippy>
2024-10-07 22:04:56 +0200 <monochrom> haha
2024-10-07 22:05:41 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 255 seconds)
2024-10-07 22:05:58 +0200 <yin> i understand the current constraints. i guess what i'm asking is if there would be something stopping us from doing it if we wanted to? c_wraith asks a good question, but i think we could get around that if we just considered sugar for implicitly passing the bound variable as an argument
2024-10-07 22:06:18 +0200ljdarj1ljdarj
2024-10-07 22:06:30 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 22:06:45 +0200 <EvanR> where clause isn't an expression by itself, is another
2024-10-07 22:06:50 +0200 <EvanR> thing
2024-10-07 22:07:04 +0200 <EvanR> it attaches to definitions and case alternatives
2024-10-07 22:07:19 +0200 <monochrom> I think you could do it in your language.
2024-10-07 22:07:43 +0200 <c_wraith> if you're going to just specify the behavior as "perform all these bindings, make these names in scope", how is it any different from just putting them in the do block?
2024-10-07 22:07:48 +0200 <monochrom> Haskell's "let x=e in b" certainly becomes Landin's "b where x=e".
2024-10-07 22:08:39 +0200 <monochrom> I don't even think you can design your language to accept "let x = 0:y in x where y = 1:x" haha
2024-10-07 22:08:52 +0200 <monochrom> err, I don't even think you can't!
2024-10-07 22:09:21 +0200 <yin> i don't know who Landin is
2024-10-07 22:09:34 +0200 <monochrom> Look for the paper "the next 700 languages"
2024-10-07 22:09:56 +0200euleritian(~euleritia@ip5f5ad3f6.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds)
2024-10-07 22:10:28 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de)
2024-10-07 22:11:22 +0200 <yin> ty
2024-10-07 22:12:51 +0200 <yin> c_wraith: just syntactical convenience
2024-10-07 22:17:56 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2024-10-07 22:18:18 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-10-07 22:20:49 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Remote host closed the connection)
2024-10-07 22:21:04 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de)
2024-10-07 22:21:08 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-10-07 22:21:32 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de)
2024-10-07 22:23:08 +0200 <EvanR> I'm finding where clause to be awkward sometimes. Unless it's a wild mess of definitions that must be necessarily out of order, or there's no logical order of presentation, I've been liking block of let bindings ending with an in
2024-10-07 22:23:28 +0200 <EvanR> where the definitions are in order
2024-10-07 22:23:48 +0200 <EvanR> like a damn math book, they define stuff seemingly out of blue before getting to the point
2024-10-07 22:27:51 +0200 <dolio> I think having `where` reference things in other scopes based on the occurrence of the bound names sounds pretty confusing and difficult to figure out.
2024-10-07 22:29:43 +0200 <dolio> Also, making where an expression like Landin has its disadvantages w/r/t how Haskell's syntax currently works.
2024-10-07 22:29:47 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 22:29:57 +0200 <monochrom> The dilemma between "defining stuff out of the blue before getting to the point" and "the point using terms out of the blue before being defined" >:)
2024-10-07 22:30:15 +0200bliminse(~bliminse@user/bliminse) (Quit: leaving)
2024-10-07 22:30:22 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-10-07 22:30:40 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-10-07 22:30:45 +0200CiaoSen(~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) CiaoSen
2024-10-07 22:30:49 +0200 <monochrom> This is why "let x = 0:y in x where y = 1:x" is the best of both worlds. >:)
2024-10-07 22:30:54 +0200 <dolio> E.G. definitions in a `where` are in scope in guards, I think, which would not be possible if the `where` were part of the expression after the guards.
2024-10-07 22:31:36 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-07 22:31:37 +0200 <monochrom> Yes that one is right.
2024-10-07 22:32:58 +0200 <monochrom> "case x:xt | x > 0 -> y | otherwise -> - y where y = x*x" y is available to both branches.
2024-10-07 22:33:34 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds)
2024-10-07 22:33:47 +0200 <monochrom> in fact, also available to the guard conditions. "case x:xt | z > 0 -> ... where z=x+2" is OK.
2024-10-07 22:33:51 +0200 <dolio> Agda has an analogous annoyance. Sometimes I'd like to define something in a `where` that I use in a `with`. But I can't do that, because the `with` introduces clauses that each have their own `where`, not vice versa.
2024-10-07 22:34:39 +0200LukeHoersten(~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2024-10-07 22:35:22 +0200 <ncf> they've added "using" or whatever recently
2024-10-07 22:35:29 +0200ljdarj1(~Thunderbi@user/ljdarj) (Remote host closed the connection)
2024-10-07 22:35:42 +0200 <monochrom> Yikes haha that sounds like syntax inflation.
2024-10-07 22:35:48 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-10-07 22:35:57 +0200 <ncf> https://agda.readthedocs.io/en/latest/language/with-abstraction.html#left-hand-side-let-bindings
2024-10-07 22:35:57 +0200 <dolio> Is that too new for readthedocs?
2024-10-07 22:36:29 +0200 <dolio> Oh, nice.
2024-10-07 22:36:39 +0200euphores(~SASL_euph@user/euphores) euphores
2024-10-07 22:50:53 +0200michalz(~michalz@185.246.207.217) (Remote host closed the connection)
2024-10-07 23:04:04 +0200CiaoSen(~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds)
2024-10-07 23:08:20 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
2024-10-07 23:12:44 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds)
2024-10-07 23:29:28 +0200sourcetarius(~sourcetar@user/sourcetarius) sourcetarius
2024-10-07 23:32:19 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2024-10-07 23:33:00 +0200 <yin> i don't think tgis would be a good thing for Haskell to have. i was just curious of the implications
2024-10-07 23:34:30 +0200bliminse(~bliminse@user/bliminse) bliminse
2024-10-07 23:37:35 +0200supercode(~supercode@user/supercode) supercode
2024-10-07 23:40:12 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2024-10-07 23:40:26 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-10-07 23:51:57 +0200takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-10-07 23:54:25 +0200chele(~chele@user/chele) (Remote host closed the connection)
2024-10-07 23:58:41 +0200Guest82(~Guest82@152.44.49.129)
2024-10-07 23:59:41 +0200Guest82(~Guest82@152.44.49.129) (Client Quit)
2024-10-07 23:59:54 +0200euleritian(~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer)