Logs: liberachat/#haskell
| 2021-06-01 15:29:29 | <ski> | bor0> :t hoareSequence |
| 2021-06-01 15:29:51 | <boxscape> | ski https://github.com/bor0/hoare-imp/blob/d7b154b8d9b68fcf6466b22ff1f40591db3dcdb4/src/Hoare.hs#L35 |
| 2021-06-01 15:29:53 | <bor0> | https://github.com/bor0/hoare-imp/blob/master/src/Hoare.hs#L35 |
| 2021-06-01 15:33:27 | × | qbt quits (~edun@user/edun) (Ping timeout: 272 seconds) |
| 2021-06-01 15:34:42 | <ski> | bor0 : you know you could use `do'-notation, for the `Either' stuff, yes ? |
| 2021-06-01 15:35:40 | × | wei2912 quits (~wei2912@112.199.250.21) (Quit: Lost terminal) |
| 2021-06-01 15:35:49 | <bor0> | I totally forgot about that one! Are you saying these can look better? :D https://github.com/bor0/hoare-imp/blob/master/examples/ExampleTNT.hs |
| 2021-06-01 15:36:08 | <bor0> | (Don't look at the other examples, I still haven't updated all of them to use monadic Either instead of hacky `fromRight`) |
| 2021-06-01 15:36:46 | <ski> | lemma1 = do |
| 2021-06-01 15:36:49 | <boxscape> | that code almost looks like you took something that was written in do-notation and translated it to non-do-notation :) |
| 2021-06-01 15:36:58 | <bor0> | Hahahah. |
| 2021-06-01 15:37:03 | <ski> | step1 <- axiom3 (Var A) (Var B) |
| 2021-06-01 15:37:10 | <ski> | step2 <- ruleSpec step1 (Var D) |
| 2021-06-01 15:37:12 | <ski> | ... |
| 2021-06-01 15:37:17 | <bor0> | Oh man... |
| 2021-06-01 15:37:24 | <bor0> | Time for another rewrite! |
| 2021-06-01 15:38:59 | <ski> | (flipping the order of the `ruleFantasy' parameters might also look nicer) |
| 2021-06-01 15:39:04 | <bor0> | Wow, it just looks amazing this way! |
| 2021-06-01 15:39:17 | × | ikex quits (~ash@user/ikex) (Ping timeout: 264 seconds) |
| 2021-06-01 15:39:17 | ski | smiles |
| 2021-06-01 15:39:35 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection) |
| 2021-06-01 15:40:25 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds) |
| 2021-06-01 15:40:26 | <bor0> | Can you expand on the `ruleFantasy` parameters? |
| 2021-06-01 15:41:41 | × | dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 264 seconds) |
| 2021-06-01 15:42:09 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-01 15:42:25 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-01 15:43:50 | <ski> | let premise = PropVar (ForAll D (PropVar (Eq (..) (..)))) |
| 2021-06-01 15:44:12 | <ski> | step7 <- ruleFantasy premise $ \premise -> do |
| 2021-06-01 15:44:30 | × | boxscape quits (~boxscape@user/boxscape) (Quit: Connection closed) |
| 2021-06-01 15:44:33 | <bor0> | Ah! |
| 2021-06-01 15:44:35 | <ski> | step8 <- ruleSpec premise (Var D) |
| 2021-06-01 15:44:39 | <APic> | ☺ |
| 2021-06-01 15:44:39 | <ski> | ... |
| 2021-06-01 15:45:00 | <bor0> | I'll definitely miss those redundant `let f premise` |
| 2021-06-01 15:45:01 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 2021-06-01 15:45:09 | <ski> | ruleGeneralize step10 D (Just premise) |
| 2021-06-01 15:45:26 | <ski> | ruleGeneralize step7 C Nothing |
| 2021-06-01 15:46:37 | <ski> | "miss", as in you'll regret removing them, or as in you'll prefer to drop them ? |
| 2021-06-01 15:46:40 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-06-01 15:46:43 | → | boxscape joins (~boxscape@user/boxscape) |
| 2021-06-01 15:46:44 | × | ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection) |
| 2021-06-01 15:47:30 | <ski> | (it's not clear to me what the relation between these two different `premise's are, but i kept your variable naming ..) |
| 2021-06-01 15:48:03 | <bor0> | I think it's safe to assume just another redundancy |
| 2021-06-01 15:48:46 | × | dunj3 quits (~dunj3@2001:16b8:3059:9800:5856:7ab4:1dd8:26ae) (Remote host closed the connection) |
| 2021-06-01 15:50:07 | <bor0> | These proofs suddenly became readable! This is fun |
| 2021-06-01 15:50:49 | <boxscape> | Haskell does have a reputation for being a good host language for EDSLs |
| 2021-06-01 15:51:03 | <ski> | readability is a good thing, yea :) |
| 2021-06-01 15:51:22 | <bor0> | boxscape, I thought it had a good reputation for being a good host language without readability, but now with this readability... ++ |
| 2021-06-01 15:51:35 | <boxscape> | hehe |
| 2021-06-01 15:51:35 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-06-01 15:51:44 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 2021-06-01 15:52:07 | <bor0> | One thing I really like about doing this in Haskell, vs e.g. in Racket is refactoring. It's a breeze. Almost like random work until ghci is happy |
| 2021-06-01 15:52:56 | <boxscape> | yep static types are pretty cool |
| 2021-06-01 15:53:05 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 2021-06-01 15:53:10 | <boxscape> | (though I think racket has an optional static type system? I've never used racket) |
| 2021-06-01 15:53:16 | → | Deide joins (~Deide@wire.desu.ga) |
| 2021-06-01 15:53:16 | × | Deide quits (~Deide@wire.desu.ga) (Changing host) |
| 2021-06-01 15:53:16 | → | Deide joins (~Deide@user/deide) |
| 2021-06-01 15:53:26 | ski | . o O ( "Follow the types where they lead -- follow the types where they lead. Follow, follow, follow, follow -- follow the types where they lead." ) |
| 2021-06-01 15:53:44 | → | hseg joins (~gesh@185.120.126.41) |
| 2021-06-01 15:54:03 | → | shailangsa joins (~shailangs@host165-120-169-73.range165-120.btcentralplus.com) |
| 2021-06-01 15:54:09 | <ski> | there's Typed Racket, yea |
| 2021-06-01 15:54:40 | <boxscape> | ok |
| 2021-06-01 15:54:43 | <hseg> | stack isn't picking up the new commonmark version (from last friday) on hackage |
| 2021-06-01 15:54:58 | <hseg> | even though I ran stack update |
| 2021-06-01 15:55:04 | <ski> | (one interesting thing is the higher-order blame tracking system, for contracts) |
| 2021-06-01 15:55:52 | <kosmikus> | xwx: lhs2tex-1.24 should work ok with HLS (within certain limits). |
| 2021-06-01 15:57:27 | × | zeenk quits (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) (Quit: Konversation terminated!) |
| 2021-06-01 15:58:43 | → | haltux joins (~lbigas@a89-154-181-47.cpe.netcabo.pt) |
| 2021-06-01 16:00:25 | → | guest61 joins (~xxx@47.245.54.240) |
| 2021-06-01 16:00:37 | × | haltux quits (~lbigas@a89-154-181-47.cpe.netcabo.pt) (Quit: Leaving) |
| 2021-06-01 16:01:43 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-01 16:02:05 | × | shryke quits (~shryke@91.103.43.254) (Ping timeout: 264 seconds) |
| 2021-06-01 16:02:18 | → | haltux joins (~lbigas@a89-154-181-47.cpe.netcabo.pt) |
| 2021-06-01 16:02:29 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-06-01 16:03:01 | <hseg> | nuked $XDG_DATA_HOME/stack, hopefully that helps things |
| 2021-06-01 16:05:18 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2021-06-01 16:07:11 | × | pe200012_ quits (~pe200012@218.107.17.245) (Read error: Connection reset by peer) |
| 2021-06-01 16:08:17 | → | shryke joins (~shryke@91.103.43.254) |
| 2021-06-01 16:08:46 | → | softinio joins (~softinio@c-73-70-215-171.hsd1.ca.comcast.net) |
| 2021-06-01 16:10:17 | <kuribas> | "cabal haddock --executables" gives an error: cabal: unrecognized 'haddock' option `--executables' |
| 2021-06-01 16:10:55 | → | v01d4lph4 joins (~v01d4lph4@122.160.65.250) |
| 2021-06-01 16:10:55 | × | v01d4lph4 quits (~v01d4lph4@122.160.65.250) (Changing host) |
| 2021-06-01 16:10:55 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 2021-06-01 16:11:25 | <bor0> | ski, boxscape https://github.com/bor0/hoare-imp/blob/master/examples/ExampleTNT.hs 😎 |
| 2021-06-01 16:11:41 | <kuribas> | hmm cabal haddock myproject:executables does work... |
| 2021-06-01 16:11:50 | <boxscape> | bor0 nice |
| 2021-06-01 16:11:55 | <kuribas> | the cabal haddock --help text is wrong however. |
| 2021-06-01 16:11:56 | <geekosaur> | looks like it's --haddock-executables ? |
| 2021-06-01 16:12:20 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-01 16:12:25 | × | Guest9 quits (~Guest9@43.241.144.2) (Quit: Connection closed) |
| 2021-06-01 16:13:08 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 2021-06-01 16:13:28 | <geekosaur> | the text at the top is wrong but the actual option descriptions later are correct |
| 2021-06-01 16:14:07 | × | softinio quits (~softinio@c-73-70-215-171.hsd1.ca.comcast.net) () |
| 2021-06-01 16:15:27 | <boxscape> | bor0 do step0, step1, step2 etc all have the same type or different types? |
| 2021-06-01 16:15:31 | <kuribas> | geekosaur: right |
| 2021-06-01 16:16:32 | <boxscape> | (whoops step0 doesn't actually exist) |
| 2021-06-01 16:16:36 | <bor0> | All same I believe - either string (error) or proof |
| 2021-06-01 16:16:42 | <boxscape> | ok |
| 2021-06-01 16:17:31 | <boxscape> | bor0 I was thinking about whether it would make sense to use the State monad which is why I asked that, but the answer is no |
All times are in UTC.