Logs: liberachat/#haskell
| 2021-06-14 18:00:16 | <eflister> | checkElement (maybe False (not . T.isInfixOf "Spanish") . M.lookup "ows_Document" . X.elementAttributes) |
| 2021-06-14 18:00:17 | <eflister> | here's a paste w/running code: https://paste.tomsmeding.com/eZbfKbES |
| 2021-06-14 18:00:17 | <eflister> | most of it is just for downloading and unzipping a .kmz, you can ignore that part. inside is a kml file, which is just xml. the `extract` function is where i need to filter out nodes that have <LineString> children |
| 2021-06-14 18:00:41 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Read error: Connection reset by peer) |
| 2021-06-14 18:01:16 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 244 seconds) |
| 2021-06-14 18:06:19 | × | Obo quits (~roberto@h-46-59-103-134.A498.priv.bahnhof.se) (Quit: WeeChat 2.8) |
| 2021-06-14 18:06:34 | → | Obo joins (~roberto@h-46-59-103-134.A498.priv.bahnhof.se) |
| 2021-06-14 18:07:19 | → | argento joins (~argent0@168-227-96-51.ptr.westnet.com.ar) |
| 2021-06-14 18:12:04 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Remote host closed the connection) |
| 2021-06-14 18:13:25 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-06-14 18:17:39 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-14 18:19:42 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-14 18:23:12 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2021-06-14 18:23:19 | → | kayprish joins (~kayprish@cable-188-2-229-172.dynamic.sbb.rs) |
| 2021-06-14 18:24:50 | → | ddellacosta joins (~ddellacos@86.106.143.216) |
| 2021-06-14 18:26:45 | → | chomwitt joins (~Pitsikoko@2a02:587:dc02:b00:98b0:cd42:bd6f:8295) |
| 2021-06-14 18:26:49 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-06-14 18:26:50 | × | MidAutumnMoon quits (~MidAutumn@user/midautumnmoon) (Quit: Ping timeout (120 seconds)) |
| 2021-06-14 18:27:10 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 2021-06-14 18:27:39 | × | ystael quits (~ystael@user/ystael) (Quit: Lost terminal) |
| 2021-06-14 18:28:27 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-14 18:29:22 | × | ddellacosta quits (~ddellacos@86.106.143.216) (Ping timeout: 244 seconds) |
| 2021-06-14 18:33:30 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 244 seconds) |
| 2021-06-14 18:33:43 | → | bfrk joins (~bfrk@200116b8451b0900bae0ed5ddd267e3d.dip.versatel-1u1.de) |
| 2021-06-14 18:35:52 | → | fishfinger joins (~fishfinge@85.255.236.178) |
| 2021-06-14 18:35:52 | × | fishfinger quits (~fishfinge@85.255.236.178) (Client Quit) |
| 2021-06-14 18:36:08 | → | fishfinger joins (~fishfinge@85.255.236.178) |
| 2021-06-14 18:36:24 | <eflister> | anyone have time to help with my xml-conduit cursor problem? :) |
| 2021-06-14 18:37:21 | → | gensyst joins (gensyst@user/gensyst) |
| 2021-06-14 18:37:22 | <monochrom> | Perhaps most haven't used xml-conduit. I certainly haven't. |
| 2021-06-14 18:37:44 | × | qbt quits (~edun@user/edun) (Ping timeout: 252 seconds) |
| 2021-06-14 18:37:44 | <gensyst> | If n is KnownNat, why isn't n+1 automatically a KnownNat? |
| 2021-06-14 18:39:12 | <eflister> | monochrom: should be able to work it out from the types tho :) i could use help just with that. the parts that aren't straightforward are the distinctions between Node and Element, and the Cursor/Axis types... |
| 2021-06-14 18:39:35 | <nshepperd> | gensyst: it can be, if you enable a ghc plugin |
| 2021-06-14 18:40:09 | <eflister> | monochrom: there's a good quick overview here: https://www.yesodweb.com/book/xml#xml_cursor |
| 2021-06-14 18:40:17 | × | mnrmnaugh quits (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 2021-06-14 18:40:40 | → | ericson2314 joins (~ericson23@2001:470:69fc:105::70c) |
| 2021-06-14 18:40:42 | → | mnrmnaugh joins (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) |
| 2021-06-14 18:40:51 | → | fizbin joins (~fizbin@2601:8a:4080:1280:8c7e:5b3f:79d6:ec26) |
| 2021-06-14 18:42:31 | <nshepperd> | as for why it's not built into ghc, it's probably because KnownNat inference is basically arithmetic theorem proving and it's not obvious what algorithm would serve all use cases best |
| 2021-06-14 18:43:15 | × | tubogram quits (~tubogram@user/tubogram) (*.net *.split) |
| 2021-06-14 18:43:35 | → | tubogram joins (~tubogram@user/tubogram) |
| 2021-06-14 18:43:40 | × | tubogram quits (~tubogram@user/tubogram) (*.net *.split) |
| 2021-06-14 18:43:40 | × | Axman6 quits (~Axman6@user/axman6) (*.net *.split) |
| 2021-06-14 18:43:52 | <nshepperd> | @hackage ghc-typelits-knownnat |
| 2021-06-14 18:43:52 | <lambdabot> | https://hackage.haskell.org/package/ghc-typelits-knownnat |
| 2021-06-14 18:44:05 | → | tubogram joins (~tubogram@user/tubogram) |
| 2021-06-14 18:44:13 | <maerwald> | is -rtsopts ignored for test suites? |
| 2021-06-14 18:44:45 | <monochrom> | The specific case of n+1 does not need very general theorem proving. However, I would attribute its absence to "on the TODO list". |
| 2021-06-14 18:45:23 | × | fizbin quits (~fizbin@2601:8a:4080:1280:8c7e:5b3f:79d6:ec26) (Ping timeout: 244 seconds) |
| 2021-06-14 18:46:04 | <monochrom> | An upon the clearly rhetorical question "why isn't" the very obvious answer is "patches welcome". |
| 2021-06-14 18:46:58 | <monochrom> | Dependent typing for Haskell is a huge program on essentially a one-person band. Expect additions to be very slowly trickling down. |
| 2021-06-14 18:47:40 | <monochrom> | Uh, unlike the usual me, no pun intended there, honest! |
| 2021-06-14 18:48:43 | tomsmeding | is suspicious |
| 2021-06-14 18:48:45 | <monochrom> | I think it is very safe to assume that: |
| 2021-06-14 18:49:14 | <monochrom> | 1. Every "why isn't foo available" question is rhetorical. The asker doesn't really care about "why", they're just complaining. |
| 2021-06-14 18:49:25 | <monochrom> | 2. Therefore the correct answer is "patches welcome". |
| 2021-06-14 18:49:45 | <monochrom> | 3. Therefore, we can set up a bot to handle those questions. |
| 2021-06-14 18:50:10 | <monochrom> | . o O ( Why isn't there such a bot??!!! >:) ) |
| 2021-06-14 18:51:38 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 2021-06-14 18:51:50 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:b9b1:9fc2:289f:a533) (Remote host closed the connection) |
| 2021-06-14 18:52:10 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-14 18:53:20 | × | dhil quits (~dhil@195.213.192.47) (Ping timeout: 268 seconds) |
| 2021-06-14 18:53:36 | × | Morrow quits (~Morrow@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 272 seconds) |
| 2021-06-14 18:54:19 | <tomsmeding> | patches welcome! |
| 2021-06-14 18:54:40 | <tomsmeding> | ... which raises the obvious question: patches to what? |
| 2021-06-14 18:55:07 | <monochrom> | The empty, newly created git repo? :) |
| 2021-06-14 18:55:19 | <nshepperd> | it doesn't seem very obvious when i think about it. like reducing KnownNat (n + 1) to KnownNat n is an intuitive reduction step but not the only one possible |
| 2021-06-14 18:55:35 | <tomsmeding> | such a bot wouldn't be able to have perfect accuracy without significant haskell domain knowledge, though |
| 2021-06-14 18:55:58 | <nshepperd> | and it must eventually terminate in whatever KnownNat instances are in scope |
| 2021-06-14 18:56:26 | <tomsmeding> | "why isn't type Abc an instance of class Xyz" could very well be a non-complaining question, depending on the asker and the type and class in question |
| 2021-06-14 18:56:53 | <gensyst> | nshepperd, thanks this plugin seems to work! |
| 2021-06-14 18:57:25 | <tomsmeding> | nshepperd: I don't know how + on Nats is defined internally in GHC; if it's the typical, naive recursive definition, then it's either recursive on the left argument or on the right |
| 2021-06-14 18:57:29 | <gensyst> | is there ANY other language that has stuff like vector-sized? this is REALLY great stuff! |
| 2021-06-14 18:57:51 | → | ddellacosta joins (~ddellacos@89.46.62.164) |
| 2021-06-14 18:57:51 | <tomsmeding> | and hence you might see different behaviour with 1 + n than with n + 1 |
| 2021-06-14 18:57:57 | <monochrom> | tomsmeding, but this one is a type-level +. KnownNat is a class; n is a type. |
| 2021-06-14 18:59:03 | <tomsmeding> | monochrom: which makes my point all the more relevant, because on the type level, at least for type families, ghc has to be careful with choosing type family branches when it's not yet clear that the argument is apart from the previous pattern |
| 2021-06-14 18:59:08 | <nshepperd> | inferring KnownNat (n + 1) from KnownNat (n+2) which is in scope might be equally valid |
| 2021-06-14 18:59:15 | <monochrom> | I am now convinced by nshepperd. "If n's kind is Nat, then n+1's kind is Nat" is easy. But the type class version is much harder. |
| 2021-06-14 19:00:05 | <tomsmeding> | but if the implementation of type-level nats in ghc is magical, then it can of course get around this tip-toeing restriction |
| 2021-06-14 19:00:22 | <tomsmeding> | but it has to explicitly implemented |
| 2021-06-14 19:00:23 | → | Morrow joins (~Morrow@bzq-110-168-31-106.red.bezeqint.net) |
| 2021-06-14 19:00:40 | <tomsmeding> | which returns to the initial response: patches welcome |
| 2021-06-14 19:01:33 | × | fishfinger quits (~fishfinge@85.255.236.178) (Remote host closed the connection) |
| 2021-06-14 19:01:45 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2021-06-14 19:02:26 | × | ddellacosta quits (~ddellacos@89.46.62.164) (Ping timeout: 244 seconds) |
| 2021-06-14 19:02:31 | × | neceve quits (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) (Ping timeout: 272 seconds) |
| 2021-06-14 19:02:44 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 2021-06-14 19:03:41 | × | warnz quits (~warnz@2600:1700:77c0:5610:210a:ba95:5325:60a6) (Remote host closed the connection) |
| 2021-06-14 19:05:03 | × | sekun quits (~sekun@180.190.222.37) (Ping timeout: 268 seconds) |
| 2021-06-14 19:06:07 | × | Scotty_Trees quits (~Scotty_Tr@162-234-179-169.lightspeed.brhmal.sbcglobal.net) (Quit: Leaving) |
| 2021-06-14 19:06:09 | → | dhil joins (~dhil@80.208.56.181) |
| 2021-06-14 19:06:14 | × | GIANTWORLDKEEPR_ quits (~pjetcetal@2.95.204.25) (Remote host closed the connection) |
| 2021-06-14 19:07:19 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:b9b1:9fc2:289f:a533) |
| 2021-06-14 19:07:25 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-06-14 19:09:08 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-14 19:10:41 | → | ystael joins (~ystael@user/ystael) |
| 2021-06-14 19:10:59 | → | MoC joins (~moc@user/moc) |
| 2021-06-14 19:12:05 | → | GIANTWORLDKEEPER joins (~pjetcetal@2.95.204.25) |
All times are in UTC.