Logs on 2024-10-07 (liberachat/#haskell)
| 00:03:03 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:07:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 00:14:50 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 00:18:00 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 272 seconds) |
| 00:18:33 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:21:41 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 00:22:42 | → | fmira joins (~user@user/fmira) |
| 00:22:57 | × | fmira quits (~user@user/fmira) (Remote host closed the connection) |
| 00:23:03 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:23:22 | → | fmira joins (~user@user/fmira) |
| 00:30:44 | × | Inst quits (~Inst@user/Inst) (Ping timeout: 255 seconds) |
| 00:31:43 | → | Inst joins (~Inst@user/Inst) |
| 00:32:40 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 00:33:58 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:36:21 | × | Inst quits (~Inst@user/Inst) (Ping timeout: 246 seconds) |
| 00:38:32 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:46:44 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 00:47:04 | × | xff0x quits (~xff0x@2405:6580:b080:900:16eb:2432:285b:7ea6) (Ping timeout: 260 seconds) |
| 00:49:24 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:53:32 | EvanR_ | is now known as EvanR |
| 00:53:56 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:58:09 | <yin> | what am i looking at here? https://hackage.haskell.org/package/ghc-prim-0.11.0/docs/src/GHC.Prim.html#readTVar%23 |
| 00:58:50 | <yin> | what does it mean for a function# to be defined as itself? |
| 00:59:24 | <yin> | is it just "magic" and we need the definition for the type signature? |
| 00:59:33 | × | ethantwardy quits (user@user/ethantwardy) (Ping timeout: 248 seconds) |
| 01:00:46 | <geekosaur> | everything in ghc-prim is "defined as itself", yes. it's just for documentation |
| 01:00:58 | <geekosaur> | the actual definitions are baked into the compiler or backend |
| 01:01:09 | <geekosaur> | necessarily |
| 01:01:10 | <yin> | ok great, thanks |
| 01:02:10 | <yin> | i wish all code was haskell all the way down to binary |
| 01:02:11 | × | fmira quits (~user@user/fmira) (Ping timeout: 260 seconds) |
| 01:03:16 | <yin> | hits the magic way too soon |
| 01:04:49 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:04:57 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 01:06:37 | <geekosaur> | how exactly do you write the platform's add instruction in haskell code? |
| 01:06:45 | → | spew joins (~spew@201.141.99.170) |
| 01:07:02 | <geekosaur> | (the answer is: `+#` and the backend emits the actual instruction) |
| 01:07:13 | <geekosaur> | the ones that aren;t that are mostly cmm code |
| 01:09:20 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:15:56 | → | ethantwardy joins (user@user/ethantwardy) |
| 01:20:21 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:23:24 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 01:25:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:33:54 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:36:19 | <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 |
| 01:36:50 | <EvanR> | it's harder for the compiler to know another sequence of asm computes the same high level values |
| 01:37:41 | <EvanR> | and if it can, and will rewrite it all, what was the point |
| 01:37:45 | <EvanR> | of writing a bunch of asm |
| 01:38:18 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:39:01 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 01:41:58 | <monochrom> | As Dennis Ritchie pointed out half a century ago, library source code means nothing if the compiler contains code to overrule it. |
| 01:43:14 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 01:44:55 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 01:45:47 | <monochrom> | Not to mention that in the 1980s commercial compilers recognized popular benchmarking code and cheated. |
| 01:46:56 | <monochrom> | (Probably part of why the benchmarks had to change every year.) |
| 01:47:53 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 265 seconds) |
| 01:49:19 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:52:18 | × | ethantwardy quits (user@user/ethantwardy) (Ping timeout: 246 seconds) |
| 01:53:31 | → | ethantwardy joins (user@user/ethantwardy) |
| 01:53:47 | × | qhong quits (~qhong@DN200outg.stanford.edu) (Remote host closed the connection) |
| 01:54:10 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 02:03:25 | → | Inst joins (~Inst@user/Inst) |
| 02:04:36 | × | identity quits (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60)) |
| 02:04:45 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:09:12 | × | Inst quits (~Inst@user/Inst) (Ping timeout: 252 seconds) |
| 02:09:54 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:13:52 | × | td_ quits (~td@i5387093A.versanet.de) (Ping timeout: 252 seconds) |
| 02:15:52 | → | td_ joins (~td@i5387091A.versanet.de) |
| 02:15:54 | × | ethantwardy quits (user@user/ethantwardy) (Ping timeout: 260 seconds) |
| 02:16:24 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 02:18:22 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 02:18:38 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 02:20:29 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:23:08 | <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 |
| 02:25:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 02:29:14 | → | weary-traveler joins (~user@user/user363627) |
| 02:32:47 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Read error: Connection timed out) |
| 02:35:09 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 02:36:17 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:41:05 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 02:52:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:52:07 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:56:46 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:00:46 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 03:04:19 | × | spew quits (~spew@201.141.99.170) (Quit: spew) |
| 03:07:19 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 03:07:35 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:07:55 | × | ZLima12 quits (~zlima12@user/meow/ZLima12) () |
| 03:08:39 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:08:45 | → | ZLima12 joins (~zlima12@user/meow/ZLima12) |
| 03:12:10 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:19:23 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 03:22:41 | → | fmira joins (~user@user/fmira) |
| 03:23:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:27:51 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 03:38:29 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:43:20 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:46:16 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 03:46:46 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 03:51:24 | → | synchromesh joins (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) |
| 03:54:03 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:56:25 | <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? |
| 03:59:32 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 03:59:37 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 04:08:40 | <haskellbridge> | <Bowuigi> According to https://ncatlab.org/nlab/show/W-type every W type should be traversable in a finite number of steps |
| 04:10:29 | <haskellbridge> | <Bowuigi> I mean, they represent well orders constructively |
| 04:10:33 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:12:13 | <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) |
| 04:12:34 | → | user4561 joins (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 04:12:54 | <haskellbridge> | <Bowuigi> Inducting in the direction of the least element of course, like induction on the natural numbers |
| 04:15:21 | <haskellbridge> | <Bowuigi> M types are the coinductive (thus possibly infinite) ones |
| 04:15:30 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 04:20:56 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: hm issue is well-ordered trees can have infinite branches |
| 04:21:13 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 04:21:46 | <haskellbridge> | <Bowuigi> Oh yeah forgot about that |
| 04:22:06 | <haskellbridge> | <thirdofmay18081814goya> so it works for induction but i'm trying to get at computable traversal |
| 04:22:19 | × | user4561 quits (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Quit: Client closed) |
| 04:23:04 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 04:23:59 | <haskellbridge> | <thirdofmay18081814goya> uh i meant wellfounded |
| 04:24:13 | <haskellbridge> | <thirdofmay18081814goya> i'm not 100% how this translates to wellfoundedness |
| 04:25:43 | <haskellbridge> | <thirdofmay18081814goya> yeah wellordered trees are less structured than wellfounded trees, only the latter must have finite chains |
| 04:25:48 | <haskellbridge> | <Bowuigi> Not sure why can the trees be infinitely wide if the relation is a total order with a minimum element |
| 04:26:09 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:26:33 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: totally ordered tree is just N |
| 04:27:51 | → | michalz joins (~michalz@185.246.207.217) |
| 04:28:28 | <haskellbridge> | <Bowuigi> https://ncatlab.org/nlab/show/well-order assumes classical reasoning a lot lmao |
| 04:30:38 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 04:31:43 | <haskellbridge> | <Bowuigi> So W-types are supposed to be a constructive counterpart to sets with a well founded irreflexive total order |
| 04:32:55 | <haskellbridge> | <thirdofmay18081814goya> hm i think we do not want well-order |
| 04:33:08 | <haskellbridge> | <thirdofmay18081814goya> because that make the tree = N |
| 04:33:16 | <haskellbridge> | <thirdofmay18081814goya> or a subset |
| 04:33:26 | <haskellbridge> | <thirdofmay18081814goya> we want wellfoundedness |
| 04:34:29 | → | user4561 joins (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 04:35:01 | user4561 | is now known as myNameIs |
| 04:35:23 | <haskellbridge> | <Bowuigi> The "constructiveness" is what seems to make the trees possibly infinitely wide |
| 04:35:44 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: even in classical logic i think we get that wellfounded trees can be infinitely wide |
| 04:36:29 | × | alp_ quits (~alp@2001:861:e3d6:8f80:f5b0:cd1b:e895:cf8a) (Ping timeout: 252 seconds) |
| 04:36:50 | <haskellbridge> | <Bowuigi> I do not understand this topic enough yet lol, lemme learn how this works first |
| 04:37:03 | <haskellbridge> | <Bowuigi> Btw this question is probably suitable for the HoTT Zulip |
| 04:37:04 | <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 |
| 04:37:48 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: ah good point, ty |
| 04:37:59 | <haskellbridge> | <thirdofmay18081814goya> i haven't gone on there yet did not know it existed |
| 04:40:39 | <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 |
| 04:40:54 | <haskellbridge> | <Bowuigi> Oh wait the HoTT book may say something about W types lemme check |
| 04:41:40 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:42:44 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 04:44:56 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 04:45:39 | × | myNameIs quits (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Changing host) |
| 04:45:39 | → | myNameIs joins (~user4561@user/myNameIs) |
| 04:46:32 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 04:53:21 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 04:54:50 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 04:57:09 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:57:25 | × | myNameIs quits (~user4561@user/myNameIs) (Ping timeout: 256 seconds) |
| 04:57:31 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 04:59:00 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:01:47 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:03:33 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 05:03:35 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 05:05:03 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:05:15 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 05:07:51 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 05:09:19 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:12:34 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:15:34 | <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 |
| 05:17:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:17:21 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:17:55 | <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" |
| 05:18:02 | → | alp_ joins (~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) |
| 05:19:50 | <haskellbridge> | <thirdofmay18081814goya> am reading |
| 05:20:25 | <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 |
| 05:23:47 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 05:25:53 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:28:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:30:06 | → | andrewboltachev joins (~andrey@178.141.123.3) |
| 05:30:11 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:32:47 | <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 |
| 05:32:49 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 05:32:58 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:34:07 | <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 |
| 05:34:28 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:34:30 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 05:36:43 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 05:37:19 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:37:26 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 05:39:12 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:39:16 | <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) |
| 05:40:18 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 05:41:53 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:46:19 | × | ZLima12 quits (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 05:46:26 | → | ZLima12_ joins (~zlima12@user/meow/ZLima12) |
| 05:49:41 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 05:51:17 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:51:41 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 05:53:13 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:53:19 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 06:05:35 | → | euphores joins (~SASL_euph@user/euphores) |
| 06:05:43 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 06:05:48 | × | cptaffe quits (~cptaffe@user/cptaffe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:13:55 | × | xacktm quits (xacktm@user/xacktm) (Ping timeout: 264 seconds) |
| 06:16:49 | → | cptaffe joins (~cptaffe@user/cptaffe) |
| 06:18:35 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 06:20:10 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 06:21:10 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 06:22:42 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 06:24:21 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 06:26:28 | → | xff0x joins (~xff0x@182.169.73.28) |
| 06:28:26 | × | Fischmiep quits (~Fischmiep@user/Fischmiep) (Remote host closed the connection) |
| 06:29:05 | → | Fischmiep joins (~Fischmiep@user/Fischmiep) |
| 06:34:35 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 06:34:59 | × | xff0x quits (~xff0x@182.169.73.28) (Ping timeout: 265 seconds) |
| 06:36:06 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 06:36:40 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 06:37:00 | → | xacktm joins (xacktm@user/xacktm) |
| 06:37:03 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:37:49 | → | merijn joins (~merijn@77.242.116.146) |
| 06:41:24 | × | Digit quits (~user@user/digit) (Ping timeout: 246 seconds) |
| 06:41:26 | → | Digitteknohippie joins (~user@user/digit) |
| 06:43:42 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 06:48:34 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 06:49:38 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:50:08 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 06:52:53 | → | merijn joins (~merijn@77.242.116.146) |
| 06:54:26 | → | rosco joins (~rosco@175.136.23.101) |
| 06:55:55 | → | madhavanmiui joins (~madhavanm@2409:40f4:101b:c402:7962:1b32:f43c:cd72) |
| 06:56:50 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Ping timeout: 244 seconds) |
| 06:57:19 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:57:54 | × | madhavanmiui quits (~madhavanm@2409:40f4:101b:c402:7962:1b32:f43c:cd72) (Client Quit) |
| 06:59:15 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 07:00:03 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:08 | × | rosco quits (~rosco@175.136.23.101) (Read error: Connection reset by peer) |
| 07:00:41 | → | caconym joins (~caconym@user/caconym) |
| 07:00:58 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 07:01:56 | × | ft quits (~ft@p4fc2a216.dip0.t-ipconnect.de) (Quit: leaving) |
| 07:04:03 | → | merijn joins (~merijn@77.242.116.146) |
| 07:05:23 | → | rosco joins (~rosco@175.136.23.101) |
| 07:09:30 | → | kuribas joins (~user@ptr-17d51em3rhcvuvotah6.18120a2.ip6.access.telenet.be) |
| 07:09:53 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 07:15:22 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:16:00 | Digitteknohippie | is now known as Digit |
| 07:16:26 | → | gawen joins (~gawen@user/gawen) |
| 07:17:50 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 07:21:46 | → | merijn joins (~merijn@77.242.116.146) |
| 07:22:58 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 07:23:00 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 07:24:54 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 07:25:24 | → | acidjnk joins (~acidjnk@p200300d6e72cfb09b827840f1f57a57d.dip0.t-ipconnect.de) |
| 07:36:47 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 07:40:51 | × | ash3en quits (~Thunderbi@89.246.174.164) (Client Quit) |
| 07:41:09 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 07:42:41 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 07:46:58 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 07:52:48 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Ping timeout: 265 seconds) |
| 07:53:23 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 07:54:46 | → | __monty__ joins (~toonn@user/toonn) |
| 08:00:54 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 08:03:06 | → | famubu joins (~julinuser@14.139.174.50) |
| 08:03:06 | × | famubu quits (~julinuser@14.139.174.50) (Changing host) |
| 08:03:06 | → | famubu joins (~julinuser@user/famubu) |
| 08:04:17 | <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. |
| 08:04:20 | <famubu> | https://hackage.haskell.org/package/hedgehog-1.5/docs/Hedgehog-Gen.html#v:sample |
| 08:05:50 | <jle`> | famubu: i wonder if you can use the Set generator |
| 08:06:16 | <jle`> | it doesn't do anything smart afaict |
| 08:07:20 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 08:08:36 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 08:09:26 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 08:12:39 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 08:19:05 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:26:09 | × | rosco quits (~rosco@175.136.23.101) (Read error: Connection reset by peer) |
| 08:35:23 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 08:35:59 | → | rvalue joins (~rvalue@user/rvalue) |
| 08:46:12 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 08:51:53 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 08:52:47 | <kuribas> | Anyone coming to munihac? |
| 08:53:33 | → | chele joins (~chele@user/chele) |
| 08:55:20 | <lortabac> | I'm coming with a couple of colleagues |
| 08:57:55 | → | merijn joins (~merijn@77.242.116.146) |
| 09:02:04 | ZLima12_ | is now known as ZLima12 |
| 09:08:04 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 09:09:50 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
| 09:09:56 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 09:10:03 | × | onliner10 quits (~onliner10@user/onliner10) (Remote host closed the connection) |
| 09:10:03 | → | CiaoSen joins (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) |
| 09:10:20 | Lord_of_Life_ | is now known as Lord_of_Life |
| 09:13:23 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 09:14:56 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 09:16:33 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 09:24:12 | <kuribas> | lortabac: You have a project? |
| 09:24:27 | <lortabac> | yes |
| 09:24:44 | <lortabac> | more like a GHC proposal |
| 09:26:39 | [exa] | curious |
| 09:27:33 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 09:28:02 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 09:29:07 | <lortabac> | I've written a library to "fix" implicit parameters via a hack + a GHC plugin |
| 09:30:05 | <lortabac> | but it's a proof of concept, a proper implementation would require modifying GHC |
| 09:31:00 | <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" |
| 09:31:08 | <lortabac> | *not doing anything |
| 09:33:18 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:34:42 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 09:40:15 | → | merijn joins (~merijn@77.242.116.146) |
| 09:40:40 | × | caubert_ quits (~caubert@user/caubert) (Quit: WeeChat 4.3.3) |
| 09:40:55 | → | caubert joins (~caubert@user/caubert) |
| 09:40:59 | × | hsw__ quits (~hsw@112-104-11-250.adsl.dynamic.seed.net.tw) (Quit: Leaving) |
| 09:41:14 | → | hsw joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 09:45:25 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 09:46:23 | <famubu> | jle`: Thanks. Let me try that. |
| 09:47:11 | → | merijn joins (~merijn@77.242.116.146) |
| 09:53:18 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 10:00:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:00:17 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 10:04:45 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 10:05:13 | → | merijn joins (~merijn@77.242.116.146) |
| 10:06:16 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 10:09:57 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 10:10:10 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 10:10:28 | → | arahael joins (~arahael@user/arahael) |
| 10:10:29 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds) |
| 10:21:34 | × | CiaoSen quits (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 10:22:20 | → | merijn joins (~merijn@77.242.116.146) |
| 10:39:52 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:41:39 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 10:49:16 | → | identity joins (~identity@user/ZharMeny) |
| 10:52:39 | → | Digitteknohippie joins (~user@user/digit) |
| 10:53:14 | × | Digit quits (~user@user/digit) (Ping timeout: 272 seconds) |
| 10:53:48 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds) |
| 10:59:06 | Digitteknohippie | is now known as Digit |
| 11:01:43 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 11:02:05 | → | comerijn joins (~merijn@77.242.116.146) |
| 11:03:34 | → | rosco joins (~rosco@175.136.22.30) |
| 11:04:36 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 11:11:14 | → | xff0x joins (~xff0x@2405:6580:b080:900:31d8:fed5:6c70:b7b9) |
| 11:17:33 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 11:20:11 | × | identity quits (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60)) |
| 11:21:16 | → | identity joins (~identity@user/ZharMeny) |
| 11:21:42 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 11:23:04 | tdammers_ | is now known as tdammers |
| 11:24:34 | → | merijn joins (~merijn@77.242.116.146) |
| 11:24:54 | × | alp_ quits (~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) (Ping timeout: 246 seconds) |
| 11:25:53 | → | Digitteknohippie joins (~user@user/digit) |
| 11:26:13 | × | Digit quits (~user@user/digit) (Ping timeout: 248 seconds) |
| 11:26:32 | → | cfricke joins (~cfricke@user/cfricke) |
| 11:31:45 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 11:32:12 | Digitteknohippie | is now known as Digit |
| 11:33:44 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 11:38:34 | → | cfricke joins (~cfricke@user/cfricke) |
| 11:43:21 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 276 seconds) |
| 11:48:21 | <hc> | Hi all, I'm curious, I'm sure in this channel are some people who are developing commercial projects with haskell |
| 11:48:49 | × | hiecaq quits (~hiecaq@user/hiecaq) (Read error: Connection reset by peer) |
| 11:48:52 | <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? |
| 11:53:12 | <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. |
| 11:54:32 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Quit: WeeChat 4.4.2) |
| 11:54:46 | <hc> | tdammers: When you say neither you mean you're not using a static analysis tool? Or you are using one? |
| 11:54:56 | <hc> | But not as an only measure? |
| 11:55:00 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 11:55:38 | <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. |
| 11:56:16 | <kuribas> | This. Haskell typesystem is great for making robust software, but it hasn't been designed with security in mind. |
| 11:56:17 | <hc> | Okay, I think my question was misleading |
| 11:56:22 | <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. |
| 11:56:25 | <kuribas> | Neither is the ghc runtime I think. |
| 11:56:31 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Client Quit) |
| 11:56:42 | <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 |
| 11:56:47 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 11:57:33 | <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 |
| 11:57:39 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 11:58:01 | → | merijn joins (~merijn@77.242.116.146) |
| 11:58:07 | <hc> | okok, because yeah, like you said, is there even an analysis tool out there that supports haskell? Or rust for that matter? |
| 11:58:46 | <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 |
| 11:59:18 | <hc> | Could be, and there's ivory and tower for niche applications |
| 11:59:28 | <hc> | But that's not really "standard" haskell anymore %} |
| 11:59:39 | <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 |
| 12:00:11 | <hc> | Okay, yeah, I have a similar view on this and you're basically confirming it, thanks :-) |
| 12:00:16 | → | dlock23 joins (~dlock23@78.red-81-40-75.staticip.rima-tde.net) |
| 12:00:17 | <hc> | Always good to get a 2nd opinion |
| 12:00:29 | <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 |
| 12:01:00 | <hc> | Yeah, and there's a special "static text only" string type for SQL queries |
| 12:01:26 | <tdammers> | yeah, stuff like that. it's not perfect, but static code analysis tools aren't either |
| 12:02:02 | <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' |
| 12:02:44 | <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? |
| 12:02:50 | <hc> | s/step/measure/ |
| 12:05:18 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 12:06:48 | → | merijn joins (~merijn@77.242.116.146) |
| 12:07:19 | → | ystael joins (~ystael@user/ystael) |
| 12:08:34 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 12:11:49 | → | comerijn joins (~merijn@77.242.116.146) |
| 12:12:15 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 12:13:00 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 252 seconds) |
| 12:15:22 | → | Leonard26 joins (~Leonard26@49.236.8.9) |
| 12:17:16 | <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 |
| 12:19:13 | <__monty__> | Leonard26: Recursive functions sometimes have an accumulator argument. Which is usually used as the result when a stop condition is reached. |
| 12:19:43 | <__monty__> | The pattern is usually expressed as a fold, left/right/monoidal. |
| 12:19:53 | <__monty__> | So check out `foldr`. |
| 12:22:49 | → | alexherbo2 joins (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) |
| 12:23:29 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 12:23:29 | <Leonard26> | Thank you, I will check it out now |
| 12:24:14 | <Lears> | :t \n -> for_ [0..n] |
| 12:24:15 | <lambdabot> | (Applicative f, Num a, Enum a) => a -> (a -> f b) -> f () |
| 12:25:03 | <Leonard26> | (y) |
| 12:25:23 | → | diod joins (~diod@142.188.102.4) |
| 12:25:50 | × | malte quits (~malte@mal.tc) (Ping timeout: 252 seconds) |
| 12:26:09 | <diod> | in object oriented and others classes/libraries are organized in hierarchy, what happens in haskell? |
| 12:26:23 | <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. |
| 12:27:17 | <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. |
| 12:27:53 | <diod> | ah ok, interesting |
| 12:27:57 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 12:28:18 | <diod> | I was thinking functions are independent so hierarchy wouldn't be needed |
| 12:28:41 | <tdammers> | it's not technically needed, but it's still useful as a code organization strategy |
| 12:29:10 | <tdammers> | also, you can have dependencies between functions too |
| 12:29:32 | → | CiaoSen joins (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) |
| 12:29:52 | <diod> | ok, ty |
| 12:29:56 | → | malte joins (~malte@mal.tc) |
| 12:35:14 | <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 |
| 12:35:14 | <Leonard26> | and on until the last value when it stops. How could this be achieved? =L |
| 12:35:15 | <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] |
| 12:36:18 | <__monty__> | What's your expected output? |
| 12:37:53 | <hc> | tdammers: kk, thanks, that makes sense :-) |
| 12:39:46 | <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. |
| 12:41:10 | <Leonard26> | I have a function that gets called every 1s, that's why the variable must change each time |
| 12:42:29 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 12:44:13 | → | merijn joins (~merijn@77.242.116.146) |
| 12:46:52 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 12:46:53 | <kuribas> | > foldr (+) [a, b, c, d] e |
| 12:46:54 | <lambdabot> | error: |
| 12:46:54 | <lambdabot> | • Couldn't match expected type ‘t0 [Expr]’ with actual type ‘Expr’ |
| 12:46:54 | <lambdabot> | • In the third argument of ‘foldr’, namely ‘e’ |
| 12:47:07 | <kuribas> | > foldr (+) e [a, b, c, d] |
| 12:47:08 | <lambdabot> | a + (b + (c + (d + e))) |
| 12:47:16 | <kuribas> | > foldl (+) e [a, b, c, d] |
| 12:47:17 | <lambdabot> | e + a + b + c + d |
| 12:47:37 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 12:49:05 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 12:49:29 | × | sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 12:53:42 | → | dyniec joins (~dyniec@dybiec.info) |
| 12:56:49 | × | Typedfern quits (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) (Ping timeout: 265 seconds) |
| 13:00:23 | × | cfricke quits (~cfricke@user/cfricke) (Remote host closed the connection) |
| 13:00:34 | → | merijn joins (~merijn@77.242.116.146) |
| 13:00:40 | → | cfricke joins (~cfricke@user/cfricke) |
| 13:00:48 | × | cfricke quits (~cfricke@user/cfricke) (Remote host closed the connection) |
| 13:01:03 | → | cfricke joins (~cfricke@user/cfricke) |
| 13:01:54 | → | Duste3 joins (~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816) |
| 13:03:19 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 13:03:23 | <Duste3> | Are Kinds the same thing as Type 1 universe level in a theorem prover like Lean? |
| 13:05:54 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 13:06:33 | → | merijn joins (~merijn@77.242.116.146) |
| 13:06:57 | × | CiaoSen quits (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 13:07:29 | → | weary-traveler joins (~user@user/user363627) |
| 13:08:30 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 13:09:11 | → | Typedfern joins (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) |
| 13:13:03 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 13:14:49 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 13:16:36 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 13:16:42 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 13:18:21 | → | merijn joins (~merijn@77.242.116.146) |
| 13:20:19 | × | picnoir quits (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.4.2) |
| 13:20:26 | <tomsmeding> | Duste3: values have types, and types have kinds |
| 13:20:47 | <tomsmeding> | not sure about the precise numbering of the universe levels, but it indeed corresponds to one universe level higher than types |
| 13:21:54 | → | picnoir joins (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) |
| 13:22:05 | <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 *) |
| 13:22:30 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 13:22:52 | <tomsmeding> | (it's also inconsistent as a theorem prover for a bunch of other reasons) |
| 13:27:20 | <Duste3> | Ok thanks |
| 13:29:33 | × | ash3en quits (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 13:29:37 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 13:29:59 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 13:37:34 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 13:39:52 | × | alexherbo2 quits (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection) |
| 13:40:11 | → | alexherbo2 joins (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) |
| 13:40:13 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 13:40:57 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:52:34 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 13:54:52 | → | mari-estel joins (~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) |
| 13:55:22 | <EvanR> | Char :: Type |
| 13:55:29 | <EvanR> | but also |
| 13:55:31 | <EvanR> | Type :: Type |
| 13:55:43 | <EvanR> | there's no Type 1 |
| 13:57:45 | <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 |
| 13:57:54 | <EvanR> | so by definition they seem to be different |
| 14:00:52 | × | ash3en quits (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 14:05:56 | × | mari-estel quits (~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) (Ping timeout: 265 seconds) |
| 14:07:33 | × | Leonard26 quits (~Leonard26@49.236.8.9) (Quit: Client closed) |
| 14:10:38 | <Duste3> | Since Type :: Type then Haskell would be considered Impredicative? (and so its inconsistent as a theorem prover) |
| 14:11:31 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 264 seconds) |
| 14:12:03 | <dolio> | Type :: Type is more than impredicative. It's is outright inconsistent. |
| 14:12:25 | <dolio> | Like having a set of all sets. |
| 14:12:45 | <dolio> | (And not being New Foundations, I suppose.) |
| 14:12:46 | × | synchromesh quits (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) (Read error: Connection reset by peer) |
| 14:13:11 | <haskellbridge> | <Bowuigi> Haskell already was inconsistent because you have access to general recursion and to undefined (bottom) |
| 14:13:18 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 14:13:49 | → | gorignak joins (~gorignak@user/gorignak) |
| 14:14:13 | → | synchromesh joins (~john@2406:5a00:241a:5600:1537:bb1c:ebe9:2fdf) |
| 14:15:44 | <dolio> | GHC is impredicative in the type theory sense once you allow data types that have `forall` in the types of fields. |
| 14:15:48 | <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 |
| 14:16:18 | <dolio> | (Despite that not being the thing that ImpredicativeTypes enables.) |
| 14:17:30 | <EvanR> | what a mess |
| 14:19:14 | ← | diod parts (~diod@142.188.102.4) () |
| 14:21:16 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 14:21:22 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 14:22:23 | <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 |
| 14:23:05 | <dolio> | It's not really two different things. GHC just divides them up strangely. |
| 14:24:56 | <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. |
| 14:25:06 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 14:25:07 | ljdarj1 | is now known as ljdarj |
| 14:25:19 | <haskellbridge> | <Bowuigi> Impredicativity just means "something that contains itself" so that checks out I guess |
| 14:26:21 | <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. |
| 14:26:57 | <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 |
| 14:27:59 | <dolio> | Yeah. I don't think you can even manually instantiate without ImpredicativeTypes, though. |
| 14:29:51 | <haskellbridge> | <Bowuigi> Perhaps a bit too conservative there |
| 14:31:02 | <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 |
| 14:31:49 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 14:32:08 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 14:34:30 | → | spew joins (~spew@201.141.99.170) |
| 14:37:05 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 14:41:00 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 14:41:57 | → | euphores joins (~SASL_euph@user/euphores) |
| 14:44:23 | <lortabac> | fr33domlover: can I ask you what your goal is? |
| 14:46:34 | <lortabac> | maybe you can use the qualified type name as a Symbol with TemplateHaskell |
| 14:47:05 | <lortabac> | but depending on what you are trying to achieve you may not actually need this |
| 14:48:33 | → | Pixi` joins (~Pixi@user/pixi) |
| 14:50:06 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 244 seconds) |
| 14:50:29 | → | mari-estel joins (~mari-este@185.238.219.77) |
| 14:57:59 | × | benjaminl quits (~benjaminl@user/benjaminl) (Ping timeout: 252 seconds) |
| 14:58:23 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 14:59:47 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 15:00:06 | × | Duste3 quits (~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816) (Remote host closed the connection) |
| 15:02:10 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 15:12:09 | × | mari-estel quits (~mari-este@185.238.219.77) () |
| 15:12:49 | Pixi` | is now known as Pixi |
| 15:12:49 | → | cfricke joins (~cfricke@user/cfricke) |
| 15:14:08 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 15:14:37 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 15:16:51 | × | alexherbo2 quits (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection) |
| 15:17:34 | → | alexherbo2 joins (~alexherbo@2a02-8440-3313-f515-a060-99c7-e89f-be85.rev.sfr.net) |
| 15:19:28 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Client Quit) |
| 15:21:23 | × | alexherbo2 quits (~alexherbo@2a02-8440-3313-f515-a060-99c7-e89f-be85.rev.sfr.net) (Remote host closed the connection) |
| 15:24:12 | → | alp_ joins (~alp@2001:861:e3d6:8f80:e06c:ffe4:c8a0:d22b) |
| 15:34:52 | → | __monty_1 joins (~toonn@user/toonn) |
| 15:35:02 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 252 seconds) |
| 15:35:05 | __monty_1 | is now known as __monty__ |
| 15:36:11 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 15:43:33 | × | fmira quits (~user@user/fmira) (Remote host closed the connection) |
| 15:43:56 | → | fmira joins (~user@user/fmira) |
| 15:52:27 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 15:56:42 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 15:57:59 | × | rosco quits (~rosco@175.136.22.30) (Quit: Lost terminal) |
| 15:58:08 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 15:58:53 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 16:00:05 | × | EvanR quits (~EvanR@user/evanr) (Quit: Leaving) |
| 16:04:42 | → | briandaed joins (~root@185.234.210.211.r.toneticgroup.pl) |
| 16:06:20 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 16:10:47 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 255 seconds) |
| 16:10:57 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 16:12:01 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 16:23:13 | × | fmira quits (~user@user/fmira) (Remote host closed the connection) |
| 16:23:36 | → | fmira joins (~user@user/fmira) |
| 16:27:03 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 16:27:22 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 16:29:56 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 16:32:28 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 16:35:14 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 16:36:36 | → | ft joins (~ft@p4fc2a216.dip0.t-ipconnect.de) |
| 16:39:00 | → | jespada_ joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 16:39:29 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Read error: Connection reset by peer) |
| 16:45:13 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 16:45:20 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 16:47:42 | × | jespada_ quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 16:48:12 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 276 seconds) |
| 16:49:42 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds) |
| 16:50:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 16:53:15 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 16:53:26 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 16:59:54 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 17:00:13 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:00:43 | → | pavonia joins (~user@user/siracusa) |
| 17:00:53 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:00:59 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:05:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 17:08:10 | × | sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 17:09:59 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 17:11:56 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:14:55 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 17:15:19 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:17:27 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 17:18:58 | × | petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 17:19:24 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 17:25:07 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 17:25:54 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:27:31 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:32:19 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 17:34:26 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:35:14 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 17:35:40 | → | euleritian joins (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) |
| 17:42:56 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:47:24 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 17:48:37 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 17:48:48 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:49:38 | → | ash3en joins (~Thunderbi@146.70.124.222) |
| 17:53:25 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:53:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 17:54:00 | × | ash3en quits (~Thunderbi@146.70.124.222) (Ping timeout: 252 seconds) |
| 17:54:06 | → | ash3en1 joins (~Thunderbi@2a02:8108:2810:ab00::1f3e) |
| 17:56:23 | ash3en1 | is now known as ash3en |
| 18:08:34 | → | petrichor joins (~znc-user@user/petrichor) |
| 18:09:23 | × | ash3en quits (~Thunderbi@2a02:8108:2810:ab00::1f3e) (Ping timeout: 252 seconds) |
| 18:09:44 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 18:10:57 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 18:15:04 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 18:24:57 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 18:25:15 | × | dlock23 quits (~dlock23@78.red-81-40-75.staticip.rima-tde.net) (Quit: Leaving) |
| 18:27:44 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 18:28:45 | × | kuribas quits (~user@ptr-17d51em3rhcvuvotah6.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 18:35:37 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 18:36:19 | → | mari-estel joins (~mari-este@2a02:3032:311:fd82:216:3eff:fe65:4eef) |
| 18:40:08 | → | hgolden_ joins (~hgolden@146.70.173.37) |
| 18:40:38 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 18:40:56 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 18:41:07 | × | euleritian quits (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:41:25 | → | euleritian joins (~euleritia@ip5f5ad3f6.dynamic.kabel-deutschland.de) |
| 18:42:53 | × | hgolden__ quits (~hgolden@169.150.203.23) (Ping timeout: 265 seconds) |
| 18:43:11 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 18:49:50 | × | mari-estel quits (~mari-este@2a02:3032:311:fd82:216:3eff:fe65:4eef) (Ping timeout: 244 seconds) |
| 18:51:52 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:00:02 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:38 | → | caconym joins (~caconym@user/caconym) |
| 19:01:52 | × | briandaed quits (~root@185.234.210.211.r.toneticgroup.pl) (Remote host closed the connection) |
| 19:02:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:05:23 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 19:05:30 | → | bearen joins (~bearen@user/bearen) |
| 19:07:52 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:08:26 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 19:08:38 | × | bearen quits (~bearen@user/bearen) (Client Quit) |
| 19:08:44 | → | simendsjo joins (~user@84.211.91.108) |
| 19:09:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:14:12 | → | mari-estel joins (~mari-este@185.238.219.66) |
| 19:16:43 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 19:17:02 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:17:02 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:20:38 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 19:22:08 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 19:22:46 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:24:12 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 19:25:28 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:37:00 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 19:39:46 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 19:40:33 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 19:41:54 | × | youthlic quits (~Thunderbi@user/youthlic) (Client Quit) |
| 19:42:01 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 19:42:20 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:42:43 | → | mantraofpie joins (~mantraofp@user/mantraofpie) |
| 19:48:02 | × | mari-estel quits (~mari-este@185.238.219.66) (Ping timeout: 252 seconds) |
| 19:48:23 | → | EvanR joins (~EvanR@user/evanr) |
| 19:53:18 | → | weary-traveler joins (~user@user/user363627) |
| 19:56:53 | → | floyza joins (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) |
| 19:58:39 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 19:58:58 | <yin> | is there any logical reason why we can't use bound variables (with `<-` in do blocks) inside where clauses? |
| 19:59:26 | <yin> | s/can't/wouldn't be able to |
| 19:59:29 | <ncf> | huh? |
| 20:00:48 | <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) |
| 20:00:49 | <monochrom> | It is because do-block is an expression but "where" is for definitions and pattern matching, so do-block is neither. |
| 20:01:14 | <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 |
| 20:01:15 | <int-e> | @undo do x <- a; b |
| 20:01:15 | <lambdabot> | a >>= \ x -> b |
| 20:02:16 | <int-e> | (after desugaring, the x is not in scope outside of that lambda) |
| 20:02:25 | <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". |
| 20:04:01 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 20:04:39 | <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. |
| 20:04:40 | <EvanR> | maybe you want to use a recursive do |
| 20:04:51 | <EvanR> | </clippy> |
| 20:04:56 | <monochrom> | haha |
| 20:05:41 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 255 seconds) |
| 20:05:58 | <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 |
| 20:06:18 | ljdarj1 | is now known as ljdarj |
| 20:06:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:06:45 | <EvanR> | where clause isn't an expression by itself, is another |
| 20:06:50 | <EvanR> | thing |
| 20:07:04 | <EvanR> | it attaches to definitions and case alternatives |
| 20:07:19 | <monochrom> | I think you could do it in your language. |
| 20:07:43 | <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? |
| 20:07:48 | <monochrom> | Haskell's "let x=e in b" certainly becomes Landin's "b where x=e". |
| 20:08:39 | <monochrom> | I don't even think you can design your language to accept "let x = 0:y in x where y = 1:x" haha |
| 20:08:52 | <monochrom> | err, I don't even think you can't! |
| 20:09:21 | <yin> | i don't know who Landin is |
| 20:09:34 | <monochrom> | Look for the paper "the next 700 languages" |
| 20:09:56 | × | euleritian quits (~euleritia@ip5f5ad3f6.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 20:10:28 | → | euleritian joins (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) |
| 20:11:22 | <yin> | ty |
| 20:12:51 | <yin> | c_wraith: just syntactical convenience |
| 20:17:56 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 20:18:18 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 20:20:49 | × | euleritian quits (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Remote host closed the connection) |
| 20:21:04 | → | euleritian joins (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) |
| 20:21:08 | × | euleritian quits (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 20:21:32 | → | euleritian joins (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) |
| 20:23:08 | <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 |
| 20:23:28 | <EvanR> | where the definitions are in order |
| 20:23:48 | <EvanR> | like a damn math book, they define stuff seemingly out of blue before getting to the point |
| 20:27:51 | <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. |
| 20:29:43 | <dolio> | Also, making where an expression like Landin has its disadvantages w/r/t how Haskell's syntax currently works. |
| 20:29:47 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 20:29:57 | <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" >:) |
| 20:30:15 | × | bliminse quits (~bliminse@user/bliminse) (Quit: leaving) |
| 20:30:22 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:30:40 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 20:30:45 | → | CiaoSen joins (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) |
| 20:30:49 | <monochrom> | This is why "let x = 0:y in x where y = 1:x" is the best of both worlds. >:) |
| 20:30:54 | <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. |
| 20:31:36 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:31:37 | <monochrom> | Yes that one is right. |
| 20:32:58 | <monochrom> | "case x:xt | x > 0 -> y | otherwise -> - y where y = x*x" y is available to both branches. |
| 20:33:34 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 20:33:47 | <monochrom> | in fact, also available to the guard conditions. "case x:xt | z > 0 -> ... where z=x+2" is OK. |
| 20:33:51 | <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. |
| 20:34:39 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 20:35:22 | <ncf> | they've added "using" or whatever recently |
| 20:35:29 | × | ljdarj1 quits (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 20:35:42 | <monochrom> | Yikes haha that sounds like syntax inflation. |
| 20:35:48 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 20:35:57 | <ncf> | https://agda.readthedocs.io/en/latest/language/with-abstraction.html#left-hand-side-let-bindings |
| 20:35:57 | <dolio> | Is that too new for readthedocs? |
| 20:36:29 | <dolio> | Oh, nice. |
| 20:36:39 | → | euphores joins (~SASL_euph@user/euphores) |
| 20:50:53 | × | michalz quits (~michalz@185.246.207.217) (Remote host closed the connection) |
| 21:04:04 | × | CiaoSen quits (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 21:08:20 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 21:12:44 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 21:29:28 | → | sourcetarius joins (~sourcetar@user/sourcetarius) |
| 21:32:19 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:33:00 | <yin> | i don't think tgis would be a good thing for Haskell to have. i was just curious of the implications |
| 21:34:30 | → | bliminse joins (~bliminse@user/bliminse) |
| 21:37:35 | → | supercode joins (~supercode@user/supercode) |
| 21:40:12 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 21:40:26 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 21:51:57 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:54:25 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 21:58:41 | → | Guest82 joins (~Guest82@152.44.49.129) |
| 21:59:41 | × | Guest82 quits (~Guest82@152.44.49.129) (Client Quit) |
| 21:59:54 | × | euleritian quits (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 22:00:11 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 22:02:58 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:04:00 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:09:12 | × | andrewboltachev quits (~andrey@178.141.123.3) (Quit: Leaving.) |
| 22:12:22 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 22:24:21 | × | mantraofpie quits (~mantraofp@user/mantraofpie) (Ping timeout: 260 seconds) |
| 22:36:43 | × | xff0x quits (~xff0x@2405:6580:b080:900:31d8:fed5:6c70:b7b9) (Ping timeout: 264 seconds) |
| 22:41:44 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 22:42:05 | × | tuxpaint quits (~a@put.gay) (Quit: gn) |
| 22:42:24 | → | tuxpaint joins (~a@put.gay) |
| 22:49:33 | → | xff0x joins (~xff0x@2405:6580:b080:900:8633:3fd0:abbc:825) |
| 22:51:47 | → | talismanick joins (~user@2601:644:937c:ed10::ae5) |
| 23:03:49 | → | thegeekinside joins (~thegeekin@189.217.93.202) |
| 23:08:13 | × | acidjnk quits (~acidjnk@p200300d6e72cfb09b827840f1f57a57d.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 23:15:00 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 265 seconds) |
| 23:16:39 | → | troojg joins (~troojg@user/troojg) |
| 23:18:29 | × | motherfsck quits (~motherfsc@user/motherfsck) (Quit: quit) |
| 23:20:39 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 23:23:53 | × | thegeekinside quits (~thegeekin@189.217.93.202) (Remote host closed the connection) |
| 23:27:24 | × | remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Ping timeout: 260 seconds) |
| 23:29:30 | → | remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz) |
| 23:32:17 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:36:45 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 23:38:01 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 23:45:43 | × | Digit quits (~user@user/digit) (Read error: Connection reset by peer) |
| 23:47:26 | → | Digit joins (~user@user/digit) |
| 23:59:34 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
All times are in UTC on 2024-10-07.