Logs: liberachat/#haskell
| 2021-06-01 12:44:25 | × | xff0x quits (~xff0x@2001:1a81:52ca:4f00:a77b:5731:d9ca:93c9) (Ping timeout: 268 seconds) |
| 2021-06-01 12:44:57 | <bor0> | Hey, ski :wave: I just did https://github.com/bor0/hoare-imp/commit/d7b154b8d9b68fcf6466b22ff1f40591db3dcdb4 per your suggestions. Now I find myself doing this a lot: https://github.com/bor0/hoare-imp/blob/master/examples/ExampleHoare.hs#L47. Is there a neater way? :) |
| 2021-06-01 12:45:05 | → | xff0x joins (~xff0x@2001:1a81:52ca:4f00:7b0a:bab9:5836:8b3b) |
| 2021-06-01 12:45:23 | ← | otoburb parts (~otoburb@user/otoburb) () |
| 2021-06-01 12:45:29 | <bor0> | Specifically, the `x >>= \x -> ...` part. `hlint` reported `>=>` but it only slightly helps |
| 2021-06-01 12:45:39 | × | xwx quits (~george@user/george) (Ping timeout: 268 seconds) |
| 2021-06-01 12:48:29 | <boxscape> | :t \pre post step5 hoareConsequence -> pre >>= \pre -> post >>= \post -> step5 >>= \step5 -> hoareConsequence pre step5 post |
| 2021-06-01 12:48:30 | <lambdabot> | Monad m => m t1 -> m t2 -> m t3 -> (t1 -> t3 -> t2 -> m b) -> m b |
| 2021-06-01 12:48:32 | <boxscape> | :t \pre post step5 hoareConsequence -> hoareConsequence <$> pre <*> step5 <*> post |
| 2021-06-01 12:48:32 | <lambdabot> | Applicative f => f a1 -> f a2 -> f a3 -> (a1 -> a3 -> a2 -> b) -> f b |
| 2021-06-01 12:48:39 | <boxscape> | ^ does that work for you bor0? |
| 2021-06-01 12:49:12 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-01 12:49:13 | <bor0> | Whoa. Let me try that. Looks like it should do it |
| 2021-06-01 12:49:30 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-01 12:49:36 | <boxscape> | :t \pre post step5 hoareConsequence -> liftA3 hoareConsequence pre step5 post -- bor0 alternatively |
| 2021-06-01 12:49:37 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-01 12:49:37 | <lambdabot> | Applicative f => f a -> f c -> f b -> (a -> b -> c -> d) -> f d |
| 2021-06-01 12:51:17 | <bor0> | It works! Magical. Looks awesome. Thanks! |
| 2021-06-01 12:51:21 | <boxscape> | np |
| 2021-06-01 12:51:42 | <boxscape> | (you'll see this "applicative style" quite often) |
| 2021-06-01 12:51:53 | × | brian_da_mage quits (~Neuromanc@user/briandamag) (Ping timeout: 264 seconds) |
| 2021-06-01 12:52:17 | <bor0> | An interesting ride. From pure functions to monads to applicative. But the end result is totally worth it |
| 2021-06-01 12:53:16 | <boxscape> | that's pretty much the timeline in terms of how people applied the concepts to functional programming, as well :) |
| 2021-06-01 12:53:38 | → | berberman joins (~berberman@user/berberman) |
| 2021-06-01 12:53:42 | × | berberman_ quits (~berberman@user/berberman) (Ping timeout: 264 seconds) |
| 2021-06-01 12:53:46 | → | pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) |
| 2021-06-01 12:53:46 | <bor0> | History repeats itself! :D |
| 2021-06-01 12:56:50 | <bor0> | Any clue why `ruleJoin <$> ruleSepR pq <*> ruleSepL pq ` doesn't work but `ruleJoin <$> ruleSepR pq <*> ruleSepL pq >>= id` does? `>>= id` seems hacky |
| 2021-06-01 12:57:30 | <boxscape> | (>>= id) is called join |
| 2021-06-01 12:57:31 | <boxscape> | :t join |
| 2021-06-01 12:57:32 | <lambdabot> | Monad m => m (m a) -> m a |
| 2021-06-01 12:57:59 | <tomsmeding> | bor0: if this is your first meeting with those applicative operators, I encourage you to look closely at the types of (<$>) (which is just fmap, by the way), (<*>) and (>>=). Then look at them again the next time you use them. At some point it will become clear how this 'f <$> a <*> b <*> c' style actually works. A bit later you'll realise how Applicative, which is defined by pure and <*>, is |
| 2021-06-01 12:57:59 | <tomsmeding> | actually a bit weaker than Monad, and them you might understand how things like applicative parsing are different from monadic parsing. For me it took a while to get familiar with these type classes, but it's worth spending a bit of time looking at type signatures now and then :) |
| 2021-06-01 12:58:07 | <boxscape> | I imagine you're ending up with a nested Monad in the first expression, and join lets you flatten that to one level of Monad |
| 2021-06-01 13:00:22 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-01 13:00:44 | <bor0> | tomsmeding, thanks. I did meet Applicative/Monad and vaguely know their definition. I'm at the level where it isn't obvious what makes a monad and what makes an applicative so my approach is usually to write it "manually" and only then to abstract when it becomes obvious (usually becomes obvious when I join and ping this channel :)) |
| 2021-06-01 13:01:00 | → | xwx joins (~george@user/george) |
| 2021-06-01 13:01:16 | → | alx741 joins (~alx741@186.178.108.160) |
| 2021-06-01 13:04:05 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-06-01 13:04:08 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 2021-06-01 13:05:30 | × | hydroxonium quits (uid500654@id-500654.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-06-01 13:05:49 | <dminuoso> | bor0: Yup, keep on doing this. At some point, Applicative/Monad will kick in completely automatically, without you forcing the issue. |
| 2021-06-01 13:06:04 | <bor0> | Thanks. Right, just like driving. I hope. :) |
| 2021-06-01 13:06:07 | <dminuoso> | Im going to argue, until then its not even important to understand what they abstract over. |
| 2021-06-01 13:06:35 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Remote host closed the connection) |
| 2021-06-01 13:06:48 | × | xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Read error: Connection reset by peer) |
| 2021-06-01 13:07:32 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 2021-06-01 13:08:01 | <dminuoso> | Applicative is probably a bit harder to grasp, because most Applicative things happen to be Monad too (which subsumes Applicative), so you're less likely to encounter "just Applicative" things. |
| 2021-06-01 13:08:05 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 2021-06-01 13:08:21 | <dminuoso> | (Though both interfaces are easy enough to learn, obviously) |
| 2021-06-01 13:08:41 | → | wei2912 joins (~wei2912@112.199.250.21) |
| 2021-06-01 13:08:54 | <bor0> | Another thing that smells is the too many `Right`'s here: https://github.com/bor0/hoare-imp/blob/master/src/Gentzen.hs#L31-L42. Any way it can be improved? |
| 2021-06-01 13:09:13 | <bor0> | (Just throwing random code lines, but happy to elaborate further on the code/ideas behind it) |
| 2021-06-01 13:09:15 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 272 seconds) |
| 2021-06-01 13:10:33 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-06-01 13:11:06 | <boxscape> | make a helper function `foo arg = go xs f x >>= \prfx -> Right $ Proof $ arg`, though choose a better name than `foo` :) |
| 2021-06-01 13:11:14 | <boxscape> | and then replace each of those lines with a call to that function |
| 2021-06-01 13:11:24 | <bor0> | I thought of that, but note `go _ f x = f (Proof x)` |
| 2021-06-01 13:11:43 | <boxscape> | right, just keep that line as is |
| 2021-06-01 13:11:53 | <boxscape> | and use the helper function in the other lines |
| 2021-06-01 13:12:16 | <dminuoso> | I can see some elaborate tricks to make the Right go away, but nothing worth your while |
| 2021-06-01 13:12:52 | × | thiross quits (~user@173.242.113.143.16clouds.com) (Remote host closed the connection) |
| 2021-06-01 13:12:53 | × | azeem quits (~azeem@dynamic-adsl-78-13-240-225.clienti.tiscali.it) (Ping timeout: 252 seconds) |
| 2021-06-01 13:12:53 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 264 seconds) |
| 2021-06-01 13:13:00 | → | thiross joins (~user@173.242.113.143.16clouds.com) |
| 2021-06-01 13:13:11 | <boxscape> | ah I suppose it has to be slightly different |
| 2021-06-01 13:13:18 | <boxscape> | because arg may depend on prfx/prfy |
| 2021-06-01 13:13:43 | <boxscape> | err, also on x/y |
| 2021-06-01 13:13:50 | <dminuoso> | bor0: though, just use fmap, rather than >>= |
| 2021-06-01 13:14:00 | <dminuoso> | That lets you avoid the Right |
| 2021-06-01 13:14:03 | <bor0> | Yeah. OK, just felt a little bit odd and wanted to double-check if it can be abstracted even further |
| 2021-06-01 13:14:13 | <dminuoso> | Yeah, that's the key thing. Just use fmap, the Right disappears :) |
| 2021-06-01 13:14:20 | → | flowz joins (~flowz@2a01:aea0:dd4:1573:a8:24ac:7db2:5b39) |
| 2021-06-01 13:14:26 | <dminuoso> | <&> fits comfortably there |
| 2021-06-01 13:14:33 | <dminuoso> | Looks ergonomically nicer than <$> or fmap |
| 2021-06-01 13:14:46 | <dminuoso> | I'd write it like this: |
| 2021-06-01 13:15:01 | <dminuoso> | go xs f <&> \(Proof f) -> Proof (Not f) |
| 2021-06-01 13:15:53 | → | azeem joins (~azeem@dynamic-adsl-94-34-16-203.clienti.tiscali.it) |
| 2021-06-01 13:16:05 | <bor0> | OK, I'll need some time to unpack that. Otherwise I won't be able to update my code when I go back to it in a few days :D |
| 2021-06-01 13:16:12 | <bor0> | Read-only! |
| 2021-06-01 13:16:20 | <dminuoso> | bor0: So let me make it easy to see for you |
| 2021-06-01 13:16:34 | <dminuoso> | First realize that `Right = return` or `Right = pure` |
| 2021-06-01 13:17:15 | <dminuoso> | Then realize you have: fmap f x = pure f <*> x |
| 2021-06-01 13:17:39 | <dminuoso> | Do a bit of juggling |
| 2021-06-01 13:17:42 | × | thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 264 seconds) |
| 2021-06-01 13:18:48 | → | thiross joins (~user@173.242.113.143.16clouds.com) |
| 2021-06-01 13:20:22 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-01 13:20:44 | <boxscape> | you could also derive Functor for Proof and then replace `\(Proof f) -> Proof (Not f)` with `fmap Not`, I think |
| 2021-06-01 13:20:54 | <dminuoso> | Yup! |
| 2021-06-01 13:21:01 | <dminuoso> | Or, with <&> that would look even nicer |
| 2021-06-01 13:21:17 | <dminuoso> | go xs f <&> fmap Not |
| 2021-06-01 13:21:27 | ← | thiross parts (~user@173.242.113.143.16clouds.com) () |
| 2021-06-01 13:21:37 | → | xsperry joins (~as@user/xsperry) |
| 2021-06-01 13:21:40 | <dminuoso> | Or maybe you write g <&&> f = fmap (fmap f) g |
| 2021-06-01 13:21:43 | <dminuoso> | And then you have |
| 2021-06-01 13:21:45 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 2021-06-01 13:21:47 | <dminuoso> | go xs f <&&> Not |
| 2021-06-01 13:22:10 | <bor0> | Reading it makes sense, thanks. Just still need some practice for it to sink in. |
| 2021-06-01 13:24:10 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-06-01 13:24:34 | × | Toast52_ quits (~Toast52@151.192.167.120) (Quit: Leaving) |
All times are in UTC.