Logs on 2024-03-27 (liberachat/#haskell)
| 00:01:26 | → | sadie_ joins (~sadie@c-76-155-235-153.hsd1.co.comcast.net) |
| 00:03:37 | × | nek0 quits (~nek0@2a01:4f8:222:2b41::12) (Quit: Ping timeout (120 seconds)) |
| 00:03:53 | infinity0 | is now known as Guest4671 |
| 00:03:53 | × | Guest4671 quits (~infinity0@pwned.gg) (Killed (tungsten.libera.chat (Nickname regained by services))) |
| 00:03:54 | → | nek0 joins (~nek0@2a01:4f8:222:2b41::12) |
| 00:04:02 | → | infinity0 joins (~infinity0@pwned.gg) |
| 00:05:23 | × | micro quits (~micro@user/micro) (Ping timeout: 264 seconds) |
| 00:05:26 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 00:05:59 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 00:07:00 | → | micro joins (~micro@user/micro) |
| 00:12:34 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 00:16:08 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 00:20:34 | → | rvalue joins (~rvalue@user/rvalue) |
| 00:32:36 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 00:35:17 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:44:37 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 272 seconds) |
| 00:45:39 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 252 seconds) |
| 00:53:09 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 00:55:10 | → | Square joins (~Square4@user/square) |
| 01:01:05 | × | tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 256 seconds) |
| 01:02:48 | → | tessier joins (~treed@ip72-220-57-194.sd.sd.cox.net) |
| 01:15:19 | → | rosco joins (~rosco@183.171.110.111) |
| 01:18:33 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 01:26:34 | × | tessier quits (~treed@ip72-220-57-194.sd.sd.cox.net) (Ping timeout: 268 seconds) |
| 01:28:12 | → | tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 01:29:33 | × | billchenchina quits (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Ping timeout: 255 seconds) |
| 01:32:44 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 01:34:42 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 01:37:37 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 01:39:44 | → | infinity0 joins (~infinity0@pwned.gg) |
| 01:40:08 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 01:43:30 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 01:43:58 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 01:46:05 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 01:50:42 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 255 seconds) |
| 01:52:47 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds) |
| 01:57:00 | × | mima quits (~mmh@aftr-62-216-211-42.dynamic.mnet-online.de) (Ping timeout: 255 seconds) |
| 02:03:19 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Ping timeout: 255 seconds) |
| 02:05:46 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 02:07:12 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 02:08:08 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 02:15:31 | × | xff0x quits (~xff0x@2405:6580:b080:900:f97d:d4c:a5b1:7ce0) (Ping timeout: 260 seconds) |
| 02:21:23 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 02:22:12 | × | otto_s quits (~user@p4ff27cae.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 02:23:40 | → | otto_s joins (~user@p5de2fa1e.dip0.t-ipconnect.de) |
| 02:33:10 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 02:33:46 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 02:36:06 | <c_wraith> | Aww, I can't do nested lack of pattern matches against empty data decls |
| 02:36:43 | <c_wraith> | Well, I can. But GHC complains that I've missed cases |
| 02:37:59 | <c_wraith> | I guess I can see why. The code difference results in different runtime diagnostics. Was it an incomplete pattern match or a bottom? Depends on which code you wrote. |
| 02:38:36 | → | benkard joins (~mulk@p5b2dc97e.dip0.t-ipconnect.de) |
| 02:39:45 | × | mulk quits (~mulk@p5b2dc4f3.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 02:39:45 | benkard | is now known as mulk |
| 02:40:06 | <probie> | If it treated them the same, then most of the machinery for deepseq wouldn't work |
| 02:40:49 | <c_wraith> | I really was more concerned with the warning than the specific way it fails at runtime |
| 02:41:49 | <c_wraith> | (case x of Nothing -> y) gives a warning about incomplete pattern matches, that is silenced by (case x of Nothing -> y ; Just z -> case z of) |
| 02:43:12 | → | triceraptor joins (~prodmezha@123.63.203.210) |
| 02:43:12 | <c_wraith> | emptiness can't be written in a nested match. I guess because there's absolutely no syntax to distinguish it from forgetting about the case. |
| 02:46:49 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 02:47:41 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 02:58:43 | <EvanR> | case x of {}? |
| 03:00:17 | → | igemnace joins (~ian@user/igemnace) |
| 03:02:37 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 03:06:34 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 03:07:08 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 03:10:28 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 03:11:03 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 03:11:56 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 03:13:16 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:21:48 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 03:23:48 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 03:24:28 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 03:28:16 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 246 seconds) |
| 03:35:34 | × | shapr` quits (~user@c-24-218-186-89.hsd1.ma.comcast.net) (Ping timeout: 255 seconds) |
| 03:38:06 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 03:40:11 | × | td_ quits (~td@i5387093F.versanet.de) (Ping timeout: 264 seconds) |
| 03:40:27 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 03:41:42 | → | td_ joins (~td@i53870933.versanet.de) |
| 03:44:00 | → | gentauro joins (~gentauro@user/gentauro) |
| 03:54:52 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 03:55:16 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 04:01:27 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 04:04:07 | × | turlando_ quits (~turlando@user/turlando) (Ping timeout: 256 seconds) |
| 04:05:04 | → | turlando joins (~turlando@user/turlando) |
| 04:16:51 | × | libertyprime quits (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Quit: leaving) |
| 04:28:06 | <ski> | case x of Nothing -> y ; Just ‾ -> ‾ -- absurd pattern (and expression) |
| 04:30:31 | <EvanR> | ‾u‾ |
| 04:36:28 | <ski> | (`‾' being the neutral element of disjunctive / or- patterns, just like `_' (wildcard / "don't care") being neutral element of conjunctive / and-pattern (`@', if we allow both sides to be arbitrary patterns (e.g. useful with view patterns or pattern synonyms))) |
| 04:38:51 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 04:43:19 | <Axman6> | so the conversation earlier, with e@(Left _) >>= _ = e/unsafeCoerce e, it would be nice if you could safely use coerce e, because the extra information available through the Left pattern means it's guaranteed to be a no-op right? |
| 04:44:14 | <Axman6> | it feels like what's possible with GADTs and pattern matching, so why doesn't it work with normal data? |
| 04:46:12 | <ski> | yes .. that's why i was suggesting assigning the type `forall b. Either a b' to `e', there |
| 04:49:34 | <ski> | (if only the patterns we've discarded mentions a type parameter in the component types of the data constructors of the discarded patterns, then we can generalize the current pattern over that type parameter. however, one could wonder how this would look like, in say an extension to System F -- also, from an abstract semantical standpoint, are there models of the original system which are not valid models of |
| 04:49:40 | <ski> | an extended system along these lines ?) |
| 04:55:52 | <dmj`> | p |
| 04:56:19 | × | dmj` quits (sid72307@id-72307.hampstead.irccloud.com) () |
| 05:01:07 | → | aforemny_ joins (~aforemny@2001:9e8:6ce5:9000:b2bf:8cbe:296e:6191) |
| 05:02:22 | × | aforemny quits (~aforemny@i59F516FD.versanet.de) (Ping timeout: 256 seconds) |
| 05:20:10 | → | michalz joins (~michalz@185.246.207.217) |
| 05:31:05 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:35:02 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 05:35:28 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 05:37:21 | <jackdk> | q |
| 05:39:03 | <Axman6> | p :- q |
| 05:41:02 | → | harveypwca joins (~harveypwc@2601:246:c200:2740:15b6:f225:14ff:9821) |
| 05:46:18 | × | michalz quits (~michalz@185.246.207.217) (Quit: ZNC 1.8.2 - https://znc.in) |
| 05:49:06 | → | michalz joins (~michalz@185.246.207.218) |
| 05:51:04 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 05:51:31 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 06:03:25 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 06:10:51 | × | Square quits (~Square4@user/square) (Ping timeout: 268 seconds) |
| 06:16:04 | × | destituion quits (~destituio@2a02:2121:655:c95b:3078:92e:b911:97ff) (Ping timeout: 260 seconds) |
| 06:16:24 | → | destituion joins (~destituio@85.221.111.174) |
| 06:21:40 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:23:36 | × | sadie_ quits (~sadie@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Leaving) |
| 06:31:11 | × | son0p quits (~ff@152.203.80.45) (Ping timeout: 264 seconds) |
| 06:32:22 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:40:25 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:44:34 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 06:50:59 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:55:31 | × | [Leary] quits (~Leary]@user/Leary/x-0910699) (Ping timeout: 260 seconds) |
| 06:57:56 | → | acidjnk_new joins (~acidjnk@p200300d6e706f453dde8176755f9f4a3.dip0.t-ipconnect.de) |
| 07:03:58 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:07:44 | → | mzg joins (mzg@37.221.213.54) |
| 07:16:12 | → | CiaoSen joins (~Jura@2a05:5800:2e6:d500:e6b9:7aff:fe80:3d03) |
| 07:16:51 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 07:21:28 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 268 seconds) |
| 07:22:44 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 07:22:45 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 07:32:17 | → | mima joins (~mmh@aftr-62-216-211-133.dynamic.mnet-online.de) |
| 07:45:49 | × | trev quits (~trev@user/trev) (Ping timeout: 268 seconds) |
| 07:49:37 | → | danza joins (~francesco@151.57.49.84) |
| 07:55:42 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:57:37 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:03:59 | × | tzh quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 08:06:07 | <cheater> | how do i remove something from lambdabot that i've put in it using @let ? |
| 08:06:13 | <cheater> | we should have a command like @delet |
| 08:09:17 | <c_wraith> | the only tool to do that is @undefine, which resets L.hs to Pristine.hs |
| 08:10:45 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 08:14:26 | ski | used to use `@define' for that |
| 08:16:45 | → | zetef joins (~quassel@5.2.182.99) |
| 08:17:01 | <cheater> | we need @delet even if just for the meme of it |
| 08:17:35 | <danza> | too bad that, with an immutable language, it would never spread |
| 08:17:49 | <cheater> | i was just typing: come to think of it... this would be an interesting feature for Haskell |
| 08:17:57 | <cheater> | it's clearly a pure, immutable feature |
| 08:18:59 | <cheater> | the semantics are obvious. delet x in f takes over all the let's from the outside context except x, and runs f in that new context |
| 08:19:36 | <danza> | ^^; |
| 08:19:54 | <cheater> | the proper pronunciation is left as an exercise to the reader |
| 08:19:58 | <c_wraith> | I'm not sure the semantics are obvious. |
| 08:20:17 | <c_wraith> | What if you use it to define a higher-order function and the function passed in closes over the unbound valu? |
| 08:20:19 | <c_wraith> | *value |
| 08:20:52 | → | gmg joins (~user@user/gehmehgeh) |
| 08:21:03 | <danza> | don't feed the joke ... it is still to early in the day ... |
| 08:21:04 | <c_wraith> | I suppose that's just lexical vs dynamic scoping? Well, ok. You could just say "use lexical scoping like everything else" |
| 08:21:07 | <cheater> | is the HOF being defined inside the delet and being passed outside, or is it being defined outside the delet and being passed inside? |
| 08:21:23 | <danza> | *too |
| 08:21:51 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 08:24:12 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 08:25:00 | → | gmg joins (~user@user/gehmehgeh) |
| 08:25:13 | <cheater> | c_wraith: |
| 08:25:16 | → | zetef joins (~quassel@5.2.182.99) |
| 08:26:41 | → | oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 08:28:11 | × | triceraptor quits (~prodmezha@123.63.203.210) (Ping timeout: 264 seconds) |
| 08:29:24 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 08:29:53 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 08:30:35 | <danza> | cheater: |
| 08:32:43 | <cheater> | well either way it's obvious that in the first case the HOF cannot be passed outside the delet just like it can't be passed outside a let. in the second case, it should work just like with shadowing, eg let one = 1, add1 x = x + one in let one = 2 in add1 10 -- should still result in 11 |
| 08:33:55 | × | rosco quits (~rosco@183.171.110.111) (Ping timeout: 268 seconds) |
| 08:36:09 | <danza> | .O_O. |
| 08:36:25 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 08:40:00 | → | mmhat joins (~mmh@p200300f1c706a2b6ee086bfffe095315.dip0.t-ipconnect.de) |
| 08:40:49 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 08:41:55 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 08:47:36 | <ski> | cheater : the HOF would take a callback as input, and also use `delet'/`forget' in its body, innside of which it'd refer to the callback |
| 08:48:33 | <cheater> | ski: that's the second case. same as shadowing. |
| 08:48:55 | <cheater> | idk about a forget keyword, never used it |
| 08:49:07 | <cheater> | you'd think it would be the opposite to a learn keyword |
| 08:49:14 | <cheater> | but i haven't used that either |
| 08:49:29 | → | son0p joins (~ff@167.0.169.98) |
| 08:50:59 | <ski> | second vs. first case ? |
| 08:52:06 | <cheater> | yes. |
| 08:52:29 | <ski> | case of what ? |
| 08:52:33 | <cheater> | read the conversation between me and c_wraith from 30 minutes ago. |
| 08:52:38 | <cheater> | it's still on the screen |
| 08:53:08 | <cheater> | (it's easier and less messy than pasting it all again in here) |
| 08:53:31 | → | dhil joins (~dhil@2001:8e0:2014:3100:348d:fdf8:7e1e:8e9) |
| 08:53:45 | <ski> | first time i see you mentioning "case" is twenty minutes ago, but it's still not clear to mean what those cases are |
| 08:53:45 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 08:53:52 | <cheater> | hold up |
| 08:55:08 | <ski> | (btw, in a categorical formulation of predicate logic, existential quantification (`right') is left adjunction of `forget'/`delet', while universal quantification (`forall') is right adjunction of `forget'/`delete') |
| 08:56:15 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 08:57:01 | <cheater> | https://i.imgur.com/4FoVLuW.png |
| 08:57:34 | <cheater> | ski: |
| 08:58:05 | <danza> | oh i see the hanging : probably come from your client |
| 08:58:15 | jinsun | is now known as Guest3181 |
| 08:58:15 | → | jinsun_ joins (~jinsun@user/jinsun) |
| 08:58:16 | × | Guest3181 quits (~jinsun@user/jinsun) (Killed (tungsten.libera.chat (Nickname regained by services))) |
| 08:58:16 | jinsun_ | is now known as jinsun |
| 08:58:40 | <cheater> | i typed s and pressed tab and it typed the rest including the colon character and space, yes |
| 08:59:14 | <cheater> | ski: ok, so you're saying there's a good reason to have delet |
| 08:59:43 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 09:00:18 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 09:04:24 | <ski> | well .. afaiui, the intent was neither of those two situations, but rather something like `let x = ...; myHof callback = ..x..(forget x in ..callback..).. in myHof (..x..)' |
| 09:04:47 | × | danza quits (~francesco@151.57.49.84) (Ping timeout: 260 seconds) |
| 09:05:22 | <cheater> | i don't understand the structure of the code with your ellipses. could you pastebin it without ellipses please? |
| 09:05:30 | <cheater> | use a simple function that adds integers or something |
| 09:05:48 | <Inst> | how would I implement forB_ :: (Traversable t, Applicative f) => (a -> Maybe (f b) ) -> t a -> f () |
| 09:06:22 | <Inst> | actually, would only need foldable |
| 09:06:23 | <ski> | but, yes, the callback `..x..' would still refer to the definition of `x', even when that `..x..' gets substituted for `x' in the body of `myHof' (namely inside the `forget x in ') .. iow, you'd need to either do some renaming, or else push/distribute the `forget x in ' inwards enough, so that it no longer surrounds the `callback' identifier |
| 09:06:53 | <Inst> | well, easier to do it on lists |
| 09:07:11 | <Inst> | forB_ f [] = pure () |
| 09:07:49 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 09:07:51 | <Inst> | forB_ f (x:xs) = case f x of Nothing -> pure (); Just a -> a >> forB_ f xs |
| 09:08:33 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 09:08:44 | <ski> | cheater : "ok, so you're saying there's a good reason to have delet" -- well, yea, at least from the theoretical standpoint. perhaps not as much from a practical one. but it's a common experience with adjunctions that if you take some uninteresting/trivial construction (here `forget x in ') - often even one that you wouldn't even think to consider - then it may have a quite more interesting adjunction (left |
| 09:08:51 | <ski> | or right, or both) |
| 09:09:20 | <cheater> | i don't really know what an adjunction is |
| 09:09:20 | → | trev joins (~trev@user/trev) |
| 09:09:31 | <Inst> | forB_ :: (Foldable t, Applicative f) => (a -> Maybe (f b) ) -> t a -> f () |
| 09:09:56 | <cheater> | without explaining that and pretty much all of category theory, can you give a motivating example as to why delet is related to existential quantification and let is related to forall? |
| 09:09:56 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 09:10:20 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 09:10:59 | → | igemnace joins (~ian@user/igemnace) |
| 09:11:06 | <Inst> | forB_ f = foldr (\a k -> case f a of Nothing -> pure (); Just b -> b >> k) (pure ()) |
| 09:11:29 | <Inst> | wondering if this is possible to do as a traversable? |
| 09:11:36 | <Inst> | forB ? |
| 09:17:44 | <ski> | @type \f -> getAp . foldMap (maybe empty Ap . f) |
| 09:17:45 | <lambdabot> | (Foldable t, Monoid a1, Alternative f) => (a2 -> Maybe (f a1)) -> t a2 -> f a1 |
| 09:17:49 | <ski> | @type (getAp .) . foldMap . (maybe empty Ap .) |
| 09:17:50 | <lambdabot> | (Foldable t, Monoid a1, Alternative f) => (a2 -> Maybe (f a1)) -> t a2 -> f a1 |
| 09:18:33 | <ski> | @type \f -> getAp . foldMap (maybe empty (Ap . (() <$)) . f) |
| 09:18:35 | <lambdabot> | (Foldable t, Alternative f) => (a -> Maybe (f b)) -> t a -> f () |
| 09:20:18 | <ski> | cheater : "why delet is related to existential quantification and let is related to forall?" -- no. `delet'/`forget' being adjunction to both (right of existential, and left of universal. `exist x --| forget x --| forall x') |
| 09:20:55 | <ski> | Inst : does that work/help ? |
| 09:21:00 | <cheater> | oh duh right yes sorry i get tiny details wrong sometimes |
| 09:21:10 | <ski> | no worry |
| 09:21:11 | <Inst> | whoa, thanks |
| 09:21:20 | <cheater> | so, for that, can you give some sort of motivating example? |
| 09:21:55 | <Inst> | :t maybe |
| 09:21:56 | <lambdabot> | b -> (a -> b) -> Maybe a -> b |
| 09:22:12 | <ski> | two things being adjunctions of each other (left and right adjunctions to each other) is kinda like two things being inverses of each other .. except these are "approximate" inverses (in the sense of approximating from "above", or from "below") |
| 09:22:41 | <Inst> | traverseB_ is more powerful on the foldable level, though |
| 09:23:01 | <Inst> | since not all applicatives have an alternative instance |
| 09:23:42 | <ski> | if you take some statement/proposition `..x..', that depends on a variable `x' (and perhaps also other variables), then `exists x. ..x..' (as well as `forall x. ..x..') is a statement that no longer depends on the variable `x' (it does not has `x' as a free variable, `x' is locally bound) (but it still depends on the rest of the variables, if any) |
| 09:24:36 | <ski> | `forget x' does the opposite, it takes some statement `...' that does *not* depend on a variable `x', and makes a new statement `forget x in ...', that "pretends" to depend on the variable `x' |
| 09:24:59 | × | Guest52 quits (~Guest52@185.57.29.142) (Quit: Client closed) |
| 09:25:15 | <cheater> | i think delet x should be a compiler error in a place where there is no x defined |
| 09:25:51 | <ski> | (in this adjunction situation, we're talking about statements/propositions, iow expressions having some kind of truth-value, so not general expressions. otherwise `forall' and `exists' wouldn't make sense here) |
| 09:26:05 | <Inst> | btw is foldr even designed correctly? |
| 09:26:10 | <Inst> | I had some convos with JSers about it |
| 09:26:17 | <ski> | yes, you can't use `forget x in ...', unless you have defined `x' somewhere in the scope surrounding this statement |
| 09:26:33 | <Inst> | foldr should be foldr :: b -> (a -> b -> b) -> t a -> b |
| 09:26:41 | <Inst> | or at least such a variant should exist |
| 09:27:11 | <ski> | (all free variables in some expression or statement that you use, must be bound (defined, or at least bound as a parameter or something) in the context surrounding the expression/statement) |
| 09:27:23 | <ski> | Inst : whyfore ? |
| 09:28:02 | <Inst> | the entire point of for is that you can write |
| 09:28:15 | <Inst> | for_ struct $ \u -> ... code |
| 09:29:00 | <Inst> | foldr is irritating because I have to either lambda the function or declare the function in a let or where clause |
| 09:29:39 | <cheater> | you can always use pointless style. |
| 09:29:48 | <ski> | ah, sorry, Inst |
| 09:30:04 | <ski> | @type \f -> getAp . foldMap (maybe (pure mempty) Ap . f) |
| 09:30:05 | <lambdabot> | (Foldable t, Applicative f, Monoid a1) => (a2 -> Maybe (f a1)) -> t a2 -> f a1 |
| 09:30:18 | <ski> | @type (getAp .) . foldMap . (maybe (pure mempty) Ap .) |
| 09:30:19 | <lambdabot> | (Foldable t, Applicative f, Monoid a1) => (a2 -> Maybe (f a1)) -> t a2 -> f a1 |
| 09:30:32 | <Inst> | foldFor :: b -> ( a -> b -> b) -> t a -> b or even foldFor :: b -> t a -> ( a -> b -> b) -> b is better |
| 09:30:35 | <ski> | @type \f -> getAp . foldMap (maybe (pure mempty) (Ap . (() <$)) . f) |
| 09:30:36 | <lambdabot> | (Foldable t, Applicative f) => (a -> Maybe (f b)) -> t a -> f () |
| 09:30:39 | <Inst> | I mean I prefer HOF zoo, and I hate foldr |
| 09:30:49 | <ski> | Inst : sorry, didn't think about the `Alternative' |
| 09:31:36 | <Inst> | the idea of all these weird things is say, you have a newbie, you're trying to do Monkey Haskell to minimize on-ramp, and you just tell them "anything you need for for, you just do with foldr, next question?" |
| 09:31:51 | <Inst> | in this case, foldr isn't the right tool |
| 09:32:34 | <ski> | Inst : i see, you want to put the lambda last, like `Foldable t => t a -> r -> (a -> r -> r) -> r' ? |
| 09:32:38 | <Inst> | ya |
| 09:32:42 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 09:33:07 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 09:33:48 | <ski> | or do you have a situation where you'd use, or prefer, `Foldable t => r -> (a -> r -> r) -> t a -> r' ? |
| 09:33:54 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 09:34:17 | <ski> | (presumably where the `t a' input is implicitly passed, e.g. if you're in a composition pipeline) |
| 09:34:33 | <Inst> | bleh, you don't need to help me that much |
| 09:34:50 | <Inst> | I hate foldr, just fantasizing about the scenario wherein I have a Chinese Serokell, emphasis on the Chinese |
| 09:35:04 | <ski> | heh, i'm just curious about why you first put the callback before the collection |
| 09:35:12 | <Inst> | enslaving cheap labor in the Harbin office and making the folks working in the Hangzhou office tearing their hair out at the spaghetti code Harbin is putting out |
| 09:35:47 | <Inst> | (Harbin is economically depressed, has a decent comp sci uni in the neighborhood, and it's freaking freezing half the time since it's on the Russian border) |
| 09:36:17 | <Inst> | (Hangzhou is wealthy and has a good standard of living, so it doesn't make sense to use abusive labor practices there, just dangle the poor folks working in Harbin with the prospect of a transfer out to Hangzhou) |
| 09:36:39 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 09:37:06 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 09:38:07 | <ski> | anyway, note no `Alternative' in these versions |
| 09:40:36 | → | danse-nr3 joins (~danse@151.57.49.84) |
| 09:45:36 | × | danse-nr3 quits (~danse@151.57.49.84) (Remote host closed the connection) |
| 09:47:53 | <ski> | re argument ordering for `foldr' and `foldl' .. in SML, you have |
| 09:48:19 | <ski> | val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b |
| 09:48:22 | <ski> | val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b |
| 09:48:51 | × | mikko quits (~mikko@user/mikko) (Ping timeout: 268 seconds) |
| 09:49:08 | <ski> | (both having the same type. also note that the callback is uncurried/tupled, probably because infix operators, turned into functions with `op', are tupled) |
| 09:50:02 | <ski> | this means that you can just swap out `foldr' for `foldl', or vice versa .. but obviously you'll then process the elements in opposite order |
| 09:50:19 | <ski> | - foldl (op ::) [] [2,3,5,7]; |
| 09:50:31 | <ski> | val it = [7,5,3,2] : int list |
| 09:50:37 | <ski> | - foldr (op ::) [] [2,3,5,7]; |
| 09:50:39 | → | danse-nr3 joins (~danse@151.57.49.84) |
| 09:50:42 | <ski> | val it = [2,3,5,7] : int list |
| 09:51:13 | <ski> | in Haskell |
| 09:51:23 | <ski> | > foldr (:) [] [2,3,5,7] |
| 09:51:24 | <lambdabot> | [2,3,5,7] |
| 09:51:30 | <ski> | > foldl (flip (:)) [] [2,3,5,7] |
| 09:51:32 | <lambdabot> | [7,5,3,2] |
| 09:51:35 | <ski> | because |
| 09:51:52 | <ski> | foldr :: (a -> b -> b) -> b -> [a] -> b |
| 09:52:02 | <ski> | foldl :: (b -> a -> b) -> b -> [a] -> b |
| 09:52:13 | <ski> | otoh, in OCaml, you have |
| 09:52:43 | <ski> | val fold_right : ('a -> 'b -> 'b) -> ('a list -> 'b -> 'b) |
| 09:53:03 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 09:53:13 | <ski> | val fold_left : ('b -> 'a -> 'b) -> ('b -> 'a list -> 'b) |
| 09:53:24 | <ski> | (curried callbacks, this time) |
| 09:53:56 | <ski> | also note that one takes the list last, the other next to last. this is to line up with the callback, so that you can do |
| 09:54:34 | <enikar> | I wonder why they are parentheses around ('a list -> 'b -> 'b) in ocaml ? |
| 09:54:49 | <ski> | # fold_right o fold_right;; |
| 09:55:03 | <ski> | - : ('a -> 'b -> 'b) -> ('a list list -> 'b -> 'b) = <fun> |
| 09:55:08 | <ski> | # fold_left o fold_left ;; |
| 09:55:20 | <ski> | - : ('b -> 'a -> 'b) -> ('b -> 'a list list -> 'b) = <fun> |
| 09:55:29 | <ski> | enikar : i added them in, for emphasis |
| 09:55:46 | <ski> | while, in Haskell, you have to go |
| 09:55:53 | <ski> | @type foldl . foldl |
| 09:55:54 | <lambdabot> | (Foldable t1, Foldable t2) => (b -> a -> b) -> b -> t1 (t2 a) -> b |
| 09:55:56 | <ski> | but |
| 09:56:07 | <ski> | @type foldr . flip . foldr |
| 09:56:08 | <lambdabot> | (Foldable t1, Foldable t2) => (a -> b -> b) -> b -> t1 (t2 a) -> b |
| 09:56:12 | <ski> | or at least |
| 09:56:15 | <ski> | @type foldr . flip . foldr . flip |
| 09:56:16 | <ski> | or |
| 09:56:16 | <lambdabot> | (Foldable t1, Foldable t2) => (b -> a -> b) -> b -> t1 (t2 a) -> b |
| 09:56:21 | <ski> | @type flip . foldr . flip . foldr |
| 09:56:22 | <lambdabot> | (Foldable t1, Foldable t2) => (a -> c -> c) -> t1 (t2 a) -> c -> c |
| 09:56:33 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 09:56:55 | × | aku_ quits (~aku@65.108.245.241) (Remote host closed the connection) |
| 09:57:22 | <ski> | when writing type signatures, i often add in such redundant brackets, to emphasize patterns like that |
| 09:57:33 | <ski> | map :: ( a -> b ) |
| 09:57:38 | <enikar> | ski: ok, I understood |
| 09:57:40 | <ski> | -> ([a] -> [b]) |
| 09:57:59 | → | aku joins (~aku@65.108.245.241) |
| 09:58:22 | <ski> | (making it more obvious when it can be a good idea to partially apply the function, often composing it with itself) |
| 09:58:27 | <ski> | @type mapM . mapM |
| 09:58:28 | <lambdabot> | (Monad m, Traversable t1, Traversable t2) => (a -> m b) -> t1 (t2 a) -> m (t1 (t2 b)) |
| 09:58:33 | <ski> | @type zipWith . zipWith |
| 09:58:34 | <lambdabot> | (a -> b -> c) -> [[a]] -> [[b]] -> [[c]] |
| 09:58:36 | <ski> | &c. |
| 10:03:47 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 10:06:25 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 10:25:55 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds) |
| 10:26:02 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 10:27:24 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:31:39 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 10:35:24 | × | ft quits (~ft@p508db238.dip0.t-ipconnect.de) (Quit: leaving) |
| 10:41:42 | <Inst> | i'm probably going too far in this direction, i.e, it's really easy and trivial to abuse Turing-Church to turn Haskell into Python |
| 10:42:12 | <Inst> | Church-Turing |
| 10:42:24 | × | AlexZenon quits (~alzenon@178.34.163.255) (Ping timeout: 252 seconds) |
| 10:42:58 | × | AlexNoo quits (~AlexNoo@178.34.163.255) (Ping timeout: 246 seconds) |
| 10:43:06 | <Inst> | And in that direction. Julia just has better speed and a more pragmatic philosophy, what's the use of going in that direction if Julia will just have you beat in terms of ergonomics? |
| 10:43:13 | <Inst> | as well as speed |
| 10:48:51 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 10:53:19 | <ski> | how's C-T thesis involved ? |
| 10:57:14 | <Inst> | in the sense that you can make Haskell fake being an imperative language quite well |
| 10:57:15 | <kuribas> | I'd love to see better data science in haskell. |
| 10:57:31 | <kuribas> | There are a lot of interesting libraries, but it is very fragmented. |
| 10:57:47 | <Inst> | all you really need to dumb down haskell would be temporary bindings, do notation, and foldr abuse |
| 10:58:09 | <kuribas> | Boring haskell is already a very nice language. |
| 10:58:39 | <kuribas> | No need for monad stacks, just "Env -> IO a" is good enough for must stuff. |
| 10:59:02 | <ski> | C-T thesis states that every (computable) function is algorithmic (iow can be coded as a finite program, or equivalently, be encoded as a single natural number) |
| 10:59:23 | <ski> | but i guess maybe you had something else in mind, with "Church-Turing" ? |
| 11:00:04 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 268 seconds) |
| 11:00:46 | <Inst> | I mean in the sense that imperative programming and functional programming, at the lowest levels, are equivalent, and it's not that hard to turn Haskell into an imperative language |
| 11:01:26 | <Inst> | it's probably a parlor game at this point |
| 11:01:44 | → | mikko joins (~mikko@user/mikko) |
| 11:03:08 | → | xff0x joins (~xff0x@2405:6580:b080:900:294d:27b0:2606:85c) |
| 11:03:24 | <ski> | oh, so just the equivalence between Church's and Turing's approaches to formalisms for computation |
| 11:05:36 | → | zetef joins (~quassel@5.2.182.99) |
| 11:06:50 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 11:08:05 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 11:10:52 | × | CiaoSen quits (~Jura@2a05:5800:2e6:d500:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 11:10:59 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 272 seconds) |
| 11:14:23 | × | destituion quits (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 11:14:38 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 11:14:44 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 11:18:40 | → | vpark45 joins (~vincent@114.205.107.110) |
| 11:23:27 | → | destituion joins (~destituio@2a02:2121:655:c95b:ba41:7897:d01f:5f0f) |
| 11:23:42 | × | vpark45 quits (~vincent@114.205.107.110) (Quit: leaving) |
| 11:24:20 | → | __monty__ joins (~toonn@user/toonn) |
| 11:27:57 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:29:03 | × | mima quits (~mmh@aftr-62-216-211-133.dynamic.mnet-online.de) (Quit: leaving) |
| 11:32:17 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 11:32:19 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 11:32:39 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 11:32:44 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 11:39:26 | × | sam113101 quits (~sam@24.157.253.231) (Remote host closed the connection) |
| 11:39:50 | → | sam113101 joins (~sam@24.157.253.231) |
| 11:40:40 | × | cayley5 quits (~cayley5@user/phileasfogg) (Quit: Ping timeout (120 seconds)) |
| 11:40:59 | → | cayley5 joins (~cayley5@user/phileasfogg) |
| 11:41:01 | × | michalz quits (~michalz@185.246.207.218) (Read error: Connection reset by peer) |
| 11:41:02 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 11:41:18 | → | michalz joins (~michalz@185.246.207.205) |
| 11:41:23 | × | m1dnight quits (~christoph@82.146.125.185) (Ping timeout: 268 seconds) |
| 11:41:25 | × | henrytill quits (e0180937c3@2a03:6000:1812:100::e8c) (Ping timeout: 256 seconds) |
| 11:41:41 | × | nschoe quits (~nschoe@82-65-202-30.subs.proxad.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 11:41:59 | → | nschoe joins (~nschoe@2a01:e0a:8e:a190:8ccb:4735:e31a:8adf) |
| 11:41:59 | × | conjunctive quits (sid433686@id-433686.helmsley.irccloud.com) (Ping timeout: 256 seconds) |
| 11:43:23 | → | mei joins (~mei@user/mei) |
| 11:44:22 | → | conjunctive joins (sid433686@id-433686.helmsley.irccloud.com) |
| 11:45:27 | → | henrytill joins (e0180937c3@2a03:6000:1812:100::e8c) |
| 11:46:48 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 11:47:38 | → | gmg joins (~user@user/gehmehgeh) |
| 11:49:55 | × | danse-nr3 quits (~danse@151.57.49.84) (Read error: Connection reset by peer) |
| 11:50:49 | → | danse-nr3 joins (~danse@151.43.82.11) |
| 11:53:25 | × | fedorafan quits (~fedorafan@user/fedorafan) (Ping timeout: 272 seconds) |
| 11:56:19 | <cheater> | what fold will take xs = [x1, x2, ... xn] and give me x1 `f` (x2 `f` ... (xn-1 `f` xn) ... ) ? |
| 11:56:59 | <tomsmeding> | :t foldr1 |
| 11:57:00 | <lambdabot> | Foldable t => (a -> a -> a) -> t a -> a |
| 11:57:18 | <cheater> | no |
| 11:57:21 | <cheater> | doesn't look like it |
| 11:57:36 | <int-e> | > foldr1 f [x,y,z] |
| 11:57:37 | <lambdabot> | f x (f y z) |
| 11:57:47 | <cheater> | hmm oh wait |
| 11:57:54 | <cheater> | you're right ty |
| 11:58:01 | → | yin joins (~yin@user/zero) |
| 11:58:55 | × | danse-nr3 quits (~danse@151.43.82.11) (Ping timeout: 246 seconds) |
| 12:03:48 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 252 seconds) |
| 12:04:24 | → | m1dnight joins (~christoph@82.146.125.185) |
| 12:05:21 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 12:10:29 | × | fr33domlover quits (~fr33domlo@towards.vision) (Quit: The Lounge - https://thelounge.chat) |
| 12:14:04 | → | fedorafan joins (~fedorafan@user/fedorafan) |
| 12:14:39 | → | fr33domlover joins (~fr33domlo@towards.vision) |
| 12:19:17 | <cheater> | had to write a total wrapper around it |
| 12:19:22 | <cheater> | but it's fine |
| 12:19:41 | → | CiaoSen joins (~Jura@2a05:5800:2e6:d500:e6b9:7aff:fe80:3d03) |
| 12:24:51 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:27:54 | → | danse-nr3 joins (~danse@151.57.43.153) |
| 12:32:45 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 12:39:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:40:35 | → | omegatron joins (~some@user/omegatron) |
| 12:46:37 | → | actioninja joins (~actioninj@user/actioninja) |
| 12:50:28 | → | akegalj joins (~akegalj@141-136-184-96.dsl.iskon.hr) |
| 13:03:49 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 13:07:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:08:38 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 13:08:58 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 13:16:53 | × | mzg quits (mzg@37.221.213.54) (Quit: Lost terminal) |
| 13:17:01 | <haskellbridge> | <eldritchcookie> do internal libraries get compiled even if my main library doesn't depend on the internal libraries and i don't specifically request for it? |
| 13:17:16 | → | trev joins (~trev@user/trev) |
| 13:20:42 | → | mzg joins (mzg@abusers.hu) |
| 13:22:31 | × | mmhat quits (~mmh@p200300f1c706a2b6ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 13:24:43 | × | yin quits (~yin@user/zero) (Quit: leaving) |
| 13:25:22 | → | yin joins (~yin@user/zero) |
| 13:31:54 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 13:34:37 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 13:39:12 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 13:41:24 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:49:35 | → | triceraptor joins (~prodmezha@123.63.203.210) |
| 13:49:51 | → | Lycurgus joins (~georg@li1192-118.members.linode.com) |
| 13:49:52 | × | Lycurgus quits (~georg@li1192-118.members.linode.com) (Changing host) |
| 13:49:52 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 13:50:32 | × | triceraptor quits (~prodmezha@123.63.203.210) (Remote host closed the connection) |
| 13:50:48 | → | hallucinagen joins (~prodmezha@123.63.203.210) |
| 13:51:15 | → | ystael joins (~ystael@user/ystael) |
| 13:51:49 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 14:03:32 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 14:08:09 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 14:15:28 | <mesaoptimizer> | Sandy Maguire has two books focused on Haskell: _Thinking in Types_ and _Algebra-Driven Design_. Does the latter supersede the former? Do you need to read the former to read the latter? |
| 14:20:08 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 14:23:10 | × | califax quits (~califax@user/califx) (Ping timeout: 260 seconds) |
| 14:23:29 | → | trev joins (~trev@user/trev) |
| 14:24:02 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 14:38:37 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 14:46:38 | <c_wraith> | They're pretty independent |
| 14:47:24 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 14:47:42 | → | trev joins (~trev@user/trev) |
| 14:47:46 | <c_wraith> | Not completely, because Algebra-Driven design does talk a lot about precise domain types. But they have different focuses and goals. |
| 14:48:15 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 14:49:15 | × | trev quits (~trev@user/trev) (Client Quit) |
| 14:50:01 | → | trev joins (~trev@user/trev) |
| 14:52:52 | × | adanwan_ quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 14:53:13 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 14:54:37 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 14:55:11 | → | califax joins (~califax@user/califx) |
| 14:55:26 | × | michalz quits (~michalz@185.246.207.205) (Quit: ZNC 1.8.2 - https://znc.in) |
| 14:58:26 | → | michalz joins (~michalz@185.246.207.205) |
| 15:13:31 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 268 seconds) |
| 15:22:46 | × | danse-nr3 quits (~danse@151.57.43.153) (Ping timeout: 268 seconds) |
| 15:26:57 | → | shapr joins (~user@c-24-218-186-89.hsd1.ma.comcast.net) |
| 15:31:00 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 15:42:35 | × | hallucinagen quits (~prodmezha@123.63.203.210) (Ping timeout: 264 seconds) |
| 15:43:58 | → | danse-nr3 joins (~danse@151.57.43.153) |
| 15:45:10 | <mesaoptimizer> | sweet, thank you |
| 15:49:54 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds) |
| 15:50:40 | → | ars23 joins (~ars23@79.114.26.206) |
| 15:50:59 | × | ars23 quits (~ars23@79.114.26.206) (Changing host) |
| 15:50:59 | → | ars23 joins (~ars23@user/ars23) |
| 15:51:08 | × | CiaoSen quits (~Jura@2a05:5800:2e6:d500:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 15:52:56 | × | ars23 quits (~ars23@user/ars23) (Client Quit) |
| 15:56:19 | → | lovasko joins (~lovasko@178.197.161.134) |
| 15:56:49 | × | lovasko quits (~lovasko@178.197.161.134) (Client Quit) |
| 15:57:39 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 15:57:48 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Client Quit) |
| 15:59:20 | → | rvalue joins (~rvalue@user/rvalue) |
| 16:01:18 | → | hallucinagen joins (~prodmezha@123.63.203.210) |
| 16:03:29 | → | ars23 joins (~ars23@79.114.26.206) |
| 16:03:40 | × | ars23 quits (~ars23@79.114.26.206) (Changing host) |
| 16:03:40 | → | ars23 joins (~ars23@user/ars23) |
| 16:04:23 | → | ania123 joins (~ania123@94-43-231-47.dsl.utg.ge) |
| 16:12:23 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:14:33 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 256 seconds) |
| 16:19:38 | → | rvalue joins (~rvalue@user/rvalue) |
| 16:21:47 | <c_wraith> | On a scale of "why?" to "what's wrong with you?", how bad is it to execute cabal clean from inside a program being run with cabal run? |
| 16:23:16 | <danse-nr3> | no i mean it is good you are helping cabal devs with such interesting corner cases |
| 16:23:36 | → | tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 16:26:10 | <c_wraith> | I'm pretty sure it can't even work on windows |
| 16:26:28 | <c_wraith> | since windows locks the file associated with running executables. |
| 16:26:46 | <c_wraith> | On linux it might accidentally work. |
| 16:26:51 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 255 seconds) |
| 16:27:38 | → | rvalue joins (~rvalue@user/rvalue) |
| 16:29:22 | × | danse-nr3 quits (~danse@151.57.43.153) (Ping timeout: 268 seconds) |
| 16:29:52 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:29:55 | → | danse-nr3 joins (~danse@151.57.89.156) |
| 16:31:26 | → | rvalue- joins (~rvalue@user/rvalue) |
| 16:32:45 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 16:33:08 | × | harveypwca quits (~harveypwc@2601:246:c200:2740:15b6:f225:14ff:9821) (Quit: Leaving) |
| 16:35:24 | rvalue- | is now known as rvalue |
| 16:37:17 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Quit: WeeChat 4.1.2) |
| 16:37:59 | → | lovasko joins (~lovasko@213.208.157.36) |
| 16:38:52 | × | danse-nr3 quits (~danse@151.57.89.156) (Quit: Leaving) |
| 16:39:16 | → | danse-nr3 joins (~danse-nr3@151.57.89.156) |
| 16:39:54 | <lovasko> | How would I go about writing a Storable instance for a type that contains a MutableByteArray#? Given a pinned array, I can write the poke function simply by getting the Addr# of the byte array and wrapping it with the Ptr constructor. But how do I implement the peek function? |
| 16:40:28 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 16:43:55 | <c_wraith> | Does the C side contain an arbitrary pointer that you want to make into a MutableByteArray? |
| 16:44:02 | <c_wraith> | Because... yeah, that's not going to work. |
| 16:44:26 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:44:54 | <cheater> | i have a bunch of values, each of which has a different type - v1 :: T1, v2 :: T2, v3 :: T3, and so on. and i have a value z which has a type that is a type level list of '[T0]. I have a function called + which can take a value that's of type '[Tm...Tn] and a value that's of type Tk and produce a value of type '[Tm...Tn, Tk]. I am currently adding all these values by doing z + v1 + v2 + ... . how can i write a fold that works with that sort of setup? |
| 16:45:13 | → | ph88 joins (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 16:46:28 | → | rvalue joins (~rvalue@user/rvalue) |
| 16:46:30 | <c_wraith> | cheater: seems difficult unless you involve existential wrapping. In which case it seems difficult to work with the result. |
| 16:47:06 | <cheater> | idk what that means |
| 16:47:12 | <cheater> | hmm |
| 16:47:29 | <lovasko> | c_wraith : it is in the context of a recvmsg syscall, where I have an already created MutableByteArray# and I want the syscall to write into it |
| 16:48:32 | × | ph88 quits (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 16:48:36 | <c_wraith> | lovasko: ah, then it's possible, but Storable isn't the interface to do it. It doesn't let you depend on additional information like you'd need to. |
| 16:49:05 | <lovasko> | wouldn't an FFI call require a Storable instance for anything it is passing in-between the boundaries? |
| 16:49:31 | → | Square joins (~Square4@user/square) |
| 16:49:53 | <c_wraith> | Yes, but you could do the marshalling to/from Ptr with your own code, and only require the FFI do work with it. |
| 16:49:59 | → | rvalue- joins (~rvalue@user/rvalue) |
| 16:50:32 | <lovasko> | so I would prepare the structure with the Ptr of the existing MBA# |
| 16:50:42 | → | ph88 joins (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 16:50:48 | <lovasko> | through mutableByteArrayContents# |
| 16:50:59 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 264 seconds) |
| 16:51:06 | <c_wraith> | Depends on exactly the workflow you want. |
| 16:51:13 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 16:51:23 | <c_wraith> | But the main thing is that you'd have to do more work yourself, and leave less to the FFI |
| 16:52:22 | <lovasko> | so my "mapping structure", in this case an IOVector (equivalent of struct iovec) would contain a "Ptr Word8" or something like that instead of the MBA# instance |
| 16:52:22 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 16:52:54 | <lovasko> | and I should pass that to FFI, because it is Storable, but then, because it points to the same memory, I can start using the MBA# as if it contains the data |
| 16:53:47 | rvalue- | is now known as rvalue |
| 16:54:19 | <c_wraith> | when doing this sort of thing, also remember to keep track of what heap data was allocated on. You don't want memory leaking because you're trying to free stuff on the wrong heap. |
| 16:54:46 | → | mei joins (~mei@user/mei) |
| 16:55:18 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds) |
| 16:55:23 | <lovasko> | could you point me more directly to the heap issue? I expect that the MBA# is located on its own heap, and then the pointer is created through some form of "alloca" call |
| 16:57:19 | <c_wraith> | More precisely, it's allocated on the GHC heap. If you always do allocating on the GHC heap, great. But if you ever end up allocating something on the C heap, you need to free it from the C heap. |
| 16:57:53 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 16:58:02 | → | rvalue- joins (~rvalue@user/rvalue) |
| 16:58:27 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 17:01:52 | rvalue- | is now known as rvalue |
| 17:05:08 | × | hallucinagen quits (~prodmezha@123.63.203.210) (Quit: Leaving) |
| 17:06:41 | × | tv quits (~tv@user/tv) (Ping timeout: 245 seconds) |
| 17:08:36 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:8aa0:2a1c:7c77:360a) (Quit: ubert) |
| 17:08:55 | → | igemnace joins (~ian@user/igemnace) |
| 17:09:51 | → | a51 joins (a51@gateway/vpn/protonvpn/a51) |
| 17:11:42 | × | danse-nr3 quits (~danse-nr3@151.57.89.156) (Ping timeout: 256 seconds) |
| 17:12:41 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 17:13:02 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 260 seconds) |
| 17:14:43 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 17:18:46 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1) |
| 17:20:17 | × | lovasko quits (~lovasko@213.208.157.36) (Quit: Client closed) |
| 17:21:28 | → | tv joins (~tv@user/tv) |
| 17:21:47 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 17:29:35 | → | rvalue joins (~rvalue@user/rvalue) |
| 17:36:54 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 17:37:16 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 17:37:19 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 17:38:23 | × | ars23 quits (~ars23@user/ars23) (Ping timeout: 264 seconds) |
| 17:38:59 | → | rvalue joins (~rvalue@user/rvalue) |
| 17:40:00 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:43:47 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 17:44:59 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 264 seconds) |
| 17:47:13 | → | ars23 joins (~ars23@79.114.26.206) |
| 17:47:36 | ars23 | is now known as Guest1680 |
| 17:48:19 | → | danse-nr3 joins (~danse-nr3@151.57.89.156) |
| 17:52:50 | → | rvalue joins (~rvalue@user/rvalue) |
| 17:57:59 | <cheater> | doing things on the cheap usually ends up costing more in the long run |
| 18:02:29 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 18:03:09 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:03:43 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 18:03:44 | × | sawilagar quits (~sawilagar@user/sawilagar) (Client Quit) |
| 18:07:18 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 18:15:05 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 18:24:37 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:26:04 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 18:33:26 | → | rvalue joins (~rvalue@user/rvalue) |
| 18:33:39 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 18:34:48 | × | ania123 quits (~ania123@94-43-231-47.dsl.utg.ge) (Quit: Client closed) |
| 18:37:58 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 18:38:42 | × | danse-nr3 quits (~danse-nr3@151.57.89.156) (Ping timeout: 255 seconds) |
| 18:40:21 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 18:40:54 | → | Square2 joins (~Square@user/square) |
| 18:45:15 | → | rvalue joins (~rvalue@user/rvalue) |
| 18:51:15 | → | y04nn joins (~username@2a03:1b20:8:f011::e10d) |
| 19:05:22 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 19:05:36 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:06:19 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 19:06:32 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Ping timeout: 260 seconds) |
| 19:08:08 | → | a51 joins (~a51@modemcable048.127-56-74.mc.videotron.ca) |
| 19:10:30 | → | ft joins (~ft@p508db238.dip0.t-ipconnect.de) |
| 19:12:52 | → | r5c4571lh01987 joins (rscastilho@179.221.142.47) |
| 19:13:15 | × | infinity0 quits (~infinity0@pwned.gg) (Killed (zirconium.libera.chat (Nickname regained by services))) |
| 19:16:53 | → | infinity0 joins (~infinity0@pwned.gg) |
| 19:20:04 | × | r5c4571lh01987 quits (rscastilho@179.221.142.47) (Remote host closed the connection) |
| 19:20:48 | × | wryishly quits (~wryish@2605:4c40:119:efa3:0:727d:19eb:1) (Quit: %blank%) |
| 19:21:00 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 19:21:04 | → | wryish joins (~wryish@2605:4c40:119:efa3:0:727d:19eb:1) |
| 19:21:41 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 19:23:51 | × | a51 quits (~a51@modemcable048.127-56-74.mc.videotron.ca) (Quit: WeeChat 4.2.1) |
| 19:30:40 | × | Square quits (~Square4@user/square) (Ping timeout: 268 seconds) |
| 19:33:09 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:36:25 | × | dhil quits (~dhil@2001:8e0:2014:3100:348d:fdf8:7e1e:8e9) (Quit: Leaving) |
| 19:36:41 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 19:37:17 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 240 seconds) |
| 19:37:34 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:39:53 | × | omegatron quits (~some@user/omegatron) (Quit: Power is a curious thing. It can be contained, hidden, locked away, and yet it always breaks free.) |
| 19:41:54 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 19:42:21 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 19:43:53 | <energizer> | what terms describe a function where the return type is the same as the argument type? |
| 19:45:52 | <geekosaur> | endofunction |
| 19:46:43 | <ncf> | or endomorphism |
| 19:46:53 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 19:49:53 | <tomsmeding> | % :i Endo |
| 19:49:53 | <yahb2> | <interactive>:1:1: error: Not in scope: ‘Endo’ |
| 19:49:55 | <tomsmeding> | % :i Data.Monoid.Endo |
| 19:49:55 | <yahb2> | type base-4.16.4.0:Data.Semigroup.Internal.Endo :: * -> * ; newtype base-4.16.4.0:Data.Semigroup.Internal.Endo a ; = base-4.16.4.0:Data.Semigroup.Internal.Endo {base-4.16.4.0:Data.Semigroup.Inter... |
| 19:50:03 | <tomsmeding> | % :m +Data.Monoid |
| 19:50:03 | <yahb2> | <no output> |
| 19:50:05 | <tomsmeding> | % :i Data.Monoid.Endo |
| 19:50:05 | <yahb2> | type Endo :: * -> * ; newtype Endo a = Endo {appEndo :: a -> a} ; -- Defined in ‘base-4.16.4.0:Data.Semigroup.Internal’ ; instance Monoid (Endo a) ; -- Defined in ‘base-4.16.4.0:Data.Semigroup... |
| 19:54:04 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 19:57:26 | → | isovector joins (~isovector@172.103.235.56) |
| 19:57:44 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 19:58:13 | → | johnw joins (~johnw@69.62.242.138) |
| 19:58:42 | <isovector> | @pointful ((runIdentity) .) <$> matchRuleM (\a b -> (Identity .) <$> matchChild a b) g d1 |
| 19:58:42 | <lambdabot> | ((\ g x -> runIdentity (g x)) <$> matchRuleM (\ a b -> (\ g x -> (Identity) (g x)) <$> matchChild a b) g d1) |
| 20:01:31 | → | mmhat joins (~mmh@p200300f1c706a2a6ee086bfffe095315.dip0.t-ipconnect.de) |
| 20:01:52 | → | AlexNoo joins (~AlexNoo@94.233.240.255) |
| 20:05:40 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 20:06:53 | → | AlexZenon joins (~alzenon@94.233.240.255) |
| 20:08:56 | × | mmhat quits (~mmh@p200300f1c706a2a6ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.2.1) |
| 20:10:00 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 252 seconds) |
| 20:13:53 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 20:14:08 | <tomsmeding> | that did not do much |
| 20:14:11 | → | tri joins (~tri@4133220a.cst.lightpath.net) |
| 20:14:56 | tomsmeding | wonders why runIdentity, which had redundant parens in the source, is normal in the output while Identity got new redundant parens |
| 20:15:26 | <tri> | hello, im trying to wrap my head around monad transformer. Im using Reader, and return a Maybe. So I don't know if I should use ReaderT with Maybe as the outer monad, or MaybeT with Reader as the outer monad. Could anyone help me please |
| 20:16:18 | → | mei joins (~mei@user/mei) |
| 20:16:43 | <dolio> | For those two it doesn't make any difference. |
| 20:17:44 | <tri> | it's more straight forward when I have an Async operation that returns an optional value (a Maybe monad). This case i would have a MaybeT, and Async monad as the outer. I can think of it as 2 layers that i need to peel. But I can't think about reader |
| 20:19:12 | × | isovector quits (~isovector@172.103.235.56) (Quit: Client closed) |
| 20:19:45 | <tri> | dolio: is it because for Async and Maybe both focus on the output, so the order is important. That is, an asynchronous operation returning an optional value would correspond to a MaybeT with outer Async monad |
| 20:20:03 | <tri> | dolio: but Reader is about input, and Maybe is output, so it doesn't matter as you said? |
| 20:20:08 | <dolio> | @unmtl MaybeT (Reader R) A |
| 20:20:08 | <lambdabot> | R -> Maybe A |
| 20:20:15 | <dolio> | @unmtl ReaderT R Maybe A |
| 20:20:15 | <lambdabot> | R -> Maybe A |
| 20:21:09 | <tri> | dolio: could you confirm my intuition please? |
| 20:22:12 | <c_wraith> | No, it's about Reader specifically. |
| 20:22:57 | <c_wraith> | It tends to commute with most transformers, because it doesn't do anything |
| 20:22:59 | <tri> | like if the 2 monads are both about output, like Maybe and Either, then the order is important. As in Async and Maybe, in that I first make a network call, only after that i will have an optional result. So therefore a MaybeT with outer Async monad |
| 20:23:15 | <tri> | i mean maybe and Async, not either |
| 20:24:04 | <tri> | hmm ok thank you both, i will just use it like that without really understand for now |
| 20:24:22 | <dolio> | It's because ReaderT R M adds `R ->` outside M, and MaybeT M adds Maybe inside M, so they end up as exactly the same thing. |
| 20:24:47 | <tri> | dolio: ah ok thank you |
| 20:25:02 | ncf | wonders if there's anything clever to be said about this |
| 20:25:29 | <ncf> | postcomposition commutes with precomposition, i guess |
| 20:25:40 | × | ystael quits (~ystael@user/ystael) (Quit: Lost terminal) |
| 20:25:48 | <tri> | dolio: the same also applies for, say State and Either right? |
| 20:25:56 | <ncf> | no! |
| 20:26:03 | <dolio> | No, those end up different. |
| 20:26:23 | <tri> | oh i thought state puts the state outside, like `S ->` |
| 20:26:24 | <dolio> | StateT actually puts things both inside and outside. |
| 20:26:42 | <dolio> | S -> M (S, A) |
| 20:27:17 | <tri> | '=( |
| 20:27:48 | → | ystael joins (~ystael@user/ystael) |
| 20:28:27 | <tomsmeding> | there is an alternative version of a state monad transformer that does 'S -> (S, M A)' |
| 20:28:40 | <tomsmeding> | it's _different_ from the usual StateT, but in some cases it is what you want (usually not) |
| 20:29:01 | <c_wraith> | That seems really restrictive - the state modifications can't depend on M actions. |
| 20:29:01 | <tomsmeding> | that one does put stuff on the outside only :) |
| 20:29:35 | <tomsmeding> | if M = Either e, then it essentially means "there is still sensible state to return even if an error occurred" |
| 20:29:46 | <tomsmeding> | which could be true, in principle |
| 20:29:52 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 20:30:27 | <ncf> | tomsmeding: wait how does join work |
| 20:31:08 | <tomsmeding> | @djinn (s -> (s, s -> (s, a))) -> s -> (s, a) |
| 20:31:08 | <lambdabot> | f a b = |
| 20:31:08 | <lambdabot> | case a b of |
| 20:31:08 | <lambdabot> | (c, d) -> d c |
| 20:31:28 | <tomsmeding> | just pass on the state? |
| 20:31:44 | <ncf> | oh |
| 20:31:58 | <tomsmeding> | I don't think the m changes things |
| 20:32:52 | <ncf> | RWMRWM → RWRMWM → RMWM → RMMW → RMW |
| 20:32:56 | <ncf> | you don't get RWM at the end |
| 20:33:20 | <ncf> | by R i mean (s →) and by W i mean (s, ) |
| 20:33:37 | <tomsmeding> | oh |
| 20:33:43 | <tomsmeding> | hm |
| 20:34:13 | <energizer> | https://stackoverflow.com/a/3275233 says the way to divide two ints into a float is (fromIntegral a) / (fromIntegral b) but |
| 20:34:16 | <energizer> | :t (fromIntegral 1) / (fromIntegral 2) |
| 20:34:17 | <lambdabot> | Fractional a => a |
| 20:34:23 | <energizer> | which isnt a float afaict |
| 20:34:36 | <tomsmeding> | Float is an instance of Fractional |
| 20:34:44 | <tomsmeding> | Double also is, as is Rational! |
| 20:34:55 | <tomsmeding> | > fromIntegral 1 / fromIntegral 2 :: Double |
| 20:34:56 | <lambdabot> | 0.5 |
| 20:34:59 | <tomsmeding> | > fromIntegral 1 / fromIntegral 2 :: Rational |
| 20:35:00 | <lambdabot> | 1 % 2 |
| 20:35:13 | <energizer> | how do i find out what type fromIntegral 1 / fromIntegral 2 has, or does it not have one? |
| 20:35:22 | <tomsmeding> | it has one: Fractional a => a |
| 20:35:24 | <tomsmeding> | ;) |
| 20:35:27 | <tomsmeding> | :t (+) |
| 20:35:28 | <lambdabot> | Num a => a -> a -> a |
| 20:35:56 | <tomsmeding> | (+) also has a type: for any type 'a' that implements the Num type class (very roughly: "is a numeric-ish type"), it takes two of those and returns another one |
| 20:36:06 | <tomsmeding> | :t fromIntegral |
| 20:36:07 | <lambdabot> | (Integral a, Num b) => a -> b |
| 20:36:07 | <energizer> | but it doesnt have a concrete type until the context requires it to have one? |
| 20:36:10 | <tomsmeding> | yes |
| 20:36:31 | <tomsmeding> | that's precisely right |
| 20:36:37 | <energizer> | what is the haskell word for 'concrete type' |
| 20:36:39 | <tomsmeding> | the technical word for "concrete" here is "monomorphic" |
| 20:36:43 | <tomsmeding> | i.e. "not polymorphic" |
| 20:37:30 | <EvanR> | unpolymorphic |
| 20:37:34 | <tomsmeding> | fromIntegral is a polymorphic function, and the expression "fromIntegral 1 / fromIntegral 2" does not narrow things down enough yet, so the whole thing is still polymorphic |
| 20:37:56 | <tomsmeding> | :t (/) |
| 20:37:57 | <lambdabot> | Fractional a => a -> a -> a |
| 20:38:36 | <tomsmeding> | the reason why you don't get a Num constraint in the type of that thing (as you may expect from the type of 'fromIntegral') is that Num is a superclass of Fractional: every type that implements Fractional also implements Num |
| 20:39:20 | <ncf> | so the WriterT join goes MWMW → MMWW by strength → MW, the ReaderT join goes RMRM → RRMM by costrength → RM |
| 20:39:34 | <ncf> | and the StateT join goes RMWRMW → RMMW by counit → RMW |
| 20:41:39 | <ncf> | there's something almost geometric about this. falling to the left, falling to the right, falling through the middle |
| 20:42:29 | <tomsmeding> | I'm doing something wrong |
| 20:42:31 | <tomsmeding> | @djinn Monad m => (s -> (s, m a)) -> (a -> s -> (s, m b)) -> s -> (s, m b) |
| 20:42:31 | <lambdabot> | f a b c = |
| 20:42:31 | <lambdabot> | case a c of |
| 20:42:31 | <lambdabot> | (d, e) -> (d, |
| 20:42:31 | <lambdabot> | e >>= (\ f -> |
| 20:42:31 | <lambdabot> | case b f d of |
| 20:42:32 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 20:42:33 | <lambdabot> | (_, g) -> g)) |
| 20:42:39 | <tomsmeding> | @djinn Monad m => (s -> (s, m (s -> (s, m a)))) -> s -> (s, m a) |
| 20:42:39 | <lambdabot> | -- f cannot be realized. |
| 20:42:52 | <tomsmeding> | and yet join == (>>= id)? |
| 20:43:16 | <tomsmeding> | oh |
| 20:43:23 | <tomsmeding> | because the """bind""" is ignoring some outputs |
| 20:43:38 | <ncf> | ha |
| 20:43:40 | <tomsmeding> | okay maybe I was mistaken :) |
| 20:43:54 | <ncf> | we need a linear djinn :^) |
| 20:44:09 | <c_wraith> | djinn tries to be linear. It just doesn't report when it fails |
| 20:44:30 | <dolio> | djinn also doesn't do polymorphism. |
| 20:45:26 | <tomsmeding> | to keep it decidable, presumably |
| 20:45:36 | → | dmj` joins (sid72307@id-72307.hampstead.irccloud.com) |
| 20:45:41 | <ncf> | in a sense it does rank-1 polymorphism i guess |
| 20:45:47 | <dolio> | So, your Monad constraint isn't going to give it license to do instantiate the parameters however it wants. |
| 20:45:57 | <ncf> | oh |
| 20:45:58 | <tomsmeding> | no, but it does give it license to use >>=, apparently |
| 20:46:33 | <tomsmeding> | and there is nothing else (well, apart from 'return') that it _could_ derive from the constraint anyway |
| 20:46:34 | <dolio> | Yes, but only if the input is exactly `m a` or something. |
| 20:46:37 | <tomsmeding> | so it seems to be doing it fine? |
| 20:46:41 | <tomsmeding> | oh |
| 20:46:48 | <tomsmeding> | I see |
| 20:47:00 | <dolio> | So, it can't use bind with `m (s -> (s, m a))` in your second example. |
| 20:47:16 | <tomsmeding> | that's unfortunate |
| 20:48:22 | <tomsmeding> | right, there is a bind and it has the same dumb behaviour as >>= |
| 20:48:24 | <tomsmeding> | of course |
| 20:48:32 | <tomsmeding> | interesting, thanks dolio :) |
| 20:48:54 | <dolio> | I still think your proposed transformer is pretty suspicious. |
| 20:49:00 | <tomsmeding> | yes certainly |
| 20:49:02 | <dolio> | It's throwing state out in places. |
| 20:49:08 | <tomsmeding> | hence my multiple scare quotes around "bind" |
| 20:49:19 | <tomsmeding> | I stand corrected that this is a (sensible) monad transformer |
| 20:49:27 | <ncf> | yeah that's certainly not gonna pass the monad laws |
| 20:49:46 | <dolio> | So it's not clear to me that it's going to actually satisfy various rules. Likely not the state rules. |
| 20:49:49 | <tomsmeding> | (to me defense, it was someone else (a mathematician) who said something to the effect) |
| 20:50:11 | <tomsmeding> | no it's certainly not going to work, or otherwise the laws are too weak :p |
| 20:50:19 | geekosaur | misses exference, btb |
| 20:50:44 | → | siw5ohs0 joins (~aiw5ohs0@user/aiw5ohs0) |
| 20:51:34 | ← | siw5ohs0 parts (~aiw5ohs0@user/aiw5ohs0) (Leaving) |
| 20:52:17 | <tri> | hi guys, in a ReaderT SomeEnv (Maybe Text), how can i return a Nothing value to indicate there is no Text? |
| 20:52:33 | <Rembane> | pure Nothing |
| 20:52:36 | <tri> | it works if the last expression is return "Something" |
| 20:52:44 | <ncf> | join (return ma) = (\s. (s, (snd . ($ s)) <$> ma)) ≠ ma |
| 20:53:17 | <ncf> | tri: empty? |
| 20:53:31 | <ncf> | Rembane: that would work with ReaderT SomeEnv m (Maybe Text) |
| 20:53:38 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 20:53:41 | <ncf> | tri: or lift Nothing |
| 20:55:16 | <tri> | ah lift |
| 20:55:23 | <Rembane> | ncf: Oh, a classic off by m error |
| 20:55:36 | <ncf> | :p |
| 20:55:43 | <tri> | thanks everyone |
| 20:56:05 | <tri> | im working in F# so it's a bit hard to go back and forth between F# and Haskell |
| 20:56:12 | <EvanR> | you can instantiate the type Monad m => whatever(m) however you want, but it doesn't mean the resulting type has any inhabitants |
| 20:56:16 | × | Square2 quits (~Square@user/square) (Remote host closed the connection) |
| 20:58:12 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 20:58:16 | × | sp1ff quits (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 20:58:25 | <EvanR> | (Odd n, PerfectNumber n) => The n |
| 20:58:37 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 20:59:05 | <tomsmeding> | is it possible to write something on the ... (or some other place) to make this typecheck? foo :: forall f. (..., Coercible a b) => f a -> f b; foo = coerce |
| 20:59:34 | <tomsmeding> | notable is that 'f' is _not_ a Functor, but it could be some constrained functor (it admits only unboxable type parameters) |
| 21:00:13 | <tomsmeding> | Coercible1? |
| 21:00:56 | <tomsmeding> | (the ghc error here is that it cannot know the roles of f; question is: can I require f to have certain roles here? I think I can't) |
| 21:01:53 | × | rvalue quits (~rvalue@user/rvalue) (Quit: ZNC - https://znc.in) |
| 21:06:18 | × | trev quits (~trev@user/trev) (Ping timeout: 255 seconds) |
| 21:08:28 | <tri> | inside a do notation of the monad ReaderT Environment (Maybe Text), I'd like to use a function of type Reader Environment (Maybe ()). How can i use it please? |
| 21:09:06 | <EvanR> | :t lift |
| 21:09:07 | × | motherfsck quits (~motherfsc@user/motherfsck) (Quit: quit) |
| 21:09:07 | <lambdabot> | (MonadTrans t, Monad m) => m a -> t m a |
| 21:09:21 | <dolio> | Yeah, I don't think there's role abstraction. |
| 21:09:43 | <EvanR> | hmm... doesn't exactly fit |
| 21:09:45 | <tomsmeding> | tri: are you sure there's no typo in that? 'Maybe Text' is not suitable as the second argument of a ReaderT |
| 21:09:53 | <dolio> | What you're asking for was how I thought things should be structured instead of roles way back. |
| 21:10:00 | → | rvalue joins (~rvalue@user/rvalue) |
| 21:10:13 | <tomsmeding> | dolio: I see :) |
| 21:10:27 | <tomsmeding> | I don't _need_ it, was just nice, so it's ok |
| 21:10:50 | <tri> | tomsmeding: actually i arbitrarily used Text to make it concrete, because i thought only the part ReaderT Environment Maybe is important |
| 21:10:58 | × | Guest1680 quits (~ars23@79.114.26.206) (Quit: Leaving) |
| 21:11:22 | <ncf> | did you mean ReaderT Environment Maybe Text |
| 21:12:17 | <tri> | ncf: actually im inside the do notation of ReaderT Environment Maybe (), and im trying to use the function type Reader Environment () |
| 21:12:57 | <tri> | is it even possible? |
| 21:13:14 | <ncf> | Reader e is just ReaderT e Identity, so you might need something like hoistReaderT |
| 21:13:29 | <ncf> | er that's not a thing |
| 21:13:48 | <ncf> | what am i looking for |
| 21:13:59 | <ncf> | ah, mapReaderT |
| 21:14:05 | <tomsmeding> | tri: 'ReaderT Environment Maybe Text' is not the same as 'ReaderT Environment (Maybe Text)' ;) |
| 21:14:37 | <tri> | tomsmeding: yea sorry, i was just trying to emphasize Text belongs to Maybe monad for clarity (but it backed fire) |
| 21:15:15 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 21:15:32 | <tomsmeding> | :t Control.Monad.Trans.Reader.mapReaderT |
| 21:15:33 | <lambdabot> | (m a -> n b) -> ReaderT r m a -> ReaderT r n b |
| 21:15:49 | <tomsmeding> | where the function is \(Identity x) -> return x |
| 21:17:29 | <tomsmeding> | @djinn Monad m => (r -> a) -> (r -> m a) |
| 21:17:29 | <lambdabot> | f a b = return (a b) |
| 21:17:42 | <tomsmeding> | er |
| 21:18:08 | <tomsmeding> | @djinn Monad m => (Environment -> Maybe ()) -> (Environment -> Maybe ()) |
| 21:18:08 | <lambdabot> | Error: Undefined type Environment |
| 21:18:12 | <tomsmeding> | lol |
| 21:18:24 | <ncf> | generalize from mmorph might be useful https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html#v:generalize |
| 21:18:38 | <tomsmeding> | unwrapping newtypes, this is id |
| 21:18:38 | <ncf> | (and then you can actually use hoist instead of mapReaderT) |
| 21:24:39 | <tri> | ncf: yea i was thinking about hoist |
| 21:25:07 | <tri> | i don't know how to word this correctly, i mean i don't even know what question i should ask follow up |
| 21:25:25 | <tri> | but i know hoist would add the outer monad around reader, in this case Maybe |
| 21:25:52 | <tri> | then you introduce mapReaderT, and that's completely new to me |
| 21:26:03 | <ncf> | hoist = mapReaderT |
| 21:26:03 | <tri> | so is mapReaderT same as hoist? |
| 21:26:08 | <tri> | ah |
| 21:27:33 | <ncf> | (hoist is part of a typeclass that has a ReaderT instance) |
| 21:29:35 | → | harveypwca joins (~harveypwc@2601:246:c200:2740:15b6:f225:14ff:9821) |
| 21:30:23 | <tri> | thank you |
| 21:30:55 | <tri> | everytime i come here and ask something, i'd be immediately lost after the first or second answer |
| 21:31:07 | <tri> | you guys are something else |
| 21:31:16 | <tri> | in a good way |
| 21:31:37 | <tri> | but really appreciate the enthusiasm |
| 21:33:40 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:36:09 | → | Square joins (~Square4@user/square) |
| 21:39:39 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 252 seconds) |
| 21:40:58 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 255 seconds) |
| 21:47:51 | × | akegalj quits (~akegalj@141-136-184-96.dsl.iskon.hr) (Remote host closed the connection) |
| 21:48:28 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:03:20 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 22:22:06 | <[Leary]> | tomsmeding: Consider `type Representational f = (forall a b. Coercible a b => Coercible (f a) (f b)) :: Constraint` |
| 22:23:47 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 22:30:19 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 22:31:40 | → | gmg joins (~user@user/gehmehgeh) |
| 22:35:20 | <[Leary]> | cheater: You can write e.g. `hfoldr :: (forall x xs. c x => f x -> r xs -> r (x:xs)) -> r '[] -> (forall xs. HList c f xs -> r xs)`, but I'm not sure it will fit your use case. |
| 22:35:55 | <cheater> | interesting, thank you |
| 22:36:38 | <shapr> | @quote |
| 22:36:39 | <lambdabot> | desrt says: man... there's this whole dark side to haskell that dr. kahl didn't teach us in 3e03 |
| 22:36:50 | → | Square2 joins (~Square@user/square) |
| 22:37:25 | <geekosaur> | ob https://www.tweag.io/blog/2021-01-07-haskell-dark-arts-part-i/ |
| 22:39:32 | <terrorjack> | a kitten dies each time someone uses the trick in the above post |
| 22:41:25 | <geekosaur> | of course. don't dark arts always involve blood sacrifice? |
| 22:42:27 | × | Square quits (~Square4@user/square) (Ping timeout: 268 seconds) |
| 22:44:23 | <EvanR> | like when star wars episode 1 through 3 sacrificed the entire franchise |
| 22:45:00 | <EvanR> | the character might as well have been using importHidden |
| 22:47:22 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 22:49:58 | → | infinity0 joins (~infinity0@pwned.gg) |
| 22:51:02 | × | michalz quits (~michalz@185.246.207.205) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:51:14 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:53:47 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:53:55 | × | acidjnk_new quits (~acidjnk@p200300d6e706f453dde8176755f9f4a3.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 22:57:14 | <cheater> | https://new.reddit.com/r/rust/comments/1bp9zr8/im_a_non_technical_founder_of_a_startup_and_a/ |
| 22:59:09 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 22:59:29 | → | infinity0 joins (~infinity0@pwned.gg) |
| 23:00:02 | <EvanR> | rust fanatics and enthusiasts everywhere, imagine if haskell had that problem |
| 23:02:21 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 23:04:48 | <ph88> | why are the haskell webservers slow compared to c and rust ? |
| 23:05:05 | <EvanR> | is that even true? |
| 23:05:35 | <ph88> | ya |
| 23:05:51 | → | infinity0 joins (~infinity0@pwned.gg) |
| 23:05:56 | <EvanR> | what happened to those snap benchmarks |
| 23:07:23 | <ph88> | they got disabled because nobody updated the benchmark https://github.com/TechEmpower/FrameworkBenchmarks/blob/2d9b618c99ba0b0073eb49ffdb9e884bf640be1a/frameworks/Haskell/snap/benchmark_config.json#L24 |
| 23:08:26 | <EvanR> | o_O |
| 23:13:28 | × | tri quits (~tri@4133220a.cst.lightpath.net) (Ping timeout: 250 seconds) |
| 23:14:06 | <ph88> | Requests/sec: 2_514_450.26 actix, 2_094_552.29 h2o, 416_888.48 snap |
| 23:14:13 | <ph88> | in 2018 |
| 23:16:47 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 23:17:08 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 23:19:39 | <dmj`> | EvanR: might try to make bindings for this https://facil.io/ |
| 23:19:48 | <dmj`> | put wai on top of it |
| 23:25:20 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:26:51 | <ph88> | hmm looks like facil has a bit too much like json parsing which we already have with aeson. Better put wai on libreactor in that case then https://github.com/fredrikwidlund/libreactorng |
| 23:31:36 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 23:31:58 | → | infinity0 joins (~infinity0@pwned.gg) |
| 23:36:36 | × | tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 255 seconds) |
| 23:38:26 | → | tessier joins (~treed@ip72-220-57-194.sd.sd.cox.net) |
| 23:43:17 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:44:39 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 272 seconds) |
| 23:55:05 | <dmj`> | ph88: yea but our json parsing is slow and GHC doesn't support SIMD afaik |
| 23:55:48 | <ph88> | dmj`, good point |
| 23:57:13 | <dmj`> | ph88: libreactor looks cool |
| 23:57:44 | <terrorjack> | @package hermes-json |
| 23:57:44 | <lambdabot> | https://hackage.haskell.org/package/hermes-json |
| 23:59:17 | <dmj`> | cool library :) |
All times are in UTC on 2024-03-27.