| 2021-07-03 00:00:02 +0000 | beka | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 265 seconds) |
| 2021-07-03 00:00:56 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 00:02:17 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 00:05:32 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 256 seconds) |
| 2021-07-03 00:06:31 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-07-03 00:06:55 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 268 seconds) |
| 2021-07-03 00:07:08 +0000 | beka__ | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-03 00:07:14 +0000 | trufas | (~trufas@177.240.218.218) (Ping timeout: 268 seconds) |
| 2021-07-03 00:08:19 +0000 | trufas | (~trufas@177.240.218.218) |
| 2021-07-03 00:08:24 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-07-03 00:08:42 +0000 | waleee | (~waleee@h-98-128-228-119.NA.cust.bahnhof.se) (Ping timeout: 240 seconds) |
| 2021-07-03 00:10:00 +0000 | beka_ | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 268 seconds) |
| 2021-07-03 00:11:26 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 00:17:03 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
| 2021-07-03 00:18:20 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 00:19:13 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2021-07-03 00:19:23 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2021-07-03 00:19:24 +0000 | allbery_b | (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 00:22:25 +0000 | oxide | (~lambda@user/oxide) |
| 2021-07-03 00:24:50 +0000 | test987689 | (~nik@cpc147288-walt27-2-0-cust442.13-2.cable.virginm.net) |
| 2021-07-03 00:25:05 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) (Quit: Free ZNC ~ Powered by LunarBNC: https://LunarBNC.net) |
| 2021-07-03 00:25:48 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 2021-07-03 00:26:46 +0000 | MorrowM | (~MorrowM_@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 272 seconds) |
| 2021-07-03 00:27:19 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit) |
| 2021-07-03 00:28:57 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 00:33:02 +0000 | P1RATEZ | (piratez@user/p1ratez) |
| 2021-07-03 00:35:07 +0000 | test987689 | (~nik@cpc147288-walt27-2-0-cust442.13-2.cable.virginm.net) (Quit: leaving) |
| 2021-07-03 00:35:48 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-07-03 00:37:00 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 00:40:16 +0000 | shailangsa | (~shailangs@host86-145-14-23.range86-145.btcentralplus.com) (Ping timeout: 244 seconds) |
| 2021-07-03 00:41:14 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 2021-07-03 00:41:19 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 00:41:22 +0000 | cheater1__ | cheater |
| 2021-07-03 00:41:40 +0000 | allbery_b | geekosaur |
| 2021-07-03 00:41:59 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 00:42:41 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 2021-07-03 00:43:06 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit) |
| 2021-07-03 00:43:36 +0000 | argento | (~argent0@168-227-96-53.ptr.westnet.com.ar) |
| 2021-07-03 00:43:38 +0000 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-07-03 00:44:15 +0000 | Deide | (~Deide@user/deide) (Quit: Seeee yaaaa) |
| 2021-07-03 00:44:19 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 2021-07-03 00:44:51 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit) |
| 2021-07-03 00:45:21 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 2021-07-03 00:47:11 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 00:48:47 +0000 | zeenk | (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) (Quit: Konversation terminated!) |
| 2021-07-03 00:55:33 +0000 | cloudy | (~user@2600:8807:c207:f00:d412:4cce:d9f1:ba0) (ERC (IRC client for Emacs 27.2)) |
| 2021-07-03 01:02:57 +0000 | Ranhir | (~Ranhir@157.97.53.139) (Read error: Connection reset by peer) |
| 2021-07-03 01:04:08 +0000 | MQ-17J | (~MQ-17J@8.21.10.15) (Ping timeout: 272 seconds) |
| 2021-07-03 01:04:22 +0000 | Ranhir | (~Ranhir@157.97.53.139) |
| 2021-07-03 01:04:46 +0000 | ph88_ | (~ph88@95.90.246.253) |
| 2021-07-03 01:08:03 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 01:08:26 +0000 | ph88^ | (~ph88@2a02:8109:9e00:7e5c:e9f2:8409:e391:bda5) (Ping timeout: 256 seconds) |
| 2021-07-03 01:09:45 +0000 | shailangsa | (~shailangs@host86-186-196-229.range86-186.btcentralplus.com) |
| 2021-07-03 01:16:26 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 01:16:36 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-03 01:16:38 +0000 | cheater1__ | cheater |
| 2021-07-03 01:17:48 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 01:22:41 +0000 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 265 seconds) |
| 2021-07-03 01:24:36 +0000 | son0p | (~ff@181.136.122.143) (Ping timeout: 252 seconds) |
| 2021-07-03 01:25:53 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 01:30:47 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-03 01:31:01 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 01:32:38 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 272 seconds) |
| 2021-07-03 01:32:55 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 01:36:16 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 01:40:10 +0000 | xff0x | (~xff0x@2001:1a81:5295:3000:f06b:55a4:6a29:7aa5) (Ping timeout: 256 seconds) |
| 2021-07-03 01:41:43 +0000 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 258 seconds) |
| 2021-07-03 01:41:57 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:b096:1d82:d091:433d) |
| 2021-07-03 01:48:11 +0000 | neurocyte407 | (~neurocyte@195.80.54.53) |
| 2021-07-03 01:48:11 +0000 | neurocyte407 | (~neurocyte@195.80.54.53) (Changing host) |
| 2021-07-03 01:48:11 +0000 | neurocyte407 | (~neurocyte@user/neurocyte) |
| 2021-07-03 01:51:29 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 01:51:52 +0000 | neurocyte40 | (~neurocyte@user/neurocyte) (Ping timeout: 246 seconds) |
| 2021-07-03 01:51:52 +0000 | neurocyte407 | neurocyte40 |
| 2021-07-03 01:53:12 +0000 | hegstal | (~hegstal@2a02:c7f:7604:8a00:f7c8:886a:a9a5:ff17) (Ping timeout: 256 seconds) |
| 2021-07-03 01:59:52 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 02:04:02 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 02:07:02 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 02:09:42 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 258 seconds) |
| 2021-07-03 02:10:00 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 02:11:54 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds) |
| 2021-07-03 02:13:00 +0000 | juhp | (~juhp@128.106.188.66) (Quit: juhp) |
| 2021-07-03 02:13:14 +0000 | juhp | (~juhp@128.106.188.66) |
| 2021-07-03 02:23:21 +0000 | alx741 | (~alx741@186.178.109.174) (Quit: alx741) |
| 2021-07-03 02:24:26 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 02:24:44 +0000 | argento | (~argent0@168-227-96-53.ptr.westnet.com.ar) (Ping timeout: 252 seconds) |
| 2021-07-03 02:27:29 +0000 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
| 2021-07-03 02:27:29 +0000 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (copper.libera.chat (Nickname regained by services))) |
| 2021-07-03 02:27:29 +0000 | finn_elija | FinnElija |
| 2021-07-03 02:29:00 +0000 | td_ | (~td@94.134.91.19) (Ping timeout: 272 seconds) |
| 2021-07-03 02:30:40 +0000 | td_ | (~td@muedsl-82-207-238-014.citykom.de) |
| 2021-07-03 02:33:24 +0000 | machinedgod | (~machinedg@24.105.81.50) |
| 2021-07-03 02:38:27 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-03 02:42:20 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 252 seconds) |
| 2021-07-03 02:45:38 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 02:46:03 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 02:49:50 +0000 | wei2912 | (~wei2912@112.199.250.21) |
| 2021-07-03 02:53:05 +0000 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2021-07-03 02:54:22 +0000 | ajar | (~ajar@1.38.44.128) |
| 2021-07-03 02:59:27 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 03:04:01 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 256 seconds) |
| 2021-07-03 03:04:03 +0000 | ajar | (~ajar@1.38.44.128) (Quit: Client closed) |
| 2021-07-03 03:05:35 +0000 | jess | (~jess@libera/staff/jess) |
| 2021-07-03 03:13:08 +0000 | Erutuon | (~Erutuon@user/erutuon) (Ping timeout: 252 seconds) |
| 2021-07-03 03:15:06 +0000 | Erutuon | (~Erutuon@user/erutuon) |
| 2021-07-03 03:20:13 +0000 | finsternis | (~X@23.226.237.192) (Remote host closed the connection) |
| 2021-07-03 03:24:08 +0000 | funsafe | (~funsafe@2601:1c1:4200:938f:32aa:eb39:2110:e2ea) |
| 2021-07-03 03:27:04 +0000 | boxscape_ | (~boxscape_@p4ff0ba7a.dip0.t-ipconnect.de) (Quit: Connection closed) |
| 2021-07-03 03:31:15 +0000 | machinedgod | (~machinedg@24.105.81.50) (Ping timeout: 265 seconds) |
| 2021-07-03 03:31:41 +0000 | pfurla_ | (~pfurla@216.131.83.59) |
| 2021-07-03 03:34:52 +0000 | pfurla | (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 272 seconds) |
| 2021-07-03 03:42:50 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 03:45:56 +0000 | dyeplexer | (~dyeplexer@user/dyeplexer) |
| 2021-07-03 03:47:41 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 265 seconds) |
| 2021-07-03 03:52:51 +0000 | rachel231 | (~rachel231@c-73-142-199-151.hsd1.nh.comcast.net) |
| 2021-07-03 03:53:16 +0000 | <rachel231> | Is there a way to get the right side of an either or throw an error if it's left? |
| 2021-07-03 03:53:27 +0000 | <rachel231> | like rust's .unwrap() |
| 2021-07-03 03:54:03 +0000 | <rachel231> | or like the either version of fromJust |
| 2021-07-03 03:54:55 +0000 | <davean> | either? |
| 2021-07-03 03:55:28 +0000 | <davean> | or fromRight? |
| 2021-07-03 03:55:31 +0000 | <davean> | Depending on what you want |
| 2021-07-03 03:58:00 +0000 | <sm[m]> | rachel231: yeah: either (error.fooShow) fooDoSomething efoo |
| 2021-07-03 03:58:00 +0000 | <sm[m]> | is pretty common |
| 2021-07-03 03:59:18 +0000 | <rachel231> | oooh tysm |
| 2021-07-03 03:59:59 +0000 | TranquilEcho | (~grom@user/tranquilecho) (Quit: WeeChat 2.8) |
| 2021-07-03 04:00:00 +0000 | jolly | (~jolly@208.180.97.158) (Quit: Connection closed) |
| 2021-07-03 04:01:50 +0000 | P1RATEZ | (piratez@user/p1ratez) (Remote host closed the connection) |
| 2021-07-03 04:04:15 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 04:04:56 +0000 | fef | (~thedawn@user/thedawn) |
| 2021-07-03 04:07:16 +0000 | edrx | (~Eduardo@2804:56c:d2e2:8b00:8d96:adf9:cdb8:eb7e) |
| 2021-07-03 04:10:12 +0000 | <dsal> | :t either (fail . show) |
| 2021-07-03 04:10:13 +0000 | <lambdabot> | (MonadFail m, Show a1) => (b -> m a2) -> Either a1 b -> m a2 |
| 2021-07-03 04:10:32 +0000 | haykam1 | (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-07-03 04:10:44 +0000 | haykam1 | (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-07-03 04:11:33 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 04:15:30 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 240 seconds) |
| 2021-07-03 04:16:54 +0000 | AgentM | (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 2021-07-03 04:18:05 +0000 | <edrx> | is this the right place to ask questions about cabal? I'm on a Debian box that has both agda and agda-mode from Debian - known to be broken - and an Agda that I've installed from Cabal... I even had to find a compilation bug and report it, here: https://lists.chalmers.se/pipermail/agda/2021/012689.html |
| 2021-07-03 04:19:54 +0000 | <edrx> | I am now trying to understand how cabal handle its paths. 1) is there a better way to specify the path to agda-mode than "~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/emacs-mode/"? |
| 2021-07-03 04:20:55 +0000 | rachel231 | (~rachel231@c-73-142-199-151.hsd1.nh.comcast.net) (Quit: Connection closed) |
| 2021-07-03 04:21:44 +0000 | <edrx> | 2) when I used the Agda from Debian I had to call it like this: "agda -i. -i/usr/share/agda-stdlib test1.agda". It seems that now the path to agda-stdlib should be replaced by something that points to the agda-stdlib from cabal, that haven't even been able to locate in ~/.cabal/... |
| 2021-07-03 04:22:19 +0000 | <edrx> | any recommended pointers? I am very newbie-ish on those things - like Haskell, Cabal, and Agda... |
| 2021-07-03 04:22:53 +0000 | <edrx> | apologies for asking here, but in #agda people usually take 12 to 24 hours to answer =/ |
| 2021-07-03 04:28:05 +0000 | <sclv> | you can ‘cabal unpack agda’ to get access to its static files directly |
| 2021-07-03 04:28:17 +0000 | <sclv> | if you don’t like the weird place cabal installs em too |
| 2021-07-03 04:29:46 +0000 | dunkeln_ | (~dunkeln@94.129.65.28) |
| 2021-07-03 04:32:26 +0000 | <edrx> | trying! |
| 2021-07-03 04:34:37 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 04:35:47 +0000 | myShoggoth | (~myShoggot@75.164.51.64) (Ping timeout: 268 seconds) |
| 2021-07-03 04:36:01 +0000 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2021-07-03 04:36:12 +0000 | myShoggoth | (~myShoggot@75.164.51.64) |
| 2021-07-03 04:37:40 +0000 | nerdypepper | (~nerdypepp@user/nerdypepper) |
| 2021-07-03 04:43:19 +0000 | <guest61> | wait, cabal can manage agda? |
| 2021-07-03 04:43:48 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 04:44:07 +0000 | <edrx> | guest61: it seems so |
| 2021-07-03 04:44:09 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 04:45:55 +0000 | <edrx> | guest61: look here: https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=12 |
| 2021-07-03 04:50:34 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 04:54:40 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 04:54:41 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 04:54:43 +0000 | cheater1__ | cheater |
| 2021-07-03 04:55:07 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 04:57:30 +0000 | berberman_ | (~berberman@user/berberman) (Ping timeout: 240 seconds) |
| 2021-07-03 04:58:03 +0000 | berberman | (~berberman@user/berberman) |
| 2021-07-03 05:00:23 +0000 | qbt | (~edun@user/edun) |
| 2021-07-03 05:01:41 +0000 | AgentM | (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.) |
| 2021-07-03 05:03:02 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 05:09:06 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-03 05:10:58 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 05:12:33 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 2021-07-03 05:17:28 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 05:22:01 +0000 | <edrx> | guest61: I am trying to comple the Hello World program now... did not work, but I reported the reason here: https://github.com/agda/agda/issues/5466 |
| 2021-07-03 05:25:32 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 05:29:22 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 05:30:49 +0000 | <edrx> | sclv: btw, "cabal unpack agda" worked great, thanks! |
| 2021-07-03 05:30:56 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 05:32:29 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 05:32:55 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 05:33:43 +0000 | <tomsmeding> | edrx: the 3rd path of the first listing is equal to the 2nd path of the second listing? |
| 2021-07-03 05:34:01 +0000 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2021-07-03 05:34:08 +0000 | <tomsmeding> | oh I misunderstood, you have the file in the first path |
| 2021-07-03 05:35:24 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 252 seconds) |
| 2021-07-03 05:35:50 +0000 | <tomsmeding> | looks like the rest of the documentation instructs to use "open import Agda.Builtin.IO", which makes sense given the paths |
| 2021-07-03 05:36:09 +0000 | <edrx> | oh, let me try that |
| 2021-07-03 05:36:11 +0000 | <tomsmeding> | e.g. section 2.3.2 |
| 2021-07-03 05:36:34 +0000 | <tomsmeding> | not sure why 2.4.4 has the different module name; looks like a documentation bug in 2.4.4 to me |
| 2021-07-03 05:36:57 +0000 | <tomsmeding> | also only hit of "open import io" :D |
| 2021-07-03 05:37:51 +0000 | <edrx> | I got another error: |
| 2021-07-03 05:37:52 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 05:37:53 +0000 | <edrx> | Not in scope: |
| 2021-07-03 05:37:53 +0000 | <edrx> | run at /home/edrx/AGDA/test1.agda:8,8-11 |
| 2021-07-03 05:37:53 +0000 | <edrx> | when scope checking run |
| 2021-07-03 05:39:04 +0000 | <tomsmeding> | ooooh I got your problem |
| 2021-07-03 05:39:18 +0000 | dunkeln_ | (~dunkeln@94.129.65.28) (Ping timeout: 256 seconds) |
| 2021-07-03 05:39:24 +0000 | <tomsmeding> | that path contains just the agda builtin base files, not the Agda Standard Library, which does have an IO module |
| 2021-07-03 05:39:33 +0000 | <tomsmeding> | and presumably also a 'run' function |
| 2021-07-03 05:40:09 +0000 | <tomsmeding> | see 2.3.2 and the note at the bottom of that section |
| 2021-07-03 05:40:15 +0000 | <edrx> | looking! |
| 2021-07-03 05:40:59 +0000 | <tomsmeding> | so you'll have to figure out not where 'agda' stores its .agda files but where 'agda-stdlib' stores its .agda files :D |
| 2021-07-03 05:41:10 +0000 | dunkeln | (~dunkeln@94.129.65.28) |
| 2021-07-03 05:41:17 +0000 | pfurla | (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-07-03 05:42:00 +0000 | pfurla_ | (~pfurla@216.131.83.59) (Ping timeout: 252 seconds) |
| 2021-07-03 05:42:47 +0000 | <edrx> | tomsmeding: I tried that... I tried "cd ~/.cabal/; find * | grep -i stdlib" but got no results... |
| 2021-07-03 05:43:06 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2021-07-03 05:43:45 +0000 | <edrx> | and the same but with grep -i io.agda only returns the IO.agda in ~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/lib/prim/Agda/Builtin/IO.agda ... |
| 2021-07-03 05:43:48 +0000 | <tomsmeding> | try 'find ~ -name agda-stdlib' |
| 2021-07-03 05:43:55 +0000 | <edrx> | ok! |
| 2021-07-03 05:44:08 +0000 | jess | (~jess@libera/staff/jess) (Remote host closed the connection) |
| 2021-07-03 05:44:19 +0000 | <tomsmeding> | "grep -i io.agda" is not going to help much, that searches the _content_ of files for that string :p |
| 2021-07-03 05:44:25 +0000 | <tomsmeding> | how did you install agda-stdlib? |
| 2021-07-03 05:44:36 +0000 | <edrx> | I didn't =( |
| 2021-07-03 05:44:54 +0000 | <tomsmeding> | then you should! |
| 2021-07-03 05:45:04 +0000 | <edrx> | I only have the agda-stdlib from Debian, not one in cabal... ok, trying! |
| 2021-07-03 05:45:09 +0000 | <tomsmeding> | either https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md or perhaps the debian package? not sure if that is remotely new enough |
| 2021-07-03 05:45:25 +0000 | <tomsmeding> | edrx: don't think you're going to get one from cabal |
| 2021-07-03 05:45:38 +0000 | <edrx> | the docs say that the Debian package is too broken |
| 2021-07-03 05:46:00 +0000 | <tomsmeding> | lol |
| 2021-07-03 05:46:07 +0000 | <tomsmeding> | then use the link I sent I guess |
| 2021-07-03 05:46:38 +0000 | <tomsmeding> | right and that also explains how to point the main 'agda' executable to wherever you put the stdlib |
| 2021-07-03 05:47:54 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:b096:1d82:d091:433d) (Ping timeout: 240 seconds) |
| 2021-07-03 05:48:01 +0000 | slack1256 | (~slack1256@191.125.188.158) |
| 2021-07-03 05:49:10 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:6abc:acbb:6923:464a) |
| 2021-07-03 05:55:34 +0000 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2021-07-03 05:57:18 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 06:00:32 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2021-07-03 06:01:07 +0000 | Xnuk | (~xnuk@45.76.202.58) (Quit: ZNC - https://znc.in) |
| 2021-07-03 06:01:24 +0000 | Xnuk | (~xnuk@vultr.xnu.kr) |
| 2021-07-03 06:01:53 +0000 | chomwitt | (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) |
| 2021-07-03 06:02:10 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2021-07-03 06:03:58 +0000 | dunkeln | (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 2021-07-03 06:03:59 +0000 | <edrx> | tomsmeding: I downloaded it, unpacked it, ran "cabal install", and patched ~/.agda/libraries and ~/.agda/defaults according to the instructions, but when I try to compile my test1.agda I still get the same error. Do I need a line like "open import Agda.Builtin.IO" in my ~/AGDA/test1.agda that loads a file that declares "run"? |
| 2021-07-03 06:04:33 +0000 | <tomsmeding> | no 'open import IO' should be enough |
| 2021-07-03 06:04:40 +0000 | <edrx> | trying! |
| 2021-07-03 06:06:29 +0000 | <tomsmeding> | O.o 'agda --compile' does something exceedingly weird on my system |
| 2021-07-03 06:07:38 +0000 | chomwitt | (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) (Ping timeout: 256 seconds) |
| 2021-07-03 06:07:45 +0000 | dunkeln | (~dunkeln@94.129.65.28) |
| 2021-07-03 06:08:12 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 06:08:24 +0000 | <edrx> | what? |
| 2021-07-03 06:09:54 +0000 | myShoggoth | (~myShoggot@75.164.51.64) (Ping timeout: 256 seconds) |
| 2021-07-03 06:10:08 +0000 | sheepduck | (~sheepduck@user/sheepduck) (Quit: Konversation terminated!) |
| 2021-07-03 06:10:35 +0000 | <edrx> | ok, now "agda test1.agda" compiled lots of stuff in agda-stdlib... |
| 2021-07-03 06:10:42 +0000 | <edrx> | but I got a new error: |
| 2021-07-03 06:10:51 +0000 | <edrx> | Importing module IO using the --guardedness flag from a module which does not. |
| 2021-07-03 06:10:51 +0000 | <edrx> | when scope checking the declaration |
| 2021-07-03 06:10:51 +0000 | <edrx> | open import IO |
| 2021-07-03 06:12:16 +0000 | <tomsmeding> | --guardedness should be the default, according to agda's option listing |
| 2021-07-03 06:12:33 +0000 | <tomsmeding> | but I guess you can try adding it (i.e. agda --compile --guardedness' |
| 2021-07-03 06:12:42 +0000 | <tomsmeding> | s/'/)/ |
| 2021-07-03 06:13:01 +0000 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-07-03 06:13:12 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2021-07-03 06:15:07 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 06:17:18 +0000 | <edrx> | new error: I ran "agda --compile --guardedness test1.agda" and it gave lots of lines like "Checking Data.List.Relation.Binary.Lex.Core (/home/edrx/usrc/agda-stdlib-1.7/src/Data/List/Relation/Binary/Lex/Core.agda)."... and then it aborted with: |
| 2021-07-03 06:17:23 +0000 | <edrx> | Unsolved metas at the following locations: |
| 2021-07-03 06:17:23 +0000 | <edrx> | /home/edrx/AGDA/test1.agda:9,8-11 |
| 2021-07-03 06:18:26 +0000 | <edrx> | at line 9, columns 8-11 of test1.agda I have "run". |
| 2021-07-03 06:20:10 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 06:20:55 +0000 | slowButPresent | (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 2021-07-03 06:23:02 +0000 | tomsmeding | is compiling a more recent agda |
| 2021-07-03 06:24:51 +0000 | chexum | (~chexum@gateway/tor-sasl/chexum) |
| 2021-07-03 06:25:33 +0000 | Erutuon | (~Erutuon@user/erutuon) (Ping timeout: 268 seconds) |
| 2021-07-03 06:26:54 +0000 | edrx | is latexing a diagram in trog mode |
| 2021-07-03 06:29:22 +0000 | <tomsmeding> | edrx: I got hello world to compile! |
| 2021-07-03 06:31:29 +0000 | <tomsmeding> | edrx: https://paste.tomsmeding.com/dNKEhru6 |
| 2021-07-03 06:31:33 +0000 | slack1256 | (~slack1256@191.125.188.158) (Remote host closed the connection) |
| 2021-07-03 06:31:46 +0000 | <tomsmeding> | the 'cabal build' exits with an error but is necessary to construct the package db, it seems |
| 2021-07-03 06:31:56 +0000 | <tomsmeding> | relevant: https://github.com/agda/agda/issues/3619 |
| 2021-07-03 06:33:34 +0000 | jespada | (~jespada@90.254.247.46) (Ping timeout: 268 seconds) |
| 2021-07-03 06:33:57 +0000 | <edrx> | works!!! thanks!!! =) |
| 2021-07-03 06:35:14 +0000 | jespada | (~jespada@90.254.247.46) |
| 2021-07-03 06:36:12 +0000 | <edrx> | I didn't need the package db or the Numeric.IEEE fix... but I when I copied the code for hello world from the manual it didn't have this line: "main : Main" |
| 2021-07-03 06:36:18 +0000 | <tomsmeding> | also relevant: https://github.com/agda/agda/issues/4627 |
| 2021-07-03 06:36:25 +0000 | <tomsmeding> | apparently they're working on making this a bit smoother :) |
| 2021-07-03 06:36:51 +0000 | <edrx> | thanks a lot!!!!!!!! =) |
| 2021-07-03 06:37:18 +0000 | <tomsmeding> | edrx: ah I see, and then you're getting this "unresolved metas" line |
| 2021-07-03 06:37:39 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 06:37:45 +0000 | <tomsmeding> | I know very little about agda the language (and in particular the standard library), but I guess that type signature is necessary? |
| 2021-07-03 06:38:03 +0000 | <tomsmeding> | and that if the compiler would have gotten past that, you would have run into the same issue |
| 2021-07-03 06:38:07 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 06:38:17 +0000 | Gurkenglas | (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) |
| 2021-07-03 06:38:40 +0000 | tomsmeding | now suddenly doesn't need the db fix either anymore? |
| 2021-07-03 06:38:46 +0000 | tomsmeding | is confused but holes edrx is happy |
| 2021-07-03 06:38:58 +0000 | mei | (~mei@user/mei) |
| 2021-07-03 06:39:07 +0000 | <tomsmeding> | s/holes/hopes/ |
| 2021-07-03 06:39:25 +0000 | <edrx> | seems to be. I just found that Main is defined in src/IO/Base.agda - I'll try to understand that... |
| 2021-07-03 06:39:37 +0000 | <edrx> | does Agda support holes like Idris? |
| 2021-07-03 06:39:45 +0000 | argento | (~argent0@168-227-96-53.ptr.westnet.com.ar) |
| 2021-07-03 06:40:26 +0000 | argento | (~argent0@168-227-96-53.ptr.westnet.com.ar) (Client Quit) |
| 2021-07-03 06:41:31 +0000 | <edrx> | anyway, don't worry about that! I need to sleep, thanks again! =) |
| 2021-07-03 06:46:19 +0000 | <tomsmeding> | edrx: it should support that! |
| 2021-07-03 06:48:14 +0000 | tomek-grzesiak | (~tomek-grz@109.206.213.203) |
| 2021-07-03 06:49:08 +0000 | <tomsmeding> | edrx: I think you're supposed to use agda from an editor with editor integration; emacs seems to be the most-supported thing, but atom, or with some configuration vim, may also work |
| 2021-07-03 06:49:12 +0000 | neo1 | (~neo3@cpe-292712.ip.primehome.com) |
| 2021-07-03 06:49:15 +0000 | <tomsmeding> | then _ or ? or {!!} are holes |
| 2021-07-03 06:49:55 +0000 | neo | (~neo3@cpe-292712.ip.primehome.com) (Ping timeout: 258 seconds) |
| 2021-07-03 06:51:18 +0000 | dunkeln | (~dunkeln@94.129.65.28) (Ping timeout: 252 seconds) |
| 2021-07-03 06:51:50 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 06:52:15 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 06:58:53 +0000 | Lycurgus | (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-07-03 06:59:26 +0000 | chomwitt | (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) |
| 2021-07-03 06:59:31 +0000 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-07-03 07:00:32 +0000 | beka__ | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 265 seconds) |
| 2021-07-03 07:02:51 +0000 | dunkeln_ | (~dunkeln@94.129.65.28) |
| 2021-07-03 07:02:56 +0000 | tomek-grzesiak | (~tomek-grz@109.206.213.203) (Quit: Leaving) |
| 2021-07-03 07:03:44 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:6abc:acbb:6923:464a) (Ping timeout: 256 seconds) |
| 2021-07-03 07:04:20 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:3a82:123e:2fdc:d4a3) |
| 2021-07-03 07:05:14 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 07:05:43 +0000 | <edrx> | tomsmeding: great! thx again! (and gnight) =) |
| 2021-07-03 07:06:20 +0000 | tomek-grzesiak | (~tomek-grz@109.206.213.203) |
| 2021-07-03 07:10:07 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 07:13:02 +0000 | mei | (~mei@user/mei) (Quit: Client closed) |
| 2021-07-03 07:14:20 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 07:14:53 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 268 seconds) |
| 2021-07-03 07:17:09 +0000 | jneira_ | (~jneira_@217.red-81-39-172.dynamicip.rima-tde.net) (Quit: Connection closed) |
| 2021-07-03 07:17:15 +0000 | tomek-grzesiak | (~tomek-grz@109.206.213.203) (Quit: Leaving) |
| 2021-07-03 07:17:44 +0000 | vursc | (~wangxm@219.137.140.171) |
| 2021-07-03 07:18:09 +0000 | mei | (~mei@user/mei) |
| 2021-07-03 07:18:54 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 265 seconds) |
| 2021-07-03 07:20:43 +0000 | Arahael | is so tempted to rewrite his iOS app in haskell. |
| 2021-07-03 07:22:11 +0000 | edrx | (~Eduardo@2804:56c:d2e2:8b00:8d96:adf9:cdb8:eb7e) (Killed buffer) |
| 2021-07-03 07:25:39 +0000 | tzh | (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 2021-07-03 07:30:07 +0000 | kuribas | (~user@ptr-25vy0i7jjgjyv5cv6ky.18120a2.ip6.access.telenet.be) |
| 2021-07-03 07:30:27 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5bf:4bd7:7b8b:fdcf) (Remote host closed the connection) |
| 2021-07-03 07:30:55 +0000 | <kuribas> | I am looking at wingman tactics. It looks kind of cool, but I wonder what is the advantage, because typing tactics looks more work that just coding it! |
| 2021-07-03 07:31:51 +0000 | <jophish> | ☝️ |
| 2021-07-03 07:32:37 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 07:32:56 +0000 | <kuribas> | Maybe it saves work if you have a huge data type... |
| 2021-07-03 07:33:10 +0000 | <Lycurgus> | what besides hs compiled to js runs on iOS? |
| 2021-07-03 07:34:04 +0000 | Lycurgus | Arahael |
| 2021-07-03 07:34:50 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 07:35:15 +0000 | <Arahael> | Lycurgus: hs compiles to the metal, too. But I'm not referring to the UI here, just the business logic. |
| 2021-07-03 07:35:43 +0000 | Tuplanolla | (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 2021-07-03 07:39:21 +0000 | <Lycurgus> | i c, the right thinking if you mean serverside imo, but then that's not iOS is it |
| 2021-07-03 07:39:33 +0000 | fabfianda | (~fabfianda@37.183.255.57) (Ping timeout: 268 seconds) |
| 2021-07-03 07:40:10 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-07-03 07:40:27 +0000 | fabfianda | (~fabfianda@mob-5-90-245-137.net.vodafone.it) |
| 2021-07-03 07:41:48 +0000 | mikoto-chan | (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-07-03 07:42:19 +0000 | <Arahael> | No, my server side is already haskell, I mean, teh business logic in the client side. |
| 2021-07-03 07:42:29 +0000 | <Arahael> | I'm _tempted_ to do it, but it's probably not worth it. |
| 2021-07-03 07:42:30 +0000 | vursc | (~wangxm@219.137.140.171) (Read error: Connection reset by peer) |
| 2021-07-03 07:47:55 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 07:50:18 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 07:51:53 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-03 07:52:03 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 07:56:25 +0000 | boxscape_ | (~boxscape_@p4ff0ba7a.dip0.t-ipconnect.de) |
| 2021-07-03 07:57:28 +0000 | <boxscape> | kuribas: From what I understood the idea is that many similar problems (e.g. writing a functor instance for various data types) can be solved with the exact same series of tactics |
| 2021-07-03 07:57:52 +0000 | <boxscape> | kuribas: though I think the tooling at the moment doesn't make it very convenient to use them in that way |
| 2021-07-03 07:58:08 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 07:58:32 +0000 | <boxscape> | (Then again, I haven't actually tried using them) |
| 2021-07-03 07:59:05 +0000 | <maerwald> | kuribas: I had the same impression... other than the "try to auto-fill in the definition", I probably wouldn't use much of wingman |
| 2021-07-03 08:00:21 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 08:00:53 +0000 | <maerwald> | I'd much rather have HLS show me the type of an expression :> |
| 2021-07-03 08:00:54 +0000 | fendor | (~fendor@77.119.220.92.wireless.dyn.drei.com) |
| 2021-07-03 08:01:54 +0000 | mc47 | (~mc47@xmonad/TheMC47) |
| 2021-07-03 08:02:31 +0000 | haykam1 | (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-07-03 08:02:45 +0000 | haykam2 | (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-07-03 08:07:08 +0000 | neo1 | (~neo3@cpe-292712.ip.primehome.com) (Remote host closed the connection) |
| 2021-07-03 08:07:14 +0000 | hendursa1 | (~weechat@user/hendursaga) |
| 2021-07-03 08:07:18 +0000 | fabfianda | (~fabfianda@mob-5-90-245-137.net.vodafone.it) (Ping timeout: 268 seconds) |
| 2021-07-03 08:07:50 +0000 | fabfianda | (~fabfianda@mob-5-90-255-101.net.vodafone.it) |
| 2021-07-03 08:08:01 +0000 | unyu | (~pyon@user/pyon) (Quit: WeeChat 3.2) |
| 2021-07-03 08:08:54 +0000 | hendursaga | (~weechat@user/hendursaga) (Ping timeout: 244 seconds) |
| 2021-07-03 08:10:58 +0000 | phma | (phma@2001:5b0:211f:42c8:39c2:9ea1:f2e8:75b1) (Read error: Connection reset by peer) |
| 2021-07-03 08:11:43 +0000 | qbt | (~edun@user/edun) (Quit: WeeChat 3.2) |
| 2021-07-03 08:11:55 +0000 | phma | (phma@2001:5b0:212a:faf8:be49:b217:da87:a28c) |
| 2021-07-03 08:12:44 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 08:12:52 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 08:12:59 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 08:14:30 +0000 | zeenk | (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) |
| 2021-07-03 08:15:18 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 08:15:53 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 08:16:50 +0000 | <kuribas> | that's already very useful. |
| 2021-07-03 08:16:58 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2021-07-03 08:17:03 +0000 | <kuribas> | maerwald: it can do that, right? |
| 2021-07-03 08:17:10 +0000 | dunkeln_ | (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 2021-07-03 08:17:20 +0000 | hnOsmium0001 | (uid453710@stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-07-03 08:17:21 +0000 | <maerwald> | kuribas: not afaik |
| 2021-07-03 08:17:24 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 256 seconds) |
| 2021-07-03 08:17:27 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 08:17:51 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 08:17:57 +0000 | <maerwald> | it's also not defined in the LSP protocol |
| 2021-07-03 08:18:26 +0000 | acidjnk | (~acidjnk@p200300d0c72b9558d4454a820777d511.dip0.t-ipconnect.de) |
| 2021-07-03 08:18:59 +0000 | _ht | (~quassel@82-169-194-8.biz.kpn.net) |
| 2021-07-03 08:19:00 +0000 | <maerwald> | https://github.com/microsoft/language-server-protocol/issues/377 |
| 2021-07-03 08:19:49 +0000 | <maerwald> | https://github.com/haskell/haskell-language-server/issues/709 |
| 2021-07-03 08:20:00 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 258 seconds) |
| 2021-07-03 08:20:01 +0000 | Lord_of_Life_ | Lord_of_Life |
| 2021-07-03 08:20:12 +0000 | <kuribas> | hmm, I can do that in flycheck-haskell |
| 2021-07-03 08:20:24 +0000 | <kuribas> | erm emacs-mode... |
| 2021-07-03 08:22:24 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 08:22:24 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds) |
| 2021-07-03 08:23:15 +0000 | dunkeln_ | (~dunkeln@94.129.65.28) |
| 2021-07-03 08:23:38 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 08:23:48 +0000 | turlando | (~turlando@93-42-250-112.ip89.fastwebnet.it) |
| 2021-07-03 08:23:48 +0000 | turlando | (~turlando@93-42-250-112.ip89.fastwebnet.it) (Changing host) |
| 2021-07-03 08:23:48 +0000 | turlando | (~turlando@user/turlando) |
| 2021-07-03 08:25:47 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 08:26:16 +0000 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2021-07-03 08:26:18 +0000 | ubert | (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) |
| 2021-07-03 08:29:38 +0000 | Guest9 | (~Guest9@103.249.233.78) |
| 2021-07-03 08:30:28 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 08:30:50 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 08:31:58 +0000 | dunkeln_ | (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 2021-07-03 08:33:08 +0000 | Cajun | (~Cajun@ip98-163-211-112.no.no.cox.net) (Quit: Client closed) |
| 2021-07-03 08:35:06 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Ping timeout: 240 seconds) |
| 2021-07-03 08:36:23 +0000 | amahl | (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-07-03 08:38:09 +0000 | amahl | (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2021-07-03 08:38:43 +0000 | dunkeln | (~dunkeln@94.129.65.28) |
| 2021-07-03 08:41:45 +0000 | amahl | (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-07-03 08:46:27 +0000 | dunkeln | (~dunkeln@94.129.65.28) (Ping timeout: 258 seconds) |
| 2021-07-03 08:48:22 +0000 | unyu | (~pyon@user/pyon) |
| 2021-07-03 08:53:59 +0000 | dunkeln | (~dunkeln@94.129.65.28) |
| 2021-07-03 08:54:10 +0000 | chris_ | (~chris@2a02:c7f:af4a:cb00:882f:b5f9:7cab:3133) |
| 2021-07-03 08:54:25 +0000 | Lycurgus | (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-07-03 08:55:32 +0000 | jumper149 | (~jumper149@80.240.31.34) |
| 2021-07-03 08:55:58 +0000 | fabfianda | (~fabfianda@mob-5-90-255-101.net.vodafone.it) (Ping timeout: 252 seconds) |
| 2021-07-03 08:56:25 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 08:56:34 +0000 | fabfianda | (~fabfianda@mob-5-90-128-19.net.vodafone.it) |
| 2021-07-03 08:56:40 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 08:57:06 +0000 | shredder | (~user@user/shredder) (Quit: quitting) |
| 2021-07-03 08:57:55 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 08:58:12 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 08:58:26 +0000 | shredder | (~user@user/shredder) |
| 2021-07-03 09:00:20 +0000 | ubert | (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2021-07-03 09:00:21 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 09:02:33 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 258 seconds) |
| 2021-07-03 09:02:49 +0000 | tomsmeding | always makes an ad-hoc let binding with the thing I want the type of |
| 2021-07-03 09:03:15 +0000 | <tomsmeding> | also I wouldn't know how the editor UI would look for requesting the type of an arbitrary subexpression |
| 2021-07-03 09:03:51 +0000 | <tomsmeding> | would you get the type of 'f x' by requesting the type of the space in between? |
| 2021-07-03 09:04:01 +0000 | <tomsmeding> | what about 'f$x' :p |
| 2021-07-03 09:04:16 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) (Ping timeout: 265 seconds) |
| 2021-07-03 09:04:25 +0000 | azeem | (~azeem@176.201.38.107) |
| 2021-07-03 09:08:27 +0000 | <maerwald> | you select the expression |
| 2021-07-03 09:08:43 +0000 | <maerwald> | if your editor can't do that, then I'm sorry :) |
| 2021-07-03 09:11:22 +0000 | vonfry | (~user@113.74.228.94) |
| 2021-07-03 09:12:22 +0000 | azeem | (~azeem@176.201.38.107) (Read error: Connection reset by peer) |
| 2021-07-03 09:12:41 +0000 | chris_ | (~chris@2a02:c7f:af4a:cb00:882f:b5f9:7cab:3133) (Remote host closed the connection) |
| 2021-07-03 09:12:56 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 09:13:23 +0000 | chris_ | (~chris@2a02:c7f:af4a:cb00:882f:b5f9:7cab:3133) |
| 2021-07-03 09:13:48 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) |
| 2021-07-03 09:15:15 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 09:16:05 +0000 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Quit: Lost terminal) |
| 2021-07-03 09:16:14 +0000 | mc47 | (~mc47@xmonad/TheMC47) (Ping timeout: 272 seconds) |
| 2021-07-03 09:16:43 +0000 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 2021-07-03 09:17:30 +0000 | chris_ | (~chris@2a02:c7f:af4a:cb00:882f:b5f9:7cab:3133) (Ping timeout: 240 seconds) |
| 2021-07-03 09:20:04 +0000 | vonfry | (~user@113.74.228.94) (Ping timeout: 268 seconds) |
| 2021-07-03 09:21:05 +0000 | crazazy | (~user@130.89.171.203) |
| 2021-07-03 09:23:25 +0000 | maerwald | stares at tomsmeding |
| 2021-07-03 09:34:22 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-03 09:36:42 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 09:39:09 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 09:41:46 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 09:46:38 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 2021-07-03 09:57:06 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 09:57:31 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 10:02:05 +0000 | <kuribas> | LSP: failed to parse the result of calling cabal... |
| 2021-07-03 10:02:10 +0000 | <kuribas> | new-build works fine... |
| 2021-07-03 10:02:10 +0000 | dunkeln__ | (~dunkeln@188.70.10.165) |
| 2021-07-03 10:02:45 +0000 | <turlando> | How should I format long import lines? Suppose I'm importing specific symbols and the namespace is very long and there's no much space for the symbols afterwards |
| 2021-07-03 10:02:49 +0000 | <kuribas> | Preprocessing library for memory-0.16.0.. cabal: The program 'hsc2hs' is required but it could not be found. |
| 2021-07-03 10:03:11 +0000 | <kuribas> | turlando: on a new line? :-) |
| 2021-07-03 10:03:14 +0000 | dunkeln | (~dunkeln@94.129.65.28) (Ping timeout: 265 seconds) |
| 2021-07-03 10:03:25 +0000 | <turlando> | Yeah but how should I align that? |
| 2021-07-03 10:04:07 +0000 | <kuribas> | turlando: doesn't matter, as long as you indent it relatively. |
| 2021-07-03 10:04:15 +0000 | <maerwald> | kuribas: on windows? |
| 2021-07-03 10:04:23 +0000 | <kuribas> | maerwald: linux |
| 2021-07-03 10:05:09 +0000 | <turlando> | kuribas right but there's some convention? |
| 2021-07-03 10:07:38 +0000 | anandprabhu | (~anandprab@94.202.243.198) |
| 2021-07-03 10:08:01 +0000 | xsperry | (~as@user/xsperry) (Remote host closed the connection) |
| 2021-07-03 10:10:38 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-07-03 10:11:05 +0000 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2021-07-03 10:20:09 +0000 | pera | (~pera@user/pera) |
| 2021-07-03 10:22:11 +0000 | <kuribas> | turlando: there are different ways |
| 2021-07-03 10:22:18 +0000 | <kuribas> | there is no one agreed style. |
| 2021-07-03 10:24:09 +0000 | ph88_ | (~ph88@95.90.246.253) (Quit: Leaving) |
| 2021-07-03 10:24:54 +0000 | chomwitt | (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) (Ping timeout: 256 seconds) |
| 2021-07-03 10:25:23 +0000 | <kuribas> | turlando: here's my style: https://github.com/kuribas/hasqlator-mysql/blob/main/src/Database/MySQL/Hasqlator.hs |
| 2021-07-03 10:26:29 +0000 | <turlando> | Thank you kuribas but I was asking what to do when the line goes over 80 chars |
| 2021-07-03 10:26:53 +0000 | <kuribas> | turlando: you mean with one very big import? |
| 2021-07-03 10:27:00 +0000 | <turlando> | Precisely |
| 2021-07-03 10:27:03 +0000 | <kuribas> | turlando: just let it go over 80 chars? |
| 2021-07-03 10:27:20 +0000 | <turlando> | :\ |
| 2021-07-03 10:27:36 +0000 | <kuribas> | I mean, firstly, don't let imports become this bug. |
| 2021-07-03 10:27:37 +0000 | <kuribas> | big |
| 2021-07-03 10:27:46 +0000 | <kuribas> | otherwise, who cares? |
| 2021-07-03 10:28:08 +0000 | <turlando> | That's pretty hard when you're importing a whole bunch of stuff from a very long namespace |
| 2021-07-03 10:28:29 +0000 | <turlando> | Well it might be silly but I don't like line wraps |
| 2021-07-03 10:28:32 +0000 | chris_ | (~chris@81.96.113.213) |
| 2021-07-03 10:29:25 +0000 | <boxscape_> | turlando the GHC codebase has a few imports that look like this https://paste.tomsmeding.com/92WPB44q |
| 2021-07-03 10:30:30 +0000 | <kuribas> | turlando: put the import list on a new line? |
| 2021-07-03 10:30:31 +0000 | <turlando> | Thank you boxscape_, that's basically what I'm doing now but it feels so wrong when you have a very long namespace and very little space for the imported symbols. Not sure if it's clear what I'm trying to explain, I can show an example |
| 2021-07-03 10:30:38 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 10:30:40 +0000 | <boxscape_> | I get what you mean |
| 2021-07-03 10:31:07 +0000 | <turlando> | kuribas yeah I think I will do that and align the symbols to the namespace |
| 2021-07-03 10:32:32 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 10:34:00 +0000 | Gurkenglas | (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) (Remote host closed the connection) |
| 2021-07-03 10:34:21 +0000 | Gurkenglas | (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) |
| 2021-07-03 10:34:29 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) |
| 2021-07-03 10:34:58 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 252 seconds) |
| 2021-07-03 10:35:31 +0000 | kuribas | (~user@ptr-25vy0i7jjgjyv5cv6ky.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-07-03 10:35:37 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 2021-07-03 10:35:41 +0000 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-07-03 10:35:59 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 10:36:21 +0000 | otulp | (~otulp@ti0187q162-2423.bb.online.no) (Quit: *POOF*) |
| 2021-07-03 10:36:42 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Ping timeout: 240 seconds) |
| 2021-07-03 10:37:03 +0000 | img | (~img@user/img) |
| 2021-07-03 10:38:02 +0000 | fabfianda | (~fabfianda@mob-5-90-128-19.net.vodafone.it) (Ping timeout: 265 seconds) |
| 2021-07-03 10:38:55 +0000 | fabfianda | (~fabfianda@37.183.255.57) |
| 2021-07-03 10:41:23 +0000 | acidjnk_new | (~acidjnk@p200300d0c72b955875652e86484602de.dip0.t-ipconnect.de) |
| 2021-07-03 10:41:43 +0000 | __monty__ | (~toonn@user/toonn) |
| 2021-07-03 10:43:36 +0000 | acidjnk | (~acidjnk@p200300d0c72b9558d4454a820777d511.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2021-07-03 10:44:24 +0000 | shredder | (~user@user/shredder) (Quit: quitting) |
| 2021-07-03 10:45:32 +0000 | Gurkenglas | (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) (Ping timeout: 272 seconds) |
| 2021-07-03 10:45:55 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 10:46:44 +0000 | shredder | (~user@user/shredder) |
| 2021-07-03 10:48:16 +0000 | chris_ | (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-07-03 10:48:18 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:3a82:123e:2fdc:d4a3) (Ping timeout: 240 seconds) |
| 2021-07-03 10:48:56 +0000 | chris_ | (~chris@81.96.113.213) |
| 2021-07-03 10:49:32 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:ff7c:fc0:389a:fc47) |
| 2021-07-03 10:50:36 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 265 seconds) |
| 2021-07-03 10:53:08 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-07-03 10:53:20 +0000 | chris_ | (~chris@81.96.113.213) (Ping timeout: 258 seconds) |
| 2021-07-03 10:54:02 +0000 | <Las[m]> | Is it possible to share the GHC process for several GHCi's when using -fexternal-interpreter? |
| 2021-07-03 10:54:53 +0000 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2021-07-03 10:55:05 +0000 | jakalx | (~jakalx@base.jakalx.net) |
| 2021-07-03 10:57:56 +0000 | chris_ | (~chris@81.96.113.213) |
| 2021-07-03 11:00:36 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 11:03:07 +0000 | pricly_yellow | (~pricly_ye@2a01:620:c04d:b00::339) |
| 2021-07-03 11:04:40 +0000 | rizary_andika_ | (sid220347@id-220347.tooting.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-07-03 11:05:39 +0000 | xsperry | (~as@user/xsperry) |
| 2021-07-03 11:06:00 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) |
| 2021-07-03 11:06:27 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 11:10:32 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 11:10:32 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-07-03 11:10:32 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Read error: Connection reset by peer) |
| 2021-07-03 11:10:59 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 11:11:36 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) |
| 2021-07-03 11:15:24 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 11:15:54 +0000 | acidjnk_new | (~acidjnk@p200300d0c72b955875652e86484602de.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2021-07-03 11:20:55 +0000 | PPK | (~mark@2a00:23c6:d280:3700:572a:c2f0:ddc5:b769) |
| 2021-07-03 11:23:11 +0000 | <PPK> | Hey. So I found generic-lens and it's great; but if I have a nested hierarchy (e.g. data A = A B C; data C = C; data B = B D E) then a ^. typed @B is fine, a ^. typed @C is fine, toListOf (types @D) a is fine (but a traversal..), but I can't do a nested lens - a ^. typed @D does not compile..I think uniplate has the same problem that it's all traversals rather than compile time. Any obvious fix? |
| 2021-07-03 11:29:56 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 11:30:15 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 11:32:42 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 11:33:39 +0000 | ubert | (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) |
| 2021-07-03 11:34:18 +0000 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 2021-07-03 11:35:14 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 11:35:20 +0000 | jess | (~jess@libera/staff/jess) |
| 2021-07-03 11:36:15 +0000 | arjun | (~user@user/arjun) |
| 2021-07-03 11:38:09 +0000 | fef | (~thedawn@user/thedawn) (Ping timeout: 244 seconds) |
| 2021-07-03 11:42:33 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 11:43:07 +0000 | fendor | (~fendor@77.119.220.92.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2021-07-03 11:43:24 +0000 | nick8325 | (~nick@2001:9b1:26f9:3e00:b7ea:ac95:e18:4c1d) |
| 2021-07-03 11:43:48 +0000 | ubert | (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2021-07-03 11:45:28 +0000 | boxscape_ | (~boxscape_@p4ff0ba7a.dip0.t-ipconnect.de) (Ping timeout: 258 seconds) |
| 2021-07-03 11:47:30 +0000 | fendor | (~fendor@77.119.220.92.wireless.dyn.drei.com) |
| 2021-07-03 11:47:36 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 11:58:26 +0000 | acidjnk_new | (~acidjnk@p200300d0c72b953339f341015709cf67.dip0.t-ipconnect.de) |
| 2021-07-03 12:02:22 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 12:02:52 +0000 | neo1 | (~neo3@cpe-292712.ip.primehome.com) |
| 2021-07-03 12:04:18 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-07-03 12:04:44 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 12:07:17 +0000 | <maerwald> | can you force autoreconf for a dependency? |
| 2021-07-03 12:11:07 +0000 | jippiedoe | (~david@2a02-a44c-e14e-1-2351-c955-5b2d-b577.fixed6.kpn.net) |
| 2021-07-03 12:14:31 +0000 | warnz | (~warnz@104-55-100-55.lightspeed.lsvlky.sbcglobal.net) |
| 2021-07-03 12:17:06 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 12:19:16 +0000 | warnz | (~warnz@104-55-100-55.lightspeed.lsvlky.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 12:19:46 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 12:19:49 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 12:19:54 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 12:20:01 +0000 | cheater1__ | cheater |
| 2021-07-03 12:21:40 +0000 | dunkeln__ | (~dunkeln@188.70.10.165) (Ping timeout: 252 seconds) |
| 2021-07-03 12:28:24 +0000 | norias | (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) |
| 2021-07-03 12:31:23 +0000 | Guest9 | (~Guest9@103.249.233.78) (Quit: Connection closed) |
| 2021-07-03 12:31:31 +0000 | xwx | (~george@user/george) |
| 2021-07-03 12:31:39 +0000 | slowButPresent | (~slowButPr@user/slowbutpresent) |
| 2021-07-03 12:34:16 +0000 | <juri_> | how do i find the closest value less than X that is divisible by Y? |
| 2021-07-03 12:34:26 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 12:34:30 +0000 | <juri_> | difficulty: Double. |
| 2021-07-03 12:35:53 +0000 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-07-03 12:36:14 +0000 | <juri_> | right now i'm using head (filter (> X) [0,Y..]) |
| 2021-07-03 12:38:43 +0000 | maerwald | (~maerwald@mail.hasufell.de) (Changing host) |
| 2021-07-03 12:38:43 +0000 | maerwald | (~maerwald@user/maerwald) |
| 2021-07-03 12:39:11 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Ping timeout: 256 seconds) |
| 2021-07-03 12:42:24 +0000 | fef | (~thedawn@user/thedawn) |
| 2021-07-03 12:42:29 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 12:45:34 +0000 | tzar_bomba | (~tzar_bomb@78-56-41-78.static.zebra.lt) |
| 2021-07-03 12:45:54 +0000 | chomwitt | (~Pitsikoko@athedsl-16082.home.otenet.gr) |
| 2021-07-03 12:46:01 +0000 | tzar_bomba | (~tzar_bomb@78-56-41-78.static.zebra.lt) (Changing host) |
| 2021-07-03 12:46:01 +0000 | tzar_bomba | (~tzar_bomb@user/tzar-bomba/x-5218718) |
| 2021-07-03 12:47:53 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 2021-07-03 12:48:20 +0000 | <xerox> | :t find |
| 2021-07-03 12:48:21 +0000 | <lambdabot> | Foldable t => (a -> Bool) -> t a -> Maybe a |
| 2021-07-03 12:48:40 +0000 | waleee | (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-07-03 12:49:30 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 2021-07-03 12:49:48 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 12:50:17 +0000 | fendor | (~fendor@77.119.220.92.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-07-03 12:50:33 +0000 | waleee | (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Client Quit) |
| 2021-07-03 12:50:49 +0000 | waleee | (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-07-03 12:52:53 +0000 | dyeplexer | (~dyeplexer@user/dyeplexer) (Ping timeout: 265 seconds) |
| 2021-07-03 12:55:06 +0000 | ubert | (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) |
| 2021-07-03 12:55:38 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 12:56:59 +0000 | <tomsmeding> | maerwald: was doing other stuff, sorry :p |
| 2021-07-03 12:57:03 +0000 | <tomsmeding> | yes my editor can select things |
| 2021-07-03 12:57:43 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 12:58:06 +0000 | <tomsmeding> | and then round up the selection to the smallest AST node that contains the source range or something |
| 2021-07-03 13:00:06 +0000 | <tomsmeding> | juri_: do you mean the _smallest_ value _larger_ than X? |
| 2021-07-03 13:00:17 +0000 | <juri_> | tomsmeding: aparently. :) |
| 2021-07-03 13:00:31 +0000 | <tomsmeding> | what about: fromIntegral (ceiling (X / Y)) * Y |
| 2021-07-03 13:00:48 +0000 | <juri_> | that's where i was going. :) |
| 2021-07-03 13:01:12 +0000 | alx741 | (~alx741@186.178.109.174) |
| 2021-07-03 13:01:31 +0000 | fendor | (~fendor@77.119.220.92.wireless.dyn.drei.com) |
| 2021-07-03 13:01:37 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 13:01:38 +0000 | shailangsa | (~shailangs@host86-186-196-229.range86-186.btcentralplus.com) (Ping timeout: 252 seconds) |
| 2021-07-03 13:01:46 +0000 | <juri_> | tho, i think that's supposed to be fromIntegral (ceiling (X*Y) +1 ) * Y |
| 2021-07-03 13:01:47 +0000 | <juri_> | ? |
| 2021-07-03 13:01:51 +0000 | juri_ | ponders. |
| 2021-07-03 13:02:05 +0000 | <juri_> | er. / Y, rather. |
| 2021-07-03 13:02:09 +0000 | <tomsmeding> | either ceiling (X / Y) or floor (X / Y) + 1 |
| 2021-07-03 13:02:21 +0000 | <tomsmeding> | depending if you want >=X or >X |
| 2021-07-03 13:03:07 +0000 | <juri_> | aha. of course. thanks. |
| 2021-07-03 13:04:05 +0000 | tzar_bomba | (~tzar_bomb@user/tzar-bomba/x-5218718) () |
| 2021-07-03 13:05:00 +0000 | dunkeln_ | (~dunkeln@188.70.10.165) |
| 2021-07-03 13:05:39 +0000 | Deide | (~Deide@wire.desu.ga) |
| 2021-07-03 13:05:39 +0000 | Deide | (~Deide@wire.desu.ga) (Changing host) |
| 2021-07-03 13:05:39 +0000 | Deide | (~Deide@user/deide) |
| 2021-07-03 13:07:54 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2021-07-03 13:09:18 +0000 | <tomsmeding> | tangentially related trick: ceil-division on _integers_ a and b can be implemented as (a + b - 1) `div` b, for anyone who didn't already know about that |
| 2021-07-03 13:13:40 +0000 | tose | (~tose@ip-85-160-2-70.eurotel.cz) |
| 2021-07-03 13:13:46 +0000 | acidjnk_new | (~acidjnk@p200300d0c72b953339f341015709cf67.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2021-07-03 13:17:47 +0000 | noctux | (~noctux@user/noctux) (Remote host closed the connection) |
| 2021-07-03 13:17:54 +0000 | feliix42 | (~felix@gibbs.uberspace.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-07-03 13:18:19 +0000 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2021-07-03 13:20:42 +0000 | arjun | (~user@user/arjun) (Ping timeout: 252 seconds) |
| 2021-07-03 13:21:54 +0000 | feliix42 | (~felix@gibbs.uberspace.de) |
| 2021-07-03 13:23:00 +0000 | dyeplexer | (~dyeplexer@user/dyeplexer) |
| 2021-07-03 13:24:53 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2021-07-03 13:25:36 +0000 | noctux | (~noctux@user/noctux) |
| 2021-07-03 13:26:40 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 13:26:58 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 13:27:06 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 13:27:25 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 13:27:27 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 13:27:51 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 13:27:56 +0000 | mc47 | (~mc47@xmonad/TheMC47) |
| 2021-07-03 13:29:57 +0000 | Guest9 | (~Guest9@103.249.233.78) |
| 2021-07-03 13:29:59 +0000 | arjun | (~user@160.202.37.228) |
| 2021-07-03 13:30:58 +0000 | arjun | (~user@160.202.37.228) (Changing host) |
| 2021-07-03 13:30:58 +0000 | arjun | (~user@user/arjun) |
| 2021-07-03 13:31:31 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 13:31:54 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 2021-07-03 13:34:52 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 13:35:00 +0000 | gawen | (~gawen@user/gawen) (Quit: cya) |
| 2021-07-03 13:35:32 +0000 | <yorick> | can I somehow access the default class implementation when I'm overriding it? |
| 2021-07-03 13:36:33 +0000 | <yorick> | the neccesary things to make my own aren't exported by the module I'm using |
| 2021-07-03 13:37:56 +0000 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2021-07-03 13:38:44 +0000 | gawen | (~gawen@user/gawen) |
| 2021-07-03 13:39:03 +0000 | fef | (~thedawn@user/thedawn) (Ping timeout: 244 seconds) |
| 2021-07-03 13:40:28 +0000 | jneira_ | (~jneira_@217.red-81-39-172.dynamicip.rima-tde.net) |
| 2021-07-03 13:42:40 +0000 | jippiedoe | (~david@2a02-a44c-e14e-1-2351-c955-5b2d-b577.fixed6.kpn.net) (Ping timeout: 256 seconds) |
| 2021-07-03 13:43:00 +0000 | stevenxl | (~stevenlei@68.235.43.109) |
| 2021-07-03 13:43:54 +0000 | wei2912 | (~wei2912@112.199.250.21) (Quit: Lost terminal) |
| 2021-07-03 13:44:18 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 13:45:21 +0000 | fef | (~thedawn@user/thedawn) |
| 2021-07-03 13:46:10 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 13:46:37 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 13:47:39 +0000 | <Axman6> | so, this feels like a dumb question, but is there a reasonably performant function to turn an Integer into a ByteString in base10? some form of pack . show would make me a bit sad, but if that's the easiest way I'll go wiht it |
| 2021-07-03 13:47:41 +0000 | <Axman6> | wiht* |
| 2021-07-03 13:47:50 +0000 | dunkeln_ | (~dunkeln@188.70.10.165) (Ping timeout: 252 seconds) |
| 2021-07-03 13:48:57 +0000 | <Axman6> | I'm just going to leave that one -_- |
| 2021-07-03 13:49:37 +0000 | <tomsmeding> | Axman6: is it performance-relevant code :p |
| 2021-07-03 13:50:46 +0000 | cheater1__ | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 13:51:32 +0000 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-07-03 13:51:56 +0000 | <Axman6> | it... might be, eventually |
| 2021-07-03 13:52:14 +0000 | <Axman6> | I guess when that day comes, and the profiler says "Show is expensive!" I will make a change |
| 2021-07-03 13:53:26 +0000 | <tomsmeding> | a while ago I was parsing large (multi-megabyte; apparently that's large) files of floating-point numbers using haskell; then I found out that Read-ing floats is bloody expensive |
| 2021-07-03 13:53:54 +0000 | <tomsmeding> | even with a dedicated float parser from a bytestring it was still slower than C I believe |
| 2021-07-03 13:54:13 +0000 | <Axman6> | yeah, doesn't surprise me too much. IIRC Scientific's parsing is pretty decent |
| 2021-07-03 13:54:29 +0000 | dunkeln | (~dunkeln@188.70.10.165) |
| 2021-07-03 13:54:37 +0000 | <Axman6> | actuallty, maybe not |
| 2021-07-03 13:54:57 +0000 | <tomsmeding> | I'm currently using bytestring-lexing |
| 2021-07-03 13:55:03 +0000 | <Axman6> | I remember reading years ago about PHP's float parsing being really fast, but there was a specific string that would put into an infinite loop |
| 2021-07-03 13:55:12 +0000 | <tomsmeding> | it's good enough for the purpose currently but it leaves a sour taste :p |
| 2021-07-03 13:55:18 +0000 | <tomsmeding> | lol |
| 2021-07-03 13:55:22 +0000 | <tomsmeding> | good old php |
| 2021-07-03 13:56:28 +0000 | <Axman6> | https://www.exploringbinary.com/php-hangs-on-numeric-value-2-2250738585072011e-308/ |
| 2021-07-03 13:58:34 +0000 | stevenxl_ | (~stevenlei@68.235.43.165) |
| 2021-07-03 14:00:51 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 14:00:59 +0000 | <Axman6> | I'm sure I've read something about fast floating point number parsing in Haskell but I can't remember where. wouldn't susprise me if it was something bos wrote |
| 2021-07-03 14:01:46 +0000 | stevenxl | (~stevenlei@68.235.43.109) (Ping timeout: 252 seconds) |
| 2021-07-03 14:02:41 +0000 | <tomsmeding> | interesting link |
| 2021-07-03 14:03:39 +0000 | <adamse> | https://lemire.me has some good reading on both integers and floats parsing somewhere, not in haskell though (yet..) |
| 2021-07-03 14:03:46 +0000 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-07-03 14:04:25 +0000 | peterhil | (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Ping timeout: 265 seconds) |
| 2021-07-03 14:06:11 +0000 | <adamse> | https://lemire.me/blog/2021/01/29/number-parsing-at-a-gigabyte-per-second/ for floats |
| 2021-07-03 14:07:33 +0000 | jakalx | (~jakalx@base.jakalx.net) |
| 2021-07-03 14:07:40 +0000 | zebrag | (~chris@user/zebrag) |
| 2021-07-03 14:08:55 +0000 | <tomsmeding> | lol bytestring-lexing doesn't even try to be intelligent with float parsing I now see |
| 2021-07-03 14:09:17 +0000 | <tomsmeding> | it parses two integers and does some exponentiation and adding |
| 2021-07-03 14:09:30 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 14:09:49 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 14:12:12 +0000 | fendor_ | (~fendor@178.115.131.211.wireless.dyn.drei.com) |
| 2021-07-03 14:12:14 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) (Read error: Connection reset by peer) |
| 2021-07-03 14:14:58 +0000 | fendor | (~fendor@77.119.220.92.wireless.dyn.drei.com) (Ping timeout: 258 seconds) |
| 2021-07-03 14:16:33 +0000 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 2021-07-03 14:17:51 +0000 | Cale | (~cale@cpef48e38ee8583-cm0c473de9d680.cpe.net.cable.rogers.com) (Remote host closed the connection) |
| 2021-07-03 14:19:42 +0000 | Cale | (~cale@cpef48e38ee8583-cm0c473de9d680.cpe.net.cable.rogers.com) |
| 2021-07-03 14:20:42 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 14:22:36 +0000 | AgentM | (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 2021-07-03 14:22:46 +0000 | tose | (~tose@ip-85-160-2-70.eurotel.cz) (Ping timeout: 272 seconds) |
| 2021-07-03 14:25:28 +0000 | son0p | (~ff@181.136.122.143) |
| 2021-07-03 14:28:06 +0000 | dunkeln | (~dunkeln@188.70.10.165) (Ping timeout: 265 seconds) |
| 2021-07-03 14:32:18 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 14:32:59 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 14:33:16 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 14:33:54 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 240 seconds) |
| 2021-07-03 14:34:46 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 14:34:48 +0000 | arjun | (~user@user/arjun) (Ping timeout: 256 seconds) |
| 2021-07-03 14:34:51 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 14:35:11 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-07-03 14:35:26 +0000 | turlando | (~turlando@user/turlando) (Ping timeout: 272 seconds) |
| 2021-07-03 14:35:53 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 14:35:56 +0000 | dunkeln | (~dunkeln@188.70.10.165) |
| 2021-07-03 14:37:04 +0000 | jess | (~jess@libera/staff/jess) () |
| 2021-07-03 14:39:30 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 14:39:38 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 14:40:28 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Ping timeout: 256 seconds) |
| 2021-07-03 14:41:46 +0000 | eight | (~eight@user/eight) (Ping timeout: 272 seconds) |
| 2021-07-03 14:42:10 +0000 | eight | (~eight@user/eight) |
| 2021-07-03 14:46:34 +0000 | tubogram | (~tubogram@user/tubogram) (Ping timeout: 244 seconds) |
| 2021-07-03 14:48:51 +0000 | magnuscake | (~magnuscak@87-121-92-61.dyn.launtel.net.au) |
| 2021-07-03 14:49:42 +0000 | fizbin_ | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 14:50:00 +0000 | Guest9 | (~Guest9@103.249.233.78) (Ping timeout: 272 seconds) |
| 2021-07-03 14:50:37 +0000 | Lycurgus | (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-07-03 14:53:04 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 14:53:30 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 256 seconds) |
| 2021-07-03 14:54:26 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 14:54:28 +0000 | cheater1__ | cheater |
| 2021-07-03 14:55:04 +0000 | magnuscake | (~magnuscak@87-121-92-61.dyn.launtel.net.au) (Ping timeout: 272 seconds) |
| 2021-07-03 14:56:03 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 14:56:25 +0000 | Gurkenglas | (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) |
| 2021-07-03 14:57:28 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 14:59:45 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 15:00:29 +0000 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 265 seconds) |
| 2021-07-03 15:01:52 +0000 | Hanicef | (~gustaf@81-229-9-108-no92.tbcn.telia.com) |
| 2021-07-03 15:03:51 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 15:10:48 +0000 | Lycurgus | (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-07-03 15:12:10 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 15:15:50 +0000 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-07-03 15:17:30 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 15:19:49 +0000 | haykam2 | (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-07-03 15:20:01 +0000 | haykam1 | (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-07-03 15:20:08 +0000 | nick8325 | (~nick@2001:9b1:26f9:3e00:b7ea:ac95:e18:4c1d) (Ping timeout: 256 seconds) |
| 2021-07-03 15:20:15 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 15:21:42 +0000 | nick8325 | (~nick@188.241.156.248) |
| 2021-07-03 15:21:54 +0000 | MoC | (~moc@user/moc) |
| 2021-07-03 15:25:28 +0000 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) (Read error: Connection reset by peer) |
| 2021-07-03 15:26:26 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 15:28:20 +0000 | lbseale | (~lbseale@user/ep1ctetus) (Read error: Connection reset by peer) |
| 2021-07-03 15:28:45 +0000 | peterhil | (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-07-03 15:29:02 +0000 | jneira_ | (~jneira_@217.red-81-39-172.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 2021-07-03 15:30:20 +0000 | lbseale | (~lbseale@user/ep1ctetus) |
| 2021-07-03 15:31:27 +0000 | lbseale | (~lbseale@user/ep1ctetus) (Client Quit) |
| 2021-07-03 15:31:35 +0000 | qbt | (~edun@user/edun) |
| 2021-07-03 15:32:52 +0000 | stevenxl_ | (~stevenlei@68.235.43.165) (Ping timeout: 265 seconds) |
| 2021-07-03 15:34:12 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 15:34:20 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 15:34:25 +0000 | cheater1__ | cheater |
| 2021-07-03 15:35:12 +0000 | fendor_ | fendor |
| 2021-07-03 15:37:30 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 272 seconds) |
| 2021-07-03 15:37:47 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 15:40:15 +0000 | stevenxl | (~stevenlei@68.235.43.165) |
| 2021-07-03 15:42:19 +0000 | fendor | (~fendor@178.115.131.211.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2021-07-03 15:43:49 +0000 | fendor | (~fendor@178.115.131.211.wireless.dyn.drei.com) |
| 2021-07-03 15:43:54 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 2021-07-03 15:44:12 +0000 | fizbin_ | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-07-03 15:46:53 +0000 | chris_ | (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-07-03 15:47:35 +0000 | chris_ | (~chris@81.96.113.213) |
| 2021-07-03 15:47:42 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 15:48:07 +0000 | alex3 | (~alex3@BSN-77-82-41.static.siol.net) (Ping timeout: 258 seconds) |
| 2021-07-03 15:48:49 +0000 | peterhil | (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Ping timeout: 265 seconds) |
| 2021-07-03 15:52:11 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 15:52:42 +0000 | chris_ | (~chris@81.96.113.213) (Ping timeout: 272 seconds) |
| 2021-07-03 15:57:08 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds) |
| 2021-07-03 15:57:32 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 15:58:58 +0000 | hendursa1 | (~weechat@user/hendursaga) (Quit: hendursa1) |
| 2021-07-03 15:59:44 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 15:59:50 +0000 | hendursaga | (~weechat@user/hendursaga) |
| 2021-07-03 16:00:56 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 16:01:05 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 16:01:53 +0000 | alex3 | (~alex3@BSN-77-82-41.static.siol.net) |
| 2021-07-03 16:03:30 +0000 | dunkeln | (~dunkeln@188.70.10.165) (Ping timeout: 252 seconds) |
| 2021-07-03 16:03:54 +0000 | tzh | (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 2021-07-03 16:07:39 +0000 | MorrowM | (~MorrowM_@bzq-110-168-31-106.red.bezeqint.net) |
| 2021-07-03 16:08:04 +0000 | alex3 | (~alex3@BSN-77-82-41.static.siol.net) (Read error: Connection reset by peer) |
| 2021-07-03 16:08:08 +0000 | qbt | (~edun@user/edun) (Quit: WeeChat 3.2) |
| 2021-07-03 16:09:32 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-03 16:09:34 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 16:09:36 +0000 | cheater1__ | cheater |
| 2021-07-03 16:09:48 +0000 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2021-07-03 16:10:21 +0000 | stevenxl | (~stevenlei@68.235.43.165) (Ping timeout: 258 seconds) |
| 2021-07-03 16:12:12 +0000 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-07-03 16:12:53 +0000 | arkeet | (arkeet@moriya.ca) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-07-03 16:13:07 +0000 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-07-03 16:13:54 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 16:14:11 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 16:14:16 +0000 | cheater1__ | cheater |
| 2021-07-03 16:15:41 +0000 | dunkeln | (~dunkeln@188.70.10.165) |
| 2021-07-03 16:15:53 +0000 | jamestmartin | (james@jtmar.me) (Quit: ZNC 1.8.2+deb2+b1 - https://znc.in) |
| 2021-07-03 16:16:35 +0000 | peterhil | (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-07-03 16:17:20 +0000 | arkeet | (~arkeet@moriya.ca) |
| 2021-07-03 16:17:54 +0000 | <maerwald> | sm[m]: https://www.youtube.com/watch?v=6PKmZSHxu0c I missed your talk... gonna have to watch now |
| 2021-07-03 16:19:45 +0000 | nshepperd | (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) (Ping timeout: 272 seconds) |
| 2021-07-03 16:20:05 +0000 | jamestmartin | (~james@jtmar.me) |
| 2021-07-03 16:20:30 +0000 | nshepperd | (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) |
| 2021-07-03 16:23:47 +0000 | hnOsmium0001 | (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-07-03 16:24:46 +0000 | jneira[m] | (~jneira@111.red-176-83-226.dynamicip.rima-tde.net) |
| 2021-07-03 16:25:21 +0000 | alex3 | (~alex3@BSN-77-82-41.static.siol.net) |
| 2021-07-03 16:25:52 +0000 | hendursaga | (~weechat@user/hendursaga) (Remote host closed the connection) |
| 2021-07-03 16:27:26 +0000 | hendursaga | (~weechat@user/hendursaga) |
| 2021-07-03 16:28:42 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 16:30:43 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 16:31:26 +0000 | Erutuon | (~Erutuon@user/erutuon) |
| 2021-07-03 16:31:29 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 16:33:55 +0000 | NieDzejkob | (~quassel@195.149.98.3) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2021-07-03 16:35:15 +0000 | jneira[m] | (~jneira@111.red-176-83-226.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2021-07-03 16:35:19 +0000 | NieDzejkob | (~quassel@195.149.98.3) |
| 2021-07-03 16:37:14 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 16:39:17 +0000 | slowButPresent | (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 2021-07-03 16:39:47 +0000 | fef | (~thedawn@user/thedawn) (Remote host closed the connection) |
| 2021-07-03 16:40:10 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 16:40:39 +0000 | fef | (~thedawn@user/thedawn) |
| 2021-07-03 16:40:48 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 16:41:44 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Ping timeout: 256 seconds) |
| 2021-07-03 16:44:18 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 16:45:51 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 2021-07-03 16:46:12 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 16:46:40 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 16:47:18 +0000 | MoC | (~moc@user/moc) (Quit: Konversation terminated!) |
| 2021-07-03 16:50:14 +0000 | nshepperd | (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) (Ping timeout: 256 seconds) |
| 2021-07-03 16:50:32 +0000 | nshepperd | (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) |
| 2021-07-03 16:53:40 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 258 seconds) |
| 2021-07-03 16:53:55 +0000 | Cale | (~cale@cpef48e38ee8583-cm0c473de9d680.cpe.net.cable.rogers.com) (Remote host closed the connection) |
| 2021-07-03 16:53:59 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 16:54:18 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 16:55:32 +0000 | Cale | (~cale@cpef48e38ee8583-cm0c473de9d680.cpe.net.cable.rogers.com) |
| 2021-07-03 16:56:46 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 16:57:28 +0000 | gehmehgeh | (~user@user/gehmehgeh) |
| 2021-07-03 16:59:52 +0000 | Erutuon | (~Erutuon@user/erutuon) (Ping timeout: 265 seconds) |
| 2021-07-03 17:00:09 +0000 | jneira[m] | (~jneira@111.red-176-83-226.dynamicip.rima-tde.net) |
| 2021-07-03 17:01:09 +0000 | anandprabhu | (~anandprab@94.202.243.198) (Quit: Leaving) |
| 2021-07-03 17:01:38 +0000 | Erutuon | (~Erutuon@user/erutuon) |
| 2021-07-03 17:03:26 +0000 | <sm[m]> | maerwald: great! |
| 2021-07-03 17:05:30 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-07-03 17:07:32 +0000 | finsternis | (~X@23.226.237.192) |
| 2021-07-03 17:09:03 +0000 | ubert | (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
| 2021-07-03 17:13:38 +0000 | jneira[m] | (~jneira@111.red-176-83-226.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2021-07-03 17:17:50 +0000 | jneira[m] | (~jneira@111.red-176-83-226.dynamicip.rima-tde.net) |
| 2021-07-03 17:18:42 +0000 | Meh | (~Meh@202.14.120.46) |
| 2021-07-03 17:19:06 +0000 | Meh | Guest2930 |
| 2021-07-03 17:21:22 +0000 | pavonia | (~user@user/siracusa) |
| 2021-07-03 17:23:04 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2021-07-03 17:23:49 +0000 | Guest2930 | (~Meh@202.14.120.46) (Quit: Connection closed) |
| 2021-07-03 17:24:26 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 17:26:11 +0000 | econo | (uid147250@user/econo) |
| 2021-07-03 17:28:18 +0000 | jneira[m] | (~jneira@111.red-176-83-226.dynamicip.rima-tde.net) (Ping timeout: 240 seconds) |
| 2021-07-03 17:29:50 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-07-03 17:30:15 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 17:30:51 +0000 | dunkeln | (~dunkeln@188.70.10.165) (Ping timeout: 258 seconds) |
| 2021-07-03 17:33:52 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:ff7c:fc0:389a:fc47) (Ping timeout: 256 seconds) |
| 2021-07-03 17:34:43 +0000 | xff0x | (~xff0x@2001:1a81:52ae:a300:7e2e:fefc:f290:c960) |
| 2021-07-03 17:38:54 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 17:38:57 +0000 | GIANTWORLDKEEPER | (~pjetcetal@128-71-13-182.broadband.corbina.ru) (Quit: EXIT) |
| 2021-07-03 17:43:06 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Ping timeout: 240 seconds) |
| 2021-07-03 17:48:24 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 17:49:14 +0000 | shailangsa | (~shailangs@host86-186-196-229.range86-186.btcentralplus.com) |
| 2021-07-03 17:49:23 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 17:49:35 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 17:51:35 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 2021-07-03 17:51:55 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 17:52:20 +0000 | shajra[m] | (~shajramat@2001:470:69fc:105::b552) |
| 2021-07-03 17:52:24 +0000 | xwx | (~george@user/george) (Ping timeout: 272 seconds) |
| 2021-07-03 17:53:53 +0000 | ddb | (~ddb@2607:5300:61:c67::196) (Remote host closed the connection) |
| 2021-07-03 17:54:03 +0000 | xwx | (~george@user/george) |
| 2021-07-03 17:54:08 +0000 | ddb | (~ddb@2607:5300:61:c67::196) |
| 2021-07-03 17:54:27 +0000 | Guest9 | (~Guest9@103.249.233.78) |
| 2021-07-03 17:55:24 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 17:56:33 +0000 | fef | (~thedawn@user/thedawn) (Quit: Leaving) |
| 2021-07-03 17:57:22 +0000 | Lycurgus | (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-07-03 17:57:45 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 17:59:00 +0000 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2021-07-03 17:59:12 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 18:00:52 +0000 | turlando | (~turlando@user/turlando) |
| 2021-07-03 18:01:54 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 18:02:17 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 258 seconds) |
| 2021-07-03 18:03:30 +0000 | warnz | (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 240 seconds) |
| 2021-07-03 18:04:18 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) |
| 2021-07-03 18:05:30 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 18:06:20 +0000 | fabfianda | (~fabfianda@37.183.255.57) (Ping timeout: 272 seconds) |
| 2021-07-03 18:06:42 +0000 | fabfianda | (~fabfianda@mob-5-90-246-95.net.vodafone.it) |
| 2021-07-03 18:07:42 +0000 | dunkeln | (~dunkeln@188.70.10.165) |
| 2021-07-03 18:07:54 +0000 | stevenxl | (~stevenlei@68.235.43.165) |
| 2021-07-03 18:08:14 +0000 | oxide | (~lambda@user/oxide) (Ping timeout: 272 seconds) |
| 2021-07-03 18:08:15 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 18:08:35 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 18:08:52 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 18:08:52 +0000 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2021-07-03 18:08:57 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 18:08:57 +0000 | cheater1__ | cheater |
| 2021-07-03 18:09:39 +0000 | oxide | (~lambda@user/oxide) |
| 2021-07-03 18:10:43 +0000 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-07-03 18:11:50 +0000 | azeem | (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) (Ping timeout: 252 seconds) |
| 2021-07-03 18:12:10 +0000 | azeem | (~azeem@176.200.221.91) |
| 2021-07-03 18:12:13 +0000 | Guest9 | (~Guest9@103.249.233.78) (Quit: Connection closed) |
| 2021-07-03 18:12:58 +0000 | xwx | (~george@user/george) (Ping timeout: 256 seconds) |
| 2021-07-03 18:14:48 +0000 | dyeplexer | (~dyeplexer@user/dyeplexer) (Remote host closed the connection) |
| 2021-07-03 18:15:30 +0000 | mikoto-chan | (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 252 seconds) |
| 2021-07-03 18:18:38 +0000 | Hanicef | (~gustaf@81-229-9-108-no92.tbcn.telia.com) (Quit: leaving) |
| 2021-07-03 18:19:00 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 18:19:04 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 18:19:06 +0000 | cheater1__ | cheater |
| 2021-07-03 18:20:20 +0000 | stevenxl_ | (~stevenlei@68.235.43.93) |
| 2021-07-03 18:22:06 +0000 | fabfianda | (~fabfianda@mob-5-90-246-95.net.vodafone.it) (Ping timeout: 252 seconds) |
| 2021-07-03 18:22:27 +0000 | Lycurgus | (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-07-03 18:22:28 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds) |
| 2021-07-03 18:22:43 +0000 | fabfianda | (~fabfianda@37.183.255.57) |
| 2021-07-03 18:22:48 +0000 | stevenxl | (~stevenlei@68.235.43.165) (Ping timeout: 272 seconds) |
| 2021-07-03 18:22:49 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2021-07-03 18:24:26 +0000 | mikoto-chan | (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-07-03 18:26:02 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 18:27:38 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 18:27:40 +0000 | <zzz> | what is the best way to store a 2d array for fast lookup and update? |
| 2021-07-03 18:27:55 +0000 | <zzz> | int indexed |
| 2021-07-03 18:29:19 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 18:29:29 +0000 | <Franciman> | zzz: in an immutable setting? |
| 2021-07-03 18:29:54 +0000 | <Franciman> | I would use an IntMap from containers |
| 2021-07-03 18:30:01 +0000 | <Franciman> | or a Data.Sequence |
| 2021-07-03 18:30:10 +0000 | dunkeln | (~dunkeln@188.70.10.165) (Ping timeout: 252 seconds) |
| 2021-07-03 18:30:10 +0000 | <Franciman> | it uses fingertrees |
| 2021-07-03 18:30:15 +0000 | <Franciman> | underneath |
| 2021-07-03 18:30:23 +0000 | <Franciman> | Data.Sequence is in containers too |
| 2021-07-03 18:30:56 +0000 | xwx | (~george@user/george) |
| 2021-07-03 18:31:12 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 18:33:00 +0000 | <c_wraith> | If you really need it, there's nothing wrong with using mutability, either. |
| 2021-07-03 18:33:22 +0000 | <Franciman> | tru |
| 2021-07-03 18:33:28 +0000 | <Franciman> | also zzz what I am hinting here |
| 2021-07-03 18:33:32 +0000 | <Franciman> | is encoding a 2d array in a 1d array |
| 2021-07-03 18:33:41 +0000 | <Franciman> | i think it is good both in a mutable and an immutable setting |
| 2021-07-03 18:33:42 +0000 | <zzz> | i have used unboxed vectors in the past |
| 2021-07-03 18:33:49 +0000 | <c_wraith> | Also, sometimes laziness can be all the mutability you need, and immutable arrays can do the job. This is especially true for dynamic programming types of problems |
| 2021-07-03 18:35:30 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2021-07-03 18:35:49 +0000 | <zzz> | i want something that allows me to conveniently and efficiently sort items |
| 2021-07-03 18:36:19 +0000 | <zzz> | | 8 {- part2 |
| 2021-07-03 18:36:22 +0000 | <zzz> | | 7 turns out there are exactly 4 possible corners, 10*4 possible edges and 10^2 possible inner til |
| 2021-07-03 18:36:25 +0000 | <zzz> | | 6 (with exactly 2, 3 and 4 edges respectively) |
| 2021-07-03 18:36:28 +0000 | <zzz> | | 5 |
| 2021-07-03 18:36:31 +0000 | <zzz> | | 4 sortSize :: M.IntMap (S.Set Int) -> [(Int,Int)] |
| 2021-07-03 18:36:34 +0000 | <zzz> | | 3 sortSize = sortBy (comparing snd) . M.toList . M.map S.size -} |
| 2021-07-03 18:36:37 +0000 | <zzz> | | 2 |
| 2021-07-03 18:36:40 +0000 | <zzz> | | 1 poss :: M.IntMap Tile -> M.IntMap Tile -- (tilen,tile) -> (pos,[flipped and rotated tile]) |
| 2021-07-03 18:36:42 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2021-07-03 18:36:43 +0000 | <zzz> | |65 poss m = go m mempty |
| 2021-07-03 18:36:44 +0000 | <c_wraith> | be careful with the paste button. :P |
| 2021-07-03 18:36:46 +0000 | <zzz> | | 1 where |
| 2021-07-03 18:36:49 +0000 | <zzz> | | 2 go :: M.IntMap Tile -> M.IntMap Tile -> M.IntMap Tile |
| 2021-07-03 18:36:52 +0000 | <zzz> | | 3 go p m'· |
| 2021-07-03 18:36:55 +0000 | <zzz> | | 4 | null m' = p |
| 2021-07-03 18:36:58 +0000 | <zzz> | | 5 | new_match· |
| 2021-07-03 18:37:01 +0000 | <zzz> | | 6 | otherwise = go (M.insert new_match p) () |
| 2021-07-03 18:37:04 +0000 | <zzz> | | 7 where |
| 2021-07-03 18:37:07 +0000 | <zzz> | | 8 new_match |
| 2021-07-03 18:37:10 +0000 | <zzz> | | 9 | px ∈ [0,pred side] && py ∈ [0,pred side] =· |
| 2021-07-03 18:37:13 +0000 | <zzz> | | 10 | px ∈ [0,pred side] || py ∈ [0,pred side] =· |
| 2021-07-03 18:37:16 +0000 | <zzz> | oh no im so sorry |
| 2021-07-03 18:37:19 +0000 | <zzz> | what the hell |
| 2021-07-03 18:37:25 +0000 | <Clint> | tsk, tsk |
| 2021-07-03 18:38:19 +0000 | <zzz> | welp |
| 2021-07-03 18:38:28 +0000 | <farn> | we'll live |
| 2021-07-03 18:38:57 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 18:42:58 +0000 | LukeHoersten | (~LukeHoers@user/lukehoersten) |
| 2021-07-03 18:46:52 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2021-07-03 18:49:09 +0000 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-07-03 18:49:13 +0000 | Sgeo | (~Sgeo@user/sgeo) |
| 2021-07-03 18:50:42 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 18:51:03 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 18:51:45 +0000 | neceve | (~quassel@2a02:c7f:607e:d600:f762:20dd:304e:4b1f) |
| 2021-07-03 18:53:07 +0000 | beka | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-03 18:54:34 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 18:54:35 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 18:54:38 +0000 | dunkeln | (~dunkeln@188.70.10.165) |
| 2021-07-03 18:58:25 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 18:59:07 +0000 | stevenxl_ | (~stevenlei@68.235.43.93) (Ping timeout: 268 seconds) |
| 2021-07-03 18:59:15 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 265 seconds) |
| 2021-07-03 18:59:30 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds) |
| 2021-07-03 19:02:07 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 19:03:14 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 2021-07-03 19:03:27 +0000 | tomsmeding | learned today that multiple consecutive spaces are collapsed on https://ircbrowse.tomsmeding.com/day/lchaskell/2021/07/03?id=77299#trid77299 |
| 2021-07-03 19:03:51 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 19:04:36 +0000 | <geekosaur> | not that surprising, absent <pre> or equivalent |
| 2021-07-03 19:04:41 +0000 | <tomsmeding> | yeah |
| 2021-07-03 19:04:59 +0000 | <tomsmeding> | don't think I'm going to do anything about that |
| 2021-07-03 19:05:33 +0000 | <tomsmeding> | zzz: tmux copy? :p |
| 2021-07-03 19:07:46 +0000 | turlando | (~turlando@user/turlando) (Ping timeout: 272 seconds) |
| 2021-07-03 19:08:44 +0000 | beka_ | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-03 19:10:02 +0000 | <zzz> | i have no idea. i'm not on my usual machine, i think it was a right-click paste from vim to irssi |
| 2021-07-03 19:10:30 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) |
| 2021-07-03 19:10:49 +0000 | <zzz> | i must have touched the trackpad with my palm |
| 2021-07-03 19:11:27 +0000 | beka | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 268 seconds) |
| 2021-07-03 19:12:20 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 19:12:21 +0000 | zeenk | (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) (Read error: Connection reset by peer) |
| 2021-07-03 19:12:48 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 19:13:39 +0000 | zeenk | (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) |
| 2021-07-03 19:15:12 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) (Ping timeout: 265 seconds) |
| 2021-07-03 19:16:05 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 19:19:16 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 19:20:52 +0000 | hexfive | (~eric@50.35.83.177) |
| 2021-07-03 19:21:04 +0000 | beka_ | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 272 seconds) |
| 2021-07-03 19:21:19 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 2021-07-03 19:21:36 +0000 | HotblackDesiato | (~HotblackD@gateway/tor-sasl/hotblackdesiato) (Ping timeout: 244 seconds) |
| 2021-07-03 19:21:43 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 19:22:23 +0000 | HotblackDesiato | (~HotblackD@gateway/tor-sasl/hotblackdesiato) |
| 2021-07-03 19:23:20 +0000 | hexfive | (~eric@50.35.83.177) (Read error: Connection reset by peer) |
| 2021-07-03 19:23:23 +0000 | hexfifty | (~eric@50.35.83.177) |
| 2021-07-03 19:23:30 +0000 | hexfifty | (~eric@50.35.83.177) (Client Quit) |
| 2021-07-03 19:25:14 +0000 | sm | (~user@plaintextaccounting/sm) |
| 2021-07-03 19:25:21 +0000 | stevenxl | (~stevenlei@68.235.43.93) |
| 2021-07-03 19:29:30 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 19:29:49 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 19:30:34 +0000 | stevenxl | (~stevenlei@68.235.43.93) (Ping timeout: 268 seconds) |
| 2021-07-03 19:30:44 +0000 | v01d4lph4 | (~v01d4lph4@user/v01d4lph4) |
| 2021-07-03 19:34:44 +0000 | Schrostfutz | (~Schrostfu@p5de88aa6.dip0.t-ipconnect.de) |
| 2021-07-03 19:35:08 +0000 | v01d4lph4 | (~v01d4lph4@user/v01d4lph4) (Ping timeout: 256 seconds) |
| 2021-07-03 19:36:35 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-03 19:36:47 +0000 | <rawles> | Is Agda a natural next step for someone who enjoys Haskell programming and wants to explore dependent types? Are there other clear options? |
| 2021-07-03 19:37:33 +0000 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-07-03 19:38:08 +0000 | natechan | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Quit: WeeChat 2.9) |
| 2021-07-03 19:38:41 +0000 | <dolio> | There's also Idris, which is a bit more programming oriented. |
| 2021-07-03 19:41:02 +0000 | <rawles> | Ah, so Idris has a proof assistant but the syntax looks more familiar. I guess I can try both and see which feels right. I like the Ivor the Engine reference! |
| 2021-07-03 19:41:36 +0000 | <dolio> | Agda generally has more fancy type theoretic features, which can be interesting to learn about. |
| 2021-07-03 19:42:30 +0000 | <dolio> | Like, a view of what might be useful for programming eventually, even if not currently. |
| 2021-07-03 19:42:34 +0000 | <rawles> | I don't have any specific goal in mind, only to development my understanding of types by dipping my toe in languages with these kind of features. |
| 2021-07-03 19:42:42 +0000 | <rawles> | *develop |
| 2021-07-03 19:42:55 +0000 | <rawles> | That's really useful. Thanks, dolio. |
| 2021-07-03 19:44:28 +0000 | <tomsmeding> | if I'm not mistaken, an example of a thing that agda has and that idris doesn't is copattern matching |
| 2021-07-03 19:44:45 +0000 | <tomsmeding> | but my search-fu may just be fooling me |
| 2021-07-03 19:45:02 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 19:45:08 +0000 | <dolio> | Oh, that may be. That's an example of something that would be useful right now. It's quite nice. |
| 2021-07-03 19:45:45 +0000 | motherfsck | (~motherfsc@user/motherfsck) |
| 2021-07-03 19:47:54 +0000 | xwx | (~george@user/george) (Ping timeout: 240 seconds) |
| 2021-07-03 19:50:48 +0000 | xwx | (~george@user/george) |
| 2021-07-03 19:53:23 +0000 | azeem | (~azeem@176.200.221.91) (Ping timeout: 265 seconds) |
| 2021-07-03 19:53:32 +0000 | chrysanthematic | (~chrysanth@user/chrysanthematic) |
| 2021-07-03 19:57:15 +0000 | azeem | (~azeem@176.200.221.91) |
| 2021-07-03 19:57:26 +0000 | dunkeln | (~dunkeln@188.70.10.165) (Ping timeout: 252 seconds) |
| 2021-07-03 19:58:16 +0000 | pricly_yellow | (~pricly_ye@2a01:620:c04d:b00::339) (Remote host closed the connection) |
| 2021-07-03 20:00:06 +0000 | <zzz> | is performance something you care about? |
| 2021-07-03 20:01:52 +0000 | <rawles> | zzz: Me? No, not really, I'm after a 'learning by doing' experience, at least at first. |
| 2021-07-03 20:02:23 +0000 | <zzz> | go for agda then |
| 2021-07-03 20:05:28 +0000 | juhp | (~juhp@128.106.188.66) (Ping timeout: 265 seconds) |
| 2021-07-03 20:06:38 +0000 | beka | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-03 20:06:54 +0000 | <rawles> | Great, thanks. |
| 2021-07-03 20:08:27 +0000 | juhp | (~juhp@128.106.188.66) |
| 2021-07-03 20:08:34 +0000 | peterhil | (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Ping timeout: 272 seconds) |
| 2021-07-03 20:10:53 +0000 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 20:12:14 +0000 | GIANTWORLDKEEPER | (~pjetcetal@128-71-13-182.broadband.corbina.ru) |
| 2021-07-03 20:13:52 +0000 | <qrpnxz> | is there a way to specify on a field that you only want to allow one of the sum type options in the field rather than any of them? So for example, only allow Right values instead of Either? |
| 2021-07-03 20:14:36 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) |
| 2021-07-03 20:14:37 +0000 | <monochrom> | No. |
| 2021-07-03 20:14:39 +0000 | GIANTWORLDKEEPR_ | (~pjetcetal@128-71-13-182.broadband.corbina.ru) |
| 2021-07-03 20:14:41 +0000 | <qrpnxz> | ty |
| 2021-07-03 20:17:19 +0000 | dunkeln | (~dunkeln@188.70.10.165) |
| 2021-07-03 20:18:39 +0000 | sh9 | (~sh9@softbank060116136158.bbtec.net) |
| 2021-07-03 20:19:57 +0000 | <qrpnxz> | is there syntax sugar for creating Data.Text type text? Or do i have to pass strings to pack every time? |
| 2021-07-03 20:20:40 +0000 | <geekosaur> | OverloadedStrings, for literals only |
| 2021-07-03 20:20:56 +0000 | <geekosaur> | you must use pack for computed ones |
| 2021-07-03 20:21:43 +0000 | <qrpnxz> | nice thanks |
| 2021-07-03 20:22:39 +0000 | <qrpnxz> | works! |
| 2021-07-03 20:22:45 +0000 | <maerwald> | qrpnxz: quasiquoters too |
| 2021-07-03 20:23:04 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 20:23:07 +0000 | <maerwald> | with neat interpolation even |
| 2021-07-03 20:23:26 +0000 | <qrpnxz> | dunno how to do that |
| 2021-07-03 20:23:53 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) (ERC (IRC client for Emacs 26.3)) |
| 2021-07-03 20:23:54 +0000 | <maerwald> | https://hackage.haskell.org/package/string-interpolate |
| 2021-07-03 20:24:32 +0000 | <qrpnxz> | okay, this is epic |
| 2021-07-03 20:24:42 +0000 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 20:25:33 +0000 | jess | (~jess@libera/staff/jess) |
| 2021-07-03 20:26:04 +0000 | dunkeln | (~dunkeln@188.70.10.165) (Ping timeout: 268 seconds) |
| 2021-07-03 20:26:29 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) |
| 2021-07-03 20:27:45 +0000 | <rawles> | Oh yeah that's really neat. |
| 2021-07-03 20:29:20 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 20:29:49 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 20:30:21 +0000 | cheater | (~Username@user/cheater) (Client Quit) |
| 2021-07-03 20:30:54 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 20:31:30 +0000 | <fengctor> | hey all! just wondering if repeated modifications on the same optic get fused, or as an example in case my terminology isn't right: does |
| 2021-07-03 20:31:30 +0000 | <fengctor> | v & l1 . l2 %~ f & l1 . l2 %~ g |
| 2021-07-03 20:31:30 +0000 | <fengctor> | produce the intermediary structure from the first modification, or does it behave as |
| 2021-07-03 20:31:30 +0000 | <fengctor> | v & l1 . l2 %~ g . f & l1 . l2 %~ g |
| 2021-07-03 20:31:57 +0000 | dunkeln_ | (~dunkeln@188.70.10.165) |
| 2021-07-03 20:31:58 +0000 | <fengctor> | sorry, as v & l1 . l2 %~ g . f |
| 2021-07-03 20:32:40 +0000 | jneira_ | (~jneira_@217.red-81-39-172.dynamicip.rima-tde.net) |
| 2021-07-03 20:34:05 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) (Remote host closed the connection) |
| 2021-07-03 20:35:41 +0000 | <c_wraith> | I doubt that'd be reduced |
| 2021-07-03 20:35:50 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) |
| 2021-07-03 20:36:09 +0000 | <c_wraith> | fengctor: I doubt that'd be fused, as that's wrong in general |
| 2021-07-03 20:36:20 +0000 | <c_wraith> | fengctor: that fusion is only valid if the lenses are lawful |
| 2021-07-03 20:37:08 +0000 | <c_wraith> | fengctor: and there's no optimization done that assumes they are - there's no technical requirement for it, and unlawful optics are useful enough that they get used sometimes |
| 2021-07-03 20:37:38 +0000 | <fengctor> | c_wraith: ah I see, that makes sense thanks! |
| 2021-07-03 20:39:40 +0000 | <c_wraith> | For what it's worth, that's why the lens laws exist - to make refactoring like that trivially correct |
| 2021-07-03 20:39:47 +0000 | beka | (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 265 seconds) |
| 2021-07-03 20:40:17 +0000 | fendor | (~fendor@178.115.131.211.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-07-03 20:40:42 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 20:41:43 +0000 | fendor | (~fendor@178.115.131.211.wireless.dyn.drei.com) |
| 2021-07-03 20:43:08 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 20:43:20 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) |
| 2021-07-03 20:44:36 +0000 | khumba | (~khumba@user/khumba) |
| 2021-07-03 20:45:41 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 20:46:06 +0000 | natechan | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 20:48:02 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) (Ping timeout: 252 seconds) |
| 2021-07-03 20:48:48 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) |
| 2021-07-03 20:49:13 +0000 | sciencentistguy | (~sciencent@hacksoc/ordinary-member) |
| 2021-07-03 20:49:52 +0000 | <sciencentistguy> | hello haskellers; i've got a list of values `[a]` and i want to fold the binary operator `(a -> a -> Maybe a)` over it. |
| 2021-07-03 20:50:16 +0000 | <sciencentistguy> | is there a library function somewhere to do this or do i have to write my own |
| 2021-07-03 20:50:26 +0000 | <qrpnxz> | fold1l or fold1r |
| 2021-07-03 20:50:30 +0000 | <qrpnxz> | maybe what you want |
| 2021-07-03 20:50:44 +0000 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 268 seconds) |
| 2021-07-03 20:50:49 +0000 | <sciencentistguy> | foldr1 doesn't like the `Maybe` though |
| 2021-07-03 20:51:14 +0000 | <qrpnxz> | ah yeah |
| 2021-07-03 20:51:40 +0000 | <qrpnxz> | uhhhh, what do you want to happen when you combine a maybe a and an a |
| 2021-07-03 20:51:58 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 268 seconds) |
| 2021-07-03 20:52:11 +0000 | <c_wraith> | :t foldM |
| 2021-07-03 20:52:12 +0000 | <lambdabot> | (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b |
| 2021-07-03 20:53:05 +0000 | <sciencentistguy> | ah thank you that's what i want |
| 2021-07-03 20:53:06 +0000 | <qrpnxz> | if you want to like do them pairwise every two elements and then collapse somehow i think you're gonna need to write your own thing |
| 2021-07-03 20:53:27 +0000 | <qrpnxz> | c_wraith, so i just patterned matched 3 things at the same time by putting them in a tuple, is that how you're supposed to do it or can you do it without a tuple? |
| 2021-07-03 20:53:59 +0000 | <c_wraith> | qrpnxz: that's a pretty normal way to do it. Don't worry about the runtime cost of the tuple - ghc is very good at optimizing away known constructors |
| 2021-07-03 20:54:21 +0000 | <qrpnxz> | thx, just felt like i was being too clever xd |
| 2021-07-03 20:54:24 +0000 | _ht | (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 2021-07-03 20:54:37 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 20:55:15 +0000 | gehmehgeh | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-07-03 20:55:25 +0000 | beka | (~beka@104-244-27-23.static.monkeybrains.net) |
| 2021-07-03 20:55:51 +0000 | <c_wraith> | nah, that's exactly the right amount of clever :) |
| 2021-07-03 20:56:09 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) |
| 2021-07-03 20:56:25 +0000 | cheater | (~Username@user/cheater) (Quit: BitchX: use it, it makes you bulletproof) |
| 2021-07-03 20:56:55 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 20:58:49 +0000 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2021-07-03 20:59:07 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 2021-07-03 20:59:25 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 21:00:35 +0000 | chrysanthematic | (~chrysanth@user/chrysanthematic) (Quit: chrysanthematic) |
| 2021-07-03 21:01:13 +0000 | yauhsien | (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) (Ping timeout: 268 seconds) |
| 2021-07-03 21:02:00 +0000 | peterhil | (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-07-03 21:04:06 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 256 seconds) |
| 2021-07-03 21:04:16 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 21:04:18 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-03 21:04:23 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 21:04:26 +0000 | cheater1__ | cheater |
| 2021-07-03 21:07:32 +0000 | dunkeln_ | (~dunkeln@188.70.10.165) (Read error: Connection reset by peer) |
| 2021-07-03 21:11:30 +0000 | GIANTWORLDKEEPER | (~pjetcetal@128-71-13-182.broadband.corbina.ru) (Quit: EXIT) |
| 2021-07-03 21:12:46 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 21:13:10 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 21:13:10 +0000 | azeem | (~azeem@176.200.221.91) (Ping timeout: 272 seconds) |
| 2021-07-03 21:13:16 +0000 | stevenxl | (~stevenlei@68.235.43.93) |
| 2021-07-03 21:13:19 +0000 | cheater1__ | cheater |
| 2021-07-03 21:13:36 +0000 | acidjnk_new | (~acidjnk@p200300d0c72b953339f341015709cf67.dip0.t-ipconnect.de) |
| 2021-07-03 21:14:03 +0000 | azeem | (~azeem@176.200.221.91) |
| 2021-07-03 21:16:52 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 21:17:58 +0000 | stevenxl | (~stevenlei@68.235.43.93) (Ping timeout: 265 seconds) |
| 2021-07-03 21:18:56 +0000 | Schrostfutz | (~Schrostfu@p5de88aa6.dip0.t-ipconnect.de) (Ping timeout: 258 seconds) |
| 2021-07-03 21:19:43 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 21:21:46 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2021-07-03 21:21:46 +0000 | haykam1 | (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-07-03 21:21:58 +0000 | haykam1 | (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-07-03 21:22:14 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 2021-07-03 21:22:17 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 21:22:19 +0000 | cheater1__ | cheater |
| 2021-07-03 21:23:25 +0000 | oxide | (~lambda@user/oxide) (Ping timeout: 268 seconds) |
| 2021-07-03 21:23:53 +0000 | oxide | (~lambda@user/oxide) |
| 2021-07-03 21:24:15 +0000 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 265 seconds) |
| 2021-07-03 21:26:41 +0000 | nick8325 | (~nick@188.241.156.248) (Quit: Leaving.) |
| 2021-07-03 21:27:01 +0000 | dka | (~code-is-a@ns3059207.ip-193-70-33.eu) (Quit: My Ex-Girlfriend once told me: I'm not a slut, I'm just popular) |
| 2021-07-03 21:28:51 +0000 | laguneucl | (~Pitsikoko@athedsl-16082.home.otenet.gr) |
| 2021-07-03 21:29:12 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-07-03 21:29:48 +0000 | chomwitt | (~Pitsikoko@athedsl-16082.home.otenet.gr) (Read error: Connection reset by peer) |
| 2021-07-03 21:31:53 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 21:31:59 +0000 | ikex1 | (~ash@user/ikex) |
| 2021-07-03 21:32:45 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 21:33:30 +0000 | ikex | (~ash@user/ikex) (Ping timeout: 240 seconds) |
| 2021-07-03 21:33:31 +0000 | ikex1 | ikex |
| 2021-07-03 21:35:51 +0000 | beka | (~beka@104-244-27-23.static.monkeybrains.net) (Ping timeout: 265 seconds) |
| 2021-07-03 21:35:52 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 21:37:52 +0000 | crazazy | (~user@130.89.171.203) (Ping timeout: 272 seconds) |
| 2021-07-03 21:38:12 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) |
| 2021-07-03 21:38:31 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) (Client Quit) |
| 2021-07-03 21:38:52 +0000 | chris_ | (~chris@81.96.113.213) |
| 2021-07-03 21:39:20 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) |
| 2021-07-03 21:40:04 +0000 | sh9 | (~sh9@softbank060116136158.bbtec.net) (Ping timeout: 268 seconds) |
| 2021-07-03 21:40:41 +0000 | sciencentistguy | (~sciencent@hacksoc/ordinary-member) (Ping timeout: 268 seconds) |
| 2021-07-03 21:41:35 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) (Read error: Connection reset by peer) |
| 2021-07-03 21:42:12 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 21:43:52 +0000 | dka | (~code-is-a@ns3059207.ip-193-70-33.eu) |
| 2021-07-03 21:44:42 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 21:46:35 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) |
| 2021-07-03 21:47:08 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 21:48:10 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 21:48:38 +0000 | neo1 | (~neo3@cpe-292712.ip.primehome.com) (Ping timeout: 272 seconds) |
| 2021-07-03 21:48:50 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 21:48:53 +0000 | cheater1__ | cheater |
| 2021-07-03 21:49:36 +0000 | Gurkenglas | (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) (Ping timeout: 258 seconds) |
| 2021-07-03 21:51:10 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 21:56:48 +0000 | azeem | (~azeem@176.200.221.91) (Ping timeout: 256 seconds) |
| 2021-07-03 21:57:09 +0000 | beka | (~beka@104-244-27-23.static.monkeybrains.net) |
| 2021-07-03 21:57:53 +0000 | azeem | (~azeem@176.200.221.91) |
| 2021-07-03 21:58:46 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) (Ping timeout: 272 seconds) |
| 2021-07-03 22:00:02 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 272 seconds) |
| 2021-07-03 22:00:20 +0000 | amahl | (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 258 seconds) |
| 2021-07-03 22:02:39 +0000 | MQ-17J | (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-03 22:03:12 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 22:03:47 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 22:04:42 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 22:06:23 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 22:07:13 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 22:07:38 +0000 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-07-03 22:08:34 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 22:08:47 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 22:12:09 +0000 | stevenxl | (~stevenlei@68.235.43.93) |
| 2021-07-03 22:16:42 +0000 | akhileshs | (~user@c-73-63-166-39.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 2021-07-03 22:16:56 +0000 | azeem | (~azeem@176.200.221.91) (Ping timeout: 265 seconds) |
| 2021-07-03 22:17:14 +0000 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2021-07-03 22:17:34 +0000 | azeem | (~azeem@176.200.221.91) |
| 2021-07-03 22:19:06 +0000 | neceve | (~quassel@2a02:c7f:607e:d600:f762:20dd:304e:4b1f) (Ping timeout: 240 seconds) |
| 2021-07-03 22:19:37 +0000 | lavaman | (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 22:20:45 +0000 | sayola | (~vekto@dslb-088-078-152-192.088.078.pools.vodafone-ip.de) |
| 2021-07-03 22:24:58 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) (Remote host closed the connection) |
| 2021-07-03 22:29:17 +0000 | nattiestnate | (~nate@180.243.15.91) |
| 2021-07-03 22:29:24 +0000 | pera | (~pera@user/pera) (Ping timeout: 268 seconds) |
| 2021-07-03 22:30:54 +0000 | pera | (~pera@user/pera) |
| 2021-07-03 22:34:35 +0000 | <xacktm> | what pattern should I use if I want to convert between a sum type and a Char? Enum is my first thought, but are those restricted to mapping between Ints only? |
| 2021-07-03 22:35:10 +0000 | <xacktm> | e.g. TypeA is 'A'; TypeB is 'B', etc |
| 2021-07-03 22:35:34 +0000 | fengctor | (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) |
| 2021-07-03 22:37:21 +0000 | <geekosaur> | Enum only works with Int, yes |
| 2021-07-03 22:38:08 +0000 | nattiestnate | (~nate@180.243.15.91) (Quit: WeeChat 3.2) |
| 2021-07-03 22:39:41 +0000 | <xacktm> | hmm, I guess a naive approach should work: fromMyType and toMyType functions and pattern matching |
| 2021-07-03 22:40:31 +0000 | <geekosaur> | there's also toConstr and using the resulting Constr value (https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-Data.html#t:Constr) |
| 2021-07-03 22:42:09 +0000 | <geekosaur> | (you can't use the Constr directly but one of its fiellds will lead you to a value which starts counting at 1 for each field of an algebraic datatype) |
| 2021-07-03 22:42:41 +0000 | zeenk | (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) (Quit: Konversation terminated!) |
| 2021-07-03 22:44:21 +0000 | <geekosaur> | and use the same mechanism in the opposite direction to reconstruct an algebraic constructor, since this is part of generics |
| 2021-07-03 22:45:46 +0000 | <xacktm> | nice, I found this blog post: does this explain everything you're referring to? https://chrisdone.com/posts/data-typeable/ |
| 2021-07-03 22:46:45 +0000 | <xacktm> | most of it is going over my head, need to go slow and unpack :P |
| 2021-07-03 22:47:13 +0000 | <geekosaur> | seems to, perhaps not in as full detail (they show the Show instance for an AlgRep but not the stuff underneath that you'll want to use to map between numbers and eventually Chars) |
| 2021-07-03 22:48:11 +0000 | <geekosaur> | oh, actually it does seem to get at least close to that detail |
| 2021-07-03 22:48:27 +0000 | <geekosaur> | so you should be set between that page and the haddock to see further detail based on that page |
| 2021-07-03 22:48:44 +0000 | <xacktm> | all right, thanks for the pointer! |
| 2021-07-03 22:49:04 +0000 | cheater1__ | (~Username@user/cheater) |
| 2021-07-03 22:49:08 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-03 22:49:16 +0000 | cheater1__ | cheater |
| 2021-07-03 22:50:18 +0000 | lavaman | (~lavaman@98.38.249.169) |
| 2021-07-03 22:50:33 +0000 | <ephemient> | if your data type itself is enum, a quick hack like this might be sufficient. data MyType = MyTypeA | MyTypeB deriving Enum; myTypeToChar :: MyType -> Char; myTypeToChar = chr . (ord 'A' +) . fromEnum -- and vice-versa |
| 2021-07-03 22:51:23 +0000 | <geekosaur> | true, but that means (for example) no fields, just constructors |
| 2021-07-03 22:51:43 +0000 | <ephemient> | yep, for anything else typeable seems like the only generic solution |
| 2021-07-03 22:53:28 +0000 | acidjnk_new | (~acidjnk@p200300d0c72b953339f341015709cf67.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2021-07-03 22:54:46 +0000 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 258 seconds) |
| 2021-07-03 22:56:19 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-03 22:59:08 +0000 | hrnz | (~ulli@irc.plumbing) (Quit: das ist mir zu bld hier; bb) |
| 2021-07-03 22:59:28 +0000 | hrnz | (~ulli@irc.plumbing) |
| 2021-07-03 23:00:15 +0000 | falafel | (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-07-03 23:00:54 +0000 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 258 seconds) |
| 2021-07-03 23:04:20 +0000 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:5061:15ea:118b:e58d) |
| 2021-07-03 23:09:20 +0000 | falafel | (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 258 seconds) |
| 2021-07-03 23:09:24 +0000 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Remote host closed the connection) |
| 2021-07-03 23:10:16 +0000 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 2021-07-03 23:10:33 +0000 | dsf | (~dsf@cpe-66-75-56-205.san.res.rr.com) (Quit: Konversation terminated!) |
| 2021-07-03 23:10:39 +0000 | dsf_ | (~dsf@cpe-66-75-56-205.san.res.rr.com) |
| 2021-07-03 23:11:36 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 23:12:03 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 23:12:59 +0000 | mc47 | (~mc47@xmonad/TheMC47) (Quit: Leaving) |
| 2021-07-03 23:15:28 +0000 | norias | (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) (Ping timeout: 258 seconds) |
| 2021-07-03 23:16:53 +0000 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 268 seconds) |
| 2021-07-03 23:17:56 +0000 | azeem | (~azeem@176.200.221.91) (Ping timeout: 272 seconds) |
| 2021-07-03 23:18:36 +0000 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2021-07-03 23:20:42 +0000 | laguneucl | (~Pitsikoko@athedsl-16082.home.otenet.gr) (Ping timeout: 240 seconds) |
| 2021-07-03 23:21:01 +0000 | azeem | (~azeem@176.200.221.91) |
| 2021-07-03 23:21:11 +0000 | v01d4lph4 | (~v01d4lph4@user/v01d4lph4) |
| 2021-07-03 23:21:40 +0000 | mikoto-chan | (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 252 seconds) |
| 2021-07-03 23:22:09 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2021-07-03 23:26:10 +0000 | v01d4lph4 | (~v01d4lph4@user/v01d4lph4) (Ping timeout: 272 seconds) |
| 2021-07-03 23:31:26 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 23:31:51 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 23:33:52 +0000 | cheater | (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 23:34:19 +0000 | cheater | (~Username@user/cheater) |
| 2021-07-03 23:34:27 +0000 | sciencentistguy | (~sciencent@hacksoc/ordinary-member) |
| 2021-07-03 23:35:57 +0000 | <sciencentistguy> | Is there a way i can have a function parameter that could take either `(+) :: Num a => a -> a -> a` or `(/) :: Fractional a => a -> a -> a` (note the different typeclass constraints) |
| 2021-07-03 23:36:17 +0000 | <sciencentistguy> | i tried `forall c. forall a. c a => a -> a -> a` but that didn't work |
| 2021-07-03 23:37:00 +0000 | <geekosaur> | I think there's a way to do that but it requires extensions? |
| 2021-07-03 23:37:07 +0000 | <sciencentistguy> | i'm fine with using extensions |
| 2021-07-03 23:37:49 +0000 | <sciencentistguy> | i already need RankNTypes for the `forall` clauses |
| 2021-07-03 23:38:38 +0000 | <geekosaur> | it will indeed be a rank-2 type. I just don't recall whatyou need to be able to talk about the constraint, aside from ConstraintKinds |
| 2021-07-03 23:38:46 +0000 | <hpc> | what's wrong with something like f (*) = 1 * 2, or whatever? |
| 2021-07-03 23:39:11 +0000 | <hpc> | :t let f (*) = 1 * 2 in f |
| 2021-07-03 23:39:12 +0000 | <lambdabot> | (Num t1, Num t2) => (t1 -> t2 -> t3) -> t3 |
| 2021-07-03 23:39:22 +0000 | waleee | (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 256 seconds) |
| 2021-07-03 23:39:26 +0000 | <hpc> | > let f (*) = 1 * 2 in (f (/), f (+)) |
| 2021-07-03 23:39:27 +0000 | <lambdabot> | (0.5,3) |
| 2021-07-03 23:39:57 +0000 | Deide | (~Deide@user/deide) (Quit: Seeee yaaaa) |
| 2021-07-03 23:41:11 +0000 | <sciencentistguy> | i'm not sure how that helps |
| 2021-07-03 23:41:22 +0000 | <sciencentistguy> | i'm trying to generalise over binary operators in general |
| 2021-07-03 23:41:46 +0000 | <sciencentistguy> | so i want a function i can pass `(*)` or `mod` or anthing of type `a->a->a` |
| 2021-07-03 23:42:27 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2021-07-03 23:42:28 +0000 | <hpc> | without allowing something like const that's a -> b -> a? |
| 2021-07-03 23:42:57 +0000 | <sciencentistguy> | i don't need to disallow that |
| 2021-07-03 23:45:20 +0000 | <sciencentistguy> | so i have this signature at the moment: |
| 2021-07-03 23:45:23 +0000 | <sciencentistguy> | `lvBinaryOp :: (forall a. a -> a -> a) -> LispValue -> LispValue -> Maybe LispValue` |
| 2021-07-03 23:45:46 +0000 | <sciencentistguy> | and both of these fail to compile: `a = lvBinaryOp (+); b = lvBinaryOp (/)` |
| 2021-07-03 23:46:09 +0000 | <keltono> | what's the error? |
| 2021-07-03 23:46:12 +0000 | <sciencentistguy> | but their error messages suggest a fix (add the constraint to the signature of the function) that are mutually exclusive |
| 2021-07-03 23:46:41 +0000 | <shachaf> | Do you need the argument to be polymorphic? How are you using it? |
| 2021-07-03 23:46:44 +0000 | favonia | (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 23:46:45 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 23:46:59 +0000 | <sciencentistguy> | keltono: "No instance for (Num a) arising from a use of ‘+’" and "No instance for (Fractional a) arising from a use of ‘/’" |
| 2021-07-03 23:47:27 +0000 | <sciencentistguy> | shachaf: i'm using it as a binary operator to number values (either an Integer, a Ratio, or a Double) |
| 2021-07-03 23:48:10 +0000 | <shachaf> | Well, it sounds like the problem here isn't with the type checker, it's with what you're trying to do. |
| 2021-07-03 23:48:28 +0000 | <shachaf> | Forget polymorphism for a moment. Imagine you had (+) :: Int -> Int -> Int and (/) :: Double -> Double -> Double |
| 2021-07-03 23:48:51 +0000 | <shachaf> | What would you want to do there? |
| 2021-07-03 23:48:59 +0000 | <sciencentistguy> | here's the context (here i just gave up and made 3 functions for the 3 different constraints i need to solve, but i really don't like the code duplication that causes) |
| 2021-07-03 23:49:01 +0000 | <sciencentistguy> | https://github.com/Sciencentistguy/haskeme/blob/654caa3bf770324de545bc23517786970d4bd40b/src/Evalu… |
| 2021-07-03 23:49:35 +0000 | favonia | (~favonia@user/favonia) |
| 2021-07-03 23:49:55 +0000 | <sciencentistguy> | s/3/2, lvIntegralOp is actually dead code |
| 2021-07-03 23:52:08 +0000 | nate1 | (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-03 23:52:26 +0000 | betelgeuse | (~john2gb@94-225-47-8.access.telenet.be) (Quit: The Lounge - https://thelounge.chat) |
| 2021-07-03 23:53:43 +0000 | <monochrom> | Nothing says you can't invent your own type class that fits LispValue better. |
| 2021-07-03 23:54:34 +0000 | azeem | (~azeem@176.200.221.91) (Ping timeout: 265 seconds) |
| 2021-07-03 23:54:44 +0000 | <monochrom> | But first of all if you truly understood parametricity then you would not begin with "forall a. a->a->a" which cannot possibly do any arithmetic. |
| 2021-07-03 23:54:57 +0000 | stevenxl | (~stevenlei@68.235.43.93) (Ping timeout: 258 seconds) |
| 2021-07-03 23:55:37 +0000 | <monochrom> | At best it has to be "forall a. C a => a -> a -> a" where C is a class that represents desired arithmetic. |
| 2021-07-03 23:56:00 +0000 | <sciencentistguy> | yeah that's what i've done in the actual code |
| 2021-07-03 23:56:04 +0000 | machinedgod | (~machinedg@24.105.81.50) |
| 2021-07-03 23:57:27 +0000 | <monochrom> | But in all likelihood LispValue does not contain polymorphic content so there is no real reason to want polymorphic arithmetic operations on them. |
| 2021-07-03 23:58:10 +0000 | wolfshappen | (~waff@irc.furworks.de) (Remote host closed the connection) |
| 2021-07-03 23:58:18 +0000 | <sciencentistguy> | I don't think i understand what you mean |
| 2021-07-03 23:58:28 +0000 | Philonous_ | (~Philonous@user/philonous) |
| 2021-07-03 23:58:51 +0000 | <monochrom> | OK, what is the definition of LispValue, really? |
| 2021-07-03 23:59:03 +0000 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 244 seconds) |
| 2021-07-03 23:59:06 +0000 | Philonous | (~Philonous@user/philonous) (Read error: Connection reset by peer) |
| 2021-07-03 23:59:09 +0000 | <sciencentistguy> | https://github.com/Sciencentistguy/haskeme/blob/654caa3bf770324de545bc23517786970d4bd40b/src/Types… |
| 2021-07-03 23:59:24 +0000 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2021-07-03 23:59:26 +0000 | wolfshappen | (~waff@irc.furworks.de) |