| 2024-09-04 00:10:26 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 00:12:35 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-20.web.vodafone.de) (Read error: Connection reset by peer) |
| 2024-09-04 00:15:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 00:18:38 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-04 00:19:55 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 264 seconds) |
| 2024-09-04 00:20:33 +0200 | Fooo | (~Square@user/square) |
| 2024-09-04 00:21:15 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 00:23:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: thanks a lot for the extensive explanation!! i'll be referring to this a lot |
| 2024-09-04 00:26:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 00:27:35 +0200 | <haskellbridge> | <magic_rb> Today during a course we were tasked to implement some very basic haskell functions, namely "equalFour" which takes 4 arguments and returns True if none of them equal and "factorial" which is self explanatory. "equalFour" can be done just be hardcoding the expression or by using a foldl to implement "equalN". And i wondered if the general fold based version would be optimized away or if it even could be... |
| 2024-09-04 00:27:40 +0200 | <haskellbridge> | ... reasonably optimized away |
| 2024-09-04 00:30:19 +0200 | guygastineau | (~guygastin@137.184.131.156) (Quit: ZNC - https://znc.in) |
| 2024-09-04 00:30:39 +0200 | RMSBach | (~guygastin@137.184.131.156) |
| 2024-09-04 00:30:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 00:37:22 +0200 | troydm | (~troydm@user/troydm) |
| 2024-09-04 00:41:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 00:43:26 +0200 | <Leary> | Bowuigi, thirdofmay18081814goya: System F /can/ represent both data and codata as the least and greatest fixpoints of functors respectively. You just can't treat one like the other without paying unreasonable penalties. |
| 2024-09-04 00:43:33 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb806d1b8dd9c0ab8f32.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2024-09-04 00:46:23 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-04 00:46:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-04 00:47:00 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-09-04 00:48:50 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-04 00:50:22 +0200 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2024-09-04 00:51:37 +0200 | malte | (~malte@mal.tc) |
| 2024-09-04 00:51:49 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-04 00:57:03 +0200 | misterfish | (~misterfis@84.53.85.146) |
| 2024-09-04 00:57:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 01:02:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 01:06:35 +0200 | <Axman6> | magic_rb: generally, recursive functions don't get optimised away easily. the compiler needs to have some way to stop inlining, but when lists can be infinite its hard to know when. it might be possible if you explicitly used build/foldr fusion though. |
| 2024-09-04 01:07:46 +0200 | <davean> | Axman6: I mean an obvious counter example is tail recursion. |
| 2024-09-04 01:08:21 +0200 | <davean> | Certain recursive cases are trivially optimized away |
| 2024-09-04 01:09:29 +0200 | <Axman6> | sure, but i'm not sure what mechanism would turn f a b c d = foldr g z [a,b,c,d] into the expansion of foldr at compile time. |
| 2024-09-04 01:09:48 +0200 | vglfr | (~vglfr@2601:14d:4e01:1370:aa26:2342:9c12:cd31) (Ping timeout: 276 seconds) |
| 2024-09-04 01:10:27 +0200 | vglfr | (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) |
| 2024-09-04 01:11:03 +0200 | <davean> | well it knows for sure the list is finite in that case. |
| 2024-09-04 01:11:06 +0200 | <c_wraith> | I'm pretty sure GHC doesn't have a pass that does that, but it certainly *could* treat fixed-length list literals specially for optimization purposes. I'm just not sure it'd be worth the implementation cost. |
| 2024-09-04 01:12:08 +0200 | <davean> | One could even add a RULE for that if one wanted it to work right now for sure. |
| 2024-09-04 01:12:28 +0200 | <c_wraith> | It's possible a foldr/build would do something useful there, though, as that would erase the recursion entirely and GHC would just see it as a few function applications. |
| 2024-09-04 01:12:29 +0200 | <davean> | its fixed enough I'd have to look at what the optimizer did, it can handle some cases like that from pure inlining. |
| 2024-09-04 01:12:39 +0200 | <davean> | c_wraith: right |
| 2024-09-04 01:13:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 01:13:38 +0200 | <davean> | This is also the sort of thing that tends not to be stable across GHC versions |
| 2024-09-04 01:13:49 +0200 | <Axman6> | if the literal {a,b,c,d} turns into build (\(*) z -> a * b * c * d * z) then it might get optimised away |
| 2024-09-04 01:14:13 +0200 | <c_wraith> | do literals get compiled like that? |
| 2024-09-04 01:14:43 +0200 | <Axman6> | not sure |
| 2024-09-04 01:14:47 +0200 | <monochrom> | "only one way to find out" :) |
| 2024-09-04 01:14:55 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 2024-09-04 01:15:18 +0200 | <Axman6> | {} -> [] |
| 2024-09-04 01:15:52 +0200 | <davean> | So I will repeat that IME this sort of thing is very unstable across GHC versions |
| 2024-09-04 01:17:04 +0200 | <monochrom> | That's fair. |
| 2024-09-04 01:18:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 01:18:50 +0200 | <davean> | Optimizations are great, but they're there to clean up your average code and so should target the best average improvements. Thus they're prone to tunning, and changes. Core peroformance critical code is best done directly. |
| 2024-09-04 01:19:31 +0200 | <c_wraith> | My general philosophy is to write the code I want to run. Not some other code that I hope the compiler magically fixes for me. :) |
| 2024-09-04 01:19:49 +0200 | oo_miguel | (~Thunderbi@78.10.207.45) (Ping timeout: 248 seconds) |
| 2024-09-04 01:19:56 +0200 | jespada | (~jespada@r190-64-133-178.su-static.adinet.com.uy) |
| 2024-09-04 01:20:04 +0200 | <davean> | c_wraith: right, for at least core stuff. I'm happy when I have a lot of code saying "it'll do a decent job on cleaning up this code that runs only a few times and isn't core" |
| 2024-09-04 01:20:12 +0200 | <davean> | It should never be terrible! |
| 2024-09-04 01:20:26 +0200 | <c_wraith> | I mean, in that case that's the code I want to run. Something simple where performance isn't critical |
| 2024-09-04 01:20:31 +0200 | <davean> | but if someone wants to abstractly think about some business logic, I'm happy to expect it to be generally improved |
| 2024-09-04 01:21:00 +0200 | <davean> | Just I better not care about any specific improvements |
| 2024-09-04 01:24:52 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 01:27:21 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-04 01:29:07 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb5469ca77b0637d5192.dip0.t-ipconnect.de) |
| 2024-09-04 01:29:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 01:30:20 +0200 | bliminse | (~bliminse@user/bliminse) (Ping timeout: 252 seconds) |
| 2024-09-04 01:34:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 01:36:13 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 2024-09-04 01:42:25 +0200 | bliminse | (~bliminse@user/bliminse) |
| 2024-09-04 01:45:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 01:50:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-04 01:51:47 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 2024-09-04 01:54:30 +0200 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 2024-09-04 01:58:11 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2024-09-04 02:00:46 +0200 | jespada | (~jespada@r190-64-133-178.su-static.adinet.com.uy) (Ping timeout: 252 seconds) |
| 2024-09-04 02:00:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 02:02:19 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-09-04 02:05:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 02:05:42 +0200 | xff0x | (~xff0x@2405:6580:b080:900:3618:2400:ae18:e1a3) (Ping timeout: 246 seconds) |
| 2024-09-04 02:08:05 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb5469ca77b0637d5192.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2024-09-04 02:10:49 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-09-04 02:10:53 +0200 | Square2 | (~Square4@user/square) |
| 2024-09-04 02:14:19 +0200 | Fooo | (~Square@user/square) (Ping timeout: 252 seconds) |
| 2024-09-04 02:16:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 02:21:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-04 02:27:09 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 02:28:40 +0200 | <haskellbridge> | <Bowuigi> Leary what about the "infinite-ness" of codata tho? You can't fold/traverse over infinite structures without taking infinite time on normal order (thus, breaking Church-Rosser and disproving totality) |
| 2024-09-04 02:29:30 +0200 | <haskellbridge> | <Bowuigi> If the only valid operations are pretty much "zip" (over codata) and take (to data) variants it makes sense though |
| 2024-09-04 02:31:27 +0200 | <Inst> | are the or patterns from GHC 9.12 actually useful? |
| 2024-09-04 02:31:48 +0200 | <Inst> | i'm sort of disappointed you can't condense multiple pattern matches into the same term, though |
| 2024-09-04 02:32:06 +0200 | <Inst> | like, say, Foo pat; Bar pat = pat * 3 |
| 2024-09-04 02:32:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 02:35:14 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-09-04 02:37:25 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 02:40:44 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) |
| 2024-09-04 02:41:23 +0200 | <Leary> | Bowuigi: GFP_F := forall r. (forall x. (x -> F x) -> x -> r) -> r; ana_F := /\a. \coalg:a -> F a. \seed:a. /\r. \expair:forall x. (x -> F x) -> x -> r. expair a coalg seed; out_F := \ff:GFP_F. ff (F GFP_F) /\a. \coalg:a -> F a. \seed:a. map_F a GFP_F (ana_F a coalg) (coalg seed) |
| 2024-09-04 02:42:28 +0200 | <Leary> | The infiniteness is in the semantics we ascribe, not in the program that actually runs. Of course that limits which operations we can support, but this is all the same whether in Haskell or System F. |
| 2024-09-04 02:42:32 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-09-04 02:45:07 +0200 | <Leary> | (in Haskell the limits are just softer, bottoming out at runtime rather than failing to type check) |
| 2024-09-04 02:48:03 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-04 02:48:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 02:48:47 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-04 02:50:59 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 02:53:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-04 02:57:25 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Quit: quit) |
| 2024-09-04 02:58:54 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 2024-09-04 02:59:09 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2024-09-04 03:01:41 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2024-09-04 03:04:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 03:08:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 03:18:29 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-09-04 03:19:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 03:24:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-04 03:30:32 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-04 03:35:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 03:40:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 03:41:36 +0200 | Batzy | (~quassel@user/batzy) (Ping timeout: 252 seconds) |
| 2024-09-04 03:49:05 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 03:51:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 03:56:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2024-09-04 04:05:33 +0200 | <haskellbridge> | <Bowuigi> I see, it works more like a generator |
| 2024-09-04 04:06:14 +0200 | <haskellbridge> | <Bowuigi> Also this means that you can get total anamorphisms (and above), which means more recursion schemes for my total lang! Thanks! |
| 2024-09-04 04:06:36 +0200 | <monochrom> | Python generators secretly dream to be codata. System F and Haskell have real codata. :) |
| 2024-09-04 04:07:08 +0200 | <haskellbridge> | <Bowuigi> Yeah, the magic of PL theory |
| 2024-09-04 04:07:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 04:08:13 +0200 | <haskellbridge> | <Bowuigi> And speaking about that, is it possible to efficiently run bulk combinators ala Kiselyov in "Lambda to SKI, semantically"? |
| 2024-09-04 04:08:15 +0200 | <monochrom> | In the next episode, I will talk about how OO secretly dreams to be codata with linearity, and Haskell has real codata with linearity. >:) |
| 2024-09-04 04:09:15 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds) |
| 2024-09-04 04:09:49 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) |
| 2024-09-04 04:10:46 +0200 | <haskellbridge> | <Bowuigi> https://crypto.stanford.edu/~blynn/lambda/kiselyov.html has an optimized compilation algorithm ("bulkOpt") and linear+logaritmic expansions. The structure of the combinators seems to hint at a way to run them as is, but I can't find it |
| 2024-09-04 04:11:54 +0200 | <haskellbridge> | <Bowuigi> If this is possible, then making a tiny and reasonably fast functional compiler is as well, which is fantastic |
| 2024-09-04 04:12:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 04:12:18 +0200 | <haskellbridge> | <Bowuigi> (As an alternative, the eta-optimized version is a good choice) |
| 2024-09-04 04:15:19 +0200 | zlqrvx | (~zlqrvx@user/zlqrvx) (Quit: %quit%) |
| 2024-09-04 04:15:40 +0200 | zlqrvx | (~zlqrvx@user/zlqrvx) |
| 2024-09-04 04:22:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 04:23:48 +0200 | random-jellyfish | (~random-je@user/random-jellyfish) (Quit: Client closed) |
| 2024-09-04 04:27:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 04:31:57 +0200 | codaraxis | (~codaraxis@user/codaraxis) (Ping timeout: 276 seconds) |
| 2024-09-04 04:38:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 04:43:33 +0200 | youthlic | (~Thunderbi@user/youthlic) |
| 2024-09-04 04:43:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 04:54:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 04:55:27 +0200 | td_ | (~td@i5387093B.versanet.de) (Ping timeout: 246 seconds) |
| 2024-09-04 04:57:31 +0200 | td_ | (~td@i5387092A.versanet.de) |
| 2024-09-04 04:59:33 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2024-09-04 05:02:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-04 05:14:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 05:19:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 05:25:33 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2024-09-04 05:28:39 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-09-04 05:29:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 05:31:51 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-04 05:34:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-04 05:38:35 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 05:39:57 +0200 | aforemny | (~aforemny@i59F516D7.versanet.de) |
| 2024-09-04 05:40:57 +0200 | aforemny_ | (~aforemny@i59F516FC.versanet.de) (Ping timeout: 246 seconds) |
| 2024-09-04 05:45:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 05:50:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 06:01:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 06:06:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 06:14:00 +0200 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) |
| 2024-09-04 06:17:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 06:21:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 06:22:41 +0200 | Fooo | (~Square@user/square) |
| 2024-09-04 06:25:34 +0200 | <haskellbridge> | <thirdofmay18081814goya> what guarantees termination in system f? |
| 2024-09-04 06:25:57 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 248 seconds) |
| 2024-09-04 06:27:45 +0200 | <Axman6> | ^C |
| 2024-09-04 06:32:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 06:36:42 +0200 | <Leary> | thirdofmay18081814goya: Strong normalisation. |
| 2024-09-04 06:37:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 06:48:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 06:50:49 +0200 | Fooo | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-09-04 06:53:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-04 06:56:15 +0200 | Pixi` | (~Pixi@user/pixi) (Quit: Leaving) |
| 2024-09-04 06:56:35 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-09-04 06:57:23 +0200 | <haskellbridge> | <thirdofmay18081814goya> ty! |
| 2024-09-04 06:59:01 +0200 | michalz | (~michalz@185.246.207.201) |
| 2024-09-04 07:11:10 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-04 07:15:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 07:15:39 +0200 | Pixi | (~Pixi@user/pixi) |
| 2024-09-04 07:17:07 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-04 07:20:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 07:22:18 +0200 | codaraxis | (~codaraxis@user/codaraxis) |
| 2024-09-04 07:24:00 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-04 07:30:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 07:36:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2024-09-04 07:38:41 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm, what extension of system F provides infinite recursion? |
| 2024-09-04 07:39:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> just inductive types right? |
| 2024-09-04 07:46:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 07:51:18 +0200 | <Leary> | thirdofmay18081814goya: The simplest way is to extend the expression langugae with a fixpoint operator `Y : forall a. (a -> a) -> a`. Infinite or negative-recursive types will also do it. Inductive types don't suffice---System F encodes these anyway. |
| 2024-09-04 07:51:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-04 07:52:32 +0200 | <haskellbridge> | <thirdofmay18081814goya> Leary: hm I see, thank you! |
| 2024-09-04 07:56:00 +0200 | Leary | (~Leary@user/Leary/x-0910699) (Remote host closed the connection) |
| 2024-09-04 07:56:12 +0200 | Leary | (~Leary@user/Leary/x-0910699) |
| 2024-09-04 07:56:24 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-04 08:00:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 08:00:57 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de) |
| 2024-09-04 08:04:25 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-09-04 08:05:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 08:16:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 08:16:54 +0200 | euleritian | (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de) |
| 2024-09-04 08:20:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 08:21:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-04 08:25:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-09-04 08:31:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 08:37:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-04 08:51:07 +0200 | alioguzhan1 | (~Thunderbi@78.173.89.238) |
| 2024-09-04 08:51:39 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-04 08:52:18 +0200 | alioguzhan | (~Thunderbi@78.173.89.238) (Ping timeout: 272 seconds) |
| 2024-09-04 08:52:18 +0200 | alioguzhan1 | alioguzhan |
| 2024-09-04 08:54:07 +0200 | crvs | (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) |
| 2024-09-04 09:00:18 +0200 | JamesMowery | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Quit: Goodbye) |
| 2024-09-04 09:00:35 +0200 | JamesMowery | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) |
| 2024-09-04 09:00:57 +0200 | vglfr | (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) (Ping timeout: 252 seconds) |
| 2024-09-04 09:01:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 09:01:42 +0200 | vglfr | (~vglfr@2607:fb91:81e:c43f:ac39:6af1:b007:6687) |
| 2024-09-04 09:03:36 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 09:06:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 09:08:17 +0200 | vglfr | (~vglfr@2607:fb91:81e:c43f:ac39:6af1:b007:6687) (Ping timeout: 252 seconds) |
| 2024-09-04 09:08:28 +0200 | vglfr | (~vglfr@2607:fb91:864:caf7:ad3:f751:af48:34dc) |
| 2024-09-04 09:09:04 +0200 | troydm | (~troydm@user/troydm) (Ping timeout: 260 seconds) |
| 2024-09-04 09:12:54 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 09:13:21 +0200 | alioguzhan | (~Thunderbi@78.173.89.238) (Ping timeout: 252 seconds) |
| 2024-09-04 09:17:27 +0200 | alioguzhan | (~Thunderbi@78.173.89.238) |
| 2024-09-04 09:18:29 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de) |
| 2024-09-04 09:18:42 +0200 | codaraxis__ | (~codaraxis@user/codaraxis) |
| 2024-09-04 09:19:18 +0200 | EvanR_ | (~EvanR@user/evanr) |
| 2024-09-04 09:19:49 +0200 | pavonia_ | (~user@user/siracusa) |
| 2024-09-04 09:20:31 +0200 | oo_miguel | (~Thunderbi@78.10.207.45) |
| 2024-09-04 09:20:38 +0200 | econo__ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-09-04 09:21:08 +0200 | DrachenMaus | (~dragonmau@user/dragonmaus) |
| 2024-09-04 09:21:14 +0200 | athan_ | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-04 09:21:21 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-04 09:21:27 +0200 | tzh_ | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-09-04 09:21:39 +0200 | pointlessslippe1 | (~pointless@62.106.85.17) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | euleritian | (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | kaskal | (~kaskal@2001:4bb8:2c3:301f:344f:f795:68cb:7518) (Quit: ZNC - https://znc.in) |
| 2024-09-04 09:21:39 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Read error: Connection reset by peer) |
| 2024-09-04 09:21:39 +0200 | connrs | (~connrs@user/connrs) (Remote host closed the connection) |
| 2024-09-04 09:21:39 +0200 | pavonia | (~user@user/siracusa) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | kaskal | (~kaskal@2001:4bb8:2c3:301f:344f:f795:68cb:7518) |
| 2024-09-04 09:21:39 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Remote host closed the connection) |
| 2024-09-04 09:21:39 +0200 | DragonMaus | (~dragonmau@user/dragonmaus) (Quit: No Ping reply in 180 seconds.) |
| 2024-09-04 09:21:39 +0200 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | dostoyevsky2 | (~sck@user/dostoyevsky2) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | dostoyevsky2 | (~sck@static.251.39.47.78.clients.your-server.de) |
| 2024-09-04 09:21:39 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:39 +0200 | econo__ | econo_ |
| 2024-09-04 09:21:40 +0200 | dostoyevsky2 | (~sck@static.251.39.47.78.clients.your-server.de) (Changing host) |
| 2024-09-04 09:21:40 +0200 | dostoyevsky2 | (~sck@user/dostoyevsky2) |
| 2024-09-04 09:21:48 +0200 | codaraxis | (~codaraxis@user/codaraxis) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:48 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:48 +0200 | EvanR | (~EvanR@user/evanr) (Ping timeout: 246 seconds) |
| 2024-09-04 09:21:53 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2024-09-04 09:22:06 +0200 | pavonia_ | pavonia |
| 2024-09-04 09:22:08 +0200 | pointlessslippe- | (~pointless@62.106.85.17) |
| 2024-09-04 09:26:31 +0200 | hammond | (proscan@gateway04.insomnia247.nl) (Ping timeout: 264 seconds) |
| 2024-09-04 09:27:01 +0200 | hammond | (proscan@gateway04.insomnia247.nl) |
| 2024-09-04 09:27:27 +0200 | connrs | (~connrs@user/connrs) |
| 2024-09-04 09:34:56 +0200 | tomboy64 | (~tomboy64@user/tomboy64) |
| 2024-09-04 09:35:22 +0200 | vglfr | (~vglfr@2607:fb91:864:caf7:ad3:f751:af48:34dc) (Ping timeout: 272 seconds) |
| 2024-09-04 09:35:35 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-09-04 09:43:30 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 246 seconds) |
| 2024-09-04 09:43:46 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-09-04 09:47:29 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-04 09:56:44 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-254.web.vodafone.de) |
| 2024-09-04 09:57:05 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 248 seconds) |
| 2024-09-04 09:58:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-04 10:01:23 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-04 10:02:19 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-04 10:08:23 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-04 10:10:13 +0200 | <bwe> | Hi, I've got a list that I want to map over and put the results under each other in a `do`. Do I just need to bind them with the bind operator? |
| 2024-09-04 10:10:33 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-09-04 10:10:44 +0200 | vglfr | (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) |
| 2024-09-04 10:13:08 +0200 | <haskellbridge> | <sm> hi @bwe, perhaps you're looking for "sequence" in Control.Monad ? |
| 2024-09-04 10:17:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2024-09-04 10:17:56 +0200 | euleritian | (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de) |
| 2024-09-04 10:18:37 +0200 | euleritian | (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-04 10:18:54 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-04 10:18:58 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-09-04 10:21:39 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2024-09-04 10:23:21 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-04 10:25:31 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) |
| 2024-09-04 10:25:49 +0200 | <haskellbridge> | <sm> -in Control.Monad |
| 2024-09-04 10:25:52 +0200 | <[exa]> | bwe: either of traverse (or for), sequence, and foldM should do it |
| 2024-09-04 10:26:58 +0200 | <bwe> | It's a pity, hoogle is down :( |
| 2024-09-04 10:27:11 +0200 | <bwe> | I correct, it was. |
| 2024-09-04 10:27:29 +0200 | tzh_ | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-09-04 10:30:59 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-09-04 10:36:04 +0200 | misterfish | (~misterfis@84.53.85.146) |
| 2024-09-04 10:42:11 +0200 | <bwe> | [exa]: oh, actually foldl did it for me with (>>) |
| 2024-09-04 10:46:52 +0200 | <[exa]> | bwe: ah cool, that's exactly `sequence_` |
| 2024-09-04 10:49:21 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 10:49:41 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 10:52:44 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-04 10:58:22 +0200 | <bwe> | [exa]: I didn't get `sequence` to work, but wasn't aware of `sequence_`. Thanks for bringing it up! |
| 2024-09-04 10:59:07 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 11:08:12 +0200 | Patternmaster | (~georg@user/Patternmaster) (Ping timeout: 252 seconds) |
| 2024-09-04 11:08:24 +0200 | Patternmaster | (~georg@user/Patternmaster) |
| 2024-09-04 11:11:38 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2024-09-04 11:22:49 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 11:25:03 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) |
| 2024-09-04 11:29:44 +0200 | chele | (~chele@user/chele) |
| 2024-09-04 11:30:32 +0200 | <[exa]> | bwe: there are many variants of that thing |
| 2024-09-04 11:31:18 +0200 | <[exa]> | map, mapM, traverse, traverse_, for, for_, sequence, sequenceA, both of sequences with _, ... |
| 2024-09-04 11:31:23 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-254.web.vodafone.de) (Read error: Connection reset by peer) |
| 2024-09-04 11:34:33 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) |
| 2024-09-04 11:35:45 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 276 seconds) |
| 2024-09-04 11:41:57 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-04 11:44:31 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-04 11:52:33 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 11:52:52 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 11:53:25 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-04 11:59:24 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 260 seconds) |
| 2024-09-04 12:03:28 +0200 | EvanR_ | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2024-09-04 12:03:30 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds) |
| 2024-09-04 12:03:47 +0200 | EvanR_ | (~EvanR@user/evanr) |
| 2024-09-04 12:03:51 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-09-04 12:04:17 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-04 12:05:35 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-04 12:06:18 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2024-09-04 12:09:25 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-04 12:15:30 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) |
| 2024-09-04 12:15:58 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-04 12:19:11 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) (Client Quit) |
| 2024-09-04 12:22:00 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-09-04 12:22:14 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) |
| 2024-09-04 12:23:00 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-09-04 12:25:40 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Remote host closed the connection) |
| 2024-09-04 12:25:49 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-04 12:27:46 +0200 | youthlic | (~Thunderbi@user/youthlic) (Ping timeout: 252 seconds) |
| 2024-09-04 12:31:39 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 12:31:59 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 12:35:05 +0200 | jespada | (~jespada@r190-64-133-178.su-static.adinet.com.uy) |
| 2024-09-04 12:36:07 +0200 | Guest21 | (~Guest21@217.64.164.1) |
| 2024-09-04 12:36:22 +0200 | Guest21 | (~Guest21@217.64.164.1) (Client Quit) |
| 2024-09-04 12:36:48 +0200 | <yin> | -/g |
| 2024-09-04 12:38:26 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-09-04 12:40:54 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-09-04 12:41:50 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-04 12:42:29 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-04 12:43:24 +0200 | <yin> | why did i just get a list of bans from 2 years ago? |
| 2024-09-04 12:43:43 +0200 | youthlic | (~Thunderbi@user/youthlic) |
| 2024-09-04 12:52:05 +0200 | <tomsmeding> | yin: who sent you that list |
| 2024-09-04 12:54:49 +0200 | jespada | (~jespada@r190-64-133-178.su-static.adinet.com.uy) (Ping timeout: 260 seconds) |
| 2024-09-04 12:57:10 +0200 | <yin> | helium.libera.chat, apparently |
| 2024-09-04 12:57:46 +0200 | xff0x | (~xff0x@2405:6580:b080:900:ccef:b4d3:d1ad:38b8) |
| 2024-09-04 12:58:51 +0200 | <yin> | must have been an error |
| 2024-09-04 12:58:52 +0200 | <tomsmeding> | interesting? |
| 2024-09-04 13:01:15 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2024-09-04 13:02:37 +0200 | <yin> | so apparently as soon as my bouncer synced i received the last few entries of the ban list, unprompted |
| 2024-09-04 13:02:59 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 13:03:18 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 13:03:46 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-04 13:04:19 +0200 | <yin> | /mode #haskell +b gives me the complete list and it checks out |
| 2024-09-04 13:04:34 +0200 | <yin> | must be a bug in znc |
| 2024-09-04 13:06:03 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 13:06:52 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-04 13:09:28 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 13:10:37 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 244 seconds) |
| 2024-09-04 13:20:20 +0200 | mesaoptimizer | (~mesaoptim@user/PapuaHardyNet) (Quit: mesaoptimizer) |
| 2024-09-04 13:20:28 +0200 | mesaoptimizer | (~mesaoptim@user/PapuaHardyNet) |
| 2024-09-04 13:21:13 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-04 13:22:36 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2024-09-04 13:25:05 +0200 | euleritian | (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de) |
| 2024-09-04 13:26:12 +0200 | euleritian | (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-04 13:27:10 +0200 | euleritian | (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de) |
| 2024-09-04 13:30:45 +0200 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2024-09-04 13:32:01 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 13:32:36 +0200 | Me-me | (~me-me@kc.randomserver.name) (Changing host) |
| 2024-09-04 13:32:36 +0200 | Me-me | (~me-me@user/me-me) |
| 2024-09-04 13:33:16 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 13:38:55 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Quit: ash3en) |
| 2024-09-04 13:39:14 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 13:40:23 +0200 | euleritian | (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-04 13:40:45 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-04 13:44:12 +0200 | <geekosaur> | yeh, znc requests all that stuff on entering a channel, and I've seen it get out of sync before (have also gotten a very large chunk of userlist in the past) |
| 2024-09-04 13:45:33 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 13:50:11 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 13:58:45 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 276 seconds) |
| 2024-09-04 14:01:23 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 14:06:31 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 14:12:46 +0200 | youthlic1 | (~Thunderbi@user/youthlic) |
| 2024-09-04 14:15:27 +0200 | youthlic | (~Thunderbi@user/youthlic) (Ping timeout: 246 seconds) |
| 2024-09-04 14:15:28 +0200 | youthlic1 | youthlic |
| 2024-09-04 14:16:47 +0200 | kalj | (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) |
| 2024-09-04 14:17:36 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 14:20:15 +0200 | kalj | (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) (Client Quit) |
| 2024-09-04 14:22:16 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 14:34:08 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 14:39:11 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 14:40:05 +0200 | <bwe> | which file watcher do you recommend to run `cabal run my-exec`? the options listed on stackoverflow sadly don't feel right |
| 2024-09-04 14:41:52 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-04 14:42:18 +0200 | <tomsmeding> | ghcid |
| 2024-09-04 14:42:35 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-09-04 14:43:00 +0200 | <tomsmeding> | i.e. `ghcid -r` probably |
| 2024-09-04 14:43:22 +0200 | <tomsmeding> | possibly `ghcid -c 'cabal repl my-exec' -r` |
| 2024-09-04 14:47:41 +0200 | <Leary> | bwe: It doesn't take much more than `inotifywait`. I have a little shell script putting a ghcid-like interface over it: https://gist.github.com/LSLeary/a7ddc196d119d52e2767f66873e24bdd |
| 2024-09-04 14:49:12 +0200 | <bwe> | tomsmeding: it's weird, why does `ghcid --restart="src" -c "cabal run web-server" -r` not react on changed file in src folder? |
| 2024-09-04 14:49:52 +0200 | vlad_ | (~vlad@102.217.157.32) |
| 2024-09-04 14:50:08 +0200 | <bwe> | seriously, why is haskell community not being able to just integrate a file watcher into cabal? |
| 2024-09-04 14:50:12 +0200 | akegalj | (~akegalj@89-164-111-213.dsl.iskon.hr) |
| 2024-09-04 14:50:32 +0200 | <Leary> | That's really not cabal's job. |
| 2024-09-04 14:50:55 +0200 | <vlad_> | i take it haskell has enter as the command terminator char |
| 2024-09-04 14:51:16 +0200 | <bwe> | Leary: whose job is it? |
| 2024-09-04 14:51:28 +0200 | <Leary> | inotifywait |
| 2024-09-04 14:51:31 +0200 | <vlad_> | could i string two commands together on one line? |
| 2024-09-04 14:51:40 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-09-04 14:51:57 +0200 | <Leary> | vlad_: With a semi-colon. |
| 2024-09-04 14:52:06 +0200 | <vlad_> | oh ok so it does use ; |
| 2024-09-04 14:53:20 +0200 | <vlad_> | hmm |
| 2024-09-04 14:53:23 +0200 | <geekosaur> | bwe, this is not at all unusual or tools like inotifywait wouldn't already exist |
| 2024-09-04 14:54:13 +0200 | <vlad_> | ghci> 1 |
| 2024-09-04 14:54:13 +0200 | <vlad_> | 1 |
| 2024-09-04 14:54:13 +0200 | <vlad_> | ghci> 1;3; |
| 2024-09-04 14:54:13 +0200 | <vlad_> | <interactive>:17:1: error: |
| 2024-09-04 14:54:13 +0200 | <vlad_> | Parse error: module header, import declaration |
| 2024-09-04 14:54:14 +0200 | <vlad_> | or top-level declaration expected. |
| 2024-09-04 14:54:16 +0200 | <vlad_> | ghci> |
| 2024-09-04 14:54:24 +0200 | <bwe> | wow, there is even: https://github.com/mercurytechnologies/ghciwatch |
| 2024-09-04 14:54:26 +0200 | <geekosaur> | (and indeed there are a bunch of other tools similar to it; which means there's a lot of demand for them) |
| 2024-09-04 14:54:35 +0200 | <vlad_> | guess i shouldn't paste |
| 2024-09-04 14:54:39 +0200 | <akegalj> | When I run `toRational 12.34` I get `3473401212609495 % 281474976710656` , but when I create rational myself `1234 % 100` I get `617 % 50`. Why? I would espect `toRational 12.34 == 1234 % 100` to be True but its not. On another hand `fromRational (toRational 12.34) == fromRational (1234 % 100)` is True. Am I doing something stupid here? |
| 2024-09-04 14:54:54 +0200 | <tomsmeding> | bwe: ghcid wants a ghci repl, it will work with 'cabal repl' but not with 'cabal run' |
| 2024-09-04 14:55:04 +0200 | <bwe> | tomsmeding: :( |
| 2024-09-04 14:55:22 +0200 | <tomsmeding> | akegalj: 0.34 is not precisely representable as a sum of (negative) powers of two |
| 2024-09-04 14:55:38 +0200 | <tomsmeding> | the floating point number "12.34" is hence not exactly equal to 1234 / 100 |
| 2024-09-04 14:55:45 +0200 | <tomsmeding> | toRational gives you reality |
| 2024-09-04 14:56:04 +0200 | <tomsmeding> | bwe: but with a repl you get faster reloading too! |
| 2024-09-04 14:56:07 +0200 | <geekosaur> | as for your semicolon issue with ghci, it's just being consistent with Haskell: semicolons separate declarations, definitions, or statements (the latter being restricted to "do" blocks and having a specific meaning) |
| 2024-09-04 14:56:31 +0200 | <vlad_> | i guess i'd better read the whole book before bothering you guys |
| 2024-09-04 14:56:34 +0200 | <vlad_> | thanks! |
| 2024-09-04 14:56:36 +0200 | <geekosaur> | it's not meaningful between expressions |
| 2024-09-04 14:56:57 +0200 | <bwe> | tomsmeding: still, I am waiting for the day of hot-reloading of haskell apps. |
| 2024-09-04 14:57:30 +0200 | <akegalj> | tomsmeding: thanks. My reality is shattered |
| 2024-09-04 14:57:47 +0200 | <geekosaur> | IEEE floating point does that to a lot of people |
| 2024-09-04 14:58:21 +0200 | <tomsmeding> | > toRational (12.34 :: Float) - 1234 % 100 |
| 2024-09-04 14:58:23 +0200 | <lambdabot> | 1 % 6553600 |
| 2024-09-04 14:58:26 +0200 | <tomsmeding> | > toRational (12.34 :: Double) - 1234 % 100 |
| 2024-09-04 14:58:27 +0200 | <lambdabot> | (-1) % 7036874417766400 |
| 2024-09-04 14:58:38 +0200 | <tomsmeding> | akegalj: Double gets closer than Float (as expected) |
| 2024-09-04 14:59:12 +0200 | <tomsmeding> | > toRational (4.0625 :: Float) - 625 % 10000 |
| 2024-09-04 14:59:13 +0200 | <lambdabot> | 4 % 1 |
| 2024-09-04 14:59:21 +0200 | <tomsmeding> | > toRational (4.0625 :: Float) - 40625 % 10000 |
| 2024-09-04 14:59:22 +0200 | <lambdabot> | 0 % 1 |
| 2024-09-04 14:59:33 +0200 | <tomsmeding> | > 1 / 16 |
| 2024-09-04 14:59:34 +0200 | <lambdabot> | 6.25e-2 |
| 2024-09-04 15:00:00 +0200 | <tomsmeding> | 0.0625 is an exact (sum of) (negative) powers of 2, and furthermore those powers aren't too large, so it's exactly representable |
| 2024-09-04 15:02:11 +0200 | <tomsmeding> | akegalj: if you want base-10 floating point numbers, check out https://hackage.haskell.org/package/scientific |
| 2024-09-04 15:03:04 +0200 | <sprout> | > 9007199254740993.0 + 1.0 |
| 2024-09-04 15:03:05 +0200 | <lambdabot> | 9.007199254740992e15 |
| 2024-09-04 15:03:10 +0200 | <Leary> | akegalj: The behaviour you expect does at least hold for literals and `Data.Fixed.Fixed 100`. |
| 2024-09-04 15:03:37 +0200 | <Leary> | Only Float and Double are sinful. |
| 2024-09-04 15:03:42 +0200 | <sprout> | at least ieee compliant |
| 2024-09-04 15:03:48 +0200 | <tomsmeding> | > 9007199254740993.0 |
| 2024-09-04 15:03:50 +0200 | <lambdabot> | 9.007199254740992e15 |
| 2024-09-04 15:07:25 +0200 | Square2 | (~Square4@user/square) |
| 2024-09-04 15:07:28 +0200 | <akegalj> | thanks guys! Will have to think a bit now |
| 2024-09-04 15:08:22 +0200 | <bwe> | which testing suite for parametrised tests is state of the art today? tasty, hedgehog, skeletest…? |
| 2024-09-04 15:09:28 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 15:09:29 +0200 | <bwe> | tomsmeding: as of now I've settled with `watchexec -w src -r -e hs -- cabal run web-server` |
| 2024-09-04 15:10:13 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-04 15:10:52 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-09-04 15:11:31 +0200 | <tomsmeding> | tasty is a framework that you can plug other stuff in, so it doesn't belong in the same list as hedgehog/quickcheck |
| 2024-09-04 15:11:55 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-04 15:12:00 +0200 | <geekosaur> | skeletest is quite new (past month) so I'd hold out or use it for experiments |
| 2024-09-04 15:12:15 +0200 | <geekosaur> | hedgehog is probably the go-to |
| 2024-09-04 15:13:14 +0200 | <tomsmeding> | if you're looking for a test framework, tasty is the "nobody got fired for choosing tasty"; for property-based tests, hedgehog tends to be nicer in practice than QuickCheck for more involved usecases |
| 2024-09-04 15:13:30 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 276 seconds) |
| 2024-09-04 15:13:39 +0200 | <tomsmeding> | both hedgehog and quickcheck can hook into tasty |
| 2024-09-04 15:14:16 +0200 | <bwe> | tomsmeding: what would be the "so. got fired for choosing…" then :) ? |
| 2024-09-04 15:14:44 +0200 | <tomsmeding> | I dunno :p |
| 2024-09-04 15:14:46 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 15:14:55 +0200 | <tomsmeding> | you own hand-rolled framework, undoubtedly |
| 2024-09-04 15:15:18 +0200 | <akegalj> | tomsmeding: Leary: thanks for scientific and Data.Fixed pointers! |
| 2024-09-04 15:16:04 +0200 | <bwe> | akegalj: (there is also safe-money, if you deal with money) |
| 2024-09-04 15:17:14 +0200 | <geekosaur> | I've also used CReal from the numbers package; it's very accurate but also very slow. (I'd used a `type` so I could experiment and switch out the actual type; started with Double which was fast but inaccurate, then CReal which was accurate but very slow, then Rational which I expected to be the worst of both worlds but for my use case it turned out to be almost as fast as Double and almost as accurate as CReal |
| 2024-09-04 15:17:20 +0200 | <geekosaur> | ) |
| 2024-09-04 15:17:24 +0200 | <akegalj> | bwe: thanks! |
| 2024-09-04 15:19:23 +0200 | <tomsmeding> | geekosaur: in what sense is Rational not accurate? |
| 2024-09-04 15:20:01 +0200 | <akegalj> | geekosaur: thanks! |
| 2024-09-04 15:20:36 +0200 | <tomsmeding> | sure, you can't express sqrt 2 as a Rational, but then Ratio doesn't implement Floating |
| 2024-09-04 15:20:58 +0200 | <geekosaur> | tomsmeding, actually I think I misphrased that. I was expecting accuracy but slowness due to huge denominators, but it was actually very fast |
| 2024-09-04 15:21:17 +0200 | <tomsmeding> | right |
| 2024-09-04 15:21:21 +0200 | <tomsmeding> | (I would expect the same) |
| 2024-09-04 15:21:27 +0200 | <tomsmeding> | interesting |
| 2024-09-04 15:22:23 +0200 | sp1ff | (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 2024-09-04 15:24:36 +0200 | <mauke> | sqrt($1.50) |
| 2024-09-04 15:24:50 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 15:25:35 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-04 15:25:46 +0200 | Alleria | (~Alleria@user/alleria) |
| 2024-09-04 15:26:16 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-09-04 15:29:02 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-04 15:31:06 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 15:41:47 +0200 | EvanR_ | EvanR |
| 2024-09-04 15:42:30 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 15:42:59 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 15:48:01 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 15:49:02 +0200 | athan_ | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-09-04 15:50:40 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Quit: ash3en) |
| 2024-09-04 15:51:31 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-09-04 15:52:25 +0200 | youthlic | (~Thunderbi@user/youthlic) |
| 2024-09-04 15:52:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-04 15:53:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-04 15:54:34 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 15:54:54 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) |
| 2024-09-04 15:54:55 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 15:59:19 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 15:59:19 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 16:03:06 +0200 | ystael | (~ystael@user/ystael) |
| 2024-09-04 16:03:51 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-09-04 16:06:06 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds) |
| 2024-09-04 16:10:40 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-04 16:18:40 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) |
| 2024-09-04 16:21:15 +0200 | Alleria | (~Alleria@user/alleria) (Ping timeout: 252 seconds) |
| 2024-09-04 16:26:01 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-04 16:33:15 +0200 | jinsun_ | (~jinsun@user/jinsun) |
| 2024-09-04 16:33:15 +0200 | jinsun | (~jinsun@user/jinsun) (Killed (erbium.libera.chat (Nickname regained by services))) |
| 2024-09-04 16:33:15 +0200 | jinsun_ | jinsun |
| 2024-09-04 16:36:30 +0200 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 2024-09-04 16:39:17 +0200 | _________ | (~nobody@user/noodly) (Quit: leaving) |
| 2024-09-04 16:42:37 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Remote host closed the connection) |
| 2024-09-04 16:43:19 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-04 16:45:33 +0200 | _________ | (~nobody@user/noodly) |
| 2024-09-04 16:46:08 +0200 | Alleria | (~Alleria@user/alleria) |
| 2024-09-04 16:50:29 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 248 seconds) |
| 2024-09-04 16:55:20 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3216-51e1-289d-5592-bb15-27a5.rev.sfr.net) |
| 2024-09-04 16:55:47 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3216-51e1-289d-5592-bb15-27a5.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 16:56:56 +0200 | alexherbo2 | (~alexherbo@119.13.23.93.rev.sfr.net) |
| 2024-09-04 16:57:31 +0200 | alexherbo2 | (~alexherbo@119.13.23.93.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 16:57:40 +0200 | CiaoSen | (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da) |
| 2024-09-04 16:58:12 +0200 | Alleria | (~Alleria@user/alleria) (Ping timeout: 246 seconds) |
| 2024-09-04 17:03:06 +0200 | sayola | (~sayola@ip-109-43-114-38.web.vodafone.de) |
| 2024-09-04 17:06:59 +0200 | CiaoSen | (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 2024-09-04 17:07:17 +0200 | ystael | (~ystael@user/ystael) |
| 2024-09-04 17:09:17 +0200 | <albet70> | I just feed LLM some context about fixed-point, and asked it how to use fixed-point to implement infinite type, and it generate something I haven't seen, LLM is so powerful now? here is its generated msg https://paste.tomsmeding.com/upmI7IN8 |
| 2024-09-04 17:11:46 +0200 | athan_ | (~athan@2600:382:3a1c:6a61:4450:dec8:4148:5c75) |
| 2024-09-04 17:12:33 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-04 17:13:26 +0200 | spew | (~spew@201.141.99.170) |
| 2024-09-04 17:17:11 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-09-04 17:18:21 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: nyaa~) |
| 2024-09-04 17:20:35 +0200 | misterfish | (~misterfis@84.53.85.146) |
| 2024-09-04 17:21:06 +0200 | ski | (~ski@ext-1-196.eduroam.chalmers.se) |
| 2024-09-04 17:21:08 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-04 17:22:52 +0200 | Square2 | (~Square4@user/square) (Remote host closed the connection) |
| 2024-09-04 17:27:06 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-09-04 17:28:51 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-09-04 17:33:02 +0200 | alexherbo2 | (~alexherbo@119.13.23.93.rev.sfr.net) |
| 2024-09-04 17:33:37 +0200 | alexherbo2 | (~alexherbo@119.13.23.93.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 17:33:40 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-04 17:35:09 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3216-51e1-7938-060c-1c69-e43c.rev.sfr.net) |
| 2024-09-04 17:48:53 +0200 | akegalj | (~akegalj@89-164-111-213.dsl.iskon.hr) (Quit: leaving) |
| 2024-09-04 17:54:45 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 252 seconds) |
| 2024-09-04 17:56:51 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 244 seconds) |
| 2024-09-04 18:04:36 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2024-09-04 18:07:13 +0200 | <EvanR> | albet70, as long as someone at some point delivered it codexes on that topic |
| 2024-09-04 18:07:19 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 2024-09-04 18:07:30 +0200 | <EvanR> | it can remix the content in ... creative ways |
| 2024-09-04 18:07:52 +0200 | <EvanR> | it really works great in D&D where the stakes for being wrong are much less xD |
| 2024-09-04 18:08:55 +0200 | ystael | (~ystael@user/ystael) |
| 2024-09-04 18:13:37 +0200 | <albet70> | haha |
| 2024-09-04 18:14:49 +0200 | infinity0 | (~infinity0@pwned.gg) |
| 2024-09-04 18:15:19 +0200 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Quit: WeeChat 4.4.1) |
| 2024-09-04 18:16:32 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-09-04 18:17:10 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 2024-09-04 18:17:20 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-04 18:22:49 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 265 seconds) |
| 2024-09-04 18:26:36 +0200 | czy | (~user@global-5-173.n-2.net.cam.ac.uk) |
| 2024-09-04 18:30:37 +0200 | mceresa | mceresaSlack |
| 2024-09-04 18:39:49 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 18:43:34 +0200 | sayola | (~sayola@ip-109-43-114-38.web.vodafone.de) (Read error: Connection reset by peer) |
| 2024-09-04 18:43:35 +0200 | sayola1 | (~sayola@ip-109-43-114-38.web.vodafone.de) |
| 2024-09-04 18:46:03 +0200 | EvanR | (~EvanR@user/evanr) (Ping timeout: 276 seconds) |
| 2024-09-04 18:46:10 +0200 | vglfr | (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) (Ping timeout: 252 seconds) |
| 2024-09-04 18:46:25 +0200 | vglfr | (~vglfr@2607:fb91:876:943b:ac39:c391:b163:cf47) |
| 2024-09-04 18:47:09 +0200 | mceresaSlack | mceresa |
| 2024-09-04 18:47:14 +0200 | sayola1 | (~sayola@ip-109-43-114-38.web.vodafone.de) (Client Quit) |
| 2024-09-04 18:47:28 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 265 seconds) |
| 2024-09-04 18:48:39 +0200 | crvs | (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) (Ping timeout: 252 seconds) |
| 2024-09-04 18:52:39 +0200 | vglfr | (~vglfr@2607:fb91:876:943b:ac39:c391:b163:cf47) (Ping timeout: 246 seconds) |
| 2024-09-04 18:53:33 +0200 | vglfr | (~vglfr@2607:fb90:ea4d:129c:ad3:f751:4fc7:4632) |
| 2024-09-04 18:55:06 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 246 seconds) |
| 2024-09-04 19:04:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-09-04 19:07:33 +0200 | hovsater | (sid499516@user/hovsater) (Ping timeout: 248 seconds) |
| 2024-09-04 19:07:57 +0200 | jonrh | (sid5185@ilkley.irccloud.com) (Read error: Connection reset by peer) |
| 2024-09-04 19:08:09 +0200 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) |
| 2024-09-04 19:09:37 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) |
| 2024-09-04 19:11:08 +0200 | hovsater | (sid499516@user/hovsater) |
| 2024-09-04 19:15:28 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-09-04 19:16:37 +0200 | ystael | (~ystael@user/ystael) |
| 2024-09-04 19:27:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 19:28:32 +0200 | EvanR | (~EvanR@user/evanr) |
| 2024-09-04 19:30:06 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-09-04 19:31:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 19:42:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 19:47:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 19:51:17 +0200 | czy | (~user@global-5-173.n-2.net.cam.ac.uk) (Ping timeout: 248 seconds) |
| 2024-09-04 19:56:24 +0200 | <Inst> | btw, standard chartered is finally backing Haskell Foundation? cheer! |
| 2024-09-04 19:58:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 20:02:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-04 20:03:10 +0200 | codaraxis__ | (~codaraxis@user/codaraxis) (Quit: Leaving) |
| 2024-09-04 20:04:39 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-04 20:07:31 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-09-04 20:08:23 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-09-04 20:13:20 +0200 | Inst_ | (~Inst@user/Inst) |
| 2024-09-04 20:14:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 20:15:03 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-09-04 20:15:45 +0200 | Inst | (~Inst@user/Inst) (Ping timeout: 276 seconds) |
| 2024-09-04 20:16:39 +0200 | <tomsmeding> | albet70: "It's important to note that the actual implementation of fixed-point combinators like the Y combinator is quite complex and involves advanced type-level programming and category theory concepts." -- that's not at all true |
| 2024-09-04 20:16:54 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-09-04 20:17:02 +0200 | <tomsmeding> | sure, the Y combiantor as commonly phrased does not quite type-check in haskell because of the self-application `x x` |
| 2024-09-04 20:17:33 +0200 | <tomsmeding> | but the trick to get around that, if you want to stay close to the original Y combinator, has nothing to do with type-level trickery or category theory |
| 2024-09-04 20:17:46 +0200 | crvs | (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) |
| 2024-09-04 20:18:16 +0200 | <EvanR> | chat-gpt should include what GPA it got during its undergrad with relevant answers |
| 2024-09-04 20:18:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 20:19:48 +0200 | athan_ | (~athan@2600:382:3a1c:6a61:4450:dec8:4148:5c75) (Ping timeout: 246 seconds) |
| 2024-09-04 20:19:57 +0200 | vglfr | (~vglfr@2607:fb90:ea4d:129c:ad3:f751:4fc7:4632) (Ping timeout: 252 seconds) |
| 2024-09-04 20:20:35 +0200 | <haskellbridge> | <Bowuigi> Note that LLMs are bad at most of the functional stuff because they involve actual thought. Consider them as "professional yappers" for now, at least until AlphaProof evolves and goes Cubical |
| 2024-09-04 20:20:46 +0200 | <tomsmeding> | albet70: https://en.wikipedia.org/wiki/Fixed-point_combinator#Type_for_the_Y_combinator |
| 2024-09-04 20:20:52 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-09-04 20:21:16 +0200 | <tomsmeding> | the second code block there is an implementation of the Y combinator in haskell that does typecheck |
| 2024-09-04 20:21:39 +0200 | <tomsmeding> | not a lot of deep stuff happening |
| 2024-09-04 20:25:09 +0200 | <Inst_> | EvanR: that would be a fun experiment |
| 2024-09-04 20:25:35 +0200 | <Inst_> | i'm susprised no one tried grading chatgpt's work, because tbh, i wouldn't be surprised if chatgpt could eek out a 2 / C |
| 2024-09-04 20:25:40 +0200 | Inst_ | Inst |
| 2024-09-04 20:25:59 +0200 | <EvanR> | it got an F for Frankenstein |
| 2024-09-04 20:26:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2024-09-04 20:27:02 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) |
| 2024-09-04 20:27:54 +0200 | euleritian | (~euleritia@dynamic-176-006-139-128.176.6.pool.telefonica.de) |
| 2024-09-04 20:29:52 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 20:32:33 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-04 20:34:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 20:35:24 +0200 | ystael | (~ystael@user/ystael) (Quit: Lost terminal) |
| 2024-09-04 20:42:26 +0200 | euleritian | (~euleritia@dynamic-176-006-139-128.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-04 20:42:43 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-04 20:44:16 +0200 | Fooo | (~Square@user/square) |
| 2024-09-04 20:45:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 20:45:44 +0200 | Fooo | Square |
| 2024-09-04 20:49:47 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-04 20:50:23 +0200 | vglfr | (~vglfr@2601:14d:4e01:1370:919a:c941:4142:9778) |
| 2024-09-04 20:50:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 20:54:57 +0200 | athan_ | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-04 20:56:05 +0200 | mikess | (~mikess@user/mikess) |
| 2024-09-04 20:59:51 +0200 | CiaoSen | (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da) |
| 2024-09-04 20:59:53 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-09-04 21:01:25 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 21:02:41 +0200 | <[exa]> | albet70: there might be a blogpost somewhere on the deep internets that says precisely the same with similar but sufficiently different words, identifiers and code structure |
| 2024-09-04 21:05:57 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-09-04 21:06:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-04 21:17:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 21:20:26 +0200 | ystael | (~ystael@user/ystael) |
| 2024-09-04 21:22:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 21:28:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 21:28:58 +0200 | gentauro_ | (~gentauro@cgn-cgn11-185-107-12-141.static.kviknet.net) (Ping timeout: 252 seconds) |
| 2024-09-04 21:30:48 +0200 | siers | (~ij@user/ij) (Ping timeout: 252 seconds) |
| 2024-09-04 21:30:53 +0200 | gentauro | (~gentauro@user/gentauro) |
| 2024-09-04 21:31:07 +0200 | <Inst> | does chatgpt imply grade deflation? |
| 2024-09-04 21:31:09 +0200 | siers | (~ij@user/ij) |
| 2024-09-04 21:31:33 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3216-51e1-7938-060c-1c69-e43c.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-04 21:31:35 +0200 | <Inst> | as in, would it result in harsher, and more aggressive grading as a way to shut down 0 effort chatgpt grabs? |
| 2024-09-04 21:32:31 +0200 | <EvanR> | lol |
| 2024-09-04 21:32:57 +0200 | <EvanR> | everyone has to get smarter to compete with chatgpt grading curve. Artificial Intelligence indeed |
| 2024-09-04 21:33:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 21:34:21 +0200 | <monochrom> | Grade deflation is happening. My colleagues and I are seeing a decrease of 10-15 percentiles in marks in 3rd-year students; they are also more passive. But we think it's COVID rather than LLMs. |
| 2024-09-04 21:36:56 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-09-04 21:37:02 +0200 | <monochrom> | LLMs are as good or as bad as what they were trained on. Essay courses and easy courses will get grade inflation because current LLMs are well-trained on those. Advanced courses will get deflation because LLMs are poorly trained on those, "insufficient data for a meaningful answer" (haha). |
| 2024-09-04 21:38:35 +0200 | <monochrom> | I am skeptical about the "it requires thinking so LLMs will do poorly" theory. I don't buy it until LLMs are trained on high-quality high-quantity data and still perform poorly. |
| 2024-09-04 21:39:09 +0200 | <monochrom> | Currently you don't even have enough Haskell code on the internet for chatgpt to steal and train on. |
| 2024-09-04 21:39:49 +0200 | <Inst> | https://knowledge.wharton.upenn.edu/article/is-chatgpt-a-better-entrepreneur-than-most/ |
| 2024-09-04 21:40:57 +0200 | <monochrom> | I say that because Copilot is doing OK with mainstream languages. Believe it or not, coding things up in mainstream languages requires just as much thinking, or "thinking". |
| 2024-09-04 21:41:23 +0200 | crvs | (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) (Ping timeout: 255 seconds) |
| 2024-09-04 21:43:33 +0200 | <monochrom> | (You think mutable states are really all that easier to get right than pure functions?) |
| 2024-09-04 21:44:27 +0200 | <mauke> | no, but I've also seen chatgpt spit out hilariously (or subtly) broken code |
| 2024-09-04 21:44:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 21:44:33 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-09-04 21:44:37 +0200 | <mauke> | it's a frickin' chat bot |
| 2024-09-04 21:45:05 +0200 | <monochrom> | (You think passing an object as an argument---recall that an object is at least a bundle of half a dozen functions---is really less complex than passing one single function as an argument?) |
| 2024-09-04 21:46:01 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-04 21:46:22 +0200 | <Inst> | (FP is easier than imperative programming, it's just substantially different) |
| 2024-09-04 21:46:24 +0200 | <mauke> | an object is no functions :-) |
| 2024-09-04 21:46:30 +0200 | <Inst> | Hmmm, I wonder how the math community is doing with chatgpt proofs |
| 2024-09-04 21:46:31 +0200 | CrunchyFlakes | (~CrunchyFl@31.18.102.35) |
| 2024-09-04 21:46:35 +0200 | <mauke> | I've been a C++ compiler before |
| 2024-09-04 21:46:37 +0200 | <Inst> | there's a huge corpus there |
| 2024-09-04 21:47:14 +0200 | <mauke> | "hoc est corpus meum" -- chatgpt, probably |
| 2024-09-04 21:47:57 +0200 | <EvanR> | I heard there has been success generating proofs using this LLM stuff |
| 2024-09-04 21:48:22 +0200 | <EvanR> | I don't know if it's in any remotely relevant realm to haskell |
| 2024-09-04 21:48:25 +0200 | <monochrom> | Oh, that. In 1st- and 2nd-year courses, we recognize which homework submissions are from chatgpt. :) Namely, those that look way too well-organized like in textbooks, e.g., complete with introduction, bullet points, conclusion. |
| 2024-09-04 21:48:50 +0200 | <justsomeguy> | Why does fmap length Just [1,2,3] evaluate to 1 instead of 3? |
| 2024-09-04 21:49:05 +0200 | <Inst> | that doesn't evaluate |
| 2024-09-04 21:49:06 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) |
| 2024-09-04 21:49:13 +0200 | <Inst> | you mean fmap length (Just [1,2,3]), right? |
| 2024-09-04 21:49:18 +0200 | <monochrom> | Because fmap length (Just whatever) = 1, regardless of whatever. |
| 2024-09-04 21:49:31 +0200 | <monochrom> | Err sorry, misread. |
| 2024-09-04 21:49:38 +0200 | <monochrom> | I need tea. I'll be back. |
| 2024-09-04 21:49:47 +0200 | <Inst> | oh, that does |
| 2024-09-04 21:49:55 +0200 | <monochrom> | > fmap length (Just [1,2,3]) |
| 2024-09-04 21:49:55 +0200 | <dolio> | > (length . Just) [1,2,3] |
| 2024-09-04 21:49:56 +0200 | <lambdabot> | Just 3 |
| 2024-09-04 21:49:57 +0200 | <lambdabot> | 1 |
| 2024-09-04 21:50:10 +0200 | <mauke> | > fmap length Just [1,2,3] |
| 2024-09-04 21:50:12 +0200 | <lambdabot> | 1 |
| 2024-09-04 21:50:22 +0200 | <monochrom> | Oh haha, didn't realize that it type-checks. |
| 2024-09-04 21:50:25 +0200 | <dolio> | fmap length Just = length . Just |
| 2024-09-04 21:50:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-04 21:50:57 +0200 | <monochrom> | OK then correction: length (Just whatever) = 1, regardless of whatever. length Nothing = 0. |
| 2024-09-04 21:51:39 +0200 | <justsomeguy> | When I try (\x -> Just (length x)) [1,2,3] it returns Just 3. |
| 2024-09-04 21:51:50 +0200 | <justsomeguy> | I think I made a mistake in the evaulation process somewhere. |
| 2024-09-04 21:52:03 +0200 | <justsomeguy> | (I tried writing out each step.) |
| 2024-09-04 21:52:09 +0200 | <dolio> | That is Just . length. |
| 2024-09-04 21:52:09 +0200 | <EvanR> | > length (Just 3) |
| 2024-09-04 21:52:11 +0200 | <lambdabot> | 1 |
| 2024-09-04 21:52:14 +0200 | <ash3en> | > fmap length $ Just [1,2,3] |
| 2024-09-04 21:52:15 +0200 | <lambdabot> | Just 3 |
| 2024-09-04 21:52:16 +0200 | <Inst> | do you know what the Functor instance for (a ->) is? |
| 2024-09-04 21:52:21 +0200 | <EvanR> | > length (1,3) |
| 2024-09-04 21:52:23 +0200 | <lambdabot> | 1 |
| 2024-09-04 21:52:24 +0200 | <ash3en> | fmap length Just [1,2,3] |
| 2024-09-04 21:52:29 +0200 | <ash3en> | > fmap length Just [1,2,3] |
| 2024-09-04 21:52:30 +0200 | <lambdabot> | 1 |
| 2024-09-04 21:52:34 +0200 | <EvanR> | > length () |
| 2024-09-04 21:52:35 +0200 | <dmj`> | the curse of FTP |
| 2024-09-04 21:52:36 +0200 | <lambdabot> | error: |
| 2024-09-04 21:52:36 +0200 | <lambdabot> | • Couldn't match expected type ‘t0 a0’ with actual type ‘()’ |
| 2024-09-04 21:52:36 +0200 | <lambdabot> | • In the first argument of ‘length’, namely ‘()’ |
| 2024-09-04 21:52:43 +0200 | <justsomeguy> | Inst: fmap |
| 2024-09-04 21:52:51 +0200 | <Inst> | fmap = (.) |
| 2024-09-04 21:52:55 +0200 | <EvanR> | really, () doesn't have a Foldable instance? |
| 2024-09-04 21:52:55 +0200 | <Inst> | like dolio said |
| 2024-09-04 21:53:01 +0200 | <mauke> | > (fmap length Just) "widdershins" |
| 2024-09-04 21:53:02 +0200 | <lambdabot> | 1 |
| 2024-09-04 21:53:02 +0200 | <Inst> | EvanR: do the kinds match? |
| 2024-09-04 21:53:06 +0200 | <EvanR> | oh |
| 2024-09-04 21:54:32 +0200 | <Inst> | more annoying, (a,b,c) is not instanced into Foldable |
| 2024-09-04 21:54:40 +0200 | <ash3en> | eh, i too don't really get why > fmap length Just [1,2,3] = 1 and > fmap length $ Just [1,2,3] = Just 3? |
| 2024-09-04 21:55:06 +0200 | <Inst> | fmap length Just [1,2,3] = (length . Just) [1,2,3] |
| 2024-09-04 21:56:27 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Ping timeout: 265 seconds) |
| 2024-09-04 21:56:31 +0200 | <Inst> | = length (Just [1,2,3]) = 1 |
| 2024-09-04 21:58:24 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 2024-09-04 21:58:42 +0200 | <ash3en> | ok, slowly I get it |
| 2024-09-04 22:00:07 +0200 | <Inst> | there's also an applicative and monad instance for (r ->), which people golf with, but a ton of people call smelly because you'd have to know how it works |
| 2024-09-04 22:00:27 +0200 | <tomsmeding> | not only that, because often it's golfing for golfing's sake :p |
| 2024-09-04 22:00:41 +0200 | <Inst> | > :t (<*>) |
| 2024-09-04 22:00:42 +0200 | <mauke> | wouldn't want people to have fun |
| 2024-09-04 22:00:42 +0200 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 2024-09-04 22:00:50 +0200 | <tomsmeding> | which is good if you're at codegolf.stackexchange.com, but not so good if you're writing code that should be read |
| 2024-09-04 22:00:59 +0200 | <mauke> | only ctional programming here |
| 2024-09-04 22:01:04 +0200 | <Inst> | @:t (<*>) |
| 2024-09-04 22:01:04 +0200 | <lambdabot> | Maybe you meant: wn v sm rc pl let id do bf @ ? . |
| 2024-09-04 22:01:31 +0200 | <tomsmeding> | mauke: fun in programming does not always go together with writing maintainable code :p |
| 2024-09-04 22:01:50 +0200 | <Inst> | > t |
| 2024-09-04 22:01:51 +0200 | <lambdabot> | t |
| 2024-09-04 22:01:51 +0200 | <tomsmeding> | doesn't mean that either is not worth doing |
| 2024-09-04 22:01:57 +0200 | <Inst> | > t (<*>) |
| 2024-09-04 22:01:59 +0200 | <lambdabot> | error: |
| 2024-09-04 22:01:59 +0200 | <lambdabot> | • Couldn't match expected type ‘(f0 (a0 -> b0) -> f0 a0 -> f0 b0) |
| 2024-09-04 22:01:59 +0200 | <lambdabot> | -> t’ |
| 2024-09-04 22:02:07 +0200 | <tomsmeding> | :t (<*>) |
| 2024-09-04 22:02:07 +0200 | <Inst> | ugh, which bot can give you types? |
| 2024-09-04 22:02:08 +0200 | <lambdabot> | Applicative f => f (a -> b) -> f a -> f b |
| 2024-09-04 22:02:14 +0200 | <mauke> | lambdabot |
| 2024-09-04 22:02:19 +0200 | <tomsmeding> | % :t (<*>) |
| 2024-09-04 22:02:19 +0200 | <yahb2> | (<*>) :: Applicative f => f (a -> b) -> f a -> f b |
| 2024-09-04 22:02:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 22:02:35 +0200 | <Inst> | let f be (r ->) |
| 2024-09-04 22:02:43 +0200 | <tomsmeding> | % :set -XTypeApplications |
| 2024-09-04 22:02:43 +0200 | <yahb2> | <no output> |
| 2024-09-04 22:02:49 +0200 | <tomsmeding> | % :t (<*>) @((->) r) |
| 2024-09-04 22:02:49 +0200 | <yahb2> | <interactive>:1:14: error: Not in scope: type variable ‘r’ |
| 2024-09-04 22:02:49 +0200 | <Inst> | try that as an exercise, ash3en |
| 2024-09-04 22:02:52 +0200 | <tomsmeding> | % :t (<*>) @((->) Bool) |
| 2024-09-04 22:02:52 +0200 | <yahb2> | (<*>) @((->) Bool) ; :: (Bool -> (a -> b)) -> (Bool -> a) -> Bool -> b |
| 2024-09-04 22:03:47 +0200 | <mauke> | @djinn (Bool -> (a -> b)) -> (Bool -> a) -> Bool -> b |
| 2024-09-04 22:03:47 +0200 | <lambdabot> | f a b c = |
| 2024-09-04 22:03:47 +0200 | <lambdabot> | case c of |
| 2024-09-04 22:03:47 +0200 | <lambdabot> | False -> a False (b False) |
| 2024-09-04 22:03:47 +0200 | <lambdabot> | True -> a True (b False) |
| 2024-09-04 22:04:12 +0200 | <tomsmeding> | @djinn (r -> (a -> b)) -> (r -> a) -> r -> b |
| 2024-09-04 22:04:12 +0200 | <lambdabot> | f a b c = a c (b c) |
| 2024-09-04 22:04:26 +0200 | tomsmeding | . o O ( f a d c ) |
| 2024-09-04 22:06:45 +0200 | itaipu | (~itaipu@168.121.98.169) (Ping timeout: 248 seconds) |
| 2024-09-04 22:07:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 22:08:39 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-04 22:10:09 +0200 | <ash3en> | oof, ok |
| 2024-09-04 22:10:26 +0200 | <Inst> | it just works out that way because of the type definition |
| 2024-09-04 22:10:55 +0200 | <Inst> | % :t (>>=) |
| 2024-09-04 22:10:55 +0200 | <yahb2> | (>>=) :: Monad m => m a -> (a -> m b) -> m b |
| 2024-09-04 22:11:13 +0200 | <Inst> | % :t (>>=) @(r ->) |
| 2024-09-04 22:11:13 +0200 | <yahb2> | <interactive>:1:13: error: parse error on input ‘)’ |
| 2024-09-04 22:11:19 +0200 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-09-04 22:11:27 +0200 | <Inst> | % :t (>>=) @((->) r) |
| 2024-09-04 22:11:27 +0200 | <yahb2> | <interactive>:1:14: error: Not in scope: type variable ‘r’ |
| 2024-09-04 22:11:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 22:11:56 +0200 | <Inst> | (r -> a) -> (a -> r -> b) -> r -> b |
| 2024-09-04 22:12:02 +0200 | <tomsmeding> | % :t (>>=) @((->) Bool) |
| 2024-09-04 22:12:02 +0200 | <yahb2> | (>>=) @((->) Bool) :: (Bool -> a) -> (a -> Bool -> b) -> Bool -> b |
| 2024-09-04 22:14:08 +0200 | <tomsmeding> | (<*>) = flip (>>=) . flip |
| 2024-09-04 22:15:11 +0200 | <tomsmeding> | :t (=<<) <$> flip |
| 2024-09-04 22:15:12 +0200 | <lambdabot> | (a1 -> a2 -> b) -> (a1 -> a2) -> a1 -> b |
| 2024-09-04 22:16:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 22:16:47 +0200 | <tomsmeding> | 1. (<*>) = (=<<) <$> flip 2. (=<<) = (<*>) <$> flip |
| 2024-09-04 22:17:31 +0200 | <tomsmeding> | (<$> flip) is involutive (at the right type) |
| 2024-09-04 22:19:22 +0200 | <tomsmeding> | no actually, (<$> flip) is just involutive always |
| 2024-09-04 22:19:36 +0200 | <tomsmeding> | (<$> flip) <$> (<$> flip) = id |
| 2024-09-04 22:19:50 +0200 | itaipu | (~itaipu@168.121.99.142) |
| 2024-09-04 22:20:16 +0200 | <tomsmeding> | which is: flip fmap flip `fmap` flip fmap flip |
| 2024-09-04 22:20:36 +0200 | <tomsmeding> | mauke: is this functional enough for you :p |
| 2024-09-04 22:20:56 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-04 22:20:58 +0200 | ash3en | (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Quit: ash3en) |
| 2024-09-04 22:21:38 +0200 | <dmj`> | what even is functional |
| 2024-09-04 22:23:03 +0200 | <tomsmeding> | well I think flip fmap flip `fmap` flip fmap flip is quite functional |
| 2024-09-04 22:24:38 +0200 | <Hecate> | :26 |
| 2024-09-04 22:24:41 +0200 | <Hecate> | (hi) |
| 2024-09-04 22:24:46 +0200 | <tomsmeding> | :) |
| 2024-09-04 22:25:17 +0200 | <Inst> | oh, condolences on your recent coup |
| 2024-09-04 22:25:48 +0200 | <Inst> | and support, but off-topic |
| 2024-09-04 22:25:53 +0200 | <Franciman> | hi, is haskell experimenting new language paradigms? |
| 2024-09-04 22:26:06 +0200 | <Franciman> | are we gonna see major changes? |
| 2024-09-04 22:27:23 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 22:28:12 +0200 | <Inst> | what are actually new language paradigms these days? |
| 2024-09-04 22:30:54 +0200 | <EvanR> | fresh paradigms, right outta the book industry oven? |
| 2024-09-04 22:31:13 +0200 | <EvanR> | smell those crispy acronyms |
| 2024-09-04 22:31:31 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2024-09-04 22:32:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 22:38:03 +0200 | <dmj`> | Franciman: there was some linear types added |
| 2024-09-04 22:38:17 +0200 | <Franciman> | nice |
| 2024-09-04 22:41:16 +0200 | <dmj`> | someone might be able to add row types into the type system, that'd be a big change |
| 2024-09-04 22:43:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 22:45:28 +0200 | <justsomeguy> | What do you think of Serokell's work on dependent types? https://serokell.io/blog/ghc-dependent-types-in-haskell |
| 2024-09-04 22:48:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-04 22:50:01 +0200 | czy | (~user@2a00:23c6:54a8:6301:5024:a70a:b7d6:6a68) |
| 2024-09-04 22:58:21 +0200 | <haskellbridge> | <thirdofmay18081814goya> in an extrinsically typed model of system f, do I need to introduce new syntax if I introduce the type-variable type and quantified-type type, can the syntax for lambda abstraction "\lambda x. term" be used for type application and type abstraction or do I need to introduce new syntax? |
| 2024-09-04 22:58:30 +0200 | kaskal- | (~kaskal@213-225-32-95.nat.highway.a1.net) |
| 2024-09-04 22:58:42 +0200 | kaskal | (~kaskal@2001:4bb8:2c3:301f:344f:f795:68cb:7518) (Ping timeout: 246 seconds) |
| 2024-09-04 22:58:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 22:59:27 +0200 | dostoyevsky2 | (~sck@user/dostoyevsky2) (Quit: leaving) |
| 2024-09-04 22:59:46 +0200 | dostoyevsky2 | (~sck@user/dostoyevsky2) |
| 2024-09-04 23:01:53 +0200 | <EvanR> | chatgpt says yes, you need new syntax xD |
| 2024-09-04 23:02:08 +0200 | <EvanR> | like capital lambda |
| 2024-09-04 23:02:38 +0200 | <ncf> | stop using chatgpt |
| 2024-09-04 23:02:46 +0200 | <haskellbridge> | <thirdofmay18081814goya> uh give me a second this question is ill-typed lmao |
| 2024-09-04 23:03:12 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-09-04 23:03:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 23:05:06 +0200 | <monochrom> | :) |
| 2024-09-04 23:06:52 +0200 | <monochrom> | I don't know extrinsically type model. But System F syntax goes like (Λt. λx:t. x) : ∀t. t->t |
| 2024-09-04 23:07:59 +0200 | <monochrom> | Type theory tends to use Π instead of Λ. |
| 2024-09-04 23:09:11 +0200 | <monochrom> | But then type theory's Π also covers more things. |
| 2024-09-04 23:09:12 +0200 | <haskellbridge> | <thirdofmay18081814goya> What I want to ask: would I run into any issues if I have expressions "\lambda x. term" typed "TypeVariable -> Nat" but also expressions "\lambda x. term" typed "Nat -> Nat" |
| 2024-09-04 23:11:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> "forall TypeVariable. TypeVariable -> Nat" I meant |
| 2024-09-04 23:12:53 +0200 | <monochrom> | I understand "forall t. t -> Nat", but I don't understnad "forall TypeVariable. TypeVariable -> Nat". |
| 2024-09-04 23:13:04 +0200 | <EvanR> | you just said the same thing has two different types |
| 2024-09-04 23:13:19 +0200 | <monochrom> | unless you say that by alpha conversion, they are the same damn thing. |
| 2024-09-04 23:14:01 +0200 | <EvanR> | maybe you meant lambda x . type |
| 2024-09-04 23:14:09 +0200 | <EvanR> | where type is a type not a variable |
| 2024-09-04 23:14:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: i meant: the following would be two typed expressions in this system: "\lambda x. term1 : forall t. t -> Nat", and "\lambda x. term2. : Nat -> Nat" |
| 2024-09-04 23:14:39 +0200 | <monochrom> | "lambda x. type" would happen in type theory, but not in System F. |
| 2024-09-04 23:14:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 23:15:45 +0200 | <monochrom> | System F also doesn't like unannotated lambdas. |
| 2024-09-04 23:16:38 +0200 | <EvanR> | thirdofmaycan'tautocompleteuhg: you still didn't give an example of a type abstraction or type application |
| 2024-09-04 23:16:42 +0200 | <EvanR> | which I thought was the original question |
| 2024-09-04 23:19:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-04 23:20:27 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-04 23:20:57 +0200 | <tomsmeding> | thirdofmay: do you mean that the following would be a valid type judgement? \t. \x. x : \forall t. t -> t |
| 2024-09-04 23:21:14 +0200 | <tomsmeding> | i.e. merging the big-lambda and small-lambda syntaxes |
| 2024-09-04 23:21:16 +0200 | <monochrom> | "(Λt. λx:t. term1) : ∀t. t->Nat" works, "(λx:Nat. term2) : Nat->Nat" also works, but note the manual annotation of x. "λx. term" System F be like "I won't do type inference for you". |
| 2024-09-04 23:21:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 23:21:33 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-09-04 23:22:04 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 2024-09-04 23:22:23 +0200 | <monochrom> | and by extension, "not let-generalization" either, so if you don't have Λ you won't get ∀. |
| 2024-09-04 23:23:16 +0200 | <tomsmeding> | if you only have a type on the outside, stuff inside gets ambiguous too. Consider: `(\p -> fst p) (42, foo) : Nat`. What is the type of that `foo`? |
| 2024-09-04 23:23:30 +0200 | <tomsmeding> | (if you don't like pairs, choose your favourite lambda encoding of pairs) |
| 2024-09-04 23:24:22 +0200 | <haskellbridge> | <thirdofmay18081814goya> am instantiating examples from your comments, very helpful ty |
| 2024-09-04 23:24:44 +0200 | <tomsmeding> | (and if you say "well foo is out of scope", read "\x -> x" for foo. That could be Nat -> Nat, Bool -> Bool, (Nat -> Bool) -> (Nat -> Bool), or anything else) |
| 2024-09-04 23:26:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 23:27:29 +0200 | michalz | (~michalz@185.246.207.201) (Remote host closed the connection) |
| 2024-09-04 23:30:27 +0200 | <monochrom> | This gives me an interesting thought. System F is strongly normalizing. That sounds assuring at first. But it is only after your term passes type-checking. If you write an arbitrary unnannotated unchecked term, type inference is undecidable. So in a sense the proof of termination is put on your shoulder in the form of manual annotations. |
| 2024-09-04 23:32:11 +0200 | <EvanR> | same as simply typed LC |
| 2024-09-04 23:37:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 23:42:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-04 23:46:00 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-04 23:47:43 +0200 | <int-e> | EvanR: not quite; there, type inference is decidable |
| 2024-09-04 23:48:03 +0200 | <int-e> | of course you pay for that by having fewer terms that can be typed successfully |
| 2024-09-04 23:49:27 +0200 | <EvanR> | oh right |
| 2024-09-04 23:52:20 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 2024-09-04 23:52:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-04 23:57:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |