Logs on 2021-03-29 (freenode/#haskell)
| 00:00:06 | × | atk quits (~Arch-TK@ircpuzzles/staff/Arch-TK) (Quit: Well this is unexpected.) |
| 00:00:27 | → | atk joins (~Arch-TK@ircpuzzles/staff/Arch-TK) |
| 00:01:47 | <solvr> | wrunt, the seatbelt analogy would be accurate if it took you hours to put on your seatbelt before you leave home, and then when you leave your house you need to leave the seatbelt at home. |
| 00:03:09 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds) |
| 00:06:02 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:07:01 | <wrunt> | No, it still holds, because I'm saying Haskell's type safety saves time, it doesn't cost extra. And you still leave the house in your car with a seatbelt on, you just can't control a truck sideswiping you. |
| 00:08:40 | <Axman6> | yeah types definitely save time, they let you tell the compiler what you think your program needs and the compiler tells you when it turns out you were wrong |
| 00:09:00 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 00:12:29 | <justsomeguy> | wrunt: How long would you estimate that the initial investment of learning haskell takes? |
| 00:12:47 | × | locrian9 quits (~mike@cpe-104-173-20-162.socal.res.rr.com) (Quit: leaving) |
| 00:13:26 | × | Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa) |
| 00:13:38 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 246 seconds) |
| 00:13:48 | → | ddellaco_ joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 00:16:03 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Ping timeout: 246 seconds) |
| 00:19:06 | → | tmciver joins (~tmciver@cpe-172-101-40-226.maine.res.rr.com) |
| 00:19:56 | × | JamesLu quits (~crazypyth@98.122.164.118) (Ping timeout: 246 seconds) |
| 00:20:23 | → | CrazyPython joins (~crazypyth@98.122.164.118) |
| 00:21:41 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:b995:956f:e934:6824) (Ping timeout: 250 seconds) |
| 00:21:47 | → | ph88 joins (~ph88@2a02:8109:9e00:7e5c:e93f:8176:4aa5:ca0b) |
| 00:22:13 | → | Jd007 joins (~Jd007@162.156.11.151) |
| 00:22:28 | → | slack1256 joins (~slack1256@dvc-186-186-101-190.movil.vtr.net) |
| 00:22:59 | × | Sheilong quits (uid293653@gateway/web/irccloud.com/x-qyihkevgdfchqfky) (Quit: Connection closed for inactivity) |
| 00:23:40 | <wrunt> | That depends on how much knowledge you bring with you. If you already have a lot of computer science / discrete maths knowledge, or already know another FP language, then maybe a year or two. Otherwise maybe as many as five, to get really productive. But I only have my own experience to go on. |
| 00:23:50 | → | robotmay joins (~beepboop@80.172.187.81.in-addr.arpa) |
| 00:26:39 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 00:27:24 | Axman6 | hates how disengenuous the whole "Learn X language in 24h" industry is, a profession takes time to master, it takes experience of making mistakes to become proficient in not making them |
| 00:27:38 | <wrunt> | It's probably similar to the amount of investment needed to get good in Python or Java, say, except you won't cause quite as much damage (in terms of horrendous, unmaintainable code) along the way. The downside being that you also won't get as much done. |
| 00:28:04 | <wrunt> | (for short-term values of 'done') |
| 00:29:12 | × | petersen quits (~petersen@redhat/juhp) (Ping timeout: 252 seconds) |
| 00:29:21 | <Axman6> | the first Haskell program I wrote professionally after uni (after two years of not programming) is still in production, and the only bug it's ever been found to have was a Postgres matertialised view which caused the database to fall over one day when it took too long to update |
| 00:32:33 | <ephemient> | I'm not sure what people's standards are for how much time and effort to put into learning a language are, either |
| 00:33:01 | <wrunt> | I'm talking about full-time professional use. |
| 00:34:05 | <wrunt> | Which is obviously hard as a beginner. You'd need a mentor guiding you, at first. The way I learned was over many years, tinkering in my spare time, until I was good enough to start using it at work. |
| 00:35:02 | <wrunt> | And the reason I learned Haskell was that I was just so frustrated with trying to enadicate certain types of bugs in C++, and with trying to express natural concepts with Java. |
| 00:35:30 | <ephemient> | I had a PL course (1 semester) in SML. from there, I found that learning Haskell on my own in an incremental fashion was easy - a lot of it was just lazier and sugarier versions of what I already knew. I'd say I was productive within a week, but as a student my "spare time" was really quite a lot :) |
| 00:36:11 | × | renzhi quits (~renzhi@modemcable070.17-177-173.mc.videotron.ca) (Ping timeout: 240 seconds) |
| 00:37:17 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 00:37:44 | → | sdrodge joins (~sdrodge@unaffiliated/sdrodge) |
| 00:40:53 | → | robotmay_ joins (~beepboop@2001:8b0:7af0:2580:6cec:6538:1c02:32bf) |
| 00:41:03 | × | robotmay quits (~beepboop@80.172.187.81.in-addr.arpa) (Ping timeout: 268 seconds) |
| 00:41:58 | <wrunt> | Most of the frustration that remains for me is in library management, not the programming itself, which is a delight. |
| 00:42:21 | → | gnumonic joins (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) |
| 00:43:45 | <wrunt> | I like where the Unison language is going in that respect. It would be nice if Haskell could be compiled at the function level (rather than the module level), and then I could import content-addressed functions from packages without importing the whole package. But this is pretty ambitious. |
| 00:47:43 | → | Tesseraction joins (~Tesseract@unaffiliated/tesseraction) |
| 00:54:13 | × | Jd007 quits (~Jd007@162.156.11.151) (Quit: Jd007) |
| 00:55:14 | → | DTZUZU_ joins (~DTZUZO@207.81.119.43) |
| 00:55:28 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 00:57:02 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 246 seconds) |
| 00:58:23 | → | CMCDragonkai joins (~Thunderbi@60-242-118-130.tpgi.com.au) |
| 00:58:56 | ski | . o O ( "Teach Yourself Programming in .." by Peter Norvig at <https://www.norvig.com/21-days.html> ) |
| 00:59:08 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 00:59:16 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 00:59:18 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:59:34 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 245 seconds) |
| 01:03:54 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 01:07:34 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 265 seconds) |
| 01:08:32 | × | Guest55480 quits (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) (Ping timeout: 265 seconds) |
| 01:09:46 | × | xiinotulp quits (~q@ppp-27-55-67-28.revip3.asianet.co.th) (Ping timeout: 240 seconds) |
| 01:09:47 | × | robotmay_ quits (~beepboop@2001:8b0:7af0:2580:6cec:6538:1c02:32bf) (Remote host closed the connection) |
| 01:11:41 | × | whataday quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:12:48 | → | whataday joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:14:59 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 01:15:36 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 01:16:23 | × | Jon quits (jon@dow.land) (Quit: ZNC - http://znc.in) |
| 01:17:36 | → | Tario joins (~Tario@200.119.186.197) |
| 01:17:52 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) |
| 01:20:19 | × | haritz quits (~hrtz@unaffiliated/haritz) (Quit: ZNC 1.6.5+deb1+deb9u2 - http://znc.in) |
| 01:21:03 | → | Jd007 joins (~Jd007@162.156.11.151) |
| 01:21:46 | × | Tario quits (~Tario@200.119.186.197) (Ping timeout: 240 seconds) |
| 01:23:38 | → | Jon joins (~jon@redmars.org) |
| 01:23:59 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 01:24:00 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 01:24:00 | → | haritz joins (~hrtz@unaffiliated/haritz) |
| 01:24:32 | × | kupi quits (uid212005@gateway/web/irccloud.com/x-rsqhffuuxfehttck) (Quit: Connection closed for inactivity) |
| 01:25:30 | → | xiinotulp joins (~q@node-ugt.pool-125-24.dynamic.totinternet.net) |
| 01:25:37 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 01:25:58 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) |
| 01:27:39 | → | Tario joins (~Tario@200.119.186.197) |
| 01:31:54 | × | Tario quits (~Tario@200.119.186.197) (Ping timeout: 252 seconds) |
| 01:31:58 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 01:33:17 | → | tpefreedom joins (~tsomers@184-157-240-110.dyn.centurytel.net) |
| 01:34:13 | <justsomeguy> | wrunt: I appreciate your take on it. I've been learning over the last eight months or so, and was trying to guage where I'm at in the process. I suppose I'm slowly getting there, but still pretty terrible at programming overall, as a mental activity. |
| 01:34:43 | × | DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 268 seconds) |
| 01:34:43 | <justsomeguy> | (Prior to this, I've only done simple scripting in Python and bash.) |
| 01:34:46 | × | aarvar quits (~foewfoiew@2601:602:a080:fa0:64a7:ab1c:edbd:150) (Ping timeout: 276 seconds) |
| 01:34:57 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) (Remote host closed the connection) |
| 01:37:20 | → | Guest29 joins (~textual@109.246.40.24) |
| 01:37:50 | → | robotmay joins (~beepboop@80.172.187.81.in-addr.arpa) |
| 01:37:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 01:38:16 | → | DataComputist joins (~lumeng@50.43.26.251) |
| 01:38:47 | → | Lovelace joins (~Android@102.141.185.135) |
| 01:39:02 | × | robwerks1 quits (~robwerks@195.140.213.38) (Remote host closed the connection) |
| 01:39:22 | × | Guest29 quits (~textual@109.246.40.24) (Client Quit) |
| 01:39:58 | × | elliott_ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 01:40:16 | × | solidus-river quits (~mike@174.127.249.180) (Remote host closed the connection) |
| 01:41:22 | → | Tario joins (~Tario@201.192.165.173) |
| 01:44:22 | → | gioyik_ joins (~gioyik@gateway/tor-sasl/gioyik) |
| 01:45:50 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 01:45:50 | × | xiinotulp quits (~q@node-ugt.pool-125-24.dynamic.totinternet.net) (Ping timeout: 252 seconds) |
| 01:46:25 | × | robotmay quits (~beepboop@80.172.187.81.in-addr.arpa) (Ping timeout: 268 seconds) |
| 01:47:33 | × | gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 240 seconds) |
| 01:48:03 | → | aarvar joins (~foewfoiew@2601:602:a080:fa0:9ccc:9e5e:6c10:6175) |
| 01:48:18 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 240 seconds) |
| 01:49:32 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 01:50:44 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 01:52:55 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) (Remote host closed the connection) |
| 01:53:33 | ← | aarvar parts (~foewfoiew@2601:602:a080:fa0:9ccc:9e5e:6c10:6175) () |
| 01:54:10 | → | Jarsto1 joins (~Jarsto@195.140.213.38) |
| 01:54:14 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 01:54:38 | × | Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 252 seconds) |
| 01:54:54 | → | rajivr joins (uid269651@gateway/web/irccloud.com/x-nlktifqfsuwtyuzw) |
| 01:57:00 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 01:57:36 | → | aarvar joins (~foewfoiew@2601:602:a080:fa0:ce9:4062:4238:ecda) |
| 01:58:39 | → | xiinotulp joins (~q@node-ugt.pool-125-24.dynamic.totinternet.net) |
| 01:59:38 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) |
| 02:01:39 | → | stree joins (~stree@68.36.8.116) |
| 02:02:51 | × | xff0x quits (~xff0x@2001:1a81:523f:7b00:3c18:a9e7:56f9:4d88) (Ping timeout: 245 seconds) |
| 02:03:54 | × | Jd007 quits (~Jd007@162.156.11.151) (Quit: Jd007) |
| 02:03:58 | DigitalKiwi | is now known as CryptoKiwi |
| 02:04:22 | CryptoKiwi | is now known as DigitalKiwi |
| 02:05:00 | → | xff0x joins (~xff0x@2001:1a81:5268:4b00:6095:39e:f552:2f81) |
| 02:05:20 | × | Lovelace quits (~Android@102.141.185.135) (Quit: -a- IRC for Android 2.1.59) |
| 02:05:23 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-phnwtlzuswvxveua) |
| 02:06:25 | → | FinnElija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) |
| 02:06:25 | finn_elija | is now known as Guest31930 |
| 02:06:25 | FinnElija | is now known as finn_elija |
| 02:08:17 | × | borne quits (~fritjof@2a06:8782:ffbb:1337:ce73:3416:bcd:fc35) (Ping timeout: 250 seconds) |
| 02:09:09 | × | Guest31930 quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Ping timeout: 240 seconds) |
| 02:10:34 | → | elliott_ joins (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) |
| 02:11:42 | × | Wizek quits (uid191769@gateway/web/irccloud.com/x-ivxcahppedejjawd) (Quit: Connection closed for inactivity) |
| 02:13:49 | → | Guest66 joins (~textual@S0106f0b4d2c39cee.va.shawcable.net) |
| 02:17:42 | × | CrazyPython quits (~crazypyth@98.122.164.118) (Read error: Connection reset by peer) |
| 02:21:26 | × | urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna) |
| 02:22:15 | → | petersen joins (~petersen@redhat/juhp) |
| 02:22:20 | → | gioyik joins (~gioyik@gateway/tor-sasl/gioyik) |
| 02:23:57 | × | gioyik_ quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 240 seconds) |
| 02:27:07 | → | ep1ctetus joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 02:27:10 | × | ep1ctetus quits (~epictetus@ip72-194-215-136.sb.sd.cox.net) (Remote host closed the connection) |
| 02:27:34 | × | slack1256 quits (~slack1256@dvc-186-186-101-190.movil.vtr.net) (Remote host closed the connection) |
| 02:31:11 | × | elliott_ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 265 seconds) |
| 02:32:14 | × | aarvar quits (~foewfoiew@2601:602:a080:fa0:ce9:4062:4238:ecda) (Quit: Leaving.) |
| 02:34:35 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) (Remote host closed the connection) |
| 02:35:54 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 02:35:56 | → | aarvar joins (~foewfoiew@2601:602:a080:fa0:4027:638f:3116:8de5) |
| 02:36:41 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 02:39:02 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 02:42:31 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) (Ping timeout: 250 seconds) |
| 02:42:43 | × | CMCDragonkai quits (~Thunderbi@60-242-118-130.tpgi.com.au) (Quit: CMCDragonkai) |
| 02:43:19 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 02:46:18 | → | CMCDragonkai joins (~Thunderbi@60-242-118-130.tpgi.com.au) |
| 02:51:17 | × | conal quits (~conal@107.181.166.205) (Quit: Computer has gone to sleep.) |
| 02:52:05 | → | elliott_ joins (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) |
| 02:53:18 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 02:55:42 | → | Tario joins (~Tario@201.192.165.173) |
| 02:56:57 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 03:00:12 | × | solvr quits (57e3c46d@87.227.196.109) (Quit: Connection closed) |
| 03:00:49 | × | xiinotulp quits (~q@node-ugt.pool-125-24.dynamic.totinternet.net) (Quit: Leaving) |
| 03:07:13 | ← | aarvar parts (~foewfoiew@2601:602:a080:fa0:4027:638f:3116:8de5) () |
| 03:07:23 | → | conal joins (~conal@107.181.166.205) |
| 03:10:05 | <wrunt> | justsomeguy: Programming happens at the intersection of maths, engineering, and whatever your problem domain is, so it typically takes a long time to get good at all three. But it's worth the effort. And don't worry, I think we were all pretty terrible at it to begin with. Like any skill it can be learned by anyone with enough persistence to stick with it. |
| 03:10:46 | → | aarvar joins (~foewfoiew@2601:602:a080:fa0:c76c:28dd:dc02:df4e) |
| 03:11:50 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:13:53 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 03:17:57 | × | andreas31 quits (~andreas@gateway/tor-sasl/andreas303) (Ping timeout: 240 seconds) |
| 03:19:47 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) (Ping timeout: 250 seconds) |
| 03:20:08 | → | andreas31 joins (~andreas@gateway/tor-sasl/andreas303) |
| 03:20:44 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 03:24:42 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 246 seconds) |
| 03:30:38 | × | Jarsto1 quits (~Jarsto@195.140.213.38) (Remote host closed the connection) |
| 03:31:08 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) |
| 03:33:16 | × | robotmay quits (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) (Ping timeout: 245 seconds) |
| 03:34:01 | × | irc_user quits (uid423822@gateway/web/irccloud.com/x-qhkvurpryivhyrpb) (Quit: Connection closed for inactivity) |
| 03:34:31 | × | aarvar quits (~foewfoiew@2601:602:a080:fa0:c76c:28dd:dc02:df4e) (Ping timeout: 245 seconds) |
| 03:34:32 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 03:36:01 | → | robotmay joins (~beepboop@2001:8b0:7af0:2580:24e0:5511:1a01:8ea8) |
| 03:38:00 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 246 seconds) |
| 03:44:20 | <bbhoss> | so I've noticed that very often the "collection" is often the last parameter to many functions. this makes sense because it makes it easier to use the same function for multiple things, as parameters are applied from the left. is this formalized somewhere? |
| 03:45:14 | × | alx741 quits (~alx741@186.178.109.231) (Quit: alx741) |
| 03:46:43 | → | flound1129 joins (~flound112@139.28.218.148) |
| 03:49:25 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 03:55:52 | → | drbean_ joins (~drbean@TC210-63-209-15.static.apol.com.tw) |
| 03:55:53 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 03:56:05 | <wrunt> | Not formal, but here's some discussion of it: https://wiki.haskell.org/Parameter_order |
| 03:56:39 | → | bitmagie1 joins (~Thunderbi@200116b8069ac20068656f6dd34a0922.dip.versatel-1u1.de) |
| 03:58:04 | <bbhoss> | this is what I was looking for, thanks |
| 03:58:31 | × | bitmagie quits (~Thunderbi@200116b80660de0030b444d902e7bc81.dip.versatel-1u1.de) (Ping timeout: 252 seconds) |
| 03:58:31 | bitmagie1 | is now known as bitmagie |
| 03:59:58 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 04:07:06 | × | elliott_ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 04:08:48 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 04:09:09 | × | zaquest quits (~notzaques@5.128.210.178) (Remote host closed the connection) |
| 04:09:32 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 246 seconds) |
| 04:10:07 | → | zaquest joins (~notzaques@5.128.210.178) |
| 04:10:47 | → | solvr joins (57e3c46d@87.227.196.109) |
| 04:17:36 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 04:19:53 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 04:22:55 | × | SaitamaPlus quits (uid272474@gateway/web/irccloud.com/x-cfuxdhlufguvidaj) (Quit: Connection closed for inactivity) |
| 04:23:02 | → | stree joins (~stree@68.36.8.116) |
| 04:27:00 | → | z0k joins (~user@115.186.169.1) |
| 04:27:22 | × | Narinas quits (~Narinas@187-178-93-112.dynamic.axtel.net) (Read error: Connection reset by peer) |
| 04:28:28 | → | Narinas joins (~Narinas@187-178-93-112.dynamic.axtel.net) |
| 04:29:33 | × | NGravity quits (csp@gateway/shell/xshellz/x-ztkryqboprznxnxa) (Ping timeout: 250 seconds) |
| 04:29:54 | → | Jd007 joins (~Jd007@162.156.11.151) |
| 04:32:11 | × | Narinas quits (~Narinas@187-178-93-112.dynamic.axtel.net) (Read error: Connection reset by peer) |
| 04:32:35 | → | Narinas joins (~Narinas@187-178-93-112.dynamic.axtel.net) |
| 04:32:53 | → | limbo joins (ar@45.63.9.236) |
| 04:35:13 | → | gioyik_ joins (~gioyik@gateway/tor-sasl/gioyik) |
| 04:35:24 | × | solvr quits (57e3c46d@87.227.196.109) (Quit: Connection closed) |
| 04:35:33 | × | gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 240 seconds) |
| 04:40:05 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 04:40:08 | → | DTZUZU_ joins (~DTZUZO@207.81.119.43) |
| 04:42:03 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 246 seconds) |
| 04:51:17 | × | ddellaco_ quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Remote host closed the connection) |
| 04:51:28 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 04:52:05 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Remote host closed the connection) |
| 04:53:06 | × | tpefreedom quits (~tsomers@184-157-240-110.dyn.centurytel.net) (Quit: Leaving) |
| 05:02:15 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:31a8:b768:9c51:16bb) (Remote host closed the connection) |
| 05:03:47 | × | incertia quits (~incertia@d4-50-26-103.nap.wideopenwest.com) (Ping timeout: 246 seconds) |
| 05:03:56 | × | Guest66 quits (~textual@S0106f0b4d2c39cee.va.shawcable.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 05:04:48 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 246 seconds) |
| 05:08:02 | → | desophos joins (~desophos@2601:249:1680:a570:dd16:7252:b42e:9895) |
| 05:09:51 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 05:13:28 | → | ddellacosta joins (~ddellacos@86.106.143.53) |
| 05:13:36 | → | incertia joins (~incertia@d4-50-26-103.nap.wideopenwest.com) |
| 05:13:38 | × | Tene quits (~tene@poipu/supporter/slacker/tene) (Ping timeout: 240 seconds) |
| 05:14:15 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 246 seconds) |
| 05:14:28 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 05:14:33 | × | desophos quits (~desophos@2601:249:1680:a570:dd16:7252:b42e:9895) (Quit: Leaving) |
| 05:14:36 | × | ByronJohnson quits (~bairyn@unaffiliated/bob0) (Ping timeout: 246 seconds) |
| 05:16:48 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 05:17:41 | × | ddellacosta quits (~ddellacos@86.106.143.53) (Ping timeout: 240 seconds) |
| 05:18:30 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 05:18:49 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 05:18:57 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 250 seconds) |
| 05:19:17 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 05:20:21 | → | Lord_of_Life joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 05:23:11 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 240 seconds) |
| 05:26:53 | → | yaroot7 joins (~yaroot@138.102.13.160.dy.iij4u.or.jp) |
| 05:26:59 | × | yaroot quits (~yaroot@138.102.13.160.dy.iij4u.or.jp) (Read error: Connection reset by peer) |
| 05:27:00 | yaroot7 | is now known as yaroot |
| 05:27:33 | × | bitmagie quits (~Thunderbi@200116b8069ac20068656f6dd34a0922.dip.versatel-1u1.de) (Quit: bitmagie) |
| 05:27:54 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 05:32:18 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 240 seconds) |
| 05:33:24 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 05:33:57 | × | Sheilong quits (uid293653@gateway/web/irccloud.com/x-phnwtlzuswvxveua) (Quit: Connection closed for inactivity) |
| 05:34:03 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 05:34:19 | → | Tario joins (~Tario@201.192.165.173) |
| 05:37:34 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 05:40:27 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:41:17 | → | Anon joins (7aab9886@122.171.152.134) |
| 05:41:19 | × | vgtw quits (~vgtw@gateway/tor-sasl/vgtw) (Remote host closed the connection) |
| 05:41:35 | → | vgtw joins (~vgtw@gateway/tor-sasl/vgtw) |
| 05:41:40 | Anon | is now known as Guest9981 |
| 05:41:58 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 240 seconds) |
| 05:42:08 | ← | Guest9981 parts (7aab9886@122.171.152.134) () |
| 05:45:39 | → | Tene joins (~tene@mail.digitalkingdom.org) |
| 05:45:40 | × | Tene quits (~tene@mail.digitalkingdom.org) (Changing host) |
| 05:45:40 | → | Tene joins (~tene@poipu/supporter/slacker/tene) |
| 05:46:27 | → | ByronJohnson joins (~bairyn@unaffiliated/bob0) |
| 05:48:42 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 05:49:06 | → | plutoniix joins (~q@184.82.195.122) |
| 05:50:22 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 05:53:06 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 05:53:30 | → | codygman__ joins (~user@209.251.131.98) |
| 05:54:45 | → | knupfer joins (~Thunderbi@200116b82b0bfe00e407e369ad43ca6f.dip.versatel-1u1.de) |
| 05:55:00 | → | madjestic joins (~Android@86-88-72-244.fixed.kpn.net) |
| 05:55:33 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 268 seconds) |
| 05:59:24 | × | hiroaki quits (~hiroaki@2a02:8108:8c40:2bb8:35c5:fb8d:f07:96c1) (Ping timeout: 246 seconds) |
| 06:00:17 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 06:05:09 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 06:05:55 | × | d34df00d quits (~d34df00d@104-14-27-213.lightspeed.austtx.sbcglobal.net) (Max SendQ exceeded) |
| 06:07:41 | × | codygman__ quits (~user@209.251.131.98) (Remote host closed the connection) |
| 06:08:01 | → | codygman__ joins (~user@209.251.131.98) |
| 06:08:07 | × | pavonia quits (~user@unaffiliated/siracusa) (Quit: Bye!) |
| 06:09:37 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 06:10:39 | → | Cetty-si joins (5809af17@23.red-88-9-175.dynamicip.rima-tde.net) |
| 06:10:56 | ← | Cetty-si parts (5809af17@23.red-88-9-175.dynamicip.rima-tde.net) () |
| 06:10:58 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 06:11:02 | → | hiroaki joins (~hiroaki@2a02:8108:8c40:2bb8:1e40:f339:ac5b:717) |
| 06:13:30 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 06:14:40 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 268 seconds) |
| 06:16:32 | × | CMCDragonkai quits (~Thunderbi@60-242-118-130.tpgi.com.au) (Ping timeout: 268 seconds) |
| 06:16:59 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 06:20:05 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 06:23:46 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 06:26:14 | × | waleee-cl quits (uid373333@gateway/web/irccloud.com/x-qsyvwqmdsnwpfrno) (Quit: Connection closed for inactivity) |
| 06:28:06 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 246 seconds) |
| 06:30:38 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 240 seconds) |
| 06:31:56 | × | codygman__ quits (~user@209.251.131.98) (Ping timeout: 268 seconds) |
| 06:35:18 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 06:36:42 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 06:37:13 | → | solvr joins (57e3c46d@87.227.196.109) |
| 06:37:15 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 06:39:00 | × | gioyik_ quits (~gioyik@gateway/tor-sasl/gioyik) (Quit: WeeChat 3.0) |
| 06:39:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 06:39:30 | → | shad0w_ joins (a0ca255a@160.202.37.90) |
| 06:42:01 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 06:43:11 | × | Wuzzy quits (~Wuzzy@p57a2ecf2.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 06:44:20 | → | stree joins (~stree@68.36.8.116) |
| 06:48:02 | → | acidjnk_new joins (~acidjnk@p200300d0c72b95797030ab852a1672b2.dip0.t-ipconnect.de) |
| 06:50:43 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 06:52:55 | → | Tops2 joins (~Tobias@dyndsl-095-033-095-007.ewe-ip-backbone.de) |
| 06:55:05 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 246 seconds) |
| 06:56:43 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 07:01:06 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 240 seconds) |
| 07:04:01 | → | chele joins (~chele@ip5b40237d.dynamic.kabel-deutschland.de) |
| 07:06:57 | → | raym joins (~ray@115.187.32.14) |
| 07:08:18 | × | azure2 quits (~azure@103.154.230.130) (Ping timeout: 240 seconds) |
| 07:08:41 | → | azure2 joins (~azure@103.154.230.130) |
| 07:11:18 | → | Guest55480 joins (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) |
| 07:12:13 | → | jespada joins (~jespada@90.254.243.187) |
| 07:14:13 | × | shad0w_ quits (a0ca255a@160.202.37.90) (Quit: Connection closed) |
| 07:16:46 | × | eruditass quits (uid248673@gateway/web/irccloud.com/x-pqiwmoliqqwvohha) (Quit: Connection closed for inactivity) |
| 07:18:12 | → | coot joins (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) |
| 07:19:13 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 07:20:34 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:21:11 | × | __minoru__shirae quits (~shiraeesh@109.166.57.99) (Ping timeout: 265 seconds) |
| 07:22:13 | × | unyu quits (~pyon@unaffiliated/pyon) (Quit: ERC (IRC client for Emacs 27.2)) |
| 07:22:58 | × | madjestic quits (~Android@86-88-72-244.fixed.kpn.net) (Remote host closed the connection) |
| 07:24:02 | × | Jd007 quits (~Jd007@162.156.11.151) (Quit: Jd007) |
| 07:26:16 | × | ddere quits (uid110888@gateway/web/irccloud.com/x-ydfajrwtbkzcpvbs) (Quit: Connection closed for inactivity) |
| 07:28:19 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 07:28:51 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 07:28:55 | × | lawid quits (~quassel@dslb-090-186-023-078.090.186.pools.vodafone-ip.de) (Ping timeout: 265 seconds) |
| 07:29:15 | → | lawid joins (~quassel@dslb-084-060-077-139.084.060.pools.vodafone-ip.de) |
| 07:29:49 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 07:32:35 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 07:32:58 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 240 seconds) |
| 07:34:17 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 246 seconds) |
| 07:34:31 | × | lawid quits (~quassel@dslb-084-060-077-139.084.060.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 07:34:36 | → | lawid_ joins (~quassel@dslb-178-005-075-142.178.005.pools.vodafone-ip.de) |
| 07:35:10 | → | borne joins (~fritjof@2a06:8782:ffbb:1337:ce73:3416:bcd:fc35) |
| 07:37:01 | → | marinelli joins (~marinelli@gateway/tor-sasl/marinelli) |
| 07:37:36 | × | gnumonic quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 07:38:02 | → | gnumonic joins (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) |
| 07:38:31 | → | LKoen joins (~LKoen@65.250.88.92.rev.sfr.net) |
| 07:40:01 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 07:41:35 | → | Yumasi joins (~guillaume@2a01:e0a:5cb:4430:dbe9:fd6c:d1a9:4bb5) |
| 07:44:24 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 07:45:27 | × | borne quits (~fritjof@2a06:8782:ffbb:1337:ce73:3416:bcd:fc35) (Ping timeout: 246 seconds) |
| 07:47:05 | → | kuribas joins (~user@ptr-25vy0i9nyhjns61vpxg.18120a2.ip6.access.telenet.be) |
| 07:47:16 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 07:47:18 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 07:47:25 | → | borne joins (~fritjof@200116b8648ef300f7ed9fd86a2491f0.dip.versatel-1u1.de) |
| 07:48:11 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Remote host closed the connection) |
| 07:49:32 | → | jonathanx joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 07:50:17 | → | kritzefitz joins (~kritzefit@fw-front.credativ.com) |
| 07:51:45 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 246 seconds) |
| 07:58:20 | → | unyu joins (~pyon@unaffiliated/pyon) |
| 07:58:52 | × | unyu quits (~pyon@unaffiliated/pyon) (Quit: brb) |
| 08:01:51 | → | Iceland_jack joins (~user@95.149.219.0) |
| 08:02:31 | × | lawid_ quits (~quassel@dslb-178-005-075-142.178.005.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 08:03:16 | → | lawid joins (~quassel@dslb-178-005-066-219.178.005.pools.vodafone-ip.de) |
| 08:04:16 | → | unyu joins (~pyon@unaffiliated/pyon) |
| 08:04:54 | → | raichoo joins (~raichoo@dslb-188-109-062-207.188.109.pools.vodafone-ip.de) |
| 08:05:11 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 08:05:57 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 08:06:38 | → | fendor joins (~fendor@77.119.130.24.wireless.dyn.drei.com) |
| 08:07:24 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 08:08:56 | → | pupuupup joins (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) |
| 08:10:16 | × | seveg quits (~gabriel@2a02-ab04-0249-8d00-dea6-32ff-fe17-0993.dynamic.v6.chello.sk) (Ping timeout: 240 seconds) |
| 08:11:31 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 08:11:37 | → | seveg joins (~gabriel@2a02-ab04-0249-8d00-dea6-32ff-fe17-0993.dynamic.v6.chello.sk) |
| 08:11:42 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 246 seconds) |
| 08:12:37 | × | Sgeo quits (~Sgeo@ool-18b98aa4.dyn.optonline.net) (Read error: Connection reset by peer) |
| 08:14:21 | → | Sorna joins (~Sornaensi@79.142.232.102.static.router4.bolignet.dk) |
| 08:14:49 | → | graf_blutwurst joins (~user@2001:171b:226e:adc0:3dbe:eebd:8040:b693) |
| 08:15:46 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 245 seconds) |
| 08:16:38 | × | Sornaensis quits (~Sornaensi@077213203030.dynamic.telenor.dk) (Ping timeout: 240 seconds) |
| 08:18:50 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 08:20:06 | × | Erutuon_ quits (~Erutuon@97-116-16-233.mpls.qwest.net) (Ping timeout: 246 seconds) |
| 08:21:30 | → | pupuupup1 joins (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) |
| 08:22:43 | → | dandart joins (~Thunderbi@home.dandart.co.uk) |
| 08:24:20 | × | pupuupup quits (~pupuupup@ppp-124-122-133-152.revip2.asianet.co.th) (Ping timeout: 246 seconds) |
| 08:25:36 | → | Franciman joins (~francesco@host-79-53-62-46.retail.telecomitalia.it) |
| 08:27:15 | × | pupuupup1 quits (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) (Ping timeout: 268 seconds) |
| 08:28:19 | × | __minoru__shirae quits (~shiraeesh@109.166.57.99) (Quit: Konversation terminated!) |
| 08:28:32 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 08:30:10 | → | pupuupup joins (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) |
| 08:32:45 | × | Unhammer quits (~Unhammer@gateway/tor-sasl/unhammer) (Ping timeout: 240 seconds) |
| 08:34:36 | × | pupuupup quits (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) (Ping timeout: 260 seconds) |
| 08:35:23 | → | Unhammer joins (~Unhammer@gateway/tor-sasl/unhammer) |
| 08:39:13 | × | berberman quits (~berberman@unaffiliated/berberman) (Ping timeout: 276 seconds) |
| 08:39:33 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 08:41:38 | × | azure2 quits (~azure@103.154.230.130) (Ping timeout: 240 seconds) |
| 08:42:18 | → | azure2 joins (~azure@180.247.95.50) |
| 08:45:04 | × | solvr quits (57e3c46d@87.227.196.109) (Quit: Connection closed) |
| 08:46:28 | → | pupuupup_ joins (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) |
| 08:46:40 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 08:48:21 | × | drbean_ quits (~drbean@TC210-63-209-15.static.apol.com.tw) (Quit: ZNC 1.8.2+cygwin2 - https://znc.in) |
| 08:48:52 | × | ixlun quits (~matthew@109.249.184.133) (Read error: Connection reset by peer) |
| 08:48:53 | Guest42457 | is now known as SIben |
| 08:49:54 | → | benkolera joins (uid285671@gateway/web/irccloud.com/x-eheuohrapvmfijla) |
| 08:50:46 | × | pupuupup_ quits (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) (Ping timeout: 240 seconds) |
| 08:51:56 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 268 seconds) |
| 08:52:33 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 268 seconds) |
| 08:58:17 | → | michalz joins (~user@185.246.204.46) |
| 09:01:50 | → | enoq joins (~textual@194-208-146-143.lampert.tv) |
| 09:02:46 | × | lawid quits (~quassel@dslb-178-005-066-219.178.005.pools.vodafone-ip.de) (Ping timeout: 240 seconds) |
| 09:03:33 | → | lawid joins (~quassel@dslb-178-005-075-139.178.005.pools.vodafone-ip.de) |
| 09:05:21 | → | stree joins (~stree@68.36.8.116) |
| 09:06:18 | → | Iryon joins (~Iryon@2a02:a31a:a045:3500:5420:2237:4aee:26f2) |
| 09:08:07 | → | SaitamaPlus joins (uid272474@gateway/web/irccloud.com/x-gljisqtsvqcmgfbx) |
| 09:16:12 | × | MarcelineVQ quits (~anja@198.254.208.159) (Read error: Connection reset by peer) |
| 09:17:32 | → | MarcelineVQ joins (~anja@198.254.208.159) |
| 09:17:46 | → | pupuupup_ joins (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) |
| 09:20:08 | → | gaff joins (~user@49.207.222.255) |
| 09:21:34 | <gaff> | is there a way to turn data Line a = Line a | Foo (a, a) | Empty into a monad instance |
| 09:21:37 | <gaff> | ? |
| 09:22:30 | × | pupuupup_ quits (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) (Ping timeout: 265 seconds) |
| 09:23:07 | <merijn> | I don't think so? |
| 09:23:14 | <gaff> | i see |
| 09:23:24 | <merijn> | gaff: Consider the type of >>= |
| 09:23:30 | <merijn> | :t (>>=) |
| 09:23:31 | <lambdabot> | Monad m => m a -> (a -> m b) -> m b |
| 09:23:39 | <gaff> | yes |
| 09:23:50 | <merijn> | So you need to take a function "a -> Line b" and return "Line b" |
| 09:24:00 | <gaff> | yes |
| 09:24:14 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 09:24:22 | <merijn> | What would that look like when the input is "Foo"? You have two a's, you can run the function twice, but then you have *two* "Line b" values that need to be turned into one "Line b" to typecheck |
| 09:24:30 | → | pupuupup joins (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) |
| 09:24:33 | <merijn> | I don't think you can write a law abiding instance that does that |
| 09:24:44 | <gaff> | the types will not match up |
| 09:25:17 | <gaff> | also, you can not define a sensible return |
| 09:25:38 | <merijn> | "return = Line" seems sensible enough |
| 09:25:52 | <gaff> | no, it isn't |
| 09:26:02 | <gaff> | how will you define return |
| 09:26:04 | <gaff> | ? |
| 09:26:30 | <gaff> | why is that sensible? |
| 09:26:53 | <merijn> | Why not? |
| 09:27:47 | <merijn> | Just looking at the "shape" of your datatype it seems reasonable enough |
| 09:28:02 | <gaff> | return (a, b) = ? |
| 09:28:32 | <gaff> | you have 2 cases: return (a, b), return a |
| 09:28:56 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 268 seconds) |
| 09:29:10 | <opqdonut> | I could see a fun applicative instance for Line though: Line f <*> Line x = Line (f x); Line f <*> Foo (x, y) = Foo (f x, f y); Foo (f, g) <*> Line x = Foo (f x, g x); Foo (f, g) <*> Foo (x, y) = Foo (f x, g y); _ <*>_ = Empty |
| 09:29:40 | <opqdonut> | gaff: there is no requirement to be able to produce all kinds of values in your type using "return" |
| 09:29:54 | <gaff> | ok |
| 09:29:54 | <opqdonut> | gaff: e.g. for lists, return x = [x]. There is no way to produce [1,2,3] using return. |
| 09:29:58 | × | azure2 quits (~azure@180.247.95.50) (Ping timeout: 260 seconds) |
| 09:30:13 | <opqdonut> | similarly for Maybe, return x = Just x. There is no way to produce Nothing using return. |
| 09:30:24 | <gaff> | so why is return = Line sensible? |
| 09:30:56 | <gaff> | why not return (a, b) = Foo (a, b)? |
| 09:30:56 | <opqdonut> | the types match, and it works with e.g. the Applicative instance I just wrote out |
| 09:31:04 | <opqdonut> | gaff: that wouldn't type |
| 09:31:24 | <opqdonut> | it needs to be return :: a -> Line a. Your return would be (a,a) -> Line a |
| 09:31:24 | → | azure2 joins (~azure@180.247.95.50) |
| 09:31:57 | <gaff> | ah, i see |
| 09:31:59 | <opqdonut> | return x = Foo (x,x) would type, as would return x = Empty |
| 09:32:22 | <gaff> | got it |
| 09:34:26 | <gaff> | so my question is, if we have f :: Line -> IO [Line], and g :: IO (), how can you extract values from Line within a do construact in g? |
| 09:34:42 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-qybeoxhtmvdqtlff) |
| 09:34:46 | <gaff> | given that Line is not a monad |
| 09:34:55 | <opqdonut> | you do it |
| 09:36:04 | <opqdonut> | something like: g = do ...; result <- f line; let foo = map something result; let final = foldr quux xyzzy foo; print final |
| 09:36:39 | <opqdonut> | IO is the monad here, Line doesn't need to be a monad |
| 09:36:46 | <gaff> | yes |
| 09:37:17 | → | mouseghost joins (~draco@87-206-9-185.dynamic.chello.pl) |
| 09:37:18 | × | mouseghost quits (~draco@87-206-9-185.dynamic.chello.pl) (Changing host) |
| 09:37:18 | → | mouseghost joins (~draco@wikipedia/desperek) |
| 09:38:40 | <gaff> | ok, i have to think about that |
| 09:39:07 | <gaff> | so you extract the values using pattern matching? |
| 09:40:16 | <opqdonut> | for example, yes |
| 09:47:30 | <gaff> | so suppose you have to call a function, say, p :: (Int, Int) -> Int in g :: IO (), where p 's tuple comes from Foo (x, y). when you pattern match an item in result, you have 2 cases: Foo (x, y) -> p (x, y). but what would you do with the other case, Line a -> ? |
| 09:47:58 | × | pupuupup quits (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) (Ping timeout: 240 seconds) |
| 09:49:31 | → | pupuupup joins (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) |
| 09:52:31 | <opqdonut> | gaff: it depends on what you want the code to do |
| 09:52:47 | <opqdonut> | `Line a -> 0` would type check |
| 09:52:57 | <opqdonut> | or you can just leave the case unhandled and get an error at runtime :) |
| 09:53:08 | <gaff> | ah, i see |
| 09:53:51 | <ski> | hm, it might be possible to make a (lawful) `Monad' instance for `Line' .. |
| 09:53:59 | <gaff> | it is cruffy stuff. i imagine people face these sort of situations often. and they have to revert to runtime checks. |
| 09:54:09 | <opqdonut> | ski: just ignore the second component of Foo? |
| 09:54:17 | <ski> | no |
| 09:54:19 | <opqdonut> | ok |
| 09:54:27 | <ski> | i don't think that would work |
| 09:55:05 | <ski> | `join (Foo (Foo (a,b),Foo (c,d)) = Foo (a,d)' sounds reasonable, i think. however, there's more cases to consider |
| 09:55:20 | × | MarcelineVQ quits (~anja@198.254.208.159) (Ping timeout: 252 seconds) |
| 09:55:52 | <opqdonut> | (hmm yes m >>= return === m doesn't hold if you ignore the other component) |
| 09:56:07 | <ski> | i think if we treat `Line a' as if it was `Foo (a,a)', then that could work. and if there's any `Empty', then the overall result is `Empty' |
| 09:56:18 | <opqdonut> | mmh |
| 09:56:38 | <gaff> | yes |
| 09:56:43 | <ski> | would need to check all cases for associativity to make sure, though. but it looks like it might work, on first thought |
| 09:56:56 | <ski> | however, it's likely that this is not what gaff really needed |
| 09:57:47 | → | MarcelineVQ joins (~anja@198.254.208.159) |
| 09:59:05 | <ski> | i guess this may be like `MaybeT Pair' or something, hm |
| 09:59:11 | <gaff> | ski: basically, i outlined the need a few minutes back. i want to extract (a, b) and pass it to a function p, where p :: (Int, Int) -> Int, and this code needs to be within a function :: IO (). |
| 09:59:14 | × | avn quits (~avn@78-56-108-78.static.zebra.lt) (Remote host closed the connection) |
| 09:59:26 | <ski> | yea, i (briefly) looked at that |
| 09:59:40 | <ski> | and that doesn't sound like you want to use `Line' as a monad |
| 10:00:16 | <ski> | hmm |
| 10:00:26 | <ski> | i think i may have a counter example |
| 10:00:33 | <gaff> | yes, i don't care if it is not a monad, but how do you solve this problem, because there is a case where you have to return some dummy value. |
| 10:00:47 | <gaff> | ? |
| 10:01:40 | × | gitgood quits (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) (Remote host closed the connection) |
| 10:03:11 | <ski> | (join . join) (Foo (Foo (Foo (a,b),Empty),Foo (Empty,Foo (g,h)))) = join (Foo (Foo (a,b),Foo (g,h))) = Foo (a,h) |
| 10:03:17 | <ski> | (join . fmap join) (Foo (Foo (Foo (a,b),Empty),Foo (Empty,Foo (g,h)))) = join (Foo (Empty,Empty)) = Empty |
| 10:03:54 | <ski> | this is assuming `join (Foo (Empty,_)) = Empty' and `join (Foo (_,Empty)) = Empty' |
| 10:03:57 | <lortabac> | gaff: how you solve this problem depends on what your program does and how you handle errors |
| 10:04:20 | <ski> | gaff : what opqdonut and lortabac said |
| 10:04:27 | → | ddellacosta joins (~ddellacos@86.106.143.10) |
| 10:04:54 | <lortabac> | you can return some default value (if there is one that makes sense), you can return an 'Either Error Int', or a 'Maybe Int', you can throw an exception... |
| 10:04:58 | × | shailangsa quits (~shailangs@host86-161-220-11.range86-161.btcentralplus.com) () |
| 10:05:16 | <gaff> | lortabac: yeah, or perhaps even call error |
| 10:05:33 | <gaff> | the easy way out. |
| 10:06:04 | <ski> | a generalization of "default value" is to use some "default value", not for the desired result of type `(Int,Int)', but for a larger expression that would include that result, if present |
| 10:06:46 | → | peanut_ joins (~peanut_@2a02:8388:a101:2600:1aac:99fd:f87d:92f0) |
| 10:06:55 | <ski> | (in your case, possibly a default value of type `Int'. to use in place of the call to `p'. or perhaps a default value of type `IO ()' to use in place of the action that would otherwise make use of that result value from `p') |
| 10:07:19 | <ski> | gaff : point is, we can't tell you how you want to handle the alternative cases, here |
| 10:07:34 | <gaff> | ski: yeah, got it |
| 10:07:56 | <ski> | it really depends on your use-case, on what you're actually trying to to, trying to achieve |
| 10:08:15 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 10:08:42 | <gaff> | in this one, my only need is for Foo (x, y) -> p (x, y). the other case no need, although it is needed elsewhere. |
| 10:09:36 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:09:37 | × | ddellacosta quits (~ddellacos@86.106.143.10) (Ping timeout: 268 seconds) |
| 10:09:40 | <gaff> | bash has a no-op operator :. is there some thing like that in haskell? |
| 10:10:22 | <gaff> | `: arg` does nothing in bash. |
| 10:10:22 | × | pupuupup quits (~pupuupup@ppp-124-122-192-176.revip2.asianet.co.th) (Ping timeout: 252 seconds) |
| 10:12:27 | × | azure2 quits (~azure@180.247.95.50) (Ping timeout: 246 seconds) |
| 10:12:29 | <lortabac> | gaff: yes, there is 'return ()' |
| 10:12:45 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 10:13:01 | <gaff> | i see, but then that works only for monad instances, right. |
| 10:13:23 | <lortabac> | no sorry, I meant 'return () :: IO ()' |
| 10:13:31 | <gaff> | ah |
| 10:14:12 | × | enoq quits (~textual@194-208-146-143.lampert.tv) (Ping timeout: 246 seconds) |
| 10:14:26 | <lortabac> | but of course you cannot use it directly in 'p :: (Int, Int) -> Int' |
| 10:14:52 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Remote host closed the connection) |
| 10:14:56 | <gaff> | i see |
| 10:14:59 | <ski> | what do you mean by "no-op operator" ? |
| 10:15:12 | <ski> | in some sense, `id' could be considered one |
| 10:15:34 | <gaff> | ski: thanks much |
| 10:15:40 | <ski> | > id 42 |
| 10:15:42 | <lambdabot> | 42 |
| 10:15:46 | <gaff> | lortabac: thanks much |
| 10:15:56 | <gaff> | opqdonut: thanks much for your time. |
| 10:16:31 | <peanut_> | > id (id (id 1)) |
| 10:16:33 | <lambdabot> | 1 |
| 10:17:04 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 245 seconds) |
| 10:17:19 | → | malumore joins (~malumore@151.62.126.223) |
| 10:17:34 | × | lawid quits (~quassel@dslb-178-005-075-139.178.005.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 10:17:34 | → | enoq joins (~textual@194-208-146-143.lampert.tv) |
| 10:18:06 | <gaff> | switching topics here -- i encounterred a situation recently where a functiion, say f, defined in one module, when called from another module, say Main, works fine. but if i move the function to Main or some other module, it hangs. i don't have the code with me now, but any idea what's going on? |
| 10:18:08 | → | lawid joins (~quassel@dslb-090-186-122-181.090.186.pools.vodafone-ip.de) |
| 10:18:56 | <gaff> | ski: no -op operator just doesn't do anything. |
| 10:19:22 | <gaff> | bash -- `: arg` doesn't do anything. |
| 10:19:35 | <peanut_> | : is just true |
| 10:19:40 | <gaff> | doesn't process or execute anything |
| 10:20:15 | × | Majiir quits (~Majiir@pool-96-237-149-35.bstnma.fios.verizon.net) (Quit: CUT THE HARDLINES!!) |
| 10:20:16 | <xsperry> | > id id id 1 |
| 10:20:16 | <gaff> | peanut_: correct. |
| 10:20:19 | <lambdabot> | 1 |
| 10:20:50 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 10:21:03 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:21:54 | × | __minoru__shirae quits (~shiraeesh@109.166.57.99) (Ping timeout: 246 seconds) |
| 10:22:48 | <peanut_> | > const 42 (putStrLn "nothing") |
| 10:22:51 | <lambdabot> | 42 |
| 10:22:54 | × | dandart quits (~Thunderbi@home.dandart.co.uk) (Remote host closed the connection) |
| 10:23:10 | <gaff> | in bash, `: arg` expands `arg` but does nothing else. |
| 10:23:23 | <peanut_> | 🤔 |
| 10:23:34 | <gaff> | like you can do : > some-file-path |
| 10:24:19 | <gaff> | peanut_: ok |
| 10:25:35 | × | MarcelineVQ quits (~anja@198.254.208.159) (Read error: Connection reset by peer) |
| 10:26:10 | <gaff> | so it is strange that which module a function lives affect performace? |
| 10:26:11 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 10:26:54 | → | MarcelineVQ joins (~anja@198.254.208.159) |
| 10:27:11 | <peanut_> | only thing i can think of is f uses another function g, defined in both modules but g doesnt terminate in Main |
| 10:27:13 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:27:13 | → | Majiir joins (~Majiir@pool-96-237-149-35.bstnma.fios.verizon.net) |
| 10:28:11 | <gaff> | peanut_: no soory, that's not case at all. f calls functions that terminate well. |
| 10:28:57 | <gaff> | and even more bizarre, call f from other modules with smaller inputs works just fine. |
| 10:29:13 | <peanut_> | I'd have to see it |
| 10:29:32 | <gaff> | yeah, i will come back here when i get the code. |
| 10:30:19 | <gaff> | btw, cabal 3.4 works pretty good so far with nix-style builds. |
| 10:30:47 | <gaff> | documentations needs catch up, though. |
| 10:32:05 | <gaff> | peanut_: thank you very much. i will come back later when i get access to the code. |
| 10:32:33 | <peanut_> | 👍 |
| 10:33:44 | × | gaff quits (~user@49.207.222.255) (Quit: ERC (IRC client for Emacs 27.1)) |
| 10:34:41 | × | lawid quits (~quassel@dslb-090-186-122-181.090.186.pools.vodafone-ip.de) (Ping timeout: 240 seconds) |
| 10:37:40 | × | idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 246 seconds) |
| 10:37:59 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 10:38:27 | → | lawid joins (~quassel@dslb-090-186-122-181.090.186.pools.vodafone-ip.de) |
| 10:38:34 | → | pyuk joins (~vroom@217.138.252.168) |
| 10:38:37 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:38:58 | × | pyuk quits (~vroom@217.138.252.168) (Client Quit) |
| 10:39:03 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 10:39:38 | × | puke quits (~vroom@217.138.252.196) (Ping timeout: 240 seconds) |
| 10:41:50 | → | bor0 joins (~boro@unaffiliated/boro/x-000000001) |
| 10:42:55 | → | ubert joins (~Thunderbi@p200300ecdf25d94cca5b76fffe29f233.dip0.t-ipconnect.de) |
| 10:43:38 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 10:43:43 | <bor0> | I have a PropCalc data type defined as `data PropCalc = P | Q | R | Not PropCalc | And PropCalc PropCalc | Or PropCalc PropCalc | Imp PropCalc PropCalc`. I want to create a function `apply` so that it modifies an element in a specific order. E.g., apply 1 (\x -> P) (And Q R) should return (And P R). Is there an elegant/easy way of doing this? One way I thought of was to create between trees and list representations |
| 10:43:44 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 252 seconds) |
| 10:44:19 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:44:36 | <ski> | what's the `1' for ? |
| 10:44:46 | <bor0> | Position of the tree node |
| 10:45:23 | <bor0> | For unary operators it is easy: go n pos f (Not x) | n == pos = Not (f x) and go n pos f (Not x) = go (n + 1) pos f (Not x). Things get trickier when I have to deal with `And` |
| 10:45:48 | <bor0> | I don't know the count of the nodes in advance... maybe I should calculate that in the interim |
| 10:48:03 | <ski> | hm. numbered leaf ? |
| 10:48:51 | <bor0> | Yeah.. that could also work - to convert every node in the structure from Node to (Int, Node) |
| 10:48:59 | <ski> | i'm wondering if you could avoid referring to things to replace by numbers, at all |
| 10:49:08 | <ski> | if you could, that would probably be nicer |
| 10:49:36 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 10:49:45 | <bor0> | Basically, I'm trying to provide a toy implementation of Gentzen's propositional calculus. In it, we can replace some rules (e.g. ~~P with P). But I want to be able to specify at which point do I want to make this replacement |
| 10:49:51 | <ski> | (but if you really want to or have to use numbering, that's also possible .. you'd thread a state through the recursion. can be done manually. state-monad would be easier, though, i think) |
| 10:50:05 | <bor0> | Maybe there is a much more elegant way to achieve this than what I'm trying to do now |
| 10:50:07 | <ski> | hm, ok |
| 10:50:14 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:50:19 | <ski> | replace an arbitrary subformula ? |
| 10:50:29 | <ski> | or just replace leaves (that is, propositional variables) ? |
| 10:50:48 | <ski> | and, replace all occurances of a particular propositional variable ? or just a single occurance ? |
| 10:50:50 | <bor0> | Yeah. I was trying to map some of the examples used in Godel Escher Bach, and in there he just replaces an arbitrary subformula |
| 10:51:15 | <ski> | instead of using number, perhaps you could use a path to the formula you want to replace |
| 10:51:40 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 10:52:31 | <bor0> | So, let's say I want to convert (Imp (And P Q) Q) to (Imp (And (~~P) Q) Q). How would that work with this path approach? |
| 10:52:58 | <ski> | hm, also, i'm wondering if it's Genzen's Natural Deductin, or perhaps his Sequent Calculus |
| 10:53:10 | <ski> | s/Deductin/Deduction/ |
| 10:54:05 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 10:54:07 | <ski> | well, in that case, the path would consist of two components, one indicating the left subtree of `Imp', and the next indicating the left subtree of `And' |
| 10:54:26 | <ski> | the indicators could be numbers. could also be symbolic, if you prefer |
| 10:54:27 | <ph88> | i'm using tasty-hunit and for one test i would like to change the current working directory. How can i find my project directory or test directory ?? (from these i can calculate the working directory i need) |
| 10:54:28 | <bor0> | Hm, I think that's not specified.. the way he uses the rules are like https://imgur.com/a/l8oV8p0 |
| 10:54:49 | <bor0> | Note how he applied contrapositive to the left argument of Imp |
| 10:54:59 | <merijn> | ph88: You can't reall, tbh |
| 10:55:12 | <ph88> | hows that ? |
| 10:55:13 | <bor0> | s/contrapositive/double-tilde/ |
| 10:55:20 | <merijn> | ph88: What's in this working directory? Input files for tests? |
| 10:55:42 | <ski> | bor0 : hm, that looks like some Hilbert-style axiomatix system. my condoleances |
| 10:55:54 | <ph88> | the input files of the test are in a specific directory. I want to set the current working directory to this directory |
| 10:55:56 | <bor0> | :D |
| 10:55:57 | <ski> | hm, or maybe it isn't |
| 10:56:04 | → | dandart joins (~Thunderbi@home.dandart.co.uk) |
| 10:56:06 | <ski> | maybe that's just a deduction tree |
| 10:56:16 | <bor0> | Looks like it |
| 10:56:45 | <ski> | although .. i don't think it's either NK or LK |
| 10:56:48 | <merijn> | ph88: When installing package, the source isn't (normally) installed, so cabal doesn't allow you to depend on the layout of your source directory/ies |
| 10:56:56 | <merijn> | ph88: You probably want data-files instead: https://cabal.readthedocs.io/en/latest/cabal-package.html?highlight=getdatafile#accessing-data-files-from-package-code |
| 10:57:09 | <bor0> | OK, so by path you mean accept a list like [Left, Left, Right] which would pinpoint to exactly the node we want? |
| 10:57:31 | <ph88> | merijn, i need to install my package for i can run its tests ? |
| 10:57:32 | <bor0> | and when I reach [] I just apply f in there |
| 10:58:09 | <ski> | bor0 : "Note how he applied contrapositive to the left argument of Imp" -- i don't think that's what he did, actually |
| 10:58:14 | <merijn> | ph88: No, you don't have to install. But cabal doesn't allow you to ask "what is the path to the source directory?" because that question is non-sensical when packages get installed |
| 10:58:16 | <ski> | hm |
| 10:58:24 | <bor0> | ski, sorry. I amended that with s/contrapositive/double-tilde/ |
| 10:58:27 | <bor0> | You probably missed that |
| 10:58:34 | <ski> | ah, just noticed your correction |
| 10:58:37 | <merijn> | ph88: Instead, you should use the data-files field and getDataFile to access read-only data from your code |
| 10:58:41 | <ski> | sure, yea |
| 10:59:07 | <merijn> | ph88: See the link I sent |
| 10:59:18 | <bor0> | I like this path approach. It's much better than converting between list/tree representations and the numbering one. Thanks! Will try doing that. |
| 10:59:24 | <ski> | bor0 : "OK, so by path you mean .. " -- yes, something like that. that would be much easier to interpret, in `Apply' |
| 10:59:34 | <ph88> | oki |
| 10:59:37 | <ph88> | thanks |
| 11:00:32 | <ski> | bor0 : if you go symbolic, i guess for `Not', you'd have a `Down' rather than arbitrarily choosing between `Left' and `Right' |
| 11:00:36 | <bor0> | Yes! |
| 11:00:37 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 11:00:42 | <bor0> | I just hit that and started asking a question lol |
| 11:01:03 | <ski> | (one could have `ImpLeft',`AndLeft' and so on .. but it probably doesn't make too much of a difference) |
| 11:01:17 | <ph88> | merijn, what do you think about this solution ? https://stackoverflow.com/a/21033253 since i know the structure of my project i can calculate the directory from any source file |
| 11:01:33 | <ski> | bor0 : heh, nice that i anticipated that, then :P |
| 11:01:46 | <bor0> | ski, in terms of front-end experience, the numbers make most sense. but in terms of simple implementation, I think [Left, Right, Down] will be acceptable |
| 11:02:05 | <ski> | you could obviously convert between the formats, if needed |
| 11:02:05 | <bor0> | (After all, it's probably only myself who will be the front-end user of this :D) |
| 11:02:06 | → | ixlun joins (~matthew@109.249.184.133) |
| 11:02:34 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 11:02:39 | <merijn> | ph88: I think it's terrible and dear god, please don't ever do that in a package you plan for other people to use... >.> |
| 11:02:47 | <ski> | (btw, "switcheroo" is a weird name ..) |
| 11:02:50 | → | puke joins (~vroom@217.138.252.168) |
| 11:02:50 | <ph88> | why terrible ?? |
| 11:03:12 | <merijn> | ph88: Because you're hardcoding the compile time source path in your code |
| 11:03:21 | <bor0> | In https://en.wikipedia.org/wiki/Switcheroo there's some clarification: "In his book G�del, Escher, Bach, Douglas Hofstadter names one of the rules in his version of propositional calculus the Switcheroo Rule, apparently in honour of an Albanian railroad engineer, name Q. Q. Switcheroo, who "worked in logic on the siding".[5] This is in reality the material implication." |
| 11:03:21 | × | stree quits (~stree@68.36.8.116) (Quit: Caught exception) |
| 11:03:21 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection) |
| 11:03:38 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 11:03:48 | → | stree joins (~stree@68.36.8.116) |
| 11:03:49 | <merijn> | ph88: When someone tries to install your package, that path will almost certainly be in a temporary directory that gets deleted, so now the installed executable refers to a non-existent temporary path |
| 11:04:07 | <merijn> | Not to mention CPP is a terrible extension >.> |
| 11:04:17 | <ski> | (bor0 : i have read GEB, but it was a long time ago, so i don't remember much specifics of the formal systems in it) |
| 11:04:25 | <merijn> | Where as data-files is literally less work *and* more robust/safer |
| 11:04:28 | <ph88> | merijn, i figured since it's just for testing it's ok |
| 11:04:49 | × | dandart quits (~Thunderbi@home.dandart.co.uk) (Quit: dandart) |
| 11:04:57 | <bor0> | ski, yeah. So I'm trying to implement in Haskell his toy implementations of Gentzen's Propositional Calculus and later I want to also tackle Peano's arithmetic (TNT) |
| 11:05:25 | <ph88> | merijn, what about data-files ? do i have to list each individual file ? |
| 11:06:45 | <ph88> | oh wildcards cool |
| 11:07:27 | ski | nods to bor0 |
| 11:07:52 | <ski> | bor0 : the basic rules of NK or LK aren't terribly complicated, either, btw |
| 11:08:05 | <bor0> | What's NK and LK? |
| 11:08:14 | <ski> | (NK is the Natural Deduction version. LK is the Sequent Calculus version) |
| 11:10:11 | <bor0> | While I have your interest here, could use your :eyes: for a quick review :) https://github.com/bor0/misc/blob/master/2021/Gentzen.hs |
| 11:10:15 | <ski> | bor0 : you might be interested in playing with the Sequent Calculus interactive tutorial, by lexilambda, at <http://logitext.mit.edu/main> |
| 11:11:00 | <ski> | er, sorry. wrong person. it's by ezyang (Edward Z. Yang) (sometime in 2012, i think) |
| 11:12:27 | <ski> | bor0 : hmm. you want `apply [Go] f P = P', rather than `apply [Go] f P = f P' ? |
| 11:13:14 | <bor0> | Thanks for sharing that. I've seen this somewhere. It reminds me of the incredible proof machine https://incredible.pm/ |
| 11:13:25 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood) |
| 11:13:46 | <ski> | it looks like you're using `Go' to terminate the path. i'd just use the end of the list (the empty list), to terminate, so that `apply' knows when to stop descending, and apply the rewriting at the currently reached node |
| 11:13:49 | <bor0> | ski, I decided to use GoLeft and GoRight just to traverse and Go to actually Apply. This seems redundant |
| 11:14:01 | <bor0> | Heh, we're almost talking the same stuff :D |
| 11:14:08 | × | Alleria__ quits (~textual@2603-7000-3040-0000-908d-bfdf-28c9-9e71.res6.spectrum.com) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 11:14:24 | × | idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 246 seconds) |
| 11:14:43 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 11:15:06 | <ski> | anyway, if applying `f' to a subformula `P' is actually meant to replace it by `f P', rather than leave it untouched (and similarly for `Q',`R'), you could in fact simplify your code, by having a single base case |
| 11:15:51 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 11:16:29 | <bor0> | How does this look? https://github.com/bor0/misc/commit/84c3bce60f4ce5448aadd561fb08e90d4938a547 |
| 11:16:52 | → | ddellacosta joins (~ddellacos@86.106.143.196) |
| 11:16:52 | <bor0> | Ah. I need to `f P`, `f Q`, `f R`... |
| 11:17:12 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 11:17:22 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Remote host closed the connection) |
| 11:17:44 | ski | . o O ( "Go West" by Pet Shop Boys at <https://www.youtube.com/watch?v=LNBjMRvOB5M>,<https://www.youtube.com/watch?v=cfGTm_viXPs> ) |
| 11:17:58 | <bor0> | Ah, you mean `apply [] f x = f x` would be the base case? |
| 11:18:13 | <ski> | yes |
| 11:19:44 | <bor0> | OK, I think I finally got it. The rule I shared earlier https://imgur.com/a/l8oV8p0 is basically `eg4` https://github.com/bor0/misc/blob/master/2021/Gentzen.hs#L115 which evaluates to `Or P (Not P)`. Quite satisfying :D |
| 11:20:22 | <ski> | and then you don't need the default case at the end (and then you'll get better diagnostics if you change the data type, while using `-Wincomplete-patterns'. cf. `-Wincomplete-uni-patterns',`-Wincomplete-record-updates') |
| 11:21:02 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 11:21:11 | <raehik> | I'm getting an HTTP 500 when trying to upload a package candidate to Hackage - is there someone I could notify? |
| 11:21:29 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 11:21:46 | × | ddellacosta quits (~ddellacos@86.106.143.196) (Ping timeout: 268 seconds) |
| 11:22:10 | <merijn> | raehik: Is this your first upload? |
| 11:22:39 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 11:22:41 | <raehik> | merijn: it's the first upload of the package in question, but no I've pushed pkgs before |
| 11:23:05 | <merijn> | ah, just checking if maybe you weren't in the uploaders group yet :) |
| 11:23:40 | <raehik> | the error says "no space left on resource", seems like /tmp got filled, unsure if it's been caught yet |
| 11:23:55 | <merijn> | raehik: There's the #hackage channel and https://github.com/haskell/hackage-server/issues |
| 11:23:58 | <merijn> | a |
| 11:24:26 | <merijn> | raehik: Hackage mainpage says: "Serious issues requiring immediate action should be reported to admin@haskell.org or on the #haskell-infrastructure irc channel on freenode." |
| 11:24:31 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 245 seconds) |
| 11:24:41 | → | idhugo__ joins (~idhugo@87-49-45-185-mobile.dk.customer.tdc.net) |
| 11:24:43 | × | Dykam quits (Dykam@dykam.nl) (Quit: Dykam) |
| 11:24:43 | <raehik> | merijn: Fab, thanks very much! |
| 11:26:29 | → | Dykam joins (Dykam@dykam.nl) |
| 11:26:58 | × | idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 11:29:50 | × | raichoo quits (~raichoo@dslb-188-109-062-207.188.109.pools.vodafone-ip.de) (Quit: Lost terminal) |
| 11:32:57 | <ph88> | does anyone know if hunit has some facilities for test setup and teardown ? |
| 11:33:03 | <ph88> | tasty-hunit in particular |
| 11:36:34 | × | LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Read error: Connection reset by peer) |
| 11:38:20 | → | LKoen joins (~LKoen@65.250.88.92.rev.sfr.net) |
| 11:40:21 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 240 seconds) |
| 11:41:28 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 11:41:46 | → | ph88^ joins (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) |
| 11:42:44 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 11:43:18 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 11:43:43 | → | Alleria joins (~textual@mskresolve-a.mskcc.org) |
| 11:44:06 | Alleria | is now known as Guest23256 |
| 11:45:12 | × | ph88 quits (~ph88@2a02:8109:9e00:7e5c:e93f:8176:4aa5:ca0b) (Ping timeout: 246 seconds) |
| 11:46:02 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 258 seconds) |
| 11:48:51 | × | ixlun quits (~matthew@109.249.184.133) (Read error: Connection reset by peer) |
| 11:50:12 | <dexterfoo> | anyone use co-log? How do I use usingLoggerT with fmtRichMessageDefault? The types don't match up |
| 11:50:19 | → | geowiesnot joins (~user@87-89-181-157.abo.bbox.fr) |
| 11:52:29 | × | flound1129 quits (~flound112@139.28.218.148) (Remote host closed the connection) |
| 11:54:14 | × | bor0 quits (~boro@unaffiliated/boro/x-000000001) (Quit: Leaving) |
| 11:55:48 | × | acidjnk_new quits (~acidjnk@p200300d0c72b95797030ab852a1672b2.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 11:56:31 | × | plutoniix quits (~q@184.82.195.122) (Quit: Leaving) |
| 11:56:51 | → | ddellacosta joins (~ddellacos@86.106.143.66) |
| 11:58:08 | <xerox_> | is there a way to collapse all collapsable dropdowns in an haddock page? |
| 11:58:30 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 246 seconds) |
| 11:58:56 | → | acidjnk_new joins (~acidjnk@p200300d0c72b9579218a2a0630d85b14.dip0.t-ipconnect.de) |
| 12:01:51 | × | ddellacosta quits (~ddellacos@86.106.143.66) (Ping timeout: 268 seconds) |
| 12:04:16 | × | MarcelineVQ quits (~anja@198.254.208.159) (Read error: Connection reset by peer) |
| 12:07:50 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 12:11:32 | → | csadilek joins (~csadilek@178.239.168.171) |
| 12:12:09 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 12:15:29 | × | coot quits (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 12:26:35 | → | solvr joins (57e3c46d@87.227.196.109) |
| 12:27:02 | → | Deide joins (~Deide@217.155.19.23) |
| 12:27:28 | → | coot joins (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) |
| 12:28:46 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 12:31:24 | × | DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 246 seconds) |
| 12:31:50 | → | NGravity joins (csp@gateway/shell/xshellz/x-beigeckolcvbhubi) |
| 12:31:51 | × | seveg quits (~gabriel@2a02-ab04-0249-8d00-dea6-32ff-fe17-0993.dynamic.v6.chello.sk) (Ping timeout: 252 seconds) |
| 12:32:22 | × | geekosaur quits (82650c7a@130.101.12.122) (Ping timeout: 240 seconds) |
| 12:33:11 | → | seveg joins (~gabriel@2a02-ab04-0249-8d00-dea6-32ff-fe17-0993.dynamic.v6.chello.sk) |
| 12:36:35 | → | urodna joins (~urodna@unaffiliated/urodna) |
| 12:37:16 | → | ddellacosta joins (~ddellacos@86.106.143.248) |
| 12:37:36 | × | coot quits (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 12:37:53 | → | drbean_ joins (~drbean@TC210-63-209-23.static.apol.com.tw) |
| 12:38:06 | × | yaroot quits (~yaroot@138.102.13.160.dy.iij4u.or.jp) (Quit: The Lounge - https://thelounge.chat) |
| 12:38:10 | × | ubert quits (~Thunderbi@p200300ecdf25d94cca5b76fffe29f233.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 12:38:14 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) |
| 12:38:29 | → | ubert joins (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) |
| 12:38:48 | → | yaroot joins (~yaroot@138.102.13.160.dy.iij4u.or.jp) |
| 12:40:06 | → | motersen joins (~motersen@217.160.212.240) |
| 12:40:34 | × | raym quits (~ray@115.187.32.14) (Quit: leaving) |
| 12:41:01 | <ph88^> | merijn, i tried data-files but the data directory is not being made :/ |
| 12:41:21 | × | gnumonic quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 12:41:56 | × | ddellacosta quits (~ddellacos@86.106.143.248) (Ping timeout: 268 seconds) |
| 12:43:37 | × | Yumasi quits (~guillaume@2a01:e0a:5cb:4430:dbe9:fd6c:d1a9:4bb5) (Ping timeout: 276 seconds) |
| 12:44:52 | → | Yumasi joins (~guillaume@static-176-175-104-214.ftth.abo.bbox.fr) |
| 12:45:24 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 12:48:40 | × | motersen quits (~motersen@217.160.212.240) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 12:48:53 | → | motersen joins (~user@2a0a-a540-7dde-0-2d1c-e683-f179-e2a.ipv6dyn.netcologne.de) |
| 12:49:03 | <ph88^> | ah something is showing up actually |
| 12:49:46 | × | todda7 quits (~torstein@athedsl-266674.home.otenet.gr) (Remote host closed the connection) |
| 12:50:58 | × | motersen quits (~user@2a0a-a540-7dde-0-2d1c-e683-f179-e2a.ipv6dyn.netcologne.de) (Client Quit) |
| 12:52:27 | → | fcortesi joins (~fcortesi@78-66-245-190.fibertel.com.ar) |
| 12:54:33 | × | fcortesi quits (~fcortesi@78-66-245-190.fibertel.com.ar) (Remote host closed the connection) |
| 12:54:44 | → | motersen joins (~motersen@217.160.212.240) |
| 12:55:32 | × | motersen quits (~motersen@217.160.212.240) (Client Quit) |
| 12:55:42 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Quit: leaving) |
| 12:59:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 13:01:57 | × | benkolera quits (uid285671@gateway/web/irccloud.com/x-eheuohrapvmfijla) (Quit: Connection closed for inactivity) |
| 13:02:26 | → | motersen joins (~user@2a0a-a540-7dde-0-2d1c-e683-f179-e2a.ipv6dyn.netcologne.de) |
| 13:02:38 | × | LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 13:04:39 | → | coot joins (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) |
| 13:05:15 | × | motersen quits (~user@2a0a-a540-7dde-0-2d1c-e683-f179-e2a.ipv6dyn.netcologne.de) (Client Quit) |
| 13:07:13 | → | carlomagno joins (~cararell@148.87.23.12) |
| 13:08:17 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 13:11:21 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-fhumobypoetbfjsj) |
| 13:11:39 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 246 seconds) |
| 13:11:51 | → | motersen joins (~motersen@217.160.212.240) |
| 13:12:55 | → | ddellacosta joins (~ddellacos@86.106.143.40) |
| 13:13:17 | × | Iceland_jack quits (~user@95.149.219.0) (Read error: Connection reset by peer) |
| 13:13:32 | → | Iceland_jack joins (~user@95.149.219.0) |
| 13:14:51 | × | motersen quits (~motersen@217.160.212.240) (Client Quit) |
| 13:15:40 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 13:15:59 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 13:17:53 | × | ddellacosta quits (~ddellacos@86.106.143.40) (Ping timeout: 265 seconds) |
| 13:19:35 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 13:24:58 | → | stree joins (~stree@68.36.8.116) |
| 13:25:08 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 13:25:27 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 13:25:58 | × | idhugo__ quits (~idhugo@87-49-45-185-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 13:27:44 | → | jonathanx_ joins (~jonathan@94.234.49.69) |
| 13:28:12 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 13:28:46 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 13:30:15 | <johnnyboy[m]> | hi |
| 13:30:40 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Ping timeout: 268 seconds) |
| 13:31:00 | <johnnyboy[m]> | how can I match a string having a tab between two tokens using regex-tdfa? |
| 13:31:14 | × | astronavt quits (~astronavt@unaffiliated/astronavt) (Remote host closed the connection) |
| 13:31:19 | <johnnyboy[m]> | I've tried these three without success: \t, \s+, [[:space:]]+ |
| 13:31:23 | <johnnyboy[m]> | none of them match |
| 13:31:36 | <johnnyboy[m]> | \s+ and [[:space:]]+ work with grep -E |
| 13:32:29 | <johnnyboy[m]> | e.g. `[0-9]+.[0-9]{3}[[:space:]]+actual` works with grep, but seems not to work with TDFA |
| 13:33:05 | → | astronavt joins (~astronavt@unaffiliated/astronavt) |
| 13:33:21 | <[exa]> | you may need something like \\t for it to actually get through. but regex-tdfa support for escape sequences is limited, I've been adding mine one time I was playing with it |
| 13:33:42 | → | alx741 joins (~alx741@181.196.68.106) |
| 13:33:54 | × | astronavt quits (~astronavt@unaffiliated/astronavt) (Remote host closed the connection) |
| 13:35:32 | → | astronavt joins (~astronavt@unaffiliated/astronavt) |
| 13:36:52 | <merijn> | tbh, I would recommend reconsidering the use of regexes |
| 13:37:44 | × | SaitamaPlus quits (uid272474@gateway/web/irccloud.com/x-gljisqtsvqcmgfbx) (Quit: Connection closed for inactivity) |
| 13:37:50 | × | astronavt quits (~astronavt@unaffiliated/astronavt) (Remote host closed the connection) |
| 13:38:18 | <maerwald> | regexes are great |
| 13:38:51 | <merijn> | maerwald: Regexes are great for accepting user input and using that too match stuff (like grep, search in vim, etc.) |
| 13:38:53 | <geekosaur> | …at being unreadable |
| 13:39:01 | <merijn> | Regexes are terrible if you embed them in source code |
| 13:39:03 | <maerwald> | merijn: merijn also, your opinions is appreciated: https://files.hasufell.de/jule/abstract-filepath/AbstractFilePath.html |
| 13:39:40 | <merijn> | My personal rule of thumb is to only use regexes when the pattern is runtime user input |
| 13:39:51 | → | astronavt joins (~astronavt@unaffiliated/astronavt) |
| 13:40:11 | × | malumore quits (~malumore@151.62.126.223) (Remote host closed the connection) |
| 13:40:34 | <merijn> | maerwald: I'll have a longer look later, but at first glance I appreciate your quixotic quest ;) |
| 13:40:37 | <johnnyboy[m]> | I also tried \t without success |
| 13:40:44 | <johnnyboy[m]> | and [:space:] |
| 13:40:53 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 13:41:10 | <merijn> | johnnyboy[m]: Any specific reason not to use some parser combinator library instead? |
| 13:41:17 | <johnnyboy[m]> | I'm kind of considering removing tabs as a preprocessing step |
| 13:41:38 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 13:41:54 | <johnnyboy[m]> | <merijn "johnnyboy: Any specific reason n"> not really, I just thought that regexes would be handy for my use case |
| 13:41:58 | → | xourt joins (d4c620ea@212-198-32-234.rev.numericable.fr) |
| 13:42:04 | <johnnyboy[m]> | so far, they've been working |
| 13:42:29 | <johnnyboy[m]> | it really seems to be the tab character that is problematic |
| 13:42:31 | <merijn> | maerwald: Maybe at version with an explicit encoding/decoding argument for linux too? |
| 13:42:40 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) |
| 13:42:47 | <maerwald> | yeah, though about that too |
| 13:42:56 | <maerwald> | not sure that's common enough though? |
| 13:43:16 | <maerwald> | the idea is that more control is easily achievable by using the "private" constructors |
| 13:43:27 | × | geekosaur quits (82650c7a@130.101.12.122) (Quit: Connection closed) |
| 13:43:29 | <maerwald> | semi-private, so to speak |
| 13:44:28 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 13:44:30 | <merijn> | johnnyboy[m]: The upside is that (speaking from personal experience) maintaining/changing the parser combinator 1.5 year in the future will be much nicer than the regex ;) |
| 13:44:48 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 13:44:55 | × | drbean_ quits (~drbean@TC210-63-209-23.static.apol.com.tw) (Quit: ZNC 1.8.2+cygwin2 - https://znc.in) |
| 13:45:41 | → | motersen joins (~motersen@217.160.212.240) |
| 13:46:13 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 13:46:30 | <johnnyboy[m]> | I'm using regexes to match output from a piece of software that has used the same output probably from the 80'ies or 90'ies |
| 13:47:04 | <johnnyboy[m]> | in fact, that's the reason why I'm writing my own tool in the first place |
| 13:47:13 | × | motersen quits (~motersen@217.160.212.240) (Client Quit) |
| 13:47:51 | kilolympus | is now known as yutotakano |
| 13:47:53 | <johnnyboy[m]> | but I suppose parser combinators could also get the job done |
| 13:48:14 | <johnnyboy[m]> | I just don't need the power of context free grammars now |
| 13:48:16 | → | motersen joins (~motersen@217.160.212.240) |
| 13:48:21 | yutotakano | is now known as kilolympus |
| 13:48:25 | <johnnyboy[m]> | regular expressions are sufficient |
| 13:48:49 | × | motersen quits (~motersen@217.160.212.240) (Client Quit) |
| 13:48:55 | <merijn> | johnnyboy[m]: I've been using them for trivial stuff like "split on : and count number of groups" and they work fine for that too :) |
| 13:49:04 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 13:49:27 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 13:49:36 | <merijn> | johnnyboy[m]: Stuff like: https://github.com/merijn/Belewitte/blob/master/benchmark-analysis/ingest-src/Parsers.hs is if much longer than the regex would be? Yes. Do I appreciate that 2 years after writing it? Also yes :p |
| 13:49:40 | → | malumore joins (~malumore@151.62.126.223) |
| 13:49:42 | <johnnyboy[m]> | I'm really just scraping output from another program, picking keywords and their associated values |
| 13:49:45 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 13:50:15 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 13:50:34 | <johnnyboy[m]> | and then I turn it into a nice structured format, e.g. JSON, XML, CSV, HTML tables, markdown tables, or LaTeX tables |
| 13:50:41 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 252 seconds) |
| 13:51:40 | <johnnyboy[m]> | I did use the optparse library for parsing the command line arguments and it works great |
| 13:52:21 | <tomsmeding> | johnnyboy[m]: can you perhaps share the code that runs that regex? |
| 13:52:39 | <tomsmeding> | to double-check syntax |
| 13:52:49 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Client Quit) |
| 13:53:09 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 13:54:08 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 13:55:11 | <johnnyboy[m]> | <tomsmeding "johnnyboy: can you perhaps share"> this is the file where my regexes are: https://gitlab.com/jllang/spin2latex/-/blob/master/src/Token.hs |
| 13:55:21 | <johnnyboy[m]> | I should really rename that project |
| 13:55:36 | <[exa]> | johnnyboy[m]: you should really use attoparsec |
| 13:55:39 | <johnnyboy[m]> | it's not really restricted to producing LaTeX tables anymore |
| 13:56:06 | <tomsmeding> | oh hi john :) |
| 13:56:21 | <johnnyboy[m]> | hi, tom :) |
| 13:57:02 | × | graf_blutwurst quits (~user@2001:171b:226e:adc0:3dbe:eebd:8040:b693) (Remote host closed the connection) |
| 13:57:13 | <johnnyboy[m]> | maybe a parser combinator library would be a good idea in the long run |
| 13:57:44 | <[exa]> | like, I understand the language may be regular so a "full" context-free grammar parser looks like an overkill |
| 13:57:57 | <johnnyboy[m]> | anyway, my intention is to simply just discard most of the input text and only pick a handful of interesting fields |
| 13:58:11 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 13:58:41 | <[exa]> | except, running normal attoparsecs is usually much less complex than compiling, optimizing and running the regexes |
| 13:59:26 | <[exa]> | also, it quite often happens that you need to do very ugly regex tricks to capture stuff that's trivial with parsers |
| 13:59:28 | <tomsmeding> | johnnyboy[m]: are you sure that [[:space:]] doesn't work? this page claims that it's supported (see under "Feature support"): https://hackage.haskell.org/package/regex-tdfa-1.3.1.0/docs/Text-Regex-TDFA.html |
| 13:59:46 | <johnnyboy[m]> | maybe there's something else wrong then |
| 13:59:48 | <[exa]> | and finally, you'll be ready for the moment you at some point realize you need to support parentheses. |
| 14:00:09 | <johnnyboy[m]> | by the way, the version in github has a mistake there |
| 14:00:23 | <tomsmeding> | [exa]: OP said that the text being parsed has been the same format since ages, so unlikely to change |
| 14:00:23 | <johnnyboy[m]> | sorry, no |
| 14:00:37 | <merijn> | tomsmeding: That's not really relevant, though :p |
| 14:01:00 | <merijn> | tomsmeding: Because the attoparsec version will be simpler to read/write even if you don't have to update it |
| 14:01:08 | <tomsmeding> | though I do agree that parser combinators are nicer than regex in Haskell, especially in Haskell, where parser combinators are so nice |
| 14:01:17 | <tomsmeding> | merijn: that latter point depends on your familiarity with regex ;) |
| 14:02:03 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 14:02:16 | <[exa]> | tomsmeding: I've heard this a few times. Usually followed by "whew what a nice export, what if we also packed in a $non_regular_feature to make the export more colorful?" |
| 14:02:35 | <tomsmeding> | export != import? |
| 14:02:39 | → | ixlun joins (~matthew@109.249.184.133) |
| 14:03:16 | <[exa]> | (I meant the export that comes from the other part of the program) |
| 14:03:48 | tomsmeding | is just trying to provide a bit of pushback to "how do I do X simple common thing with technique A? -- Well, please use technique PQR that does 10 other things but is much nicer" :) |
| 14:03:53 | <tomsmeding> | not trying to be hostile |
| 14:04:24 | <maerwald> | tomsmeding: parser combinators are more expressive and as such may not be desired :) that is following the principle of using the least powerful tool. |
| 14:04:45 | <tomsmeding> | [exa]: ah, I see |
| 14:04:46 | <maerwald> | That argument has also repeatedly been made by the LANGSEC authors |
| 14:05:35 | <maerwald> | treat input as a language, write a validator and use the least expressive tool |
| 14:05:52 | <maerwald> | in that sense, they also created parser combinator library for C |
| 14:06:03 | → | MarcelineVQ joins (~anja@198.254.208.159) |
| 14:06:10 | <maerwald> | (arguing that parser combinators are magnitudes more safer than a hand-written one) |
| 14:06:14 | <merijn> | maerwald: parser combinators are just recursive descent parsers with a convenient paint of code |
| 14:07:00 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 14:07:57 | <merijn> | Well written recursive descent parsers are just as efficient and minimal as their corresponding LALR(k) version. But most humans find recursive descent much easier to write/think about (and better errors) |
| 14:08:29 | <tomsmeding> | % import Text.Regex.TDFA |
| 14:08:30 | <yahb> | tomsmeding: ; <no location info>: error:; Could not find module `Text.Regex.TDFA'; It is not a module in the current program, or in any known package. |
| 14:08:33 | <tomsmeding> | boo |
| 14:08:50 | <tomsmeding> | anyway johnnyboy[m]: 'match (makeRegex "\t" :: Regex) "\t" :: Bool' gives True for me |
| 14:09:05 | <johnnyboy[m]> | I think I'm going to replace tabs with spaces and see if I can then match against `[[:space:]]` |
| 14:09:08 | <tomsmeding> | just a literal tab character is apparently valid in a regex-tdfa regex |
| 14:09:19 | <johnnyboy[m]> | just to rule out the possibility that it's the tabs that somehow mess things up |
| 14:10:10 | <[exa]> | tomsmeding: in the "pushback" direction I'd probably suggest awk :] |
| 14:11:06 | <johnnyboy[m]> | okay, it's not the tabs |
| 14:11:14 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 245 seconds) |
| 14:11:15 | <johnnyboy[m]> | my regexes are just wrong somehow |
| 14:11:31 | <tomsmeding> | cue the rest here saying you should use parser combinators :p |
| 14:11:37 | <tomsmeding> | what's your source text and what's your regex |
| 14:11:52 | → | malumore_ joins (~malumore@151.62.126.223) |
| 14:12:12 | <johnnyboy[m]> | https://gitlab.com/jllang/spin2latex/-/blob/master/testdata/success1.txt |
| 14:12:18 | <johnnyboy[m]> | that's a test file I'm using now |
| 14:12:34 | → | waleee-cl joins (uid373333@gateway/web/irccloud.com/x-mhbpgvvowjjnvcmn) |
| 14:14:01 | <johnnyboy[m]> | this is my regex: https://privatebin.net/?cea173e3eb0202b4#EJcfvuZf734KwdZUG8CBhoHfiNNj6cPH3E3M8hLs4o8u |
| 14:14:07 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 14:14:19 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 14:14:29 | <johnnyboy[m]> | so I'm looking for a number, followed by "actual memory use for states" |
| 14:14:42 | <johnnyboy[m]> | with whitespace (tab) between |
| 14:14:45 | → | rj joins (~x@gateway/tor-sasl/rj) |
| 14:15:03 | × | malumore quits (~malumore@151.62.126.223) (Ping timeout: 268 seconds) |
| 14:15:11 | <tomsmeding> | johnnyboy[m]: are you sure you're skipping the initial whitespace? i.e. aren't you missing a prefix ' *'? |
| 14:15:28 | <johnnyboy[m]> | `$ cat success1.txt | grep -E "[0-9]+.[0-9]{3}[[:space:]]+actual"` returns `0.292 actual memory usage for states` |
| 14:16:08 | <tomsmeding> | yes because 'grep' allows matching at any point in a line |
| 14:16:14 | <johnnyboy[m]> | ah |
| 14:16:22 | <tomsmeding> | oh TDFA also does; ignore |
| 14:16:24 | <johnnyboy[m]> | ok, I'll try adding an initial [[:space:]]+ |
| 14:16:31 | <johnnyboy[m]> | or [[:space:]]* |
| 14:16:41 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 14:17:10 | <tomsmeding> | it matches that line for me :p |
| 14:17:18 | <dminuoso> | Regular expressions. How to introduce long lasting bugs by carelessly bolted-on regular expressions. |
| 14:17:20 | <tomsmeding> | so your problem is outside of the regex I think |
| 14:17:51 | <johnnyboy[m]> | but I have this other regex for picking the error count |
| 14:18:11 | <johnnyboy[m]> | it works even if the line containing "errors: xxx" does start with something else |
| 14:18:27 | <tomsmeding> | regexen are like excel: computer scientists are embarrassed to admit their effectiveness |
| 14:18:33 | → | slack1256 joins (~slack1256@dvc-186-186-101-190.movil.vtr.net) |
| 14:18:36 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 258 seconds) |
| 14:18:46 | × | Iceland_jack quits (~user@95.149.219.0) (Ping timeout: 268 seconds) |
| 14:18:46 | <tdammers> | what about regexcel? |
| 14:18:48 | <tomsmeding> | johnnyboy[m]: indeed, for me your regex matches that line |
| 14:19:01 | <tomsmeding> | so I'm thinking the problem is not with the regex, but with the code that runs the regex |
| 14:19:16 | <tomsmeding> | tdammers: excel has gotten lambdas recently, surely it can also have regex |
| 14:19:17 | → | Jd007 joins (~Jd007@162.156.11.151) |
| 14:19:32 | <tomsmeding> | oh it already does |
| 14:20:42 | <tdammers> | I bet it includes an email system too |
| 14:20:50 | ski | . o O ( <https://www.microsoft.com/en-us/research/blog/lambda-the-ultimatae-excel-worksheet-function/>,<https://www.microsoft.com/en-us/research/publication/a-user-centred-approach-to-functions-in-excel/> ) |
| 14:21:04 | → | dcbdan joins (~dcbdan@c-73-76-129-120.hsd1.tx.comcast.net) |
| 14:21:09 | <johnnyboy[m]> | <tdammers "I bet it includes an email syste"> I thought that was emacs |
| 14:21:53 | <ski> | Emacs includes an editor |
| 14:23:06 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 14:23:23 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Remote host closed the connection) |
| 14:23:44 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 14:24:13 | <tomsmeding> | tdammers: you can access Outlook from VBA in any Office application, which includes Excel https://docs.microsoft.com/en-us/office/vba/outlook/Concepts/Getting-Started/automating-outlook-from-a-visual-basic-application |
| 14:25:40 | → | malumore joins (~malumore@151.62.126.223) |
| 14:26:36 | × | solvr quits (57e3c46d@87.227.196.109) (Quit: Connection closed) |
| 14:27:55 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 14:28:18 | × | borne quits (~fritjof@200116b8648ef300f7ed9fd86a2491f0.dip.versatel-1u1.de) (Ping timeout: 246 seconds) |
| 14:28:36 | → | borne joins (~fritjof@87.123.110.6) |
| 14:30:10 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 14:32:07 | <johnnyboy[m]> | doesn't adding Turing completeness to a spreadsheet processor also imply that it allows all sorts of nasty viruses etc? |
| 14:32:29 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 252 seconds) |
| 14:32:59 | × | DataComputist quits (~lumeng@50.43.26.251) (Quit: Leaving...) |
| 14:33:30 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-qybeoxhtmvdqtlff) () |
| 14:33:41 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-edqceocpkulqhglr) |
| 14:34:51 | <tomsmeding> | johnnyboy[m]: browsers with javascript have been Turing complete since ages; same question applies |
| 14:35:22 | <johnnyboy[m]> | and browsers are known to have been subject to nasty malware |
| 14:38:00 | <johnnyboy[m]> | I tried processing a one megabyte CSV file with both excel and libreoffice calc once, and both of them struggled with it |
| 14:38:11 | <johnnyboy[m]> | I guess spreadsheet programs aren't lazy |
| 14:38:16 | × | Paks quits (~paks@c-69-136-183-189.hsd1.il.comcast.net) (Ping timeout: 245 seconds) |
| 14:40:54 | → | Iceland_jack joins (~user@95.149.219.0) |
| 14:43:08 | <johnnyboy[m]> | sorry, it was around a million lines |
| 14:43:26 | <johnnyboy[m]> | the file size might have been dozens or a hundred megabytes maybe |
| 14:44:37 | × | malumore quits (~malumore@151.62.126.223) (Quit: Leaving) |
| 14:44:38 | × | malumore_ quits (~malumore@151.62.126.223) (Quit: Leaving) |
| 14:44:54 | → | malumore joins (~malumore@151.62.126.223) |
| 14:45:26 | <tomsmeding> | johnnyboy[m]: spreadsheet programs indeed have strict evaluation semantics (unless you turn off automatic evaluation, that is) |
| 14:46:00 | <tomsmeding> | and they also do far too much with their individual cells to be able to have the efficiency of a database engine, which is sometimes unfortunate |
| 14:46:04 | × | Iceland_jack quits (~user@95.149.219.0) (Read error: Connection reset by peer) |
| 14:46:07 | <ski> | i recall hearing someone describe functional programming as "a bit like spreadsheets", before i'd seen Haskell |
| 14:46:40 | <ski> | (well, i think it was specifically Haskell this person was trying to describe) |
| 14:47:19 | <johnnyboy[m]> | my first real programming project involved an NGO who used excel as a database |
| 14:47:36 | <johnnyboy[m]> | and we were supposed to write a real database application to replace it |
| 14:47:45 | <johnnyboy[m]> | but I think they still use excel |
| 14:48:03 | <johnnyboy[m]> | I can't really blame them |
| 14:48:12 | <johnnyboy[m]> | we used mongodb :P |
| 14:48:40 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 14:48:42 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 14:51:24 | → | Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 14:51:57 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 14:53:07 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 250 seconds) |
| 14:54:03 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 14:56:07 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 14:56:29 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 14:58:28 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 14:59:59 | → | DTZUZU_ joins (~DTZUZO@207.81.119.43) |
| 15:00:06 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 15:00:07 | × | ubert quits (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 15:00:24 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 15:00:42 | × | dpl_ quits (~dpl@77.121.78.163) (Ping timeout: 268 seconds) |
| 15:02:01 | × | acidjnk_new quits (~acidjnk@p200300d0c72b9579218a2a0630d85b14.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 15:02:17 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 265 seconds) |
| 15:03:44 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) |
| 15:04:04 | → | zjp joins (~zjp@66-45-138-104-dynamic.midco.net) |
| 15:06:16 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 15:07:22 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 252 seconds) |
| 15:08:51 | → | motersen joins (~motersen@gateway/tor-sasl/motersen) |
| 15:09:28 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 15:09:29 | → | ubert joins (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) |
| 15:10:38 | × | borne quits (~fritjof@87.123.110.6) (Ping timeout: 240 seconds) |
| 15:11:41 | × | peanut_ quits (~peanut_@2a02:8388:a101:2600:1aac:99fd:f87d:92f0) (Quit: Leaving) |
| 15:12:50 | × | Narinas quits (~Narinas@187-178-93-112.dynamic.axtel.net) (Read error: Connection reset by peer) |
| 15:13:12 | → | Narinas joins (~Narinas@187-178-93-112.dynamic.axtel.net) |
| 15:13:41 | × | ubert quits (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 15:13:48 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 258 seconds) |
| 15:17:06 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 15:18:02 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 246 seconds) |
| 15:19:09 | × | andreas31 quits (~andreas@gateway/tor-sasl/andreas303) (Ping timeout: 240 seconds) |
| 15:20:06 | × | geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 15:21:09 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 15:23:15 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 15:24:19 | → | Hildegunst joins (~luc@80.248.12.109.rev.sfr.net) |
| 15:24:33 | ← | Hildegunst parts (~luc@80.248.12.109.rev.sfr.net) () |
| 15:25:42 | → | ezrakilty joins (~ezrakilty@97-113-58-224.tukw.qwest.net) |
| 15:25:49 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-ykxhqtpjefqrmdft) |
| 15:25:54 | → | Hildegunst joins (~luc@80.248.12.109.rev.sfr.net) |
| 15:25:55 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 15:25:57 | → | andreas31 joins (~andreas@gateway/tor-sasl/andreas303) |
| 15:26:02 | × | Hildegunst quits (~luc@80.248.12.109.rev.sfr.net) (Client Quit) |
| 15:26:13 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 15:26:48 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Quit: WeeChat 3.0.1) |
| 15:27:27 | × | hiroaki quits (~hiroaki@2a02:8108:8c40:2bb8:1e40:f339:ac5b:717) (Ping timeout: 246 seconds) |
| 15:27:37 | × | ezrakilty quits (~ezrakilty@97-113-58-224.tukw.qwest.net) (Remote host closed the connection) |
| 15:30:11 | → | shailangsa joins (~shailangs@host86-186-136-70.range86-186.btcentralplus.com) |
| 15:30:14 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 15:30:38 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 15:30:54 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection) |
| 15:32:05 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 15:32:42 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 246 seconds) |
| 15:34:34 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 245 seconds) |
| 15:36:09 | → | borne joins (~fritjof@200116b864978000f7ed9fd86a2491f0.dip.versatel-1u1.de) |
| 15:37:22 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 15:38:08 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 15:39:42 | → | hiroaki joins (~hiroaki@2a02:8108:8c40:2bb8:3133:71df:e36c:dfbb) |
| 15:41:55 | → | supercoven joins (~Supercove@dsl-hkibng31-54fabd-233.dhcp.inet.fi) |
| 15:42:18 | × | Pickchea quits (~private@unaffiliated/pickchea) (Ping timeout: 240 seconds) |
| 15:43:56 | × | supercoven quits (~Supercove@dsl-hkibng31-54fabd-233.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 15:44:31 | × | __minoru__shirae quits (~shiraeesh@109.166.57.99) (Ping timeout: 260 seconds) |
| 15:44:56 | × | gaze__ quits (sid387101@gateway/web/irccloud.com/x-avezvxuxwafmkbvn) (Ping timeout: 245 seconds) |
| 15:45:25 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 15:45:37 | × | SrPx quits (sid108780@gateway/web/irccloud.com/x-bbnjzembhmbnppsc) (Ping timeout: 276 seconds) |
| 15:46:16 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-edqceocpkulqhglr) (Ping timeout: 276 seconds) |
| 15:46:19 | → | stree joins (~stree@68.36.8.116) |
| 15:46:55 | × | mudri quits (sid317655@gateway/web/irccloud.com/x-mxbgcmszbbzcrnwx) (Ping timeout: 276 seconds) |
| 15:47:08 | → | gaze__ joins (sid387101@gateway/web/irccloud.com/x-jyfzdgulluqjzdzf) |
| 15:47:33 | → | SrPx joins (sid108780@gateway/web/irccloud.com/x-mmboofbtgdacydlo) |
| 15:47:38 | → | kiweun joins (~kiweun@2607:fea8:2a62:9600:30e4:9f38:5ce5:23cb) |
| 15:48:06 | → | mudri joins (sid317655@gateway/web/irccloud.com/x-bcigdzdisjxobsht) |
| 15:48:21 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-kcdtjlkqhzglspxx) |
| 15:49:07 | → | ep1ctetus joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 15:49:51 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 15:50:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 15:50:30 | → | Sorny joins (~Sornaensi@077213203030.dynamic.telenor.dk) |
| 15:51:08 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 15:51:11 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 15:51:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 15:53:41 | × | Sorna quits (~Sornaensi@79.142.232.102.static.router4.bolignet.dk) (Ping timeout: 240 seconds) |
| 15:54:17 | × | enoq quits (~textual@194-208-146-143.lampert.tv) (Quit: Textual IRC Client: www.textualapp.com) |
| 15:54:18 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:55:31 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 250 seconds) |
| 15:57:22 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) |
| 15:57:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 15:57:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 15:58:05 | → | ezrakilty joins (~ezrakilty@97-113-58-224.tukw.qwest.net) |
| 15:59:41 | → | vicfred joins (vicfred@gateway/vpn/mullvad/vicfred) |
| 16:00:05 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 16:00:27 | → | Rudd0 joins (~Rudd0@185.189.115.103) |
| 16:00:37 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Remote host closed the connection) |
| 16:01:03 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 16:02:46 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 16:03:27 | → | codygman__ joins (~user@47.186.207.161) |
| 16:03:44 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:04:12 | × | xff0x quits (~xff0x@2001:1a81:5268:4b00:6095:39e:f552:2f81) (Ping timeout: 246 seconds) |
| 16:04:13 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 16:05:13 | → | xff0x joins (~xff0x@2001:1a81:5268:4b00:52c4:a3b3:40c7:ac40) |
| 16:05:46 | <Gurkenglas> | What language or language extension do I want to model types like "real numbers where a less defined than b <=> a at most b" and "1-lipschitz functions on the previous type"? |
| 16:05:48 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 16:05:54 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 16:08:12 | <xerox_> | am I completely off track wanting this? deriving instance Enum a => Enum (Maybe a |
| 16:08:26 | <xerox_> | (using StandaloneDeriving and friends) |
| 16:08:28 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 16:08:37 | × | ezrakilty quits (~ezrakilty@97-113-58-224.tukw.qwest.net) (Remote host closed the connection) |
| 16:08:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 16:09:23 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:11:37 | <[exa]> | xerox_: it's been discussed already for sure, but I don't remember the result |
| 16:12:15 | <[exa]> | uh what, hackage down? |
| 16:12:40 | <[exa]> | anyway, xerox_: Data.Enum.Deriving wouldn't work? |
| 16:13:38 | × | codygman__ quits (~user@47.186.207.161) (Ping timeout: 240 seconds) |
| 16:13:59 | <xerox_> | first time delving into (non-haskell-2010-)deriving, didn't know about that package, just trying to figure out what ghc allows me to do as is for starters |
| 16:14:41 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 16:15:38 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:16:38 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 16:17:09 | × | andreas31 quits (~andreas@gateway/tor-sasl/andreas303) (Ping timeout: 240 seconds) |
| 16:17:40 | <xerox_> | open to other ideas as well, trying to go from a newtype Foo = .. with deriving Enum to data Bar = Other | Foo and get that extra "Other" snuck in there into Enum |
| 16:18:00 | <dexterfoo> | hello when will hackage docs be back online? |
| 16:18:36 | <xerox_> | I guess in the meanwhile one can use stackage.org |
| 16:18:41 | <xerox_> | I often default to that one anyway |
| 16:18:48 | → | andreas31 joins (~andreas@gateway/tor-sasl/andreas303) |
| 16:19:48 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:30e4:9f38:5ce5:23cb) (Remote host closed the connection) |
| 16:20:16 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 16:20:18 | × | zjp quits (~zjp@66-45-138-104-dynamic.midco.net) (Remote host closed the connection) |
| 16:20:52 | → | kiweun joins (~kiweun@2607:fea8:2a62:9600:bd23:b03d:cd6e:b210) |
| 16:20:54 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 16:21:51 | → | cake_eater joins (~kiweun@2607:fea8:2a62:9600:b1d8:81d4:b440:7736) |
| 16:23:19 | → | blackriversoftwa joins (sid364914@gateway/web/irccloud.com/x-elfvrucbyuzljosj) |
| 16:23:21 | × | conal quits (~conal@107.181.166.205) (Quit: Computer has gone to sleep.) |
| 16:24:00 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 16:25:25 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:bd23:b03d:cd6e:b210) (Ping timeout: 252 seconds) |
| 16:25:49 | → | conal joins (~conal@64.71.133.70) |
| 16:26:03 | × | [exa] quits (exa@srv3.blesmrt.net) (Changing host) |
| 16:26:03 | → | [exa] joins (exa@unaffiliated/exa/x-5381537) |
| 16:26:14 | × | cake_eater quits (~kiweun@2607:fea8:2a62:9600:b1d8:81d4:b440:7736) (Ping timeout: 245 seconds) |
| 16:26:24 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 16:27:35 | → | codygman__ joins (~user@209.251.131.98) |
| 16:28:23 | <slack1256> | Gurkenglas: you probably want agda by then |
| 16:28:33 | <slack1256> | Computable real numbers and all that jazz |
| 16:29:36 | × | haritz quits (~hrtz@unaffiliated/haritz) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 16:30:26 | <slack1256> | dexterfoo: If you have a local copy of the libraries you want documentation of, you can see where those html are with the command `ghc-pkg field <package> haddock-html`. |
| 16:31:28 | <statusbot> | Status update: Due to a disk space issue the hackage web interface is down for a storage upgrade. -- http://status.haskell.org/pages/incident/537c07b0cf1fad5830000093/606200df2a84ed05341dcbf1 |
| 16:32:09 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 16:32:54 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 16:33:00 | × | jonathanx_ quits (~jonathan@94.234.49.69) (Read error: Connection reset by peer) |
| 16:33:11 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 16:35:24 | <Gurkenglas> | slack1256, not quite computable real numbers. I mean a type where each element corresponds to a real number and the definedness relation (in the sense that undefined is less defined than "asd") corresponds to the usual order on real numbers |
| 16:35:30 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 16:36:05 | <Gurkenglas> | (i mean, i can kinda make one: newtype Real = UnsafeReal {greaterThan :: Double -> ()}; embedDouble :: Double -> Real; embedDouble d = UnsafeReal (\d' -> if d>d' then () else error ("embedDouble" + show d + show d')) -- but it's not type safe) |
| 16:36:39 | × | borne quits (~fritjof@200116b864978000f7ed9fd86a2491f0.dip.versatel-1u1.de) (Ping timeout: 245 seconds) |
| 16:39:24 | × | codygman__ quits (~user@209.251.131.98) (Remote host closed the connection) |
| 16:39:46 | → | codygman__ joins (~user@209.251.131.98) |
| 16:40:52 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Disconnected: Replaced by new connection") |
| 16:40:52 | × | ph88^ quits (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 16:40:57 | <dolio> | That description isn't real numbers, just like the other description wasn't natural numbers. |
| 16:41:02 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 16:41:14 | × | z0k quits (~user@115.186.169.1) (Quit: WeeChat 3.0) |
| 16:41:15 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 16:41:21 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 16:41:57 | <dolio> | Also the usual ordering on the reals doesn't have a bottom to be a domain. |
| 16:42:20 | → | ubert joins (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) |
| 16:42:58 | <dolio> | It's also not directed complete, I think. |
| 16:43:18 | <Gurkenglas> | dolio, yeah add -inf and inf |
| 16:43:24 | × | Tene quits (~tene@poipu/supporter/slacker/tene) (Ping timeout: 246 seconds) |
| 16:44:06 | × | ByronJohnson quits (~bairyn@unaffiliated/bob0) (Ping timeout: 246 seconds) |
| 16:44:17 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 16:45:56 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 16:46:10 | <sclv> | psa btw, hackage web interface is down while we fix disk storage issues |
| 16:46:18 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 260 seconds) |
| 16:46:21 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Client Quit) |
| 16:46:32 | <Gurkenglas> | do dependent types get me "that subtype of A defined by the property f : A -> Bool"? (or perhaps A -> ()) |
| 16:47:23 | × | zaquest quits (~notzaques@5.128.210.178) (Read error: Connection reset by peer) |
| 16:47:45 | → | LKoen joins (~LKoen@65.250.88.92.rev.sfr.net) |
| 16:47:49 | → | zaquest joins (~notzaques@5.128.210.178) |
| 16:47:52 | → | CrazyPython joins (~crazypyth@98.122.164.118) |
| 16:50:25 | <dolio> | A -> () is isomorphic to () in most dependently typed languages. |
| 16:50:57 | → | jonathanx_ joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 16:52:26 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Remote host closed the connection) |
| 16:52:44 | <dolio> | The Sierpinski type would need to be defined instead. |
| 16:52:55 | × | jonathanx_ quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Remote host closed the connection) |
| 16:53:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:53:49 | ← | justsomeguy parts (~justsomeg@unaffiliated/--/x-3805311) ("WeeChat 3.0.1") |
| 16:53:52 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 16:54:13 | → | jonathanx joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 16:54:30 | <dolio> | Or a Sierpinski type, since there wouldn't be a unique choice in a lot of cases. |
| 16:55:08 | → | ByronJohnson joins (~bairyn@unaffiliated/bob0) |
| 16:55:25 | → | Tene joins (~tene@mail.digitalkingdom.org) |
| 16:55:25 | × | Tene quits (~tene@mail.digitalkingdom.org) (Changing host) |
| 16:55:25 | → | Tene joins (~tene@poipu/supporter/slacker/tene) |
| 16:56:38 | × | ukari quits (~ukari@unaffiliated/ukari) (Ping timeout: 240 seconds) |
| 16:58:27 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 16:58:36 | × | evanjs quits (~evanjs@075-129-098-007.res.spectrum.com) (Ping timeout: 260 seconds) |
| 16:58:38 | → | pupuupup joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 17:03:02 | → | average joins (uid473595@gateway/web/irccloud.com/x-tblkdtktwteghrni) |
| 17:03:24 | × | codygman__ quits (~user@209.251.131.98) (Remote host closed the connection) |
| 17:03:28 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 17:03:35 | ski | . o O ( "First Steps in Synthetic Computability Theory" by Andrej Bauer in 2004 at <http://math.andrej.com/2005/05/08/first-steps-in-synthetic-computability-theory/> ) |
| 17:03:51 | → | gitgood joins (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) |
| 17:03:57 | → | codygman__ joins (~user@209.251.131.98) |
| 17:06:52 | <monochrom> | I think when you wrote "A -> ()" you had "relation between A and ()" in mind. |
| 17:06:56 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 17:07:32 | <monochrom> | Because I recently used that in parametricity theorems to obtain induction/elimination principles. :) |
| 17:08:06 | × | pupuupup quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 240 seconds) |
| 17:09:29 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 17:10:10 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 17:12:10 | → | Erutuon_ joins (~Erutuon@97-116-16-233.mpls.qwest.net) |
| 17:12:39 | × | DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 268 seconds) |
| 17:12:54 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 17:12:56 | × | chele quits (~chele@ip5b40237d.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 17:13:32 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 17:14:52 | → | pupuupup_ joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 17:14:59 | × | knupfer quits (~Thunderbi@200116b82b0bfe00e407e369ad43ca6f.dip.versatel-1u1.de) (Ping timeout: 245 seconds) |
| 17:17:13 | <dolio> | Well, you don't just want any relation. |
| 17:17:31 | <dolio> | Because that is A -> Ω. |
| 17:17:36 | <dolio> | Not A -> Σ |
| 17:17:37 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 258 seconds) |
| 17:19:57 | <dolio> | You can kind of pretend that () is Σ in some ways in something like Haskell, although there is no good encoding of the other truth value types. |
| 17:20:29 | <dolio> | At least, I think. |
| 17:21:27 | × | lawid quits (~quassel@dslb-090-186-122-181.090.186.pools.vodafone-ip.de) (Quit: lawid) |
| 17:22:19 | × | astronavt quits (~astronavt@unaffiliated/astronavt) (Remote host closed the connection) |
| 17:23:21 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 17:25:39 | × | Jesin quits (~Jesin@pool-72-66-101-18.washdc.fios.verizon.net) (Quit: Leaving) |
| 17:26:31 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 17:26:46 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 17:27:55 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 17:29:11 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 17:30:38 | × | __minoru__shirae quits (~shiraeesh@109.166.57.99) (Ping timeout: 240 seconds) |
| 17:30:49 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 245 seconds) |
| 17:31:21 | × | gentauro quits (~gentauro@unaffiliated/gentauro) (Read error: Connection reset by peer) |
| 17:31:43 | → | gentauro joins (~gentauro@unaffiliated/gentauro) |
| 17:33:09 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds) |
| 17:34:19 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 17:37:18 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 17:38:06 | × | pupuupup_ quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 260 seconds) |
| 17:39:22 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 276 seconds) |
| 17:39:43 | → | nuncanada joins (~dude@179.235.160.168) |
| 17:40:12 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:44:28 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 17:44:38 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 17:44:54 | → | pupuupup_ joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 17:46:00 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 17:47:11 | × | ixlun quits (~matthew@109.249.184.133) (Ping timeout: 240 seconds) |
| 17:49:12 | × | pupuupup_ quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 246 seconds) |
| 17:49:23 | × | ubert quits (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 17:49:30 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 17:49:35 | → | dandart joins (~Thunderbi@home.dandart.co.uk) |
| 17:49:49 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 17:50:02 | × | geekosaur quits (82650c7a@130.101.12.122) (Ping timeout: 240 seconds) |
| 17:51:46 | × | dandart quits (~Thunderbi@home.dandart.co.uk) (Client Quit) |
| 17:52:23 | × | vicfred quits (vicfred@gateway/vpn/mullvad/vicfred) (Quit: Leaving) |
| 17:52:27 | → | dmoerner joins (~dmoerner@fedora/dmoerner) |
| 17:52:58 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Ping timeout: 240 seconds) |
| 17:53:24 | <dmoerner> | hackage is down, I guess |
| 17:53:45 | <tomsmeding> | dmoerner: disk space issues, it's being worked on |
| 17:53:58 | <tdammers> | talk about spofs... |
| 17:54:23 | <dmoerner> | tomsmeding: no problem. |
| 17:54:26 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 260 seconds) |
| 17:54:26 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 240 seconds) |
| 17:54:47 | <tomsmeding> | Does haskell have some kind of "injective type classes"? In particular, given 'instance C b => C (a, b)' and the information 'C (a, b)', I'd like to be able to infer 'C b', but GHC can't |
| 17:55:01 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 17:55:14 | <Gurkenglas> | monochrom, by A -> () I mean the monotonic functions from A to (), not necessarily strict, one-to-one with the Scott-open sets in A |
| 17:55:34 | <tomsmeding> | (my actual use case has 'a -> b' instead of '(a, b)', but I can't imagine that to make a difference) |
| 17:55:38 | → | sgibber2018 joins (d055ed90@208.85.237.144) |
| 17:59:22 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 18:00:19 | × | xourt quits (d4c620ea@212-198-32-234.rev.numericable.fr) (Quit: Connection closed) |
| 18:00:21 | ← | drakonis parts (~drakonis@unaffiliated/drakonis) ("WeeChat 3.1") |
| 18:01:25 | <infinisil> | I have a GADT like `data Method i o where IsRoot :: Method Int Bool GetName :: Method Int String` |
| 18:02:40 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 18:03:00 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:b98b:75b0:1d5d:7be4) |
| 18:03:05 | <infinisil> | Now I want to be able to have a `Show` instance for something like `ReqResp (Method i o) i o` |
| 18:03:28 | <infinisil> | data ReqResp i o = ReqResp (Method i o) i o |
| 18:03:32 | → | pupuupup_ joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 18:04:36 | <tomsmeding> | infinisil: use StandaloneDeriving, write 'deriving instance Show (Method i o)', and attach 'deriving (Show)' to ReqResp? |
| 18:04:39 | <infinisil> | Now I can't just `derive Show`, but that gives me an `instance (Show i, Show o) => Show (ReqResp i o)` |
| 18:04:44 | <infinisil> | s/can't/can |
| 18:06:39 | <infinisil> | I want an instance like `Show (ReqResp i o)`, without any dependent constraints |
| 18:06:39 | <tomsmeding> | infinisil: I don't think you can derive an unconstrained Show instance for ReqResp automatically |
| 18:06:46 | <infinisil> | Hmm |
| 18:07:08 | <infinisil> | Yeah currently I'm doing it manually. My question indeed would've been how that could be automated |
| 18:07:08 | → | electricityZZZZ joins (~electrici@135-180-3-82.static.sonic.net) |
| 18:07:36 | <Gurkenglas> | tomsmeding, isn't the following absence of overlapping instances just the injective type classes you want? |
| 18:07:39 | <Gurkenglas> | @let class Gurk a; instance Gurk Int; instance Gurk b => Gurk (a -> b) |
| 18:07:41 | <lambdabot> | Defined. |
| 18:07:43 | → | stree joins (~stree@68.36.8.116) |
| 18:07:48 | <tomsmeding> | infinisil: well you could do it using generics but not sure whether that's better :p |
| 18:07:57 | <Gurkenglas> | :t undefined :: Gurk (String -> Char) => () |
| 18:07:59 | <lambdabot> | error: |
| 18:07:59 | <lambdabot> | No instance for (Gurk Char) |
| 18:07:59 | <lambdabot> | arising from an expression type signature |
| 18:08:08 | <Gurkenglas> | As you see, it looked directly for the Gurk Char instance |
| 18:08:14 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 18:08:40 | ← | dmoerner parts (~dmoerner@fedora/dmoerner) ("WeeChat 1.9.1") |
| 18:08:41 | <tomsmeding> | :t undefined :: Gurk (a -> b) => () |
| 18:08:43 | <lambdabot> | error: |
| 18:08:43 | <lambdabot> | • Overlapping instances for Gurk (a0 -> b0) |
| 18:08:43 | <lambdabot> | Matching givens (or their superclasses): |
| 18:08:48 | <tomsmeding> | that's the problem |
| 18:09:00 | <tomsmeding> | wait what, why overlappign |
| 18:09:14 | <tomsmeding> | anyway that doesn't work :p |
| 18:09:33 | <Gurkenglas> | @let class Gurk2 a; instance Gurk2 b => Gurk2 (a -> b) |
| 18:09:35 | <lambdabot> | Defined. |
| 18:09:43 | <Gurkenglas> | :t undefined :: Gurk2 (a -> b) => () |
| 18:09:44 | <lambdabot> | error: |
| 18:09:44 | <lambdabot> | • Overlapping instances for Gurk2 (a0 -> b0) |
| 18:09:44 | <lambdabot> | Matching givens (or their superclasses): |
| 18:09:49 | <Gurkenglas> | ruh roh |
| 18:10:18 | × | gitgood quits (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) (Remote host closed the connection) |
| 18:10:29 | → | DTZUZU_ joins (~DTZUZO@207.81.119.43) |
| 18:10:36 | <tomsmeding> | wait now I can't reproduce it locally, let me have a look |
| 18:11:38 | <Gurkenglas> | @let class Gurk4 a; instance Gurk4 (a -> b) |
| 18:11:39 | <lambdabot> | Defined. |
| 18:11:41 | <tomsmeding> | okay apparently the introduction of GADTs complicates the matter |
| 18:11:47 | <Gurkenglas> | :t undefined :: Gurk4 (a -> b) => () |
| 18:11:48 | <lambdabot> | error: |
| 18:11:48 | <lambdabot> | • Overlapping instances for Gurk4 (a0 -> b0) |
| 18:11:48 | <lambdabot> | Matching givens (or their superclasses): |
| 18:11:50 | <Gurkenglas> | RUH ROH |
| 18:12:12 | <tomsmeding> | @let data Thing a where Tup :: a -> b -> Thing (a -> b) |
| 18:12:14 | <lambdabot> | Defined. |
| 18:12:28 | <tomsmeding> | @let foo :: Gurk4 a => a -> Int ; foo = undefined |
| 18:12:29 | <lambdabot> | Defined. |
| 18:12:41 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 246 seconds) |
| 18:12:43 | <tomsmeding> | @let bar :: Gurk4 a => Thing a -> Int ; bar (Tup x y) = foo y |
| 18:12:44 | <lambdabot> | .L.hs:174:17: error: |
| 18:12:45 | <lambdabot> | • Could not deduce (Gurk4 b) arising from a use of ‘foo’ |
| 18:12:45 | <lambdabot> | from the context: Gurk4 a |
| 18:13:02 | <tomsmeding> | this is the exact issue I'm talking about, not sure what the "overlapping instances" is about |
| 18:14:20 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 18:14:36 | <infinisil> | Maybe I could derive a Show instance automatically for |
| 18:14:38 | <infinisil> | data ReqResp m = forall i o. m ~ Method i o => ReqResp m i o |
| 18:14:50 | <infinisil> | Something with QuantifiedConstraints |
| 18:16:08 | <infinisil> | Or maybe for |
| 18:16:10 | <infinisil> | data ReqResp (m :: Method i o) = ReqResp i o |
| 18:16:44 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 18:16:49 | <infinisil> | That kinda works |
| 18:16:51 | × | shailangsa quits (~shailangs@host86-186-136-70.range86-186.btcentralplus.com) (Ping timeout: 246 seconds) |
| 18:16:53 | <infinisil> | deriving instance Show (ReqResp 'IsRoot) |
| 18:16:59 | <infinisil> | deriving instance Show (ReqResp 'GetName) |
| 18:17:11 | <infinisil> | The method is lifted to the type level, but maybe that's fine for me |
| 18:17:13 | × | rajivr quits (uid269651@gateway/web/irccloud.com/x-nlktifqfsuwtyuzw) (Quit: Connection closed for inactivity) |
| 18:17:17 | <tomsmeding> | infinisil: the problem is that if the Method is on the value level, you need to explicitly pattern match on it to obtain the Show dictionaries |
| 18:17:37 | <tomsmeding> | in fact, at runtime, that's _necessary_, because otherwise the runtime doesn't know what 'show' method to call |
| 18:17:55 | <infinisil> | Yeah, but it could theoretically be derived automatically still |
| 18:20:26 | <Gurkenglas> | dolio, what do you mean by Σ? I can find Ω on https://ncatlab.org/nlab/show/truth+value but not Σ |
| 18:27:50 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 18:30:41 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 18:31:04 | → | dpl_ joins (~dpl@77.121.78.163) |
| 18:31:22 | <tomsmeding> | Gurkenglas: I believe the "overlapping instances" error is a side effect of writing a context mentioning variables 'a', 'b', without the constrained type (here '()') also mentioning them |
| 18:31:33 | → | gitgood joins (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) |
| 18:32:56 | × | kuribas quits (~user@ptr-25vy0i9nyhjns61vpxg.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 18:33:03 | <infinisil> | I want to write `makeRequest :: forall (method :: Method i o) i o. ...` |
| 18:33:21 | <infinisil> | So that I can e.g. do `makeRequest @IsRoot` |
| 18:33:37 | <infinisil> | But this doesn't work, because `i` and `o` aren't in scope when `method` is defined |
| 18:33:57 | <infinisil> | And if I do `forall i o (method :: Method i o)`, I won't be able to do `makeRequest @IsRoot` |
| 18:34:05 | <infinisil> | Is there a solution for this? |
| 18:34:17 | <dolio> | Gurkenglas: Σ is the Sierpinski space. |
| 18:34:21 | <Gurkenglas> | dolio, can't one see () as Ω? One need merely admit that () is the terminal object, and then true: * -> Ω is id, and every (mono)morphism m: U -> X is the pullback of true and (\x:X -> if x is above m ⊥ then () else ⊥), yes? |
| 18:34:51 | → | knupfer joins (~Thunderbi@dynamic-046-114-145-192.46.114.pool.telefonica.de) |
| 18:36:00 | <dolio> | If () is Ω then it isn't also the terminal object. |
| 18:36:29 | <tomsmeding> | infinisil: makeRequest @_ @_ @IsRoot, or do `makeRequest :: Proxy (Method i o) -> ...` and write `makeRequest (Proxy @IsRoot) ...` |
| 18:36:57 | <infinisil> | Yeah that's a workaround, but I wonder if `makeRequest @IsRoot` can be made to work |
| 18:37:15 | <infinisil> | Seems so simple |
| 18:37:45 | <dolio> | Anyhow, domain theory is not the right setting for having these kind of distinctions, I think. |
| 18:37:53 | <ski> | @where topology |
| 18:37:53 | <lambdabot> | "topology in Haskell" <http://www.haskell.org/pipermail/haskell/2004-June/014134.html> and "Synthetic topology of data types and classical spaces" <http://www.cs.bham.ac.uk/~mhe/papers/entcs87.(pdf| |
| 18:37:53 | <lambdabot> | dvi|ps)> by Mart�n Escard� |
| 18:37:54 | × | stree quits (~stree@68.36.8.116) (Quit: Caught exception) |
| 18:37:59 | <ski> | Gurkenglas ^ |
| 18:38:01 | <ski> | also |
| 18:38:02 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Read error: Connection reset by peer) |
| 18:38:05 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Remote host closed the connection) |
| 18:38:06 | <ski> | @where impossible |
| 18:38:06 | <lambdabot> | <http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/>,<http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/> |
| 18:38:21 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 18:38:23 | → | stree joins (~stree@68.36.8.116) |
| 18:38:28 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 18:38:48 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 18:39:16 | → | pera joins (~pera@unaffiliated/pera) |
| 18:39:29 | <ski> | Gurkenglas : and the paper by Andrej Bauer i linked to, one and a half hour ago |
| 18:41:27 | <dolio> | Anyhow, there are many sorts of truth values computably. There is 2, for decidable truth, Σ for semi-decidable truth, and Ω for provable truth. |
| 18:41:43 | × | darjeeling_ quits (~darjeelin@115.215.42.89) (Ping timeout: 265 seconds) |
| 18:42:02 | <dolio> | Also perhaps ∇Ω for classical truth. |
| 18:42:38 | <infinisil> | Okay I'm bringing out the big guns, type families |
| 18:42:50 | <infinisil> | data Method = IsRoot | GetName |
| 18:43:17 | <infinisil> | type family MethodInput (m :: Method) where MethodInput IsRoot = Int MethodInput GetName = Int |
| 18:43:23 | <infinisil> | Similarly for MethodOutput |
| 18:43:26 | × | ystael quits (~ystael@209.6.50.55) (Ping timeout: 240 seconds) |
| 18:43:29 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 18:43:34 | <dolio> | Domain theoretic semantics of something like Haskell allow you to encode some of the Σ part as procedures, but it doesn't have a good story for the rest. |
| 18:43:36 | <infinisil> | This feels like a step in the right direction |
| 18:43:39 | <infinisil> | tomsmeding: ^ |
| 18:43:41 | <ski> | "How many is two?" by ibid in 2005-05-16 at <http://math.andrej.com/2005/05/16/how-many-is-two/> could also be interesting, yea |
| 18:43:58 | × | pera quits (~pera@unaffiliated/pera) (Ping timeout: 240 seconds) |
| 18:45:36 | × | slack1256 quits (~slack1256@dvc-186-186-101-190.movil.vtr.net) (Remote host closed the connection) |
| 18:47:50 | → | shailangsa joins (~shailangs@host86-186-196-238.range86-186.btcentralplus.com) |
| 18:48:07 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood) |
| 18:49:28 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 18:49:47 | <tomsmeding> | infinisil: if it works, it works, but I don't see yet how to get the Show constraints in the right place that way; but I haven't thought about it much either :) |
| 18:51:56 | → | Guest29 joins (~textual@109.246.40.24) |
| 18:53:47 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 18:54:07 | <monochrom> | ski: There is a Chinese novel that has this plot point of how a villain aquitted himself of a promise of "I won't tell this secret to the 5th person". So eventually he told the secret to a conference of a hundred people, and defended with "can you point out who's the 5th person?" >:) |
| 18:54:34 | → | darjeeling_ joins (~darjeelin@122.245.122.120) |
| 18:54:52 | <ski> | hm |
| 18:55:08 | <monochrom> | (The number was 5 because initially this was a secret among 4 persons.) |
| 18:55:27 | <ski> | i see |
| 18:55:28 | × | atk quits (~Arch-TK@ircpuzzles/staff/Arch-TK) (Quit: Well this is unexpected.) |
| 18:56:16 | <monochrom> | Conclusion: Intuitionistic constructivist logics are the root of all evil. >:) |
| 18:56:30 | <ski> | slightly apropos, i always found it weird, how apparently, at least in some jurisdictions, two people who've helped each other to commit a crime, can both be acquitted by the court, on the grounds that it can't be determined "who held the knife" (or whatever) |
| 18:57:07 | → | ph88 joins (~ph88@2a02:8109:9e00:7e5c:4080:7dc1:315d:729) |
| 18:57:12 | <justsomeguy> | It seems like hackage is down. Is there a way for me to generate local documentation for QuickCheck with stack? |
| 18:57:42 | <ski> | it always seemed to me that, at least in common cases, it ought to be possible to charge and convict both of them of commiting either of the two deeds, and, serving out the greatest lower bound of the two associated penances, to both of them |
| 18:58:24 | → | ByteEater joins (57cd846a@gateway/web/cgi-irc/kiwiirc.com/ip.87.205.132.106) |
| 18:58:28 | <ski> | hehe, monochrom ;) |
| 18:59:13 | <monochrom> | Generally it looks like that if you put the burden of proof on one side you are bound to have this kind of asymmetries. |
| 19:00:08 | <dolio> | You can easily well-order finite sets, though. :) |
| 19:00:14 | → | atk joins (~Arch-TK@ircpuzzles/staff/Arch-TK) |
| 19:00:20 | <dolio> | Even intuitionistically. |
| 19:02:49 | <ski> | monochrom : iow, not "Either you committed this crime, or you committed that crime." but rather "You committed either this crime or that crime.". convicting both of them for the disjunction of the crimes |
| 19:03:15 | <monochrom> | The story was set in 11th century China, and the conference was of the martial art community. So unfortunately most of them were easily bluffed by these logical subtleties, apart from a few exceptional smartass villains. |
| 19:03:37 | <justsomeguy> | Seems that ''stack haddock'' was able to generate the html docs I was after. |
| 19:03:48 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 19:05:03 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Quit: WeeChat 3.0.1) |
| 19:05:35 | <monochrom> | ski: Hey, how about this idea: Order the formation of a company of those two persons. Now there is just one legal person, the company, to convict. Then the sole two shareholders take the common punishment. |
| 19:06:21 | <monochrom> | "homotopic criminal theory" >:) |
| 19:07:24 | <ski> | monochrom : hm. around when was it written ? |
| 19:07:41 | <monochrom> | 1960s or 1970s. |
| 19:07:49 | <ski> | monochrom : hehe :) .. could a court really order such a formation ? |
| 19:07:50 | <ski> | okay |
| 19:08:18 | <ski> | (also, wouldn't that legal person have had to existed, at the time in question for the deed ?) |
| 19:08:35 | → | ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 19:08:52 | <monochrom> | Just another cunning plan from monochrom that doesn't really work in practice. :) |
| 19:09:52 | → | ystael joins (~ystael@141.sub-174-242-80.myvzw.com) |
| 19:10:05 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Remote host closed the connection) |
| 19:10:24 | × | Erutuon_ quits (~Erutuon@97-116-16-233.mpls.qwest.net) (Ping timeout: 246 seconds) |
| 19:12:37 | → | Erutuon_ joins (~Erutuon@97-116-16-233.mpls.qwest.net) |
| 19:13:43 | ski | . o O ( "I have a cunning plan" <https://www.youtube.com/watch?v=AsXKS8Nyu8Q> ) |
| 19:15:32 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) (Remote host closed the connection) |
| 19:17:33 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 19:19:13 | → | sorki joins (~sorki@gateway/tor-sasl/sorki) |
| 19:19:33 | → | hacxman joins (~hexo@gateway/tor-sasl/hexo) |
| 19:19:57 | × | srk quits (~sorki@gateway/tor-sasl/sorki) (Ping timeout: 240 seconds) |
| 19:19:57 | × | hexo quits (~hexo@gateway/tor-sasl/hexo) (Ping timeout: 240 seconds) |
| 19:19:58 | hacxman | is now known as hexo |
| 19:20:17 | → | woffs joins (3cd46299b2@woffs.de) |
| 19:20:25 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 19:20:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds) |
| 19:21:02 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 19:21:38 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 19:21:59 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 19:22:08 | <wz1000> | is there any nice way to define folds with unboxed result types? |
| 19:22:16 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 19:22:23 | sorki | is now known as srk |
| 19:22:26 | <wz1000> | I want something like `foldl :: forall r a (b :: TYPE r). (b -> a -> b) -> b -> [a] -> b` |
| 19:22:34 | ← | woffs parts (3cd46299b2@woffs.de) () |
| 19:22:57 | <wz1000> | s/unboxed result types/levity polymorphic result types/g |
| 19:24:12 | <wz1000> | This is my best attempt so far: https://gist.github.com/wz1000/2dee93d3b07825d1ae43cf43012adcc0 |
| 19:24:44 | <wz1000> | it works fine for "simple" RuntimeReps, but breaks down for anything more compilicated involving unboxed tuples/sums etc. |
| 19:25:02 | <wz1000> | edwardk maybe? |
| 19:27:11 | × | michalz quits (~user@185.246.204.46) (Ping timeout: 240 seconds) |
| 19:27:26 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 19:33:51 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 19:34:07 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.1) |
| 19:39:05 | × | electricityZZZZ quits (~electrici@135-180-3-82.static.sonic.net) (Quit: Leaving) |
| 19:39:35 | <ph88> | is there any way to grab the data constructor functions from a data type ? |
| 19:40:40 | → | andrew2 joins (602a442a@gateway/web/cgi-irc/kiwiirc.com/ip.96.42.68.42) |
| 19:42:31 | → | Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 19:42:58 | × | Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 240 seconds) |
| 19:43:44 | × | Natch quits (~Natch@c-b471e255.014-297-73746f25.bbcust.telenor.se) (Remote host closed the connection) |
| 19:43:50 | <maerwald> | with generics? |
| 19:44:05 | → | raichoo joins (~raichoo@dslb-188-109-062-207.188.109.pools.vodafone-ip.de) |
| 19:44:17 | <ph88> | ye ? |
| 19:44:26 | <maerwald> | yeah |
| 19:44:54 | <ph88> | oki thank you |
| 19:45:35 | Lord_of_Life_ | is now known as Lord_of_Life |
| 19:45:53 | → | lawid joins (~quassel@dslb-090-186-122-181.090.186.pools.vodafone-ip.de) |
| 19:46:32 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 19:48:15 | × | knupfer quits (~Thunderbi@dynamic-046-114-145-192.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 19:50:20 | × | andrew2 quits (602a442a@gateway/web/cgi-irc/kiwiirc.com/ip.96.42.68.42) (Quit: Connection closed) |
| 19:50:57 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 258 seconds) |
| 19:52:57 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 19:59:30 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Remote host closed the connection) |
| 20:00:25 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 20:01:03 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 20:01:57 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 20:02:56 | → | aarvar joins (~foewfoiew@2601:602:a080:fa0:b1a9:3010:b3b8:f76d) |
| 20:04:11 | × | jjhoo quits (jahakala@dsl-trebng21-b048b5-171.dhcp.inet.fi) (Remote host closed the connection) |
| 20:05:00 | × | petersen quits (~petersen@redhat/juhp) (Ping timeout: 246 seconds) |
| 20:07:06 | × | pupuupup_ quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 246 seconds) |
| 20:07:30 | → | petersen joins (~petersen@redhat/juhp) |
| 20:08:58 | → | solidus-river joins (~mike@174.127.249.180) |
| 20:10:48 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:11:47 | × | ByteEater quits (57cd846a@gateway/web/cgi-irc/kiwiirc.com/ip.87.205.132.106) (Quit: Connection closed) |
| 20:12:30 | <mpickering> | lyxia: Do you know of a "bind-like" operation for profunctors? Perhaps something like `p a b -> (b -> p c d) -> p (a, c) d` |
| 20:12:54 | <mpickering> | I want the structure to be able to depend on the result of the first computation |
| 20:13:08 | <mpickering> | but not sure how to generalise to the in/out parameters |
| 20:14:01 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 20:16:37 | × | ystael quits (~ystael@141.sub-174-242-80.myvzw.com) (Read error: Connection reset by peer) |
| 20:17:00 | <mpickering> | I suppose you could just have `(p a) b -> (b -> (p a) c) -> (p a) c` |
| 20:18:03 | → | jjhoo joins (jahakala@dsl-trebng21-b048b5-171.dhcp.inet.fi) |
| 20:20:10 | <koz_> | :t foldl' |
| 20:20:11 | <lambdabot> | Foldable t => (b -> a -> b) -> b -> t a -> b |
| 20:21:18 | → | Natch joins (~natch@c-b471e255.014-297-73746f25.bbcust.telenor.se) |
| 20:24:00 | <joel135> | (p a) is a monad that depends contravariantly on a ? |
| 20:25:45 | × | nuncanada quits (~dude@179.235.160.168) (Read error: Connection reset by peer) |
| 20:26:10 | × | csadilek quits (~csadilek@178.239.168.171) (Remote host closed the connection) |
| 20:28:22 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:29:51 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) (Remote host closed the connection) |
| 20:30:11 | → | codygman` joins (~user@47.186.207.161) |
| 20:30:34 | → | mach1speed joins (~textual@S0106f0b4d2c39cee.va.shawcable.net) |
| 20:31:37 | × | marinelli quits (~marinelli@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 20:32:06 | × | geekosaur quits (82650c7a@130.101.12.122) (Quit: Connection closed) |
| 20:32:10 | × | codygman__ quits (~user@209.251.131.98) (Ping timeout: 260 seconds) |
| 20:32:10 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 20:36:28 | × | raichoo quits (~raichoo@dslb-188-109-062-207.188.109.pools.vodafone-ip.de) (Quit: Lost terminal) |
| 20:36:39 | → | viluon joins (uid453725@gateway/web/irccloud.com/x-retpginqhscxyaoj) |
| 20:37:01 | → | Sornaensis joins (~Sornaensi@79.142.232.102.static.router4.bolignet.dk) |
| 20:39:26 | × | Sorny quits (~Sornaensi@077213203030.dynamic.telenor.dk) (Ping timeout: 240 seconds) |
| 20:41:33 | → | kenran joins (~kenran@i59F67B6E.versanet.de) |
| 20:41:37 | × | Pickchea quits (~private@unaffiliated/pickchea) (Quit: Leaving) |
| 20:42:19 | × | mach1speed quits (~textual@S0106f0b4d2c39cee.va.shawcable.net) (Ping timeout: 268 seconds) |
| 20:44:39 | → | mach1speed joins (~textual@S0106f0b4d2c39cee.va.shawcable.net) |
| 20:44:56 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 20:45:06 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 20:46:18 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 240 seconds) |
| 20:46:55 | × | mach1speed quits (~textual@S0106f0b4d2c39cee.va.shawcable.net) (Client Quit) |
| 20:48:08 | → | nuncanada joins (~dude@179.235.160.168) |
| 20:50:08 | × | Natch quits (~natch@c-b471e255.014-297-73746f25.bbcust.telenor.se) (Read error: Connection reset by peer) |
| 20:50:36 | × | aarvar quits (~foewfoiew@2601:602:a080:fa0:b1a9:3010:b3b8:f76d) (Quit: Leaving.) |
| 20:53:43 | → | aarvar joins (~foewfoiew@2601:602:a080:fa0:e872:21d9:dd64:69e7) |
| 20:53:43 | → | Natch joins (~natch@c-b471e255.014-297-73746f25.bbcust.telenor.se) |
| 20:54:49 | <lyxia> | mpickering: indeed, that's also what I do in my paper and you can derive a thing with your former bind-like type from it. |
| 20:56:29 | × | coot quits (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 20:57:01 | × | Guest29 quits (~textual@109.246.40.24) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 20:59:39 | → | stree joins (~stree@68.36.8.116) |
| 20:59:59 | × | outerpassage_ quits (outerpassa@2600:3c01::f03c:92ff:fed1:4643) (Quit: quitting) |
| 21:00:14 | → | outerpassage joins (~outerpass@li1196-30.members.linode.com) |
| 21:00:32 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:b98b:75b0:1d5d:7be4) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 21:02:32 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving) |
| 21:03:53 | → | aplainze1akind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 21:04:16 | × | mflux quits (flux@2001:708:310:3430:4506:8c48:1ba0:18ff) (Ping timeout: 240 seconds) |
| 21:04:23 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 21:05:09 | → | flx_ joins (flux@coffee.modeemi.fi) |
| 21:05:11 | → | sparsity joins (5ce955fb@gateway/web/cgi-irc/kiwiirc.com/ip.92.233.85.251) |
| 21:05:19 | → | fen joins (5ce955fb@gateway/web/cgi-irc/kiwiirc.com/ip.92.233.85.251) |
| 21:05:22 | flx_ | is now known as mflux |
| 21:05:39 | × | aplainze1akind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit) |
| 21:06:16 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 21:08:01 | × | aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Ping timeout: 276 seconds) |
| 21:11:05 | <fen> | @let scanner f a = snd . mapAccumL f a |
| 21:11:07 | <lambdabot> | .L.hs:173:1: error: [-Woverlapping-patterns, -Werror=overlapping-patterns] |
| 21:11:07 | <lambdabot> | Pattern match is redundant |
| 21:11:07 | <lambdabot> | In an equation for ‘scanner’: scanner f a = ... |
| 21:11:38 | <fen> | @undefine |
| 21:11:38 | <lambdabot> | Undefined. |
| 21:11:41 | <fen> | @let scanner f a = snd . mapAccumL f a |
| 21:11:42 | <lambdabot> | Defined. |
| 21:11:58 | <fen> | :t \ f g a b -> sum $ uncurry (zipWith (+)) $ fmap (scanner f a) $ unzip $ unfoldr g b |
| 21:11:59 | <lambdabot> | Num a1 => (a2 -> b1 -> (a2, a1)) -> (b2 -> Maybe ((a1, b1), b2)) -> a2 -> b2 -> a1 |
| 21:12:05 | → | Ahmuck joins (~Ahmuck@139.28.218.148) |
| 21:13:32 | → | arturh joins (~arturh@93.176.180.48) |
| 21:16:46 | × | zaquest quits (~notzaques@5.128.210.178) (Ping timeout: 240 seconds) |
| 21:19:37 | <sparsity> | (a=s_t0,(x_tn,w_tn,s_tn+1) = g s_tn) |
| 21:19:39 | <sparsity> | (b=r_t0,(y_tn,r_tn+1)= f (r_tn,w_tn) |
| 21:19:45 | <sparsity> | ) |
| 21:21:17 | → | son0p joins (~son0p@181.136.122.143) |
| 21:21:48 | ← | arturh parts (~arturh@93.176.180.48) () |
| 21:22:46 | → | zaquest joins (~notzaques@5.128.210.178) |
| 21:23:46 | × | kenran quits (~kenran@i59F67B6E.versanet.de) (Quit: leaving) |
| 21:23:57 | → | acidjnk_new joins (~acidjnk@p200300d0c72b95739d8477eb9e4283c0.dip0.t-ipconnect.de) |
| 21:24:32 | × | sgibber2018 quits (d055ed90@208.85.237.144) (Quit: Connection closed) |
| 21:26:38 | → | aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 21:26:58 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 240 seconds) |
| 21:27:06 | × | dbmikus quits (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) (Ping timeout: 240 seconds) |
| 21:27:33 | × | aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Read error: Connection reset by peer) |
| 21:27:51 | → | aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 21:28:15 | × | Franciman quits (~francesco@host-79-53-62-46.retail.telecomitalia.it) (Quit: Leaving) |
| 21:28:35 | × | Guest23256 quits (~textual@mskresolve-a.mskcc.org) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 21:28:48 | → | dpl__ joins (~dpl@77.121.78.163) |
| 21:28:48 | × | aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit) |
| 21:28:48 | → | ystael joins (~ystael@209.6.50.55) |
| 21:30:17 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 21:32:11 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 21:32:38 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 21:33:04 | <statusbot> | Status update: Hackage storage update complete -- back up and running. -- http://status.haskell.org/pages/incident/537c07b0cf1fad5830000093/606200df2a84ed05341dcbf1 |
| 21:33:35 | × | Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 246 seconds) |
| 21:34:34 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) (Ping timeout: 245 seconds) |
| 21:34:46 | → | Sorna joins (~Sornaensi@185.217.117.121) |
| 21:35:09 | × | dpl__ quits (~dpl@77.121.78.163) (Quit: dpl__) |
| 21:35:47 | → | fendor_ joins (~fendor@91.141.2.121.wireless.dyn.drei.com) |
| 21:36:01 | → | conal joins (~conal@64.71.133.70) |
| 21:37:08 | × | Sornaensis quits (~Sornaensi@79.142.232.102.static.router4.bolignet.dk) (Ping timeout: 252 seconds) |
| 21:38:02 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 21:38:03 | → | borne joins (~fritjof@200116b864978000f7ed9fd86a2491f0.dip.versatel-1u1.de) |
| 21:38:06 | × | fendor quits (~fendor@77.119.130.24.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 21:38:39 | × | stree quits (~stree@68.36.8.116) (Quit: Caught exception) |
| 21:39:06 | → | stree joins (~stree@68.36.8.116) |
| 21:40:03 | → | aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 21:40:49 | <mpickering> | lyxia: Thanks, I am playing with the idea of a build system built on free profunctors |
| 21:45:48 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 21:46:07 | × | dpl_ quits (~dpl@77.121.78.163) (Read error: Connection reset by peer) |
| 21:46:20 | → | Wuzzy joins (~Wuzzy@p5790e118.dip0.t-ipconnect.de) |
| 21:47:03 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 21:50:23 | <sparsity> | i thought free things only could have functors in |
| 21:50:32 | → | kupi joins (uid212005@gateway/web/irccloud.com/x-ufrrxovbropqrvyy) |
| 21:50:33 | <sparsity> | or something |
| 21:50:44 | <sparsity> | free monads for less |
| 21:50:55 | <sparsity> | i see no profunctors |
| 21:51:35 | → | Alleria joins (~textual@2603-7000-3040-0000-29c5-30e3-fcb5-0c65.res6.spectrum.com) |
| 21:51:54 | <sparsity> | its probably quite technical... |
| 21:51:58 | Alleria | is now known as Guest5519 |
| 21:52:19 | × | fendor_ quits (~fendor@91.141.2.121.wireless.dyn.drei.com) (Remote host closed the connection) |
| 21:54:49 | → | conal joins (~conal@64.71.133.70) |
| 21:55:46 | × | Guest5519 quits (~textual@2603-7000-3040-0000-29c5-30e3-fcb5-0c65.res6.spectrum.com) (Ping timeout: 245 seconds) |
| 21:57:57 | → | usr25 joins (~J@121.red-88-0-140.dynamicip.rima-tde.net) |
| 21:58:00 | × | mouseghost quits (~draco@wikipedia/desperek) (Quit: mew wew) |
| 22:05:45 | → | gnumonic joins (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) |
| 22:06:15 | <ski> | sparsity : "could have functors in" ? |
| 22:06:30 | <sparsity> | i realise how stupid that sounds |
| 22:06:35 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 22:06:38 | → | ph88^ joins (~ph88@2a02:8109:9e00:7e5c:44c9:a8ba:908e:c8fa) |
| 22:06:43 | → | Alleria__ joins (~textual@2603-7000-3040-0000-29c5-30e3-fcb5-0c65.res6.spectrum.com) |
| 22:06:59 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 22:07:01 | <sparsity> | idk how you use free profunctors for "build systems" anyway |
| 22:07:15 | <ski> | i dunno what you meant by that phrase |
| 22:07:24 | × | Iryon quits (~Iryon@2a02:a31a:a045:3500:5420:2237:4aee:26f2) (Remote host closed the connection) |
| 22:07:57 | → | pera joins (~pera@unaffiliated/pera) |
| 22:08:00 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 22:08:19 | <mpickering> | sparsity: https://elvishjerricco.github.io/2017/03/10/profunctors-arrows-and-static-analysis.html |
| 22:08:19 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 22:08:21 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 22:08:21 | → | haritz joins (~hrtz@unaffiliated/haritz) |
| 22:08:35 | <mpickering> | This post explains somewhat |
| 22:08:51 | × | ixian quits (~mgold@2002:4a74:ba78:1701:0:ff:fe78:6269) (Ping timeout: 248 seconds) |
| 22:08:57 | × | pera quits (~pera@unaffiliated/pera) (Client Quit) |
| 22:09:05 | <sparsity> | whats the tldr |
| 22:09:52 | <mpickering> | If you use free profunctors and some other things you can inspect the build graph before you execute it |
| 22:09:55 | <mpickering> | unlike if you use a free monad |
| 22:10:02 | <mpickering> | and free applicatives are too weak |
| 22:10:04 | → | ixian joins (~mgold@terra.bitplane.org) |
| 22:10:18 | × | ph88 quits (~ph88@2a02:8109:9e00:7e5c:4080:7dc1:315d:729) (Ping timeout: 246 seconds) |
| 22:10:19 | <dibblego> | why can't you inspect it with free? |
| 22:10:32 | <sparsity> | it collapses? |
| 22:10:49 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) (Ping timeout: 245 seconds) |
| 22:11:00 | <sparsity> | why would profunctorisation allow this preservation of inspectability, seems very strange |
| 22:11:06 | <mpickering> | because the structure of the graph depends on the result of a previous computation, so you have to evaluate part of the graph in order to work out what the rest looks like |
| 22:11:20 | <dibblego> | ah yeah makes sense |
| 22:11:40 | <sparsity> | how can you build up the graph any other way? |
| 22:11:58 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 22:12:10 | <mpickering> | sparsity: What do you mean? |
| 22:12:12 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 22:12:17 | <mpickering> | Any other way as opposed to what? |
| 22:12:36 | <sparsity> | your saying it changes as you consume it, but that somehow the profunctors allow it to be all in place at the same time |
| 22:13:07 | <mpickering> | yeah the structure of the graph is known ahead of time but not what each node produces |
| 22:13:45 | <mpickering> | Perhaps I will write a paper about it |
| 22:14:00 | <sparsity> | a few words could be more effecient now |
| 22:14:06 | → | nij joins (~user@2001-48F8-9021-806-0-0-0-49D8-dynamic.midco.net) |
| 22:14:13 | <sparsity> | we are still none the wiser as to whats going on with these profunctors |
| 22:14:56 | <dibblego> | code pls :) |
| 22:15:01 | <nij> | Hello! While writing a program with lots of complicated objects, how would I stay functional? Especially when it frequently reads/writes database.. |
| 22:15:16 | <sparsity> | dibblego: that could be huge and incomprehensible |
| 22:15:18 | <dibblego> | nij: what is "complicated objects"? Do you have an example? |
| 22:15:29 | <dibblego> | sparsity: I fully intend to comprehend it |
| 22:15:43 | <sparsity> | then the blog post? |
| 22:15:58 | <dibblego> | maybe that too; I'll write it after :) |
| 22:16:02 | <sparsity> | the scrolldown threshold was too strong |
| 22:16:49 | <sparsity> | it went from "whats a value" to cojibberish in the blink of an eye |
| 22:17:05 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 22:17:34 | <nij> | dibblego: so each object is a list of list of lists. |
| 22:17:35 | <sparsity> | and the "heres what your trying to understand" was not placed before "lest make reference to a databasing example" |
| 22:17:56 | <nij> | I might say plists.. they have many slots, and i need to read and write frequently |
| 22:18:11 | <nij> | sometimes just to the memory, but also frequently to database. |
| 22:20:14 | <sparsity> | "Before we get to an example, I want to talk about free prearrows" |
| 22:20:25 | <mpickering> | yes sparsity, I get that completely. |
| 22:20:26 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 22:20:27 | <sparsity> | * never * do * this * |
| 22:20:35 | <mpickering> | It's just the only reference I could find |
| 22:20:37 | <monochrom> | I still don't understand, but perhaps the function that maps old object to new object is functional. |
| 22:22:04 | <sparsity> | i think i managed to glean it has something to do with "strength" |
| 22:22:25 | <sparsity> | "strenght of arrows enables static checking" |
| 22:22:36 | <sparsity> | or so they say... |
| 22:24:13 | <sparsity> | my mind is flipping a profunctor arrow back and forth and trying to see how this stops the graph of a program undergoing evaluation from tearing apart |
| 22:25:46 | <sparsity> | "A profunctor is strong if it can freely pass unknown values through it without modification. This is represented by adding an input to the profunctor in a tuple, and adding that same type to the output in a tuple, allowing a value to safely pass through." |
| 22:25:53 | <sparsity> | that explains the arrows link at least |
| 22:26:49 | <sparsity> | "This lets you pass in anything you want to preserve after the computation is done" |
| 22:27:11 | <sm[m]> | nij: is your choice of database restricted ? will it be postgres ? |
| 22:27:32 | <sparsity> | right, so you can use profunctors to preserve the internals of some term rewriting process or something? |
| 22:27:46 | × | malumore quits (~malumore@151.62.126.223) (Ping timeout: 268 seconds) |
| 22:28:29 | <sparsity> | im sure this is just a convoluted axample of something much more simple |
| 22:28:39 | <nij> | sm[m]: no. it's a general question. |
| 22:28:57 | <nij> | I wonder what's the principle to stay functional, while needing to deal with dbs |
| 22:29:19 | <sparsity> | ah, right, so strength is like fmapping into *part* of something |
| 22:29:49 | <monochrom> | Do you think it's like lens but for database? |
| 22:30:32 | <mpickering> | sparsity: It's not so complicated. A value of type `P a b` is a build rule which takes an `a` as input and `b` as output. Then various ways to compose these rules correspond to constructing a graph. |
| 22:30:46 | <mpickering> | Which you can then recover by appropiately choosing how to interpret `P`. |
| 22:31:06 | <monochrom> | Our current lens is a specification of where to dive into a complex immutable object for tinkering or reading. Perhaps there is an analogue for s/immutable object/mutable record/ |
| 22:31:33 | <sparsity> | isnt mutability a hangup from worser languages? |
| 22:31:51 | <monochrom> | I am not talking to you, sparsity. |
| 22:32:11 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 22:32:28 | <monochrom> | Unless you also want to deny nij's problem about accessing databases. |
| 22:33:11 | × | Yumasi quits (~guillaume@static-176-175-104-214.ftth.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 22:33:59 | <sparsity> | i think the way your pushing the idea of DBs in a way thats "idiomatic in a functional language" (or functorial or whatever it was being said like) to mean something like lenses as in a "pure" db, conflaiting that with mutability, is somewhat, droll |
| 22:34:03 | <sm[m]> | nij: I think your question has some db dependence though. For working purely in-memory, the answer will probably be "use mutable vectors" or some such. If you need to store frequently in a db, the answer is probably "use postgres and a db abstraction layer of choice". |
| 22:34:34 | <sm[m]> | in between, there is acid-state, a db you can write any haskell data type to, but it's generally not recommended. |
| 22:35:18 | × | solidus-river quits (~mike@174.127.249.180) (Remote host closed the connection) |
| 22:35:46 | <sparsity> | yeah, it gets confused around record accessors and generics |
| 22:36:24 | <sparsity> | i would question if the memory managment abstractions of higher order languages alone almost make redundant some of these "traditional databasing" concerns |
| 22:36:51 | × | niklasb quits (~niklasb@unaffiliated/codeslay0r) (Ping timeout: 252 seconds) |
| 22:37:26 | <sparsity> | i guess its a problem of cross language integration essentially, so more like an FFI to any particular standard |
| 22:37:43 | × | borne quits (~fritjof@200116b864978000f7ed9fd86a2491f0.dip.versatel-1u1.de) (Ping timeout: 276 seconds) |
| 22:37:48 | <sclv> | as far as i know any serious db writes effectively its own memory manager |
| 22:37:58 | <sclv> | no matter what language its written in |
| 22:38:27 | <sclv> | for lightweight datastores you can get away without this, but at a certain scale of data you need a manager suited precisely to your abstractions and representation forms |
| 22:38:40 | × | nuncanada quits (~dude@179.235.160.168) (Read error: Connection reset by peer) |
| 22:38:48 | <sm[m]> | nij: there is a range of db abstraction libs on hackage, from simple (postgresql-simple) to convenient (yesod) to powerful (beam, opaleye and a bunch of others) - maybe these will give ideas |
| 22:38:57 | <sclv> | very serious dbs effectively implement their own file system too |
| 22:39:22 | <sparsity> | and can offer pretty bizzare language interfaces as a consequence |
| 22:39:23 | <sclv> | its the closest in application systems programming i know of to needing to write an entire "mini-os" |
| 22:39:47 | <sparsity> | yeah but we have all that these things offer |
| 22:40:12 | <sparsity> | maybe they are more like fledgling programing language runtimes like the JVM or something |
| 22:40:42 | <sparsity> | ie, legacy crap |
| 22:41:14 | <sclv> | i should mention regarding the above discussion btw the "a la carte" approach https://www.microsoft.com/en-us/research/uploads/prod/2018/03/build-systems.pdf |
| 22:41:26 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 22:41:48 | <sparsity> | you might lose some folklore by totally replacing the entire notion of DBs with better languages, but i doubt it would be too bad |
| 22:43:54 | <sparsity> | the thing is, all of this stuff, all the libraries you want your build systems to be built on, its all slowly aiming towards being canonical and prinicpled |
| 22:44:06 | <sparsity> | is there a fixed point? |
| 22:44:27 | <sparsity> | is there tangible strength in diversity of styles? |
| 22:44:43 | <ph88^> | does anyone know a good library to simplify symbolic (boolean) expressions ? |
| 22:45:49 | <sparsity> | i guess you elucidate the fundamental structures of mathematical programming along the way, and that these then naturally form those fundamental canonical abstractions |
| 22:46:08 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:f159:ca44:c706:a1d8) |
| 22:46:24 | <sclv> | ph88^: i did this one back in the day and it still builds: https://hackage.haskell.org/package/boolsimplifier |
| 22:46:43 | <ph88^> | nice sclv |
| 22:46:44 | <monochrom> | neato |
| 22:46:49 | <sclv> | the strategy it takes was specifically made to reduce obvious redundancy from machine generated expressions |
| 22:47:02 | → | zjp joins (~zjp@66-45-138-104-dynamic.midco.net) |
| 22:47:07 | <sclv> | its not like full featured propositional logic manipulation, so its not necc what you want for all purposes |
| 22:47:24 | <sclv> | and the types are Somewhat Fancy just because that's what my collaborator wanted to do as an exercise |
| 22:47:26 | <sparsity> | you get something similar in the structure of group automorphisms |
| 22:47:50 | <sparsity> | i mean, logic is good too though |
| 22:48:17 | <ph88^> | sclv, do you know how this class of programs is called ? i would also like to search for alternatives. ... But yours looks pretty nice at first glance :) |
| 22:48:19 | <sparsity> | probably have to splice the two together somehow |
| 22:48:24 | → | irc_user joins (uid423822@gateway/web/irccloud.com/x-tjmapcziuxjtvokq) |
| 22:48:38 | × | Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 240 seconds) |
| 22:48:56 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 22:49:36 | <sclv> | ph88^: probably you'd look for "first order logic" or "propositional logic" |
| 22:49:47 | <sparsity> | there are dualities in maths for various cannonicalisations |
| 22:50:07 | <sclv> | there are approaches that might also use binary decision diagrams as in https://hackage.haskell.org/package/obdd |
| 22:50:11 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 22:50:15 | <sparsity> | matrix factorisation making a model for hierarchical decomposition of matter etc. |
| 22:50:20 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:b177:1e40:d97b:578c) |
| 22:50:25 | <sparsity> | i dont get how programming uses logic though |
| 22:50:47 | <sparsity> | combinatorics? |
| 22:50:56 | <sparsity> | is everything some fundamental result of counting? |
| 22:51:56 | <monochrom> | sparsity: Are you done? |
| 22:51:59 | <sparsity> | i was reading about the factorisation of finite automata and how that relates to a higher order functional paradigm |
| 22:52:30 | <dibblego> | I could do with some sparsity |
| 22:52:34 | <sparsity> | monochrom: im trying to ask about this counting diagrams idea, and about graph isomporphic programs that are being discussed |
| 22:53:06 | ChanServ | sets mode +o monochrom |
| 22:53:09 | <sparsity> | i like how logic seems to solve this, but cant see how that fits in with other approaches to cannonicalisation |
| 22:53:12 | monochrom | sets mode +b *!*@gateway/web/cgi-irc/kiwiirc.com/ip.92.233.85.251 |
| 22:53:12 | sparsity | is kicked by monochrom (sparsity) |
| 22:53:15 | fen | is kicked by monochrom (fen) |
| 22:53:20 | monochrom | sets mode -o monochrom |
| 22:53:21 | <sclv> | ph88^: there's libs like eg https://hackage.haskell.org/package/boolean-normal-forms but note that putting expressions in unique normal forms can make them far bigger. general "smallest expression" is np hard. so the lib i worked on tried to find a pragmatic procedure that usually worked |
| 22:53:27 | sclv | thanks monochrom |
| 22:53:54 | <sclv> | (and i think, by construction, really didn't ever make things worse) |
| 22:54:41 | → | hiptobecubic joins (~john@unaffiliated/hiptobecubic) |
| 22:54:53 | <sclv> | if you know the specific structure of your expressions ahead of time, you can often decide on a normalization procedure for _precisely those expressions_ that is suited to your domain, and is straightforward and efficient to calculate. |
| 22:55:12 | <sclv> | that's the general law of algorithms -- the more you know about the input, the better the algo you can write |
| 22:55:13 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:f159:ca44:c706:a1d8) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:56:14 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:b177:1e40:d97b:578c) (Remote host closed the connection) |
| 22:57:41 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 22:58:36 | × | DavidEichmann quits (~david@47.27.93.209.dyn.plus.net) (Ping timeout: 268 seconds) |
| 23:00:59 | → | geowiesnot joins (~user@87-89-181-157.abo.bbox.fr) |
| 23:01:03 | → | mouseghost joins (~draco@wikipedia/desperek) |
| 23:01:03 | → | niklasb joins (~niklasb@dtun.de) |
| 23:01:03 | × | niklasb quits (~niklasb@dtun.de) (Changing host) |
| 23:01:03 | → | niklasb joins (~niklasb@unaffiliated/codeslay0r) |
| 23:02:06 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 23:04:27 | → | ukari joins (~ukari@unaffiliated/ukari) |
| 23:08:05 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:b177:1e40:d97b:578c) |
| 23:08:32 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6903:50f7:234a:96c5) |
| 23:12:46 | × | geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 23:14:34 | × | acidjnk_new quits (~acidjnk@p200300d0c72b95739d8477eb9e4283c0.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 23:15:24 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 23:16:02 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 23:16:16 | <ph88^> | thank you sclv |
| 23:16:55 | × | ph88^ quits (~ph88@2a02:8109:9e00:7e5c:44c9:a8ba:908e:c8fa) (Quit: Leaving) |
| 23:17:59 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 23:17:59 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 23:18:07 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6903:50f7:234a:96c5) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 23:18:25 | → | Tario joins (~Tario@201.192.165.173) |
| 23:20:55 | → | nbloomf joins (~nbloomf@76.217.43.73) |
| 23:21:05 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 23:21:59 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 23:23:08 | × | LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 23:23:16 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 23:23:50 | × | codygman` quits (~user@47.186.207.161) (Ping timeout: 246 seconds) |
| 23:24:46 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:26:06 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) (Remote host closed the connection) |
| 23:29:58 | × | usr25 quits (~J@121.red-88-0-140.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 23:30:33 | × | zjp quits (~zjp@66-45-138-104-dynamic.midco.net) (Remote host closed the connection) |
| 23:32:41 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 23:33:25 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 23:35:14 | → | ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 23:38:45 | × | rj quits (~x@gateway/tor-sasl/rj) (Ping timeout: 240 seconds) |
| 23:40:46 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 23:41:06 | × | gnumonic quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 23:46:56 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 246 seconds) |
| 23:49:44 | × | niklasb quits (~niklasb@unaffiliated/codeslay0r) (Ping timeout: 246 seconds) |
| 23:52:38 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 240 seconds) |
| 23:53:02 | → | Tario joins (~Tario@200.119.187.104) |
| 23:56:29 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 23:56:36 | → | niklasb joins (~niklasb@unaffiliated/codeslay0r) |
All times are in UTC on 2021-03-29.