Logs: liberachat/#haskell
| 2021-05-31 16:32:38 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 252 seconds) |
| 2021-05-31 16:32:40 | × | chomwitt quits (~Pitsikoko@athedsl-20549.home.otenet.gr) (Ping timeout: 268 seconds) |
| 2021-05-31 16:32:45 | <tomsmeding> | you also get the ability to print out proofs that way :) |
| 2021-05-31 16:33:05 | <bor0> | Ah! :) Yeah.. Proofs right now are just basically Haskell functions |
| 2021-05-31 16:33:18 | <bor0> | I get to use all the fancy stuff like let = ... etc for free |
| 2021-05-31 16:33:26 | <tomsmeding> | Maybe there's a way to ensure your implementation never goes wrong, but I think it's a very risky endeavour :) |
| 2021-05-31 16:33:29 | <bor0> | But it seems it isn't really for free.. |
| 2021-05-31 16:33:36 | <tomsmeding> | yeah |
| 2021-05-31 16:33:51 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-05-31 16:34:08 | <tomsmeding> | I have to go though; good luck :) |
| 2021-05-31 16:34:35 | <bor0> | Thank you! Discussion was great. I will look into the bits you suggested earlier and see if it's easy to incorporate some of them with small refactors :) |
| 2021-05-31 16:35:22 | × | whaletechho quits (~whaletech@user/whaletechno) (Quit: ha det bra) |
| 2021-05-31 16:35:23 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 2021-05-31 16:36:53 | × | Topsi quits (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 2021-05-31 16:36:59 | <ski> | bor0 : `whenRight' is called `(>>=)' |
| 2021-05-31 16:37:29 | <ski> | @src Either (>>=) |
| 2021-05-31 16:37:29 | <lambdabot> | Left l >>= _ = Left l |
| 2021-05-31 16:37:29 | <lambdabot> | Right r >>= k = k r |
| 2021-05-31 16:37:36 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 16:38:05 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 264 seconds) |
| 2021-05-31 16:38:07 | <bor0> | Hah. I now need to rewrite all the examples! :D Thanks ski. That's definitely an improvement! |
| 2021-05-31 16:39:18 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 2021-05-31 16:39:24 | → | schuelermine joins (~anselmsch@user/schuelermine) |
| 2021-05-31 16:39:38 | → | oxide joins (~lambda@user/oxide) |
| 2021-05-31 16:40:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-31 16:40:48 | → | Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-133-134.cust.tzulo.com) |
| 2021-05-31 16:41:00 | <ski> | it seems like `applyFOLRule' should perhaps allow its callback to possibly fail .. if it's going to be an arbitrary (uninspectable) Haskell function |
| 2021-05-31 16:41:53 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 244 seconds) |
| 2021-05-31 16:45:19 | → | imdoor joins (~imdoor@balticom-142-78-50.balticom.lv) |
| 2021-05-31 16:45:27 | × | notzmv quits (~zmv@user/notzmv) (Read error: Connection reset by peer) |
| 2021-05-31 16:46:55 | <kuribas``> | Why does cassava have so crappy error handling? |
| 2021-05-31 16:46:56 | <bor0> | What if `go` keeps track of the bound variables, and if one of those appear in `x` within https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L65 then just error? |
| 2021-05-31 16:47:03 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-31 16:47:41 | <bor0> | That's probably too strict... |
| 2021-05-31 16:48:12 | → | Deide joins (~Deide@wire.desu.ga) |
| 2021-05-31 16:48:12 | × | Deide quits (~Deide@wire.desu.ga) (Changing host) |
| 2021-05-31 16:48:12 | → | Deide joins (~Deide@user/deide) |
| 2021-05-31 16:50:18 | × | igghibu quits (~igghibu@37.120.201.126) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-05-31 16:50:22 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 2021-05-31 16:51:10 | × | the-coot quits (~coot@37.30.49.19.nat.umts.dynamic.t-mobile.pl) (Quit: the-coot) |
| 2021-05-31 16:51:11 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 16:51:13 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 2021-05-31 16:52:41 | → | mononote joins (~mononote@user/mononote) |
| 2021-05-31 16:55:19 | → | rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) |
| 2021-05-31 16:56:05 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 2021-05-31 16:58:20 | × | mononote quits (~mononote@user/mononote) (Quit: Quit) |
| 2021-05-31 16:58:47 | × | brandonh quits (~brandonh@151.38.151.222) (Read error: Connection reset by peer) |
| 2021-05-31 16:59:15 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 17:01:29 | × | sciencentistguy quits (~sciencent@194.110.13.3) (Ping timeout: 264 seconds) |
| 2021-05-31 17:02:25 | <ski> | bor0 : fwiw, i dunno why "Using `applyFOLRule` within `applyFOLRule` is not allowed." |
| 2021-05-31 17:02:45 | <bor0> | It's a temporary patch to avoid this error :) |
| 2021-05-31 17:02:58 | <ski> | it seems to me it would naturally satisfy a distributive law |
| 2021-05-31 17:03:01 | <bor0> | (Until I/we get it right xD) |
| 2021-05-31 17:03:17 | <dminuoso> | kuribas``: No idea, but it's a recurring theme. |
| 2021-05-31 17:03:23 | <dminuoso> | Perhaps you can help and improve it? |
| 2021-05-31 17:03:56 | <kuribas``> | dminuoso: if they don't mind breaking changes... |
| 2021-05-31 17:04:08 | → | shiraeeshi joins (~shiraeesh@109.166.59.30) |
| 2021-05-31 17:04:26 | <ski> | bor0 : a minor thing, there's no need to pass `f' as a parameter to `go' |
| 2021-05-31 17:04:43 | <ski> | (since it never changes) |
| 2021-05-31 17:04:58 | → | bfrk joins (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) |
| 2021-05-31 17:05:00 | <kuribas``> | dminuoso: for example, FromNamedRecord returning a structured error, with column and row information |
| 2021-05-31 17:05:17 | <dminuoso> | kuribas``: I suspect the poor diagnostics is from ruthless usage of attoparsec. :-) |
| 2021-05-31 17:05:34 | <ski> | (you will need `ScopedTypeVariables' to have a type signature on `go', though, if you go for that) |
| 2021-05-31 17:06:00 | <kuribas``> | dminuoso: that could be it... |
| 2021-05-31 17:06:46 | × | nschoe quits (~quassel@2a04:cec0:118b:9ec7:45a:fcee:e159:4f31) (Ping timeout: 265 seconds) |
| 2021-05-31 17:07:19 | → | econo joins (uid147250@user/econo) |
| 2021-05-31 17:07:22 | × | waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 264 seconds) |
| 2021-05-31 17:08:02 | <ski> | bor0 : where's `PropCalc' and `FOL' (and `Arith') defined ? |
| 2021-05-31 17:08:26 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-05-31 17:08:29 | → | dpl_ joins (~dpl@77-121-78-163.chn.volia.net) |
| 2021-05-31 17:08:30 | <bor0> | https://github.com/bor0/hoare-imp/blob/master/src/Gentzen.hs and https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs |
| 2021-05-31 17:08:40 | → | cheater joins (~Username@user/cheater) |
| 2021-05-31 17:08:44 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-05-31 17:09:15 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-05-31 17:09:18 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-05-31 17:09:25 | <dminuoso> | kuribas``: Realistically the only thing you can do in attoparsec, is decorate stuff with (<?>) |
| 2021-05-31 17:09:56 | → | notzmv joins (~zmv@user/notzmv) |
| 2021-05-31 17:09:59 | <kuribas``> | dminuoso: still, adding column and row info seems very doable... |
| 2021-05-31 17:10:16 | <kuribas``> | dminuoso: as attoparsec only needs to split the rows into columns. |
| 2021-05-31 17:10:32 | → | peach joins (sid482179@id-482179.charlton.irccloud.com) |
| 2021-05-31 17:10:46 | <dminuoso> | kuribas``: column/row info? |
| 2021-05-31 17:10:55 | <dminuoso> | How can you even track that? |
| 2021-05-31 17:11:12 | <dminuoso> | This is not megaparsec where you can add some monadic state |
| 2021-05-31 17:11:31 | × | dpl quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 268 seconds) |
| 2021-05-31 17:11:48 | <kuribas``> | dminuoso: parse in two steps, step one is split row into fields |
| 2021-05-31 17:11:54 | <kuribas``> | as a list |
| 2021-05-31 17:11:58 | <bor0> | ski, Interestingly, applyPropRule doesn't seem to have the same defect https://github.com/bor0/hoare-imp/blob/master/src/Gentzen.hs#L31. Likely because it doesn't have any support for quantifiers |
| 2021-05-31 17:12:01 | <kuribas``> | then parse each list |
| 2021-05-31 17:12:03 | → | brandonh joins (~brandonh@151.38.139.116) |
| 2021-05-31 17:12:06 | <kuribas``> | list element |
| 2021-05-31 17:12:21 | <dminuoso> | kuribas``: I suspect this drastically impact performance |
| 2021-05-31 17:12:35 | <dminuoso> | Since you'd be running many tiny attoparsec parsers for each row |
| 2021-05-31 17:12:55 | <kuribas``> | I would care more about good errors than blazing performance |
| 2021-05-31 17:13:53 | <dminuoso> | Then your goals are incompatible with cassavas goal, which strives to be competitive with pythons 'cvs' |
| 2021-05-31 17:13:55 | <dminuoso> | *csv |
| 2021-05-31 17:14:45 | <dminuoso> | kuribas``: What one could do, is rework `cassava` to work with `parsers` perhaps, so you can re-parse with trifecta and generate better error messages? |
| 2021-05-31 17:14:51 | <dminuoso> | Im not sure how viable this is, though. |
| 2021-05-31 17:15:25 | <kuribas``> | I suppose I could parse into (Vector (Vector ByteString)), then use my own parser ByteString -> a |
| 2021-05-31 17:15:38 | <kuribas``> | that would not be so hard to implement |
| 2021-05-31 17:15:47 | × | imdoor quits (~imdoor@balticom-142-78-50.balticom.lv) (Quit: imdoor) |
All times are in UTC.