Logs on 2023-11-11 (liberachat/#haskell)
| 00:00:42 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 00:03:38 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:05:52 | <geekosaur> | probably for the best |
| 00:05:54 | <geekosaur> | > (1 :+ 5) :+ (2 :+ 3) |
| 00:05:55 | <lambdabot> | (1 :+ 5) :+ (2 :+ 3) |
| 00:11:37 | × | alp_ quits (~alp@2001:861:5e02:eff0:7ec6:459:f36f:4240) (Ping timeout: 246 seconds) |
| 00:13:21 | × | neceve quits (~neceve@user/neceve) (Ping timeout: 240 seconds) |
| 00:13:35 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 00:14:44 | → | pavonia joins (~user@user/siracusa) |
| 00:15:51 | × | thegeekinside quits (~thegeekin@189.141.80.123) (Remote host closed the connection) |
| 00:26:56 | × | ph88 quits (~ph88@2a02:8109:9e26:c800::302a) (Remote host closed the connection) |
| 00:41:02 | × | arahael quits (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (Ping timeout: 255 seconds) |
| 00:41:57 | → | sansk joins (~sansk@user/sansk) |
| 00:51:31 | × | Square quits (~Square@user/square) (Ping timeout: 246 seconds) |
| 00:54:00 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 00:56:45 | → | derpyxdhs joins (~Thunderbi@user/derpyxdhs) |
| 00:57:01 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
| 01:02:19 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 01:06:28 | × | ddellacosta quits (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 01:06:37 | × | sansk quits (~sansk@user/sansk) (Quit: WeeChat 4.0.4) |
| 01:10:14 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 01:10:42 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 01:12:58 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 01:13:28 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 01:14:27 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 01:14:38 | × | chomwitt quits (~chomwitt@2a02:587:7a12:2d00:1ac0:4dff:fedb:a3f1) (Ping timeout: 252 seconds) |
| 01:29:11 | × | hueso quits (~root@user/hueso) (Ping timeout: 255 seconds) |
| 01:29:12 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 01:30:09 | → | hueso joins (~root@user/hueso) |
| 01:33:03 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 258 seconds) |
| 01:33:48 | × | Me-me quits (~me-me@user/me-me) (Server closed connection) |
| 01:35:32 | → | Me-me joins (~me-me@2602:ff16:3:0:1:dc:beef:d00d) |
| 01:44:12 | × | derpyxdhs quits (~Thunderbi@user/derpyxdhs) (Quit: derpyxdhs) |
| 01:46:45 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 01:51:22 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 01:53:42 | ec_ | is now known as ec |
| 01:59:32 | × | pie_ quits (~pie_bnc@user/pie/x-2818909) (Server closed connection) |
| 01:59:42 | → | pie_ joins (~pie_bnc@user/pie/x-2818909) |
| 02:15:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Ping timeout: 272 seconds) |
| 02:18:09 | × | otto_s quits (~user@p5de2fb17.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 02:18:19 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 02:19:48 | → | otto_s joins (~user@p5de2f676.dip0.t-ipconnect.de) |
| 02:25:21 | × | glguy quits (g@libera/staff/glguy) (*.net *.split) |
| 02:25:35 | → | glguy joins (g@libera/staff/glguy) |
| 02:37:57 | → | thegman joins (~thegman@072-239-207-086.res.spectrum.com) |
| 02:49:57 | <monochrom> | w00t Complex (Complex a) |
| 02:50:12 | <monochrom> | I think I heard that Complex is actually a Monad instance! |
| 02:50:52 | <monochrom> | Haha yes, even better, MonadFix and MonadZip too. |
| 02:51:18 | <monochrom> | "since base-4.15.0.0" |
| 02:51:46 | <monochrom> | OK Functor Applicative Monad were since 4.9.0.0. |
| 02:51:56 | <EvanR> | 🤔 |
| 02:52:39 | <monochrom> | > join (1 :+ 5) :+ (2 :+ 3) |
| 02:52:41 | <lambdabot> | (1.0 :+ 0.0) :+ (2.0 :+ 3.0) |
| 02:52:45 | <monochrom> | :) |
| 02:53:28 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 02:53:51 | <EvanR> | shouldn't that be -2 :+ 7 |
| 02:53:59 | <EvanR> | er |
| 02:54:13 | <monochrom> | "It's complicated." :) |
| 02:56:30 | <monochrom> | Yeah I was thinking 1 :+ 3 |
| 02:56:47 | <EvanR> | lol |
| 02:57:30 | <EvanR> | :t (1 :+ 5) :+ (2 :+ 3) |
| 02:57:31 | <lambdabot> | Num a => Complex (Complex a) |
| 02:57:39 | <EvanR> | :t join (1 :+ 5) :+ (2 :+ 3) |
| 02:57:40 | <lambdabot> | RealFloat a => Complex (Complex a) |
| 02:57:44 | <EvanR> | wtf |
| 02:58:11 | <EvanR> | :t join ((1 :+ 5) :+ (2 :+ 3)) |
| 02:58:12 | <lambdabot> | Num a => Complex a |
| 02:58:29 | <monochrom> | Oh! Right, I blew the parentheses. |
| 02:58:45 | <monochrom> | > join ((1 :+ 5) :+ (2 :+ 3)) |
| 02:58:46 | <lambdabot> | 1 :+ 3 |
| 02:58:47 | <geekosaur> | gutter quaternions? 😛 |
| 02:58:51 | <monochrom> | better |
| 02:59:44 | <EvanR> | a discarding monad |
| 02:59:56 | <EvanR> | > return 7 :: Complex Double |
| 02:59:58 | <lambdabot> | 7.0 :+ 7.0 |
| 03:00:31 | <monochrom> | Generally if you have "data P a = P a a" then the only correct join is join (P (P x _) (P _ y)) = P x y. |
| 03:01:05 | <EvanR> | taking the diagonal |
| 03:01:15 | <monochrom> | It is discarding because you have an isomorphism with Bool->a |
| 03:01:23 | <monochrom> | Or yeah, diagonal |
| 03:02:04 | <EvanR> | MONADS. you can't explain that |
| 03:02:38 | <EvanR> | must be a miracle 🤡 |
| 03:04:17 | <EvanR> | so every representable functor is a monad in a unique way because function monad |
| 03:04:21 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:04:21 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:04:21 | finn_elija | is now known as FinnElija |
| 03:07:15 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 03:08:32 | × | edr quits (~edr@user/edr) (Quit: Leaving) |
| 03:16:33 | × | td_ quits (~td@i53870938.versanet.de) (Ping timeout: 258 seconds) |
| 03:18:19 | → | td_ joins (~td@i53870937.versanet.de) |
| 03:18:31 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 03:20:22 | <catilina> | jackdk: following your and [exa]'s pointers, I've got the code to not fail upon running now in https://paste.tomsmeding.com/UUEr8bhj. It still breaks the workflow as the meta values are assigned (in line 5 and 6) before the filter in line 7. |
| 03:21:07 | <catilina> | do you see how I can merge the 3 lines? |
| 03:24:21 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 240 seconds) |
| 03:25:13 | <jackdk> | catilina: move the `@(Pandoc meta _)` pattern match to the second binding of `pandoc <-`? |
| 03:28:39 | <catilina> | Hmm, that seems to somewhat work: https://paste.tomsmeding.com/XLgzznfh |
| 03:29:13 | <catilina> | but now there's an error in the type somewhere else, so not fully? |
| 03:34:46 | <jackdk> | don't know, sorry. I have too much on this weekend to crack open the project and look at it, I hope someone else can help |
| 03:36:42 | <catilina> | no worries - hope you have a good weekend! |
| 03:42:25 | → | rosco joins (~rosco@yp-150-69.tm.net.my) |
| 03:47:40 | → | Inst joins (~Inst@120.244.192.250) |
| 03:51:15 | × | user2 quits (~user@162.255.84.96) (Server closed connection) |
| 03:51:37 | → | user2 joins (~user@162.255.84.96) |
| 03:57:59 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 04:09:53 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 04:10:56 | × | Xe quits (~cadey@perl/impostor/xe) (Server closed connection) |
| 04:11:23 | → | Xe joins (~cadey@perl/impostor/xe) |
| 04:12:54 | × | xff0x quits (~xff0x@2405:6580:b080:900:451:c5fa:806e:352e) (Ping timeout: 258 seconds) |
| 04:14:40 | → | xff0x joins (~xff0x@178.255.149.135) |
| 04:16:12 | → | aforemny_ joins (~aforemny@2001:9e8:6cd8:e200:b35d:4788:701d:c1c7) |
| 04:16:34 | → | mud joins (~mud@user/kadoban) |
| 04:17:30 | × | aforemny quits (~aforemny@2001:9e8:6cf3:9f00:3f53:5505:c25d:bb07) (Ping timeout: 258 seconds) |
| 04:21:05 | × | xff0x quits (~xff0x@178.255.149.135) (Ping timeout: 252 seconds) |
| 04:22:55 | → | xff0x joins (~xff0x@2405:6580:b080:900:ad36:3751:9aba:5ce7) |
| 04:24:32 | × | myme quits (~myme@2a01:799:d60:e400:303:74c0:223b:e4a8) (Ping timeout: 272 seconds) |
| 04:25:21 | → | myme joins (~myme@2a01:799:d60:e400:8378:aee3:77de:c4de) |
| 04:28:15 | × | YuutaW quits (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Ping timeout: 240 seconds) |
| 04:29:54 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 04:32:51 | zero | is now known as yin |
| 04:35:19 | × | rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
| 04:47:35 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 04:49:09 | × | zups quits (~meow@2a01:4f9:c010:6036::1) (Server closed connection) |
| 04:49:27 | → | zups joins (~meow@2a01:4f9:c010:6036::1) |
| 04:55:43 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 05:08:45 | → | qqq joins (~qqq@92.43.167.61) |
| 05:11:36 | → | trev joins (~trev@user/trev) |
| 05:22:50 | → | rosco joins (~rosco@193.138.218.161) |
| 05:40:58 | × | Inst quits (~Inst@120.244.192.250) (Remote host closed the connection) |
| 05:41:15 | → | Inst joins (~Inst@120.244.192.250) |
| 05:45:21 | × | rosco quits (~rosco@193.138.218.161) (Ping timeout: 240 seconds) |
| 05:47:35 | → | rosco joins (~rosco@193.138.218.161) |
| 05:51:01 | × | td_ quits (~td@i53870937.versanet.de) (Ping timeout: 240 seconds) |
| 05:51:41 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 05:51:49 | <Inst> | I think it's possible to have an IO instance for traversable, but why isn't it in base? |
| 05:52:58 | → | td_ joins (~td@i53870901.versanet.de) |
| 05:53:39 | <Inst> | I know about chshersh's IO as an instance of Num, you guys were making fun of me for a IsString instance of IO, but IO is still a Semigroup and Monoid, not sure why Traversable IO is a bad idea? |
| 05:53:55 | × | rosco quits (~rosco@193.138.218.161) (Ping timeout: 246 seconds) |
| 05:54:28 | <Inst> | oh, Foldable |
| 05:54:37 | <Inst> | Traversable requires Foldable, and Foldable IO -> unsafePerformIO |
| 05:54:38 | <Inst> | doip |
| 05:59:20 | <monochrom> | I think I speak for most regular when I say that I am mostly skeptical of most implicit type conversion puns. |
| 05:59:38 | <monochrom> | s/regular/regulars/ |
| 06:00:08 | <Inst> | Yeah, I know, I had it explained to me why throwing IsString around, especially with outside library types, is a bad idea. |
| 06:00:08 | → | bilegeek joins (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
| 06:00:15 | <monochrom> | Even IsString, I refuse to use it except for very specific scenerios. |
| 06:00:18 | <Inst> | *base library types |
| 06:00:26 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 06:00:32 | → | euleritian joins (~euleritia@dynamic-046-114-206-043.46.114.pool.telefonica.de) |
| 06:00:36 | <Inst> | I got around my problem by converting my string into a lambda, then fmap / <*> into the effects I wanted |
| 06:00:55 | × | euleritian quits (~euleritia@dynamic-046-114-206-043.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:01:12 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:01:15 | <Inst> | I have no objection to purity, and am willing to pay a reasonable price for it. |
| 06:02:21 | <Inst> | Thanks for the response monochrom :) |
| 06:02:24 | <monochrom> | Num IO and IsString IO cross the grey area and unambiguosly step into "why don't you just go with javascript and tcl and leave us alone" territory. |
| 06:03:42 | <Inst> | ChShersh, btw, is now talking about how he likes Typescript and Python now :) |
| 06:04:06 | <monochrom> | Equivalently I am not saying they are wrong, I am saying they are against the spirit of Haskell, they are shoehorning other languages into Haskell. javscript and tcl exist for a reason, for people or scenerios who need that. |
| 06:04:53 | <Inst> | monochrom: as far as I understand, it's a matter of scale, you can do all sorts of weird tricks with Haskell to break it at small scales, but Haskell will have a nasty revenge once you scale up |
| 06:05:11 | <Inst> | and all the inconveniences are there for a reason |
| 06:06:00 | → | _xor joins (~xor@72.49.195.41) |
| 06:06:29 | <monochrom> | There is no way you can shoehorn all programming styles into one language. They conflict with each other. You must accept a trade off and give up something. |
| 06:08:05 | <Inst> | I think looking at a certain legacied 132k SLOC codebase with varying code styles |
| 06:08:19 | <Inst> | I used to not understand why people loved their monad transformers, effect systems, etc, so much |
| 06:09:13 | <Inst> | now I understand, with very simple code, small programs, it doesn't really matter what you do, or what architectures you use, but working on larger programs / codebases, architecture, safety, all the ideological constraints of Haskell, make sense |
| 06:11:26 | × | fweht quits (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:12:47 | × | totbwf quits (sid402332@id-402332.uxbridge.irccloud.com) (Server closed connection) |
| 06:13:01 | → | totbwf joins (sid402332@id-402332.uxbridge.irccloud.com) |
| 06:21:58 | → | arahael joins (~arahael@1.145.75.174) |
| 06:22:19 | <hammond> | does increased modularity and granularity affect readability? |
| 06:22:45 | <Hecate> | hammond: yes |
| 06:22:51 | <monochrom> | Define readability, e.g., readable by 3yo? readable by educated people? |
| 06:23:35 | <hammond> | should i make my objects bigger and coarser? to improve readability? aka use broader strokes? |
| 06:23:40 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 06:24:06 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 06:24:11 | <Hecate> | monochrom: more like "readable by the same person with less headache" |
| 06:24:11 | <hammond> | well readable would be something that takes an average human a reasonable amount of time to understand. |
| 06:24:15 | <Inst> | Sorry if this is not helpful, or boring, but I can understand why people prefer abstractions, even at the small scale |
| 06:24:45 | <monochrom> | The average human is not even programming-literate. |
| 06:24:45 | <Hecate> | hammond: if you're looking to create abstractions, determine first if you will use them more than twice |
| 06:25:10 | <Inst> | When you start with a language, you are working at the small scale, but you develop habits there. What might work for scripts won't work for larger programs, and you're going to end up taking your scripting habits up when working with larger programs, so it's better to start with good habits. |
| 06:25:24 | <monochrom> | That may change in the near future but even 10 years from now it will only be, say, Swift-literate. |
| 06:25:52 | <Hecate> | monochrom: I think hammond is talking about something else here |
| 06:25:57 | <hammond> | hecate that's the thing. you make this ultra fine grained library and say you will reuse the code, and it kinda makes things harder. |
| 06:26:00 | → | bilegeek_ joins (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
| 06:26:37 | <monochrom> | s/talking/thinking/ |
| 06:27:09 | <monochrom> | But I am not going to play telepathy. I can only work with the exact wording. |
| 06:27:21 | <Hecate> | hammond: that's why we have refactorings. :) But it's better to have something that works first before generalising it |
| 06:27:23 | <hammond> | monochrom: so you say readibility doesnt matter. |
| 06:27:36 | <monochrom> | No, I say readability is undefined. |
| 06:27:49 | <monochrom> | Or even better, moving goalpost. |
| 06:27:50 | <hammond> | code should can be difficult, because we are supposed to be programmers. |
| 06:27:51 | × | bilegeek quits (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Ping timeout: 240 seconds) |
| 06:28:22 | → | harveypwca joins (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) |
| 06:28:25 | <Inst> | monochrom: can we define it as "readable by the end user", or "readable by probable collaborators"? Although, the latter seems trivial (i.e, if it's not readable, they won't collaborate). |
| 06:29:40 | × | bilegeek_ quits (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Read error: Connection reset by peer) |
| 06:29:57 | → | bilegeek_ joins (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
| 06:31:17 | <hammond> | Hecate, the opposite of generalization is specialization. say i write a large function that only does one thing. I can probably break that function into smaller generalized pieces of code. by doing that i'm reducing readability. |
| 06:31:30 | <hammond> | it's kinda like having a bunch of GOTOs. |
| 06:32:42 | <monochrom> | It is always personal. It is always an echo chamber. You make your a library in a certain way, a certain style. Then it attracts people who understand it and repels people who don't. But you forget the selection bias echo chamber and jump from "this library is readable by people who like it this way" to "this library is readable, absolutely, unconditionally, universally, period, now why some other people don't get it?". It is always personal, it is |
| 06:32:42 | <monochrom> | always an echo chamber. |
| 06:32:53 | <Hecate> | hammond: I don't necessarily agree, taken individually these pieces become more readable because their dependencies are made more explicit |
| 06:33:31 | <Inst> | Maybe that's a question of culture, i.e, some people might find a monolith more readable, others would have an easier time with smaller functions. |
| 06:33:51 | <Inst> | It's weird, what attracted me to Haskell in the first place was how short and comprehensible the individual pieces of Haskell programs were. |
| 06:34:01 | <Inst> | Now I'm more addicted to where clause abuse. |
| 06:34:52 | × | bilegeek_ quits (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Ping timeout: 246 seconds) |
| 06:37:16 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 264 seconds) |
| 06:38:04 | <hammond> | Hecate but you would have to jump from this file to another file and back again, just to understand a portion. code reuseability is great, and can still be done, but at a coarser level. this is horrible example, but think bash script. |
| 06:39:52 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 06:40:44 | → | califax joins (~califax@user/califx) |
| 06:46:08 | <Hecate> | hammond: yeah it's alright to jump files. Well first of all you can have two files open side by side, but also you should be taking notes when diving into a code base |
| 06:46:18 | <hammond> | "The animal jumped on my desk and was playing with my keyboard." as opposed to "The cat jumped ... etc" by being specific you are more readible. Lisp is great, you can really abstract a lof of things, but it's incredibly unreadible. |
| 06:46:30 | <hammond> | haha ok |
| 06:54:25 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 07:00:53 | → | danza joins (~francesco@151.35.107.96) |
| 07:07:08 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Read error: Connection reset by peer) |
| 07:07:51 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 07:11:01 | × | danza quits (~francesco@151.35.107.96) (Ping timeout: 240 seconds) |
| 07:14:03 | → | zaquest joins (~notzaques@5.130.79.72) |
| 07:16:11 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 07:19:52 | × | thegman quits (~thegman@072-239-207-086.res.spectrum.com) (Quit: leaving) |
| 07:20:43 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 07:22:50 | → | alp_ joins (~alp@2001:861:5e02:eff0:40ee:54d5:8b84:9bc6) |
| 07:26:15 | → | yoyofreeman joins (~yoyofreem@176.97.76.178) |
| 07:27:40 | × | califax quits (~califax@user/califx) (Ping timeout: 264 seconds) |
| 07:29:31 | → | califax joins (~califax@user/califx) |
| 07:40:51 | → | acidjnk joins (~acidjnk@p200300d6e72b9351ac6f5a8b7958b98c.dip0.t-ipconnect.de) |
| 07:45:16 | × | td_ quits (~td@i53870901.versanet.de) (Ping timeout: 258 seconds) |
| 07:45:22 | → | Square joins (~Square@user/square) |
| 07:50:42 | × | arahael quits (~arahael@1.145.75.174) (Ping timeout: 255 seconds) |
| 07:51:59 | → | td_ joins (~td@i5387091C.versanet.de) |
| 07:57:56 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 08:01:44 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 08:02:31 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 08:09:37 | × | harveypwca quits (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) (Quit: Leaving) |
| 08:11:14 | <Inst> | this is weird |
| 08:11:22 | <Inst> | > u.moo = "Moo!" |
| 08:11:24 | <lambdabot> | <hint>:1:7: error: parse error on input ‘=’ |
| 08:11:36 | <Inst> | > uuoouo.moo = "Moo!" |
| 08:11:37 | <lambdabot> | <hint>:1:12: error: parse error on input ‘=’ |
| 08:11:44 | <Inst> | well, GHCI will accept this, however |
| 08:11:51 | <Inst> | oh, it's accepting it as a definition of . |
| 08:12:52 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 08:13:50 | → | euleritian joins (~euleritia@dynamic-046-114-203-139.46.114.pool.telefonica.de) |
| 08:13:52 | → | ddellacosta joins (~ddellacos@ool-44c738de.dyn.optonline.net) |
| 08:16:42 | → | fendor joins (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) |
| 08:17:11 | → | bilegeek_ joins (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
| 08:20:11 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 08:23:54 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 08:24:07 | → | AlexZenon_2 joins (~alzenon@94.233.241.129) |
| 08:24:30 | → | Pickchea joins (~private@user/pickchea) |
| 08:25:40 | × | AlexZenon quits (~alzenon@94.233.241.129) (Ping timeout: 255 seconds) |
| 08:26:43 | → | kimiamania464 joins (~b4f4a2ab@user/kimiamania) |
| 08:27:01 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 255 seconds) |
| 08:27:01 | × | bah quits (~bah@l1.tel) (Ping timeout: 255 seconds) |
| 08:27:10 | → | bah joins (~bah@l1.tel) |
| 08:28:22 | × | kimiamania46 quits (~b4f4a2ab@user/kimiamania) (Ping timeout: 255 seconds) |
| 08:28:22 | kimiamania464 | is now known as kimiamania46 |
| 08:33:20 | → | CiaoSen joins (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
| 08:37:32 | × | joel135 quits (sid136450@id-136450.hampstead.irccloud.com) (Server closed connection) |
| 08:37:50 | → | joel135 joins (sid136450@id-136450.hampstead.irccloud.com) |
| 08:44:37 | → | danza joins (~francesco@151.43.102.160) |
| 08:48:00 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 08:48:45 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
| 08:49:50 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:50:34 | × | drlkf quits (~drlkf@192.184.163.34.bc.googleusercontent.com) (Server closed connection) |
| 08:51:00 | → | drlkf joins (~drlkf@192.184.163.34.bc.googleusercontent.com) |
| 08:52:44 | × | CiaoSen quits (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 258 seconds) |
| 09:00:49 | × | alp_ quits (~alp@2001:861:5e02:eff0:40ee:54d5:8b84:9bc6) (Ping timeout: 246 seconds) |
| 09:03:57 | → | ss4 joins (~wootehfoo@user/wootehfoot) |
| 09:04:14 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 09:05:17 | × | euleritian quits (~euleritia@dynamic-046-114-203-139.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 09:05:28 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
| 09:05:35 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 09:08:52 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 09:12:44 | × | ss4 quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 09:13:01 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 09:13:49 | × | yushyin quits (9DYMgg4QG5@mail.karif.server-speed.net) (Server closed connection) |
| 09:14:11 | → | yushyin joins (lVHsxtO6yj@mail.karif.server-speed.net) |
| 09:21:10 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 09:21:51 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 09:25:56 | → | CO2 joins (CO2@gateway/vpn/protonvpn/co2) |
| 09:27:11 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 09:29:52 | × | caubert_ quits (~caubert@user/caubert) (Server closed connection) |
| 09:30:11 | → | caubert joins (~caubert@user/caubert) |
| 09:31:37 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 09:32:18 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 09:33:04 | → | gmg joins (~user@user/gehmehgeh) |
| 09:37:04 | × | codedmart quits (~codedmart@li335-49.members.linode.com) (Server closed connection) |
| 09:37:22 | → | codedmart joins (~codedmart@li335-49.members.linode.com) |
| 09:40:24 | → | davl_ joins (~davl@207.154.228.18) |
| 09:40:43 | × | kiriakos quits (~kiriakos@p5b03e4a6.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 09:40:58 | × | disconnect3d quits (~disconnec@user/disconnect3d) (Ping timeout: 255 seconds) |
| 09:40:58 | × | davl quits (~davl@207.154.228.18) (Ping timeout: 255 seconds) |
| 09:41:04 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 09:42:42 | → | disconnect3d joins (~disconnec@user/disconnect3d) |
| 09:42:55 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 09:43:52 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 264 seconds) |
| 09:44:52 | × | danza quits (~francesco@151.43.102.160) (Ping timeout: 255 seconds) |
| 09:46:41 | → | alp_ joins (~alp@2001:861:5e02:eff0:59a7:a2ca:543c:6e8) |
| 09:47:02 | → | Jackneill joins (~Jackneill@20014C4E1E058A00ABC7937222D6C543.dsl.pool.telekom.hu) |
| 09:47:55 | × | bjs quits (sid190364@user/bjs) (Server closed connection) |
| 09:48:06 | → | bjs joins (sid190364@user/bjs) |
| 09:48:58 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 09:50:09 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 09:52:21 | × | bilegeek_ quits (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Quit: Leaving) |
| 09:54:31 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 09:56:03 | × | YuutaW quits (~YuutaW@mail.yuuta.moe) (Ping timeout: 260 seconds) |
| 09:58:52 | × | chiselfu1e quits (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
| 10:00:51 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:04:14 | → | arahael joins (~arahael@1.145.109.210) |
| 10:05:33 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:07:37 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 10:12:28 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 255 seconds) |
| 10:25:05 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 10:27:46 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 10:39:10 | × | acidjnk quits (~acidjnk@p200300d6e72b9351ac6f5a8b7958b98c.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 10:43:26 | × | arahael quits (~arahael@1.145.109.210) (Quit: leaving) |
| 10:49:34 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 10:49:40 | → | arahael joins (~arahael@21.127.96.58.static.exetel.com.au) |
| 10:52:27 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 10:53:33 | → | __monty__ joins (~toonn@user/toonn) |
| 10:59:56 | × | meooow quits (~meooow@165.232.184.169) (Server closed connection) |
| 11:00:11 | → | meooow joins (~meooow@2400:6180:100:d0::ad9:e001) |
| 11:10:12 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 11:17:41 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 11:20:42 | × | alp_ quits (~alp@2001:861:5e02:eff0:59a7:a2ca:543c:6e8) (Ping timeout: 258 seconds) |
| 11:22:51 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 11:26:25 | × | catilina quits (~user@49.235.216.139.sta.wbroadband.net.au) (Changing host) |
| 11:26:25 | → | catilina joins (~user@user/catilina) |
| 11:28:53 | × | nonzen_ quits (~nonzen@user/nonzen) (Server closed connection) |
| 11:29:09 | → | nonzen joins (~nonzen@user/nonzen) |
| 11:31:22 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 11:33:47 | → | alp_ joins (~alp@2001:861:5e02:eff0:fda7:f942:c2a6:6612) |
| 11:33:49 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 11:41:35 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 11:42:20 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Remote host closed the connection) |
| 11:47:09 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 11:53:45 | × | duncan quits (~duncan@nat-server.ehlab.uk) (Server closed connection) |
| 11:54:01 | → | duncan joins (~duncan@nat-server.ehlab.uk) |
| 11:55:56 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 11:56:23 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 11:56:37 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 11:57:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:59:41 | × | Sgeo quits (~Sgeo@user/sgeo) (Ping timeout: 240 seconds) |
| 12:00:23 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:06:25 | × | sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 12:06:50 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 12:07:29 | × | Inst quits (~Inst@120.244.192.250) (Read error: Connection reset by peer) |
| 12:09:34 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 12:09:49 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 12:09:54 | → | Lycurgus joins (~georg@li1192-118.members.linode.com) |
| 12:09:54 | × | Lycurgus quits (~georg@li1192-118.members.linode.com) (Changing host) |
| 12:09:54 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 12:15:56 | → | Inst joins (~Inst@120.244.192.250) |
| 12:17:08 | × | mankyKitty quits (sid31287@id-31287.helmsley.irccloud.com) (Server closed connection) |
| 12:17:16 | → | mankyKitty joins (sid31287@id-31287.helmsley.irccloud.com) |
| 12:27:34 | × | innegatives quits (uid621315@id-621315.tinside.irccloud.com) (Server closed connection) |
| 12:28:13 | → | innegatives joins (sid621315@id-621315.tinside.irccloud.com) |
| 12:35:01 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 12:35:22 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 12:38:30 | × | CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
| 12:39:24 | → | neceve joins (~neceve@user/neceve) |
| 12:42:52 | × | amir quits (sid22336@user/amir) (Server closed connection) |
| 12:43:01 | → | amir joins (sid22336@user/amir) |
| 12:45:03 | × | alp_ quits (~alp@2001:861:5e02:eff0:fda7:f942:c2a6:6612) (Ping timeout: 240 seconds) |
| 12:45:13 | × | nckx quits (~nckx@libera/staff/owl/nckx) (Server closed connection) |
| 12:45:18 | → | zombiboo joins (~user@2001:2042:3c78:ab00:ce0:e802:ba9d:f9d3) |
| 12:46:29 | → | nckx joins (~nckx@libera/staff/owl/nckx) |
| 12:46:56 | × | fendor quits (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) (Remote host closed the connection) |
| 12:51:19 | → | target_i joins (~target_i@217.175.14.39) |
| 12:54:02 | ← | zombiboo parts (~user@2001:2042:3c78:ab00:ce0:e802:ba9d:f9d3) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.1)) |
| 13:04:31 | × | Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 13:11:07 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 13:12:14 | → | euleritian joins (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
| 13:12:35 | → | Umeaboy joins (~Umeaboy@94-255-145-133.cust.bredband2.com) |
| 13:13:40 | <Umeaboy> | Hi! To solve this issue I need to recompile the kernel right? https://pastebin.mozilla.org/1VssEDFs |
| 13:20:44 | <exarkun> | I don't know, but I wouldn't guess that building ghc ever requires support for more deeply nested symbolic links than is standard. |
| 13:21:26 | <tomsmeding> | "...../opt/lib/ghc-9.2.3/lib/package.conf.d/Cabal-3.6.3.0.conf" failed: mode 120777 broken symbolic link to ../../../../../opt/lib/ghc-9.2.3/lib/package.conf.d/Cabal-3.6.3.0.conf |
| 13:21:30 | <tomsmeding> | that's a symbolic link to itself |
| 13:21:39 | <tomsmeding> | you can count the number of ".." |
| 13:21:48 | <tomsmeding> | so no, that's not suppose to happen |
| 13:27:04 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 13:28:52 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 13:30:24 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 13:31:42 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Max SendQ exceeded) |
| 13:32:10 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 13:32:46 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 246 seconds) |
| 13:33:22 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 13:35:24 | × | dunj3 quits (~dunj3@kingdread.de) (Quit: ZNC 1.8.2+deb2+b1 - https://znc.in) |
| 13:36:45 | × | eL_Bart0 quits (eL_Bart0@dietunichtguten.org) (Ping timeout: 255 seconds) |
| 13:38:43 | × | arahael quits (~arahael@21.127.96.58.static.exetel.com.au) (Ping timeout: 246 seconds) |
| 13:42:23 | × | euleritian quits (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 13:42:41 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 13:42:46 | → | billchenchina joins (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
| 13:42:50 | → | eL_Bart0 joins (eL_Bart0@dietunichtguten.org) |
| 13:44:43 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 13:48:29 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:51:15 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 13:52:39 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 240 seconds) |
| 13:53:22 | → | infinity0 joins (~infinity0@pwned.gg) |
| 13:53:38 | × | aspen quits (sid449115@id-449115.helmsley.irccloud.com) (Server closed connection) |
| 13:53:47 | → | aspen joins (sid449115@id-449115.helmsley.irccloud.com) |
| 13:58:15 | <Umeaboy> | tomsmeding: So, what Can I do? |
| 13:58:34 | <Umeaboy> | Try with a little older version? |
| 13:59:10 | × | eL_Bart0 quits (eL_Bart0@dietunichtguten.org) (Quit: Restarting) |
| 13:59:22 | AlexZenon_2 | is now known as AlexZenon |
| 14:09:52 | × | flukiluke quits (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Server closed connection) |
| 14:10:12 | → | flukiluke joins (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 14:13:47 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 14:23:57 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 14:25:02 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 14:31:22 | → | michalz joins (~michalz@185.246.207.203) |
| 14:31:27 | × | neceve quits (~neceve@user/neceve) (Ping timeout: 240 seconds) |
| 14:31:55 | × | qqq quits (~qqq@92.43.167.61) (Ping timeout: 246 seconds) |
| 14:37:08 | → | qqq joins (~qqq@92.43.167.61) |
| 14:47:56 | × | mud quits (~mud@user/kadoban) (Quit: quit) |
| 15:02:22 | → | chomwitt joins (~chomwitt@2a02:587:7a12:2d00:1ac0:4dff:fedb:a3f1) |
| 15:06:39 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 15:07:22 | → | euleritian joins (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
| 15:14:55 | × | euleritian quits (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 15:15:13 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:16:08 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 15:29:33 | → | eL_Bart0 joins (eL_Bart0@dietunichtguten.org) |
| 15:31:27 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 15:31:33 | → | mechap joins (~mechap@user/mechap) |
| 15:31:50 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:38:35 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 15:38:57 | → | euleritian joins (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
| 15:39:38 | → | acidjnk joins (~acidjnk@p200300d6e72b9351ac6f5a8b7958b98c.dip0.t-ipconnect.de) |
| 15:39:47 | × | sajith quits (~sajith@user/sajith) (Server closed connection) |
| 15:40:07 | → | sajith_ joins (~sajith@user/sajith) |
| 15:40:27 | → | alguem joins (~alguem@45.163.64.23) |
| 15:40:40 | <alguem> | test |
| 15:41:22 | → | Guest65 joins (~Guest65@45.163.64.23) |
| 15:41:27 | <geekosaur> | pass |
| 15:42:08 | <alguem> | it is my frist time using this "libera chat" is it like discord or what? |
| 15:42:28 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:42:42 | <geekosaur> | not very |
| 15:43:46 | <Clint> | depends on how you spin it |
| 15:45:28 | <exarkun> | it's like N pieces of software sending small messages to M other pieces of software which then retransmits those messages largely in-tact to Q pieces of software |
| 15:45:37 | <exarkun> | which I think is exactly identical to discord? |
| 15:45:49 | <exarkun> | also, other things! |
| 15:47:24 | <alguem> | it's like a text based chat protocol? |
| 15:48:00 | <ski> | yes |
| 15:48:18 | <geekosaur> | it just lacks a lot of modern amenities |
| 15:48:36 | geekosaur | *poofs* — busy morning |
| 15:48:57 | <c_wraith> | it's from.. the early 90s? |
| 15:49:15 | <ski> | 1988 |
| 15:49:26 | <ski> | by Jarkko Oikarinen |
| 15:50:12 | <alguem> | it seems very cool, except that apparently it has no message historic, it seems |
| 15:50:25 | <ski> | (i consider that a feature) |
| 15:50:34 | <alguem> | and since I didn't gave any password in, i guess its less moderated? |
| 15:50:40 | <alguem> | like |
| 15:50:45 | <ski> | there's moderation |
| 15:51:01 | <alguem> | how is that? |
| 15:51:13 | <ski> | but you tend to be able to join channels, without necessarily making an account first, yea |
| 15:51:14 | <exarkun> | in each channel, there are participants enabled to take certain actions |
| 15:51:26 | <exarkun> | like mute a user, or kick them out |
| 15:51:50 | <ski> | (some channels do require registration, though. either as a temporary measure, to say avoid spammers for a period. or more permanently) |
| 15:51:51 | <exarkun> | also, this network _does_ have accounts and authentication, it's just optional most of the time |
| 15:52:27 | <alguem> | I think that with an account, Ill be able to read old messages? |
| 15:52:57 | <yushyin> | ircv3 has a chathistory extension, but it's only a draft and the libera network doesn't support it (yet) |
| 15:52:57 | <alguem> | at least since when I joint ? |
| 15:53:02 | <ski> | network staff for the most part stays away from getting involved in individual channel moderation, deals more with people being a problem with multiple channels |
| 15:53:50 | <ski> | alguem : "I think that with an account, Ill be able to read old messages?" -- no. you'll be able to read (and send) MemoServ messages, though |
| 15:54:12 | <alguem> | hmmm |
| 15:54:21 | <alguem> | still interesting |
| 15:55:14 | <ski> | (i see to remember seeing your nickname before, though .. perhaps from the Freenode days, maybe ? or maybe i'm confusing with someone else) |
| 15:55:40 | <alguem> | wondering what kind of topics go here, I guess it's not meant for support with haskell? since it doesn't seem to allow images |
| 15:55:52 | × | acro quits (~acro@user/acro) (Server closed connection) |
| 15:56:01 | <ski> | Haskell support and discussion goes here |
| 15:56:07 | → | acro joins (~acro@user/acro) |
| 15:56:41 | <ski> | people tend to paste snippets of code on paste sites, and give the resulting links to the pastes in their messages here |
| 15:57:32 | <ski> | (that also works for image paste sites .. although it's generally considered a bit rude to use that for code pastes, unless it's really necessary to use an image rather than text, to display the issue in question) |
| 15:57:40 | <alguem> | Maybe you've seen, ski, "alguem" literally means "someone" in direct translation to English, so it wouldn't surprise me if someone before me used this nick, but it wasn't me, it's my first time using something like this chat |
| 15:57:49 | <ski> | ah, that could be it :) |
| 15:59:09 | <alguem> | I guess once I saw a guy from Youtube using something similar tho |
| 15:59:56 | <EvanR> | alguem, IRC is like two cargo ships rendezvous in the middle of the ocean, no names no serial numbers no record the transaction takes place |
| 16:00:10 | <alguem> | but it seemed to be complex to set up, he used it in terminal haha |
| 16:00:31 | <EvanR> | https://www.youtube.com/watch?v=O2rGTXHvPCQ |
| 16:00:54 | <ski> | oh, i guess i should mention .. a common mistake newbies make is thinking that noone's there, if noone appears to be responding directly within a few minutes (at best). people generally are commonly connected to IRC, while doing other things (working, eating, watching a film, and even going for a walk or sleeping) |
| 16:02:12 | <ski> | so .. be patient, preferably wait at least half an hour after announcing your presence. also, of course, some times of day tend to be more active that others. also, people may be around, lurking or glancing at the channel, but not saying anything, until someone brings up an interesting topic |
| 16:02:15 | <ncf> | the five human activities |
| 16:03:27 | <EvanR> | libera has an easy to use web client |
| 16:03:32 | <EvanR> | not complex |
| 16:03:43 | <alguem> | i doubt that he was using libera |
| 16:04:05 | <EvanR> | if you have your own client you can connect to any IRC network |
| 16:04:24 | <alguem> | btw, thank you for the advice, ski :) |
| 16:04:28 | <ski> | (also, it's not uncommon that people are a bit loathe to announce their presence, until they feel they know enough about your issue to have a chance of being able to contribute. moral : be upfront with the details of your problem. don't just say "anyone here ?" or "anyone know about X ?", since (only) saying something like that will lower your chances of getting a response. saying what you've already tried |
| 16:04:34 | <ski> | also helps) |
| 16:04:36 | <yushyin> | libera is one of the bigger irc networks |
| 16:04:56 | <ski> | no problem, alguem :) |
| 16:10:40 | <mauke> | re: message history, this channel specifically has public logs |
| 16:11:33 | → | ph88 joins (~ph88@2a02:8109:9e26:c800::302a) |
| 16:12:07 | <ski> | yea, check the topic. on Libera, it's policy that channels are supposed to mention in topic when there's publicly available logging |
| 16:12:32 | <ph88> | does optparse-applicative support nested commands? like ./app command1 commandA --flag ? |
| 16:14:07 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 246 seconds) |
| 16:15:36 | × | Guest65 quits (~Guest65@45.163.64.23) (Quit: Client closed) |
| 16:18:38 | <ph88> | i think i found my answer here https://github.com/pcapriotti/optparse-applicative/issues/296#issuecomment-375837196 will try |
| 16:20:37 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:21:24 | × | auri quits (~auri@fsf/member/auri) () |
| 16:24:04 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 16:24:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 16:26:43 | × | xff0x quits (~xff0x@2405:6580:b080:900:ad36:3751:9aba:5ce7) (Ping timeout: 246 seconds) |
| 16:27:56 | → | xff0x joins (~xff0x@2405:6580:b080:900:fcad:32c3:a424:90e2) |
| 16:29:06 | <EvanR> | barendregt "lambda calculus with types" goes over many lambda calculi with types, one that is not mentioned in the lambda cube is "lambda-intersection" which is like simply typed lambda calculus with intersection types. Ok. Conspicuously missing is a lambda calculus with unions. Is it because that makes no sense? Or it makes sense but is too complicated? |
| 16:30:17 | <ski> | it can make sense, if you have (labelled, light-weight) variant types |
| 16:30:26 | → | ystael joins (~ystael@user/ystael) |
| 16:31:11 | → | auri joins (~auri@fsf/member/auri) |
| 16:31:40 | <EvanR> | so while lambda intersection has syntax for taking the union of types, and then parallel juxtaposition of terms to match the intersection types, union requires labeled variant syntax? |
| 16:31:46 | <ski> | intersection of two record types could involve intersection of the field types, and if one field is a function type, that could in turn take union of corresponding argument types, i think ? |
| 16:32:35 | <EvanR> | i meant to say, taking the intersection of types |
| 16:32:39 | <ski> | i dunno, haven't seen this particular "lambda-intersection" system |
| 16:32:54 | <EvanR> | it seems pretty funky |
| 16:33:12 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:33:50 | <EvanR> | the gimmick being, term has type A and B both |
| 16:34:50 | <EvanR> | 3|'a' : Int intersect Char, aiui |
| 16:37:02 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 16:37:07 | × | edmundnoble_ quits (sid229620@id-229620.helmsley.irccloud.com) (Server closed connection) |
| 16:37:16 | → | edmundnoble_ joins (sid229620@id-229620.helmsley.irccloud.com) |
| 16:38:31 | <ski> | ah, i guess i've not seen this `... | ...' |
| 16:40:34 | → | CiaoSen joins (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
| 16:41:31 | <EvanR> | there's also a special type omega, and you can say any term : omega |
| 16:42:01 | <EvanR> | I guess that stands for any |
| 16:42:03 | <ski> | yea, the neutral element of intersection |
| 16:45:19 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 16:48:44 | <ncf> | wouldn't 3|'a' just be an element of a pair type |
| 16:49:01 | <EvanR> | yeah I probably misunderstand something |
| 16:50:22 | × | bliminse quits (~bliminse@user/bliminse) (Ping timeout: 258 seconds) |
| 16:50:49 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 16:51:30 | <ph88> | how can i make a mutable integer? it's supposed to be 1 first time the function gets called and +1 after |
| 16:52:08 | <ski> | `IORef Int' ? |
| 16:52:15 | <ph88> | thanks ! |
| 16:53:24 | <ph88> | ski, maybe something else? With IORef i have to pass in the ref to the function i think |
| 16:53:27 | <ski> | i guess it would be commutative, ncf |
| 16:53:34 | → | oo_miguel joins (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) |
| 16:53:40 | <ski> | ph88 : not if the function is declared in a local scope |
| 16:54:01 | <EvanR> | STRef Int ? |
| 16:55:09 | → | alp_ joins (~alp@2001:861:5e02:eff0:fc3a:5bf6:1b0e:f883) |
| 16:55:22 | <ski> | @wiki Top level mutable state |
| 16:55:22 | <lambdabot> | https://wiki.haskell.org/Top_level_mutable_state |
| 16:55:27 | <ski> | might be interesting, ph88 ? |
| 16:56:21 | <ph88> | looks good, thanks guys |
| 16:56:39 | ski | would tend to opt for "Proposal 1: Don't do that", though |
| 16:56:39 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 16:57:02 | <EvanR> | what's wrong with taking IORef Int as an argument |
| 16:57:33 | <EvanR> | or the application's entire context record |
| 16:58:02 | × | CiaoSen quits (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 258 seconds) |
| 16:59:06 | <EvanR> | ok I must have seen this pipe thing somewhere entirely else on a different subject, barendregt's lambda-intersection has no pipe thing |
| 16:59:07 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 255 seconds) |
| 17:14:44 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:22:33 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 17:31:15 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
| 17:31:30 | × | tired quits (~tired@user/tired) (Server closed connection) |
| 17:31:32 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 17:31:54 | → | tired joins (~tired@user/tired) |
| 17:39:02 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 17:45:43 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 17:45:46 | → | Lycurgus joins (~georg@li1192-118.members.linode.com) |
| 17:45:46 | × | Lycurgus quits (~georg@li1192-118.members.linode.com) (Changing host) |
| 17:45:46 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 17:47:45 | → | dsrt^ joins (~cd@76.145.193.217) |
| 17:48:12 | → | Guest17 joins (~Guest17@2401:4900:80a9:b778::243:ecc0) |
| 17:48:23 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 17:48:29 | × | euleritian quits (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 17:48:49 | → | euleritian joins (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
| 17:48:50 | <Guest17> | A question about Haskell diagrams: can one change an attribute, like the colour, of a subdiagram, possibly by referring to its name? |
| 17:52:38 | <tomsmeding> | Umeaboy: not sure, something in the ghc build process has gone wrong to make that symlink cycle. But it might also be due to incorrect configuration; I know little about custom ghc builds, but perhaps you entered some path in some configuration where you incorrectly interpreted what path ought to go there? (Or the documentation was inaccurate, of course.) |
| 17:53:27 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 17:53:27 | <ncf> | Guest17: what's a haskell diagram? |
| 17:53:58 | <Guest17> | The Haskell Diagrams package |
| 17:59:23 | <EvanR> | diagrams, it's great |
| 17:59:35 | <EvanR> | SICP picture language on acid |
| 18:00:03 | <EvanR> | well this is haskell so, on base |
| 18:03:06 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 18:03:52 | × | Guest17 quits (~Guest17@2401:4900:80a9:b778::243:ecc0) (Ping timeout: 250 seconds) |
| 18:05:26 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 18:07:11 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 252 seconds) |
| 18:08:25 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 18:08:36 | × | MelanieMalik quits (ellenor@callbox.trd.is) (Ping timeout: 240 seconds) |
| 18:10:07 | × | SrPx quits (sid108780@id-108780.uxbridge.irccloud.com) (Server closed connection) |
| 18:10:51 | → | SrPx joins (sid108780@id-108780.uxbridge.irccloud.com) |
| 18:11:21 | → | Guest17 joins (~Guest17@2401:4900:80a9:b778::243:ecc0) |
| 18:11:40 | × | edm quits (sid147314@id-147314.hampstead.irccloud.com) (Server closed connection) |
| 18:12:10 | → | edm joins (sid147314@id-147314.hampstead.irccloud.com) |
| 18:13:42 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 18:13:53 | → | notzmv joins (~zmv@user/notzmv) |
| 18:16:55 | × | turlando quits (~turlando@user/turlando) (Server closed connection) |
| 18:17:11 | → | turlando joins (~turlando@user/turlando) |
| 18:17:15 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 18:18:53 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 18:19:15 | <monochrom> | Neeeeaaat, 9.4.8 has -split-sections for Windows too. Finally! |
| 18:20:39 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 18:20:57 | → | trev joins (~trev@user/trev) |
| 18:21:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
| 18:23:48 | × | Guest17 quits (~Guest17@2401:4900:80a9:b778::243:ecc0) (Ping timeout: 250 seconds) |
| 18:24:05 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 18:24:26 | × | alp_ quits (~alp@2001:861:5e02:eff0:fc3a:5bf6:1b0e:f883) (Remote host closed the connection) |
| 18:24:31 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 18:24:44 | → | alp_ joins (~alp@2001:861:5e02:eff0:d2d5:46e1:ee50:3986) |
| 18:29:07 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
| 18:29:27 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:30:11 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 18:30:16 | × | edwardk quits (sid47016@haskell/developer/edwardk) (Server closed connection) |
| 18:30:26 | → | edwardk joins (sid47016@haskell/developer/edwardk) |
| 18:30:54 | <ph88> | how can i match on an entire record? i tried this syntax r@{..} |
| 18:32:07 | <EvanR> | r@TheConstructor{} would match |
| 18:33:15 | <EvanR> | to write .. you need RecordWildcards |
| 18:33:19 | <ph88> | got it :D |
| 18:33:54 | <EvanR> | which introduces things invisibly into scope... |
| 18:34:44 | × | alp_ quits (~alp@2001:861:5e02:eff0:d2d5:46e1:ee50:3986) (Ping timeout: 255 seconds) |
| 18:37:00 | <EvanR> | if you use NamedFieldPuns instead, you can easily denote the fields you wanted to use |
| 18:37:21 | → | CiaoSen joins (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
| 18:38:03 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:42:06 | <geekosaur> | if you don't need to specify the constructor, why not just: r |
| 18:42:31 | <geekosaur> | unless you want some fields from it as well, in which case NamedFieldPuns is your friend |
| 18:48:44 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:13:09 | <ph88> | real world haskell example uses json web token https://github.com/nodew/haskell-realworld-example/blob/master/src/Conduit/JWT.hs i have just a simple client-server setup should i use jwt to make things future proof or better to use some alternative ? |
| 19:13:43 | <ph88> | geekosaur EvanR thanks was not up to date yet with NamedFieldPuns |
| 19:18:02 | → | neceve joins (~neceve@user/neceve) |
| 19:19:03 | → | ania123 joins (~ania123@wl-pool2-ont-004.uni-muenster.de) |
| 19:21:46 | <ania123> | does anyone can me point a paper where this problem is studied: https://math.stackexchange.com/questions/42210/number-of-ways-of-partitioning-a-sum-into-ordered-non-negative-summands |
| 19:22:42 | <geekosaur> | sounds like a question for ##math to me? |
| 19:24:29 | <ania123> | haskell community love math |
| 19:24:46 | <geekosaur> | true, but not necessarily number theory which this sounds like |
| 19:24:53 | <geekosaur> | there's a lot of kinds of math |
| 19:26:23 | <monochrom> | I never understood that logic. Those who like to discuss math are already in ##math. Therefore, regardless of whether I love math, if I am not there then it clearly means I don't want to talk about it. Therefore, why are you disturbing my peace? |
| 19:26:59 | <monochrom> | OK that's a rhetorical question. I know the answer of course. Because you think the world owes it to you. |
| 19:27:33 | <int-e> | they did ask on ##math, FWIW |
| 19:29:35 | × | kimiamania46 quits (~b4f4a2ab@user/kimiamania) (Ping timeout: 260 seconds) |
| 19:31:01 | <ph88> | how is one supposed to do cookie based authentication with servant these days? i found this package with a topic from 2018 where people ask to make it work with newer servant versions https://github.com/zohl/servant-auth-cookie/issues/48 |
| 19:32:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:35:39 | × | euleritian quits (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 19:36:22 | <ddellacosta> | ph88: I'm looking at the docs here: https://docs.servant.dev/en/stable/tutorial/Authentication.html#generalized-authentication-in-action ...and while I haven't dug too deep, it seems like they implement a cookie-based authentication scheme without servant-auth-cookie, unless I'm missing something. Have you tried building on the approach laid out there? |
| 19:36:55 | × | chymera quits (~chymera@ns1000526.ip-51-81-46.us) (Server closed connection) |
| 19:37:10 | → | chymera joins (~chymera@ns1000526.ip-51-81-46.us) |
| 19:38:50 | <ph88> | ddellacosta, it's just an example not a full implementation. I look for more batteries included like web frameworks in other languages |
| 19:39:39 | → | fweht joins (uid404746@id-404746.lymington.irccloud.com) |
| 19:41:41 | <ph88> | for example https://symfony.com/doc/current/security.html it has all of the stuff you want out of the box |
| 19:44:24 | <ph88> | maybe i should move from servant to another haskell framework which offers more, but which one ? |
| 19:44:40 | <ddellacosta> | ph88: I see, in that case have you checked out IHP? https://ihp.digitallyinduced.com/ |
| 19:45:02 | <ddellacosta> | I don't know enough about that or symfony to compare, but sounds more like what you're looking for |
| 19:46:53 | <ddellacosta> | also fwiw, since I was poking at it already, there's a number of other examples of servant apps here: https://github.com/haskell-servant/servant/blob/master/doc/examples.md, with some more cookie examples like https://github.com/FlogFr/FlashCard/blob/master/src/Auth.hs |
| 19:47:51 | × | billchenchina quits (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Ping timeout: 240 seconds) |
| 19:48:34 | → | Pickchea joins (~private@user/pickchea) |
| 19:49:47 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:50:00 | <ph88> | ddellacosta, thanks ! |
| 19:51:02 | <ddellacosta> | ph88: sure thing, I hope you find what you're looking for |
| 19:51:07 | → | kimiamania46 joins (~b4f4a2ab@user/kimiamania) |
| 19:52:46 | <ddellacosta> | ph88: oh and I would be remiss to not mention yesod, which is older but more mature and similarly full featured: https://www.yesodweb.com/ |
| 19:59:27 | × | Square quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 20:01:03 | × | Batzy quits (~quassel@user/batzy) (Quit: No Ping reply in 180 seconds.) |
| 20:02:15 | <ph88> | it seems i should either use yesod or ihp |
| 20:02:30 | → | Batzy joins (~quassel@user/batzy) |
| 20:06:21 | <monochrom> | yesod is s/batteries/kitchen sink/ |
| 20:06:54 | × | Inst quits (~Inst@120.244.192.250) (Ping timeout: 255 seconds) |
| 20:08:11 | × | CiaoSen quits (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 252 seconds) |
| 20:08:54 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 20:10:50 | → | Ellenor joins (~Ellenor@callbox.trd.is) |
| 20:11:54 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:14:07 | × | delyan_ quits (sid523379@id-523379.hampstead.irccloud.com) (Server closed connection) |
| 20:14:24 | → | delyan_ joins (sid523379@id-523379.hampstead.irccloud.com) |
| 20:15:56 | × | myxos quits (~myxos@cpe-65-28-251-121.cinci.res.rr.com) (Server closed connection) |
| 20:16:39 | → | myxos joins (~myxos@cpe-65-28-251-121.cinci.res.rr.com) |
| 20:20:19 | × | haasn quits (sid579015@id-579015.hampstead.irccloud.com) (Server closed connection) |
| 20:20:29 | → | haasn joins (sid579015@id-579015.hampstead.irccloud.com) |
| 20:22:51 | × | hiredman quits (~hiredman@frontier1.downey.family) (Server closed connection) |
| 20:23:02 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 20:28:31 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 20:32:59 | Ellenor | is now known as MelanieMalik |
| 20:34:11 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 20:50:50 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 20:55:35 | × | sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 20:56:00 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 20:58:53 | <Unicorn_Princess> | when haddock documenting records, fourmolu keeps changing -- | to -- ^ and moving them, so the comment comes after, instead of before, the record. how can i get it to not do that? none of the options in https://fourmolu.github.io/config/ seem to be what i want |
| 20:59:03 | × | sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 20:59:22 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 21:01:49 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 21:04:25 | <monochrom> | Fork again? fourmolu is already a fork from ormolu just to customize spacing. |
| 21:09:04 | <yushyin> | 'We encourage any contributions which add further flexibility.' i guess this means, PRs welcome? :) |
| 21:17:56 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 21:20:48 | × | ania123 quits (~ania123@wl-pool2-ont-004.uni-muenster.de) (Quit: Client closed) |
| 21:20:50 | × | Katarushisu1 quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 21:22:28 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 260 seconds) |
| 21:23:25 | → | Katarushisu1 joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 21:24:53 | → | rye|53 joins (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) |
| 21:24:58 | <monochrom> | To be sure, fork-then-PR is still nicer than just fork. :) |
| 21:25:19 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 21:25:50 | → | rye|5376 joins (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) |
| 21:25:52 | × | rye|5376 quits (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) (Client Quit) |
| 21:31:22 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 21:31:38 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 21:33:07 | <EvanR> | in the untyped lambda calculus, the question of whether some term has a beta normal form is undecidable. When that LC is equipped with a simple type system + intersection types but not an omega type, then a term can be typed if and only if it is strongly normalizing. Which means type inference in that case is undecidable |
| 21:33:46 | <EvanR> | in the relevant subset of haskell, type inference is decidable. But haskell doesn't have the intersection types. |
| 21:34:34 | × | rye|53 quits (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) (Quit: Connection closed) |
| 21:34:51 | <EvanR> | weird! |
| 21:35:43 | <monochrom> | With just a simple type system, type inference is decidable too. |
| 21:37:14 | <monochrom> | I think simple type system + fix also has decidable type inference. |
| 21:38:03 | <monochrom> | Haskell minus type classes (or SML) is when you have polymorphic type system + fix, and type inference is still decidable. |
| 21:38:09 | <EvanR> | https://i.imgur.com/40ulrg8.png (simply type system + intersection - omega not shown, but M:? in that case is no) |
| 21:38:48 | <monochrom> | Then again last time we discussed this, we reckoned that it is only a thin line between simply-typed and polymorphic. |
| 21:39:17 | <EvanR> | my confusion on that was cleared up by this paper which makes a distinction between curry style and church style systems |
| 21:40:09 | <monochrom> | Oh, that. |
| 21:40:18 | <EvanR> | but anyway... the stated reasoning for simple + intersection - omega having undecidable type inference is because that would be equivalent to determining if an arbitrary term has a normal form |
| 21:40:21 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 21:40:34 | <EvanR> | because of a theorem not proven here |
| 21:40:53 | <EvanR> | how does simple by itself avoid this fate, and get decidable type inference |
| 21:40:55 | × | V quits (~v@ircpuzzles/2022/april/winner/V) (Server closed connection) |
| 21:41:14 | → | V joins (~v@ircpuzzles/2022/april/winner/V) |
| 21:41:44 | <int-e> | It's also decidable whether a term in the simply typed lambda calculus with fix has a normal form. "On the lambda Y calculus", R. Statman, Proc. 17th IEEE Symposium on Logic in Computer Science, 2002. |
| 21:42:10 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 21:42:42 | <EvanR> | STLC which usually has the type signature on the lambda variable right |
| 21:42:57 | <EvanR> | (what barendregt calls church style) |
| 21:43:05 | <monochrom> | I forgot which one is curry or church, but when answering beginner questions in #haskell, it is more useful to take the stance of "if your code doesn't type-check then we need not discuss its 'meaning' and consequent crackpot ideas". :) |
| 21:43:38 | <int-e> | Hmm, it doesn't really matter whether it's Church style or Curry style... that's just syntax. |
| 21:44:27 | <EvanR> | in curry style, you can write whatever (unannotated) lambda term you want and it's fine. Whether anyone can find a type in some type system is a separate problem, and it's a big difference |
| 21:44:52 | <monochrom> | But I am OK with mature, learned discussions of terms that fail a certain type system because the participants are not crackpots. :) |
| 21:44:55 | <EvanR> | and you can view haskell this way if you want |
| 21:45:23 | <Lycurgus> | 'other crackpot ideas' refers to 'meaning'? |
| 21:46:52 | <Lycurgus> | (understood to be a jest, just not how broad) |
| 21:46:55 | <int-e> | EvanR: But it doesn't matter for the simply typed calculus, even if you add `fix`. |
| 21:47:32 | <EvanR> | ... right, hence my question |
| 21:47:55 | <monochrom> | Doesn't the omega type make sense only in the context of intersection types? |
| 21:48:07 | <EvanR> | the premise is you don't have omega so it doesn't matter |
| 21:48:15 | <monochrom> | Its sole purpose being to complete the type-level monoid. |
| 21:48:21 | <int-e> | EvanR: Yeah but the answer is that there are two styles and it doesn't really matter which one you use. (And indeed I can't remember which one is which either.) |
| 21:48:43 | <monochrom> | And I apologize for bringing up fix to muddle the issues. >:) |
| 21:48:46 | <EvanR> | it doesn't, you can write haskell with no type annotations |
| 21:48:52 | <EvanR> | somehow |
| 21:49:13 | <monochrom> | Well let's say SML instead of Haskell. Type classes muddle the issues, too. |
| 21:49:21 | <int-e> | As long as you stay in the mildly polymorphic Hindley Milner fragment... sure. |
| 21:49:54 | → | nate3 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 21:50:17 | <int-e> | (And a bit of type classes doesn't hurt either. But it's not unconditional, as witnessed by rhe existence of UndecidableInstances) |
| 21:51:00 | <EvanR> | on this hand, intersection (no omega) typability corresponds to normalization which is undecidable (in curry style!). On the other hand, haskell is decidably typable (ignoring type classes I guess) |
| 21:51:13 | <EvanR> | (also curry style) |
| 21:51:28 | → | arahael joins (~arahael@21.127.96.58.static.exetel.com.au) |
| 21:51:29 | monochrom | 's joke cube: Copenhagen vs multiple-world, Curry vs Church, big endian vs little endian. >:) |
| 21:51:32 | <EvanR> | so where is the secret sauce disconnect |
| 21:52:03 | × | ddb quits (ddb@tilde.club) (Server closed connection) |
| 21:52:22 | → | ddb joins (ddb@tilde.club) |
| 21:52:27 | <monochrom> | But Haskell lacks intersection types. |
| 21:52:40 | <int-e> | EvanR: The question is what you mean by "Haskell", because that usually comes with many type system extensions that people use casually. |
| 21:52:41 | <EvanR> | yes |
| 21:53:01 | <EvanR> | obviously ignoring the haskell stuff that defeats type inference |
| 21:53:07 | <int-e> | Many of which make type inference undecidable. |
| 21:53:12 | <EvanR> | or none of what i said makes sense |
| 21:53:37 | <int-e> | Sorry, as usual I don't know where this started. |
| 21:54:02 | <monochrom> | The lambda cube. |
| 21:54:16 | <monochrom> | Or maybe some lambda cube? |
| 21:54:29 | <EvanR> | it's funny because this system isn't on the cube |
| 21:54:36 | <Unicorn_Princess> | nvm fixed it |
| 21:54:38 | <EvanR> | despite having this normalizing property |
| 21:54:52 | × | yahb2 quits (~yahb2@2a01:4f8:c0c:5c7b::2) (Server closed connection) |
| 21:55:07 | × | nate3 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 21:55:14 | → | yahb2 joins (~yahb2@2a01:4f8:c0c:5c7b::2) |
| 21:55:14 | ChanServ | sets mode +v yahb2 |
| 21:55:31 | <EvanR> | anyway I guess my confusion is well-founded because a typability <=> normalizing property makes no sense in haskell because recursion |
| 21:55:38 | <EvanR> | my confusiong isn't well-founded* |
| 21:55:42 | <Unicorn_Princess> | (turns out -- |-style haddock on records is incompatible with leading comma style. setting it to trailing switched the haddock to --|-style automatically: https://fourmolu.github.io/config/comma-style/) |
| 21:56:09 | <monochrom> | I confess that I did not study these normalizability and computability questions at all. Except ad-hoc-ly for the few systems I came across. |
| 21:56:18 | <Unicorn_Princess> | (some github issues mentioned it, i think there's a reason it's not compatible, but here my investigation will cease) |
| 21:57:21 | <geekosaur> | sounds like the sort of thing haddock would have opinions about |
| 21:57:45 | <geekosaur> | -- | foo \n , foo :: X |
| 21:58:06 | <geekosaur> | haddock probably sees the comma as separating the comment from the field |
| 21:58:54 | <monochrom> | Yeah I think "-- |doc for the next thing" cannot make sense until after comma ends the previous thing. |
| 21:59:31 | × | mht-wtf quits (~mht@2a03:b0c0:3:e0::1e2:c001) (Server closed connection) |
| 21:59:44 | → | mht-wtf joins (~mht@mht.wtf) |
| 21:59:44 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 21:59:48 | <monochrom> | Then again in an ideal world comma neither ends or begins anything, it's just syntax. |
| 21:59:48 | <int-e> | EvanR: Hmm that interesection logic claim isn't too useful anyway, because often we're not interested in the halting problem (program halts on a particular input) but in the universal halting problem instead. And I rather suspect that the proof works by extracting (potentially highly complicated) types from an actual reduction to normal form. |
| 22:00:06 | × | Jackneill quits (~Jackneill@20014C4E1E058A00ABC7937222D6C543.dsl.pool.telekom.hu) (Ping timeout: 258 seconds) |
| 22:00:40 | <EvanR> | it goes both ways, so seems kind of interesting |
| 22:01:19 | <int-e> | Oh there are plenty of interesting things that aren't very useful :-) |
| 22:01:33 | <monochrom> | :( |
| 22:01:40 | <EvanR> | let me see if I can put it in a form that is obviously confusing, and also obviously wrong to shrink the problem |
| 22:01:55 | <Unicorn_Princess> | that makes sense, i am happy with this comma-explanation, thanks. i know i said investigation ceased, but it was gonna bug me |
| 22:02:01 | × | arahael quits (~arahael@21.127.96.58.static.exetel.com.au) (Ping timeout: 246 seconds) |
| 22:02:07 | <monochrom> | Wait, you can't have both confusing and obviously wrong. |
| 22:02:28 | <Unicorn_Princess> | perhaps it is only the wrongness that is obvious |
| 22:02:40 | <int-e> | monochrom: Heh. "this is obviously wrong but I don't know why" |
| 22:02:46 | <EvanR> | it will be confusing to me and obviously wrong to you! |
| 22:02:56 | <monochrom> | OK I can buy that. |
| 22:03:36 | <EvanR> | intersection no omega: has a type <=> strongly normalizing, undecidable. simple types: has a type <=> strongly normalizing, decidable |
| 22:03:48 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 22:04:37 | <monochrom> | OK that's obviously confusing but I think it's also obviously correct? :) |
| 22:04:59 | <EvanR> | the justification for undecidable is the equivalence to checking for a normal form, which is true in both cases |
| 22:05:18 | <EvanR> | but this justification doesn't work for simple types because it's decidable after all |
| 22:06:24 | <EvanR> | so why would the justification ever work |
| 22:06:51 | <int-e> | EvanR: where does "has a type <=> strongly normalizing" come from? |
| 22:06:59 | <EvanR> | for intersection? |
| 22:07:07 | <int-e> | No for simple types, where it's demonstrably false. |
| 22:07:16 | × | urdh quits (~urdh@user/urdh) (Server closed connection) |
| 22:07:27 | <int-e> | That, or vacuously true. |
| 22:07:28 | <EvanR> | is it? then that was the "obviously wrong" part |
| 22:07:39 | <int-e> | s/vacuously/trivially/ |
| 22:07:40 | → | urdh joins (~urdh@user/urdh) |
| 22:07:46 | <EvanR> | is it trivially true or trivially false? |
| 22:08:16 | <int-e> | It depends on whether you start with terms of the simply typed lambda calculus, which all have a type and are all strongly normalizing |
| 22:08:24 | <monochrom> | TIme to also introduce "obviously paradoxical" >:) |
| 22:08:57 | <EvanR> | the table I showed shows that type inference for STLC (curry style) is decidable, but I thought the strongly normalizing property carried over, maybe not |
| 22:09:11 | <EvanR> | could be the key |
| 22:09:13 | <int-e> | Or whether you consider terms of the untyped lambda calculus, which can be strongly normalizing (undecidable) and/or typeable in the simply typed lambda calculus (which is decidable), and those two notions aren't the same. |
| 22:09:54 | <EvanR> | i thought the result was if it could be ascribed a simply typed type it's normalizing to something |
| 22:09:54 | <int-e> | You only have an implication (typeable implies strongly normalizing). |
| 22:10:10 | <EvanR> | so you're saying it's one way not both ways |
| 22:10:23 | <geekosaur> | are we talking about the same kind of normalizing? |
| 22:10:24 | <int-e> | you can write down a normal form \x. x x which isn't typeable. |
| 22:10:46 | <EvanR> | ok! |
| 22:11:05 | × | xigua quits (~xigua@user/xigua) (Remote host closed the connection) |
| 22:11:09 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 22:11:23 | <int-e> | (aside, how does that type with intersection types?) |
| 22:11:40 | → | xigua joins (~xigua@user/xigua) |
| 22:11:43 | <EvanR> | it has a type, I can tell you once I get an intersection symbol off unicode site |
| 22:11:43 | int-e | doesn't know how intersection types work. |
| 22:12:07 | <EvanR> | but, x has type tau -> sigma, and also type tau |
| 22:12:12 | <EvanR> | intersect those |
| 22:12:19 | <tomsmeding> | EvanR: https://tomsmeding.com/unicode#intersec |
| 22:12:24 | <monochrom> | ∩ |
| 22:12:36 | <tomsmeding> | or wait until monochrom turns up |
| 22:13:07 | <EvanR> | \x . x x : ((a -> b) ∩ a) -> b |
| 22:14:14 | <EvanR> | so x is a hyperfunction or something xD |
| 22:14:15 | <int-e> | Oh so you kind of defer unification (including its potential to fail). |
| 22:15:07 | <EvanR> | unification? type inference is undecidable as we saw earlier |
| 22:16:18 | <EvanR> | the normal typing rule for function application combined with a rule that says x has type a and type a -> b lets you prove that typing |
| 22:16:19 | <int-e> | I mean, where you have (a -> b) ∩ a, the simply typed lambda calculus would unify a -> b and a. |
| 22:16:34 | × | gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Server closed connection) |
| 22:16:51 | <tomsmeding> | EvanR: how do I construct a value of type (a -> b) ∩ a |
| 22:16:55 | <EvanR> | hmm... I don't know about that. Maybe you're talking about HM |
| 22:17:02 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 22:17:02 | <int-e> | besides, you can ask about unifiers even when that problem isn't decidable. |
| 22:17:16 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:17:42 | <EvanR> | a type that is both a and a -> b, well that's a ∩ (a -> b) |
| 22:17:46 | <EvanR> | tomsmeding, in haskell? |
| 22:18:05 | <tomsmeding> | well haskell doesn't have intersection types, but haskell syntax might be nice for understandability :p |
| 22:18:20 | <EvanR> | cue the hyperfunction guru for an example |
| 22:18:25 | <tomsmeding> | like, what is the typing rule that introduces ∩ |
| 22:18:42 | <EvanR> | if x : t1 and x : t2, then you can have x : t1 ∩ t2 |
| 22:18:51 | <tomsmeding> | I get how the typing rule for application looks into the arguments of ∩ to see if there's a function type in there somewhere |
| 22:18:58 | <tomsmeding> | oh |
| 22:18:59 | <tomsmeding> | right |
| 22:19:12 | <tomsmeding> | ew |
| 22:19:15 | <EvanR> | lol |
| 22:19:33 | <EvanR> | apparently this stuff is all the rage in typescript |
| 22:19:42 | tomsmeding | scurries back to more normal type systems |
| 22:20:03 | <monochrom> | It is possible that you can justify that a second copy of (\x. x x) has type (a -> b) ∩ a. |
| 22:20:47 | <tomsmeding> | yeah like how would that typing derivation even look |
| 22:20:50 | <ski> | $ ocaml -rectypes |
| 22:20:56 | <ski> | # fun x -> x x;; |
| 22:21:01 | <ski> | - : ('a -> 'b as 'a) -> 'b = <fun> |
| 22:21:14 | <geekosaur> | we're talking about lambda calculus, no? I thought little things like actually producing values weren't relevant? |
| 22:21:15 | <monochrom> | Nevermind, non-normalizing terms cannot be typed. (\x. x x)(\x. x x) is supposed to be illegal. |
| 22:21:22 | <EvanR> | tomsmeding, exercise for the reader, or check this paper out xD |
| 22:21:27 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:22:13 | <monochrom> | OK, it is possible that no term has type (a -> b) ∩ a. This doesn't stop (\x. x x) from wanting such a parameter. |
| 22:22:32 | <tomsmeding> | right |
| 22:22:38 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
| 22:22:43 | <EvanR> | tomsmeding, but when checking the inside of the lambda... you have x : (a -> b) ∩ a in context, then you can use another rule which says you get x : a -> b and x : a |
| 22:22:59 | <int-e> | (\x. x x) (\x. x) would be legal though. So you'll derive (\x. x) : (a -> b) ∩ a for some a and b. a = b = c -> c works, right? |
| 22:23:06 | <monochrom> | Humans suffer the same problem too. "I want fast and cheap and good" always happens. It is never fulfilled. :) |
| 22:23:39 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 22:24:15 | <tomsmeding> | EvanR: is that about type-checking (\x. x x) : ((a -> b) ∩ a) -> b ? I get that :p |
| 22:24:21 | <tomsmeding> | it's how to produce anything with type (a -> b) ∩ a |
| 22:24:30 | <int-e> | tomsmeding: see what I just wrote? |
| 22:24:50 | <tomsmeding> | oh heh |
| 22:24:52 | <tomsmeding> | yes |
| 22:24:52 | <int-e> | it's not *that* type but it's an instance of that type. |
| 22:25:28 | <tomsmeding> | "a function that you can apply to itself and get something (a 'b')" |
| 22:25:37 | <tomsmeding> | an example of which is... id |
| 22:25:46 | <tomsmeding> | this was not very enlightening |
| 22:25:48 | <EvanR> | a couple days ago someone was doing hyperfunctions in here which I think is this |
| 22:25:48 | <int-e> | :t const const |
| 22:25:49 | <lambdabot> | b1 -> a -> b2 -> a |
| 22:25:51 | <EvanR> | and a blog post to go with it |
| 22:25:58 | <EvanR> | because "they're super useful" |
| 22:26:21 | <EvanR> | https://doisinkidney.com/posts/2021-03-14-hyperfunctions.html |
| 22:26:39 | <EvanR> | shoot no, they reverse the arguments |
| 22:27:04 | <EvanR> | so a ∩ (b -> a) |
| 22:27:12 | × | yoyofreeman quits (~yoyofreem@176.97.76.178) (Remote host closed the connection) |
| 22:27:30 | <EvanR> | no |
| 22:27:44 | <int-e> | Sometimes people see a single use case that's important to them and a tool that they think would fit that use case, and suddenly that tool becomes "super useful". |
| 22:27:44 | <EvanR> | yes |
| 22:27:53 | → | yoyofreeman joins (~yoyofreem@176.97.76.178) |
| 22:27:54 | <EvanR> | also yes |
| 22:28:35 | <int-e> | (Been there, done that. It's an easy trap to fall into.) |
| 22:28:49 | <EvanR> | (a -> b) ∩ ((b -> a) -> b) |
| 22:28:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 22:29:34 | <monochrom> | Oh may I introduce you to the Giry monad, it's super useful... https://www.cs.utoronto.ca/~trebla/cpm.pdf >:) |
| 22:30:08 | <monochrom> | But generally, s/Sometimes/Always/ |
| 22:30:32 | <monochrom> | But we can do worse. |
| 22:30:48 | → | arahael joins (~arahael@21.127.96.58.static.exetel.com.au) |
| 22:31:09 | <exarkun> | typo in the citation, "probabaility" |
| 22:31:16 | <monochrom> | Just last night, someone asked about readability, and it soon turned out that clearly they just want other people to say yes to "exclusively only my favourite style is readable". |
| 22:31:22 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 22:32:07 | <tomsmeding> | okay I proved (? with some imagined typing rules that seem reasonable) that (\x. x x) : ∀a b. ((a -> b) -> b) ∩ (a -> b) |
| 22:32:32 | <monochrom> | exarkun: :( |
| 22:32:57 | <tomsmeding> | if you start with (a -> b) ∩ a and try to apply typing rules you're forced to refine the type to this |
| 22:33:18 | <EvanR> | oh you got forall now? xD |
| 22:33:36 | <EvanR> | that's a whole nother thing |
| 22:33:40 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
| 22:33:42 | <tomsmeding> | just wanna be explicit :p |
| 22:33:54 | <tomsmeding> | it's not like it doesn't mean the same thing if I remove the forall |
| 22:34:05 | <tomsmeding> | yes, triple negation, deal with it |
| 22:34:06 | <EvanR> | semantics! |
| 22:34:43 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
| 22:35:07 | <monochrom> | Fortunately negation is self-adjoint so triple negation is simplifiable to single negation. |
| 22:35:17 | <tomsmeding> | er no my proof is bonkers |
| 22:35:26 | <tomsmeding> | scratch that |
| 22:35:53 | <tomsmeding> | okay sorry my brain is not ready for this, I'm off to bed |
| 22:36:09 | <monochrom> | Calculus of Constructions is so much simpler. :) |
| 22:37:01 | <EvanR> | also if you're using the exact system barendregt says, you have this if x : t and t ≤ u, you can have x : u |
| 22:37:11 | <EvanR> | which might let you simplify something |
| 22:37:12 | <int-e> | EvanR: that post reminds me of this silly trick: https://paste.tomsmeding.com/VxiOKUN7 |
| 22:38:04 | <monochrom> | That was what I brought up last time. :) |
| 22:38:15 | <EvanR> | that looks like a ∩ (a -> b) if I ever seen one |
| 22:38:18 | <int-e> | Oh no, am I becoming monochrom? |
| 22:38:30 | <monochrom> | We are entangled! |
| 22:38:57 | → | accord joins (uid568320@id-568320.hampstead.irccloud.com) |
| 22:39:18 | <monochrom> | I would say it is the simpler a ≅ a -> b. |
| 22:39:40 | <EvanR> | yeah |
| 22:40:31 | <EvanR> | this system comes with a subtyping preorder which is probably where the real complexity comes in |
| 22:42:29 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 22:43:00 | <monochrom> | No, my experience with lattice theory is that having ≤ is implied by having ∩, so any complexity traces back to ∩ itself. |
| 22:44:35 | <monochrom> | For example, you can rephrase that rule as: if x : foo ∩ u, then x : u. |
| 22:44:38 | <EvanR> | well there's only 6 total typing rules and like 8 axioms of the preorder |
| 22:45:18 | <EvanR> | that's one of the typing rules |
| 22:50:32 | <mauke> | real complexity is an oxymoron |
| 22:51:00 | <EvanR> | otoh real ∩ complex makes total sense! |
| 22:51:04 | <monochrom> | Why? |
| 22:51:10 | × | neceve quits (~neceve@user/neceve) (Remote host closed the connection) |
| 22:53:04 | <monochrom> | In Haskell land, real ∩ complex is called Floating. >:) |
| 22:54:11 | <EvanR> | yes somehow corporate languages which have intersection all over their brochures seem to be talking about (ad-hoc) polymorphism, I wonder if this is simply an instance of record subtypes |
| 22:54:15 | <monochrom> | So I'm thinking that GADTs may be able to emulate intersection types. |
| 22:54:20 | → | CiaoSen joins (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
| 22:55:23 | <monochrom> | Or closed type families can. |
| 22:56:21 | <int-e> | monochrom: Have you seen this before? slide 5 from https://latticehacks.cr.yp.to/ ...presenter said "this is not a lattice", and apologized to the live translation team |
| 22:57:12 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 22:57:31 | <int-e> | (of course it's about a different type of lattice) |
| 22:57:35 | <monochrom> | Eh I recongize the name Natalie Wolchover from Quanta Magazine. |
| 22:58:16 | <monochrom> | Haha lettuce. |
| 22:59:05 | <mauke> | I knew exactly what I was going to find on that slide :-D |
| 22:59:25 | × | arahael quits (~arahael@21.127.96.58.static.exetel.com.au) (Ping timeout: 246 seconds) |
| 23:00:38 | <EvanR> | too bad we can't base crypto on all these undecidable problems |
| 23:00:40 | × | alguem quits (~alguem@45.163.64.23) (Remote host closed the connection) |
| 23:01:57 | <EvanR> | it would be guaranteed unbreakable |
| 23:02:33 | <int-e> | EvanR: https://xkcd.com/538/ |
| 23:02:39 | <EvanR> | I send you a lambda term, if it's got a normal form that's a 1, otherwise 0 |
| 23:07:08 | → | arahael_ joins (~arahael@21.127.96.58.static.exetel.com.au) |
| 23:10:49 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 23:12:28 | × | megaTherion quits (~therion@unix.io) (Server closed connection) |
| 23:12:38 | → | megaTherion joins (~therion@unix.io) |
| 23:13:42 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 23:17:05 | → | masterbuilder joins (~master@user/masterbuilder) |
| 23:18:17 | <ph88> | i saw in the docs that State takes a single parameter, why do i get this error? Expecting one more argument to ‘State QueryPart’ |
| 23:18:28 | → | Guest45 joins (~Guest45@pub082136073213.dh-hfc.datazug.ch) |
| 23:19:04 | <EvanR> | :k State |
| 23:19:05 | <lambdabot> | * -> * -> * |
| 23:19:12 | <EvanR> | @unmtl State |
| 23:19:12 | <lambdabot> | err: `State' is not applied to enough arguments, giving `/\A B. A -> (B, A)' |
| 23:19:24 | <ph88> | https://hackage.haskell.org/package/transformers-0.6.1.1/docs/Control-Monad-Trans-State-Lazy.html#t:State |
| 23:19:40 | <EvanR> | StateT takes 3 parameters |
| 23:19:42 | <ph88> | only see `s` as argument |
| 23:19:53 | <c_wraith> | ph88: that's been eta-contracted. For good reasons related to limitations of type aliases |
| 23:20:06 | × | Guest45 quits (~Guest45@pub082136073213.dh-hfc.datazug.ch) (Client Quit) |
| 23:20:20 | <ph88> | type State s a = StateT s Identity a why didn't they write it like this? it should be the same and much easier to understand |
| 23:20:29 | <EvanR> | wouldn't work, right |
| 23:20:33 | <EvanR> | unfortunately |
| 23:20:36 | × | masterbuilder quits (~master@user/masterbuilder) (Quit: Leaving) |
| 23:20:50 | <c_wraith> | ph88: because it would make it illegal to write State s anywhere |
| 23:21:00 | × | arahael_ quits (~arahael@21.127.96.58.static.exetel.com.au) (Quit: I'm off! Laters!) |
| 23:21:03 | <c_wraith> | ph88: because type aliases must always be fully applied |
| 23:21:36 | <ph88> | hmmm interesting |
| 23:21:40 | <ph88> | thanks |
| 23:23:16 | <EvanR> | that you can get the same effect by defining more type aliases seems suspicious |
| 23:23:39 | <EvanR> | why can't they be auto curried |
| 23:23:50 | <c_wraith> | I guess that limitation exists because otherwise they'd be type lambdas |
| 23:24:19 | <c_wraith> | and type lambdas break a lot of stuff |
| 23:24:35 | <ph88> | how can i write this function? intersperseS :: forall s a. State s a -> [State s a] -> [State s a] |
| 23:24:57 | <monochrom> | could make type inference too difficult. |
| 23:25:07 | <EvanR> | that's just intersperse specialized to State s a right |
| 23:25:11 | <ph88> | yes |
| 23:25:15 | <geekosaur> | looks like it to me |
| 23:25:22 | <EvanR> | did you want State s a -> [State s a] -> State s [a] or something |
| 23:25:29 | <ph88> | no |
| 23:25:39 | <EvanR> | ok so intersperse should just work |
| 23:25:42 | <ph88> | oh ok |
| 23:25:44 | <ph88> | thank you |
| 23:25:48 | <geekosaur> | so what goes wrong if you just use intersperse? |
| 23:25:52 | <geekosaur> | oh, slow me |
| 23:26:10 | <ski> | % :i ReadS |
| 23:26:10 | <yahb2> | type ReadS :: * -> * ; type ReadS a = String -> [(a, String)] ; -- Defined in ‘Text.ParserCombinators.ReadP’ |
| 23:26:18 | <ski> | % type Const c a = c |
| 23:26:18 | <yahb2> | <no output> |
| 23:26:26 | <ski> | % :k Const Int ReadS |
| 23:26:26 | <yahb2> | <interactive>:1:1: error: ; The type synonym ‘ReadS’ should have 1 argument, but has been given none |
| 23:26:29 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
| 23:26:32 | <ski> | % :set -XLiberalTypeSynonyms |
| 23:26:32 | <yahb2> | <no output> |
| 23:26:35 | <ski> | % :k Const Int ReadS |
| 23:26:35 | <yahb2> | Const Int ReadS :: * |
| 23:26:45 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
| 23:27:30 | <ski> | (apropos "type aliases must always be fully applied") |
| 23:27:40 | → | masterbuilder joins (~quassel@user/masterbuilder) |
| 23:28:46 | → | andrewboltachev joins (~andrey@178.141.201.173) |
| 23:28:56 | × | CiaoSen quits (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 252 seconds) |
| 23:35:28 | <EvanR> | does that extension have any downside? |
| 23:36:01 | × | Buggys quits (Buggys@shelltalk.net) (Ping timeout: 255 seconds) |
| 23:36:31 | × | chomwitt quits (~chomwitt@2a02:587:7a12:2d00:1ac0:4dff:fedb:a3f1) (Ping timeout: 264 seconds) |
| 23:38:06 | <ski> | it delays checking full application of type synonyms until after synonym expansion, so to speak |
| 23:38:43 | × | gawen quits (~gawen@user/gawen) (Server closed connection) |
| 23:39:42 | <ski> | (in the above example, `a' is unused in expansion of `Const Int ReadS', and so checking full application of `ReadS' amounts to checking zero things. instead of `type Const c a = c', i could have used `type Foo f = f Int', and then `Foo ReadS' would have been fine as well, since `f' is fully applied (at all occurances)) |
| 23:39:48 | → | gawen joins (~gawen@user/gawen) |
| 23:39:52 | × | sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection) |
| 23:43:59 | <EvanR> | is there anyway reason why that shouldn't be enabled by default |
| 23:44:06 | → | sefidel joins (~sefidel@user/sefidel) |
| 23:44:48 | → | harveypwca joins (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) |
| 23:45:54 | <ski> | i'm not sure. apart from being conservative |
| 23:46:20 | <ski> | type synonyms are kinda like macros. `LiberalTypeSynonyms' then allow higher-order "type macros" |
| 23:47:01 | → | Buggys joins (Buggys@Buggy.shelltalk.net) |
| 23:50:09 | × | target_i quits (~target_i@217.175.14.39) (Quit: leaving) |
| 23:54:12 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
All times are in UTC on 2023-11-11.