Home liberachat/#haskell: Logs Calendar

Logs on 2021-07-03 (liberachat/#haskell)

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

All times are in UTC on 2021-07-03.