Logs on 2025-03-21 (liberachat/#haskell)
| 00:01:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 00:02:36 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 252 seconds) |
| 00:04:08 | → | kh0d joins (~kh0d@212.200.247.167) |
| 00:11:21 | × | abiss27 quits (~abiss27@user/abiss) (Quit: I'm off, Goodbye!) |
| 00:11:49 | → | alfiee joins (~alfiee@user/alfiee) |
| 00:12:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:14:52 | → | abiss27 joins (~abiss27@190.213.236.106) |
| 00:15:59 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 265 seconds) |
| 00:16:34 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 00:17:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 00:19:04 | × | xff0x quits (~xff0x@2405:6580:b080:900:d229:f63b:2d49:ccd3) (Ping timeout: 260 seconds) |
| 00:20:58 | → | xff0x joins (~xff0x@2405:6580:b080:900:b993:7de8:b31e:5325) |
| 00:22:05 | × | abiss27 quits (~abiss27@190.213.236.106) (Changing host) |
| 00:22:05 | → | abiss27 joins (~abiss27@user/abiss) |
| 00:23:12 | → | LainExperiments joins (~LainExper@user/LainExperiments) |
| 00:24:03 | × | abiss27 quits (~abiss27@user/abiss) (Quit: I'm off, Goodbye!) |
| 00:24:42 | → | abiss27 joins (~abiss27@190.213.236.106) |
| 00:26:06 | × | abiss27 quits (~abiss27@190.213.236.106) (Client Quit) |
| 00:28:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:28:41 | → | LainExperiments4 joins (~LainExper@user/LainExperiments) |
| 00:28:59 | → | kh0d joins (~kh0d@212.200.247.167) |
| 00:30:27 | × | LainExperiments4 quits (~LainExper@user/LainExperiments) (Client Quit) |
| 00:30:45 | × | tabaqui quits (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 00:31:18 | × | LainExperiments quits (~LainExper@user/LainExperiments) (Ping timeout: 240 seconds) |
| 00:35:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 00:35:34 | × | sprotte24 quits (~sprotte24@p200300d16f3eed00f17f1149f1ad7273.dip0.t-ipconnect.de) (Quit: Leaving) |
| 00:36:34 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 260 seconds) |
| 00:38:07 | × | notdabs quits (~Owner@2600:1700:69cf:9000:99ef:5e1b:cda4:8b3) (Read error: Connection reset by peer) |
| 00:39:50 | → | Square joins (~Square@user/square) |
| 00:40:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:41:53 | × | acidjnk quits (~acidjnk@p200300d6e71c4f9399301ab9560bdae8.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 00:43:24 | × | xff0x quits (~xff0x@2405:6580:b080:900:b993:7de8:b31e:5325) (Ping timeout: 260 seconds) |
| 00:43:56 | → | xff0x joins (~xff0x@2405:6580:b080:900:3522:3957:cbed:8aef) |
| 00:45:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 00:48:18 | → | acidjnk joins (~acidjnk@p200300d6e71c4f9399301ab9560bdae8.dip0.t-ipconnect.de) |
| 00:50:18 | → | kh0d joins (~kh0d@212.200.247.167) |
| 00:51:46 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 00:53:35 | × | euleritian quits (~euleritia@95.90.214.149) (Remote host closed the connection) |
| 00:54:03 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 00:54:19 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 00:55:00 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 00:56:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:57:33 | → | alfiee joins (~alfiee@user/alfiee) |
| 00:57:44 | × | Googulator88 quits (~Googulato@2a01-036d-0106-0ae4-b88c-ff83-9891-e272.pool6.digikabel.hu) (Quit: Client closed) |
| 00:58:02 | → | Googulator88 joins (~Googulato@80-95-93-233.pool.digikabel.hu) |
| 00:59:33 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 245 seconds) |
| 01:01:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 01:02:14 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 01:12:10 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 01:12:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:13:18 | × | xff0x quits (~xff0x@2405:6580:b080:900:3522:3957:cbed:8aef) (Ping timeout: 245 seconds) |
| 01:13:37 | → | Digit joins (~user@user/digit) |
| 01:13:58 | → | kh0d joins (~kh0d@212.200.247.167) |
| 01:16:51 | → | j1n37 joins (~j1n37@user/j1n37) |
| 01:17:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 01:22:44 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 01:24:05 | × | acidjnk quits (~acidjnk@p200300d6e71c4f9399301ab9560bdae8.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 01:28:15 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:32:41 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 01:32:56 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 01:33:29 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 01:34:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 01:34:20 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 01:38:22 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 244 seconds) |
| 01:39:03 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 01:39:23 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 01:42:37 | → | alfiee joins (~alfiee@user/alfiee) |
| 01:44:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:45:10 | → | Square2 joins (~Square4@user/square) |
| 01:46:51 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 01:47:53 | × | Square quits (~Square@user/square) (Ping timeout: 245 seconds) |
| 01:48:29 | ← | tusko parts (uid478376@user/tusko) () |
| 01:49:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 01:55:25 | → | mvk joins (~mvk@2607:fea8:5c96:5800::7ea9) |
| 01:55:25 | × | mvk quits (~mvk@2607:fea8:5c96:5800::7ea9) (Client Quit) |
| 01:58:56 | → | kh0d joins (~kh0d@212.200.247.167) |
| 01:59:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:03:36 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 252 seconds) |
| 02:04:32 | → | user363627 joins (~user@user/user363627) |
| 02:04:42 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 02:07:20 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 02:08:20 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 02:08:36 | × | weary-traveler quits (~user@user/user363627) (Ping timeout: 265 seconds) |
| 02:12:41 | × | sabathan quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Ping timeout: 244 seconds) |
| 02:15:36 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:19:30 | → | sabathan joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 02:22:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 02:28:01 | → | alfiee joins (~alfiee@user/alfiee) |
| 02:32:09 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
| 02:33:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:34:57 | → | kh0d joins (~kh0d@212.200.247.167) |
| 02:38:07 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 02:38:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 02:40:12 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 246 seconds) |
| 02:41:49 | → | j1n37 joins (~j1n37@user/j1n37) |
| 02:44:55 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 02:48:00 | → | j1n37 joins (~j1n37@user/j1n37) |
| 02:49:03 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 02:49:26 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 02:49:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:50:24 | × | tromp quits (~textual@2a02:a210:cba:8500:f085:be23:3f4e:4a7a) (Ping timeout: 244 seconds) |
| 02:54:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 02:59:23 | → | Guest9 joins (~Guest9@2600:4040:52fa:9700:fd29:3b63:e979:8aca) |
| 02:59:52 | × | Guest9 quits (~Guest9@2600:4040:52fa:9700:fd29:3b63:e979:8aca) (Client Quit) |
| 03:01:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:06:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 03:09:29 | → | j1n37 joins (~j1n37@user/j1n37) |
| 03:10:16 | → | kh0d joins (~kh0d@212.200.247.167) |
| 03:13:25 | → | alfiee joins (~alfiee@user/alfiee) |
| 03:15:23 | × | kh0d quits (~kh0d@212.200.247.167) (Ping timeout: 245 seconds) |
| 03:16:37 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 03:17:13 | → | rvalue joins (~rvalue@user/rvalue) |
| 03:17:15 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:17:40 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 03:18:45 | × | sudden quits (~cat@user/sudden) (Ping timeout: 248 seconds) |
| 03:19:49 | × | dsrt^ quits (~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) (Ping timeout: 248 seconds) |
| 03:20:26 | → | sudden joins (~cat@user/sudden) |
| 03:20:31 | → | dsrt^ joins (~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) |
| 03:22:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 03:27:44 | → | kh0d joins (~kh0d@212.200.65.86) |
| 03:33:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:33:19 | × | kh0d quits (~kh0d@212.200.65.86) (Ping timeout: 260 seconds) |
| 03:36:57 | user363627 | is now known as weary-traveler |
| 03:37:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 03:47:41 | → | kh0d joins (~kh0d@212.200.65.86) |
| 03:48:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:53:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 03:55:23 | × | Xe quits (~Xe@perl/impostor/xe) (Ping timeout: 245 seconds) |
| 03:57:04 | → | Xe joins (~Xe@perl/impostor/xe) |
| 03:58:49 | → | alfiee joins (~alfiee@user/alfiee) |
| 04:03:02 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 04:04:13 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:08:09 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 04:08:15 | × | Fijxu quits (~Fijxu@user/fijxu) (Quit: XD!!) |
| 04:11:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 04:12:17 | → | Fijxu joins (~Fijxu@user/fijxu) |
| 04:15:17 | → | azh_ming joins (~aaron@pool-108-48-188-212.washdc.fios.verizon.net) |
| 04:17:28 | → | aazh_anon_ming joins (~aazh_anon@pool-108-48-188-212.washdc.fios.verizon.net) |
| 04:18:46 | × | azh_ming quits (~aaron@pool-108-48-188-212.washdc.fios.verizon.net) (Quit: leaving) |
| 04:19:12 | × | aazh_anon_ming quits (~aazh_anon@pool-108-48-188-212.washdc.fios.verizon.net) (Remote host closed the connection) |
| 04:19:22 | → | azh_ming joins (~azh_ming@pool-108-48-188-212.washdc.fios.verizon.net) |
| 04:20:25 | <azh_ming> | @pl \f g x y -> f (x ++ g x) (g y) |
| 04:20:25 | <lambdabot> | join . ((flip . ((.) .)) .) . (. ap (++)) . (.) |
| 04:21:44 | → | Square joins (~Square@user/square) |
| 04:22:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:24:06 | × | azh_ming quits (~azh_ming@pool-108-48-188-212.washdc.fios.verizon.net) (Changing host) |
| 04:24:06 | → | azh_ming joins (~azh_ming@user/azh-ming:58353) |
| 04:25:04 | × | Square2 quits (~Square4@user/square) (Ping timeout: 260 seconds) |
| 04:27:21 | <haskellbridge> | <Bowuigi> Peak Haskell |
| 04:27:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 04:28:22 | × | azh_ming quits (~azh_ming@user/azh-ming:58353) (Remote host closed the connection) |
| 04:28:46 | → | azh_ming joins (~azh_ming@user/azh-ming:58353) |
| 04:28:48 | × | azh_ming quits (~azh_ming@user/azh-ming:58353) (Remote host closed the connection) |
| 04:29:58 | → | azh_ming joins (~aaron@user/azh-ming:58353) |
| 04:30:45 | <azh_ming> | /join #politics |
| 04:30:51 | × | azh_ming quits (~aaron@user/azh-ming:58353) (Client Quit) |
| 04:34:57 | → | azh_ming joins (~aaron@user/azh-ming:58353) |
| 04:38:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:43:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 04:44:13 | → | alfiee joins (~alfiee@user/alfiee) |
| 04:48:30 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 04:54:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:56:46 | × | kh0d quits (~kh0d@212.200.65.86) (Ping timeout: 244 seconds) |
| 04:57:24 | × | azh_ming quits (~aaron@user/azh-ming:58353) (Quit: leaving) |
| 04:58:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 05:01:12 | → | tavare joins (~tavare@user/tavare) |
| 05:02:30 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:07:17 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 05:10:25 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 05:11:06 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 05:11:43 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 05:11:46 | → | kh0d joins (~kh0d@212.200.65.86) |
| 05:13:18 | × | olivial quits (~benjaminl@user/benjaminl) (Ping timeout: 244 seconds) |
| 05:14:53 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 05:15:06 | × | Square quits (~Square@user/square) (Ping timeout: 252 seconds) |
| 05:15:39 | → | olivial joins (~benjaminl@user/benjaminl) |
| 05:15:57 | × | jmcantrell quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.5.2) |
| 05:16:24 | × | kh0d quits (~kh0d@212.200.65.86) (Ping timeout: 244 seconds) |
| 05:18:04 | → | shr\ke_ joins (~shrike@user/paxhumana) |
| 05:18:18 | × | shr\ke quits (~shrike@user/shrke:31298) (Ping timeout: 252 seconds) |
| 05:18:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:18:21 | shr\ke_ | is now known as shr\ke |
| 05:23:01 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 05:26:17 | → | michalz joins (~michalz@185.246.207.193) |
| 05:27:25 | → | arahael joins (~arahael@user/arahael) |
| 05:29:17 | → | alfiee joins (~alfiee@user/alfiee) |
| 05:29:47 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:31:12 | × | sabathan quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 05:33:42 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 05:34:04 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 05:34:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:35:13 | → | sabathan joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 05:39:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 05:45:29 | → | kh0d joins (~kh0d@212.200.65.86) |
| 05:49:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:50:13 | × | kh0d quits (~kh0d@212.200.65.86) (Ping timeout: 248 seconds) |
| 05:50:52 | × | dolio quits (~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in) |
| 05:54:25 | → | dolio joins (~dolio@130.44.140.168) |
| 05:56:00 | × | poscat quits (~poscat@user/poscat) (Quit: Bye) |
| 05:56:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 05:58:22 | → | poscat joins (~poscat@user/poscat) |
| 06:00:20 | × | dolio quits (~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in) |
| 06:03:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:08:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 06:09:33 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 06:15:21 | → | alfiee joins (~alfiee@user/alfiee) |
| 06:18:04 | → | kh0d joins (~kh0d@212.200.65.86) |
| 06:19:20 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:19:26 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 06:24:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 06:24:46 | × | kh0d quits (~kh0d@212.200.65.86) (Ping timeout: 265 seconds) |
| 06:35:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:40:03 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 06:43:10 | → | Inst joins (~Inst@user/Inst) |
| 06:43:25 | <Inst> | curious, do you need to use IORef (or relatives) to cache top-level data? |
| 06:43:47 | → | acidjnk joins (~acidjnk@p200300d6e71c4f937555fc5a67c80b19.dip0.t-ipconnect.de) |
| 06:44:00 | <Inst> | Let's say, I'm using a web framework. I define a webpage under Lucid, Lucid2, or Blaze on the top-level. |
| 06:45:14 | <Inst> | Every time the page is served, is the top-level definition re-evaluated? Or would it be more efficient to freeze it with IORef, then pass the IORef to the route handler as an argument, with the route handler being in MonadIO? |
| 06:47:24 | × | Inst quits (~Inst@user/Inst) (Remote host closed the connection) |
| 06:48:29 | × | synchromesh quits (~john@2406:5a00:24cf:bb00:19d8:9179:8622:bdf3) (Read error: Connection reset by peer) |
| 06:49:29 | → | synchromesh joins (~john@2406:5a00:24cf:bb00:19d8:9179:8622:bdf3) |
| 06:49:50 | → | Inst joins (~Inst@user/Inst) |
| 06:50:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:52:00 | × | Inst quits (~Inst@user/Inst) (Remote host closed the connection) |
| 06:54:35 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 06:55:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 06:56:55 | → | kh0d joins (~kh0d@212.200.65.86) |
| 06:58:41 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 07:00:01 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:46 | → | alfiee joins (~alfiee@user/alfiee) |
| 07:00:56 | → | caconym joins (~caconym@user/caconym) |
| 07:02:02 | <Axman6> | top level values are generally only evaluated once, just like all named things in Haskell. There are caveats to that though, if it's a function I can't remember what happens |
| 07:02:19 | <Axman6> | if it has a generic type, it might also not be cached |
| 07:02:53 | × | kh0d quits (~kh0d@212.200.65.86) (Ping timeout: 245 seconds) |
| 07:03:09 | × | ash3en quits (~Thunderbi@89.56.182.235) (Client Quit) |
| 07:04:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:04:47 | <haskellbridge> | <Liamzee> thanks, couldn't find an answer on Google |
| 07:04:58 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 07:05:17 | <Axman6> | I think CAF, constant applicative form, is a useful thing to search for, but my memory's rusty |
| 07:06:13 | <haskellbridge> | <Liamzee> thanks, but the term has confusion with the typeclass |
| 07:07:27 | <haskellbridge> | <Liamzee> With Lucid I suspect it might be better to burn the HTML down to a bytestring first |
| 07:07:38 | <haskellbridge> | <Liamzee> since it's a builder function |
| 07:07:51 | <haskellbridge> | <Liamzee> that's also a monad transformer |
| 07:08:27 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 07:08:43 | × | ft quits (~ft@p508db463.dip0.t-ipconnect.de) (Quit: leaving) |
| 07:09:04 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 07:09:48 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Quit: wildsalander) |
| 07:11:07 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 07:11:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 07:13:27 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 07:13:56 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 07:14:00 | → | euleritian joins (~euleritia@95.90.214.149) |
| 07:14:33 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
| 07:14:47 | <[exa]> | Liamzee: what's the type of your toplevel definition btw? that usually determines whether it's gonna get cached or not. |
| 07:15:20 | Lord_of_Life_ | is now known as Lord_of_Life |
| 07:18:21 | → | kh0d joins (~kh0d@109.111.226.14) |
| 07:22:35 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:23:15 | × | kh0d quits (~kh0d@109.111.226.14) (Ping timeout: 252 seconds) |
| 07:26:00 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 07:28:06 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 07:29:59 | × | euleritian quits (~euleritia@95.90.214.149) (Ping timeout: 260 seconds) |
| 07:30:20 | × | dsrt^ quits (~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) (Read error: Connection reset by peer) |
| 07:30:25 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 07:31:59 | → | j1n37- joins (~j1n37@user/j1n37) |
| 07:32:17 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 07:33:15 | → | dsrt^ joins (~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) |
| 07:37:36 | × | ash3en quits (~Thunderbi@89.56.182.235) (Ping timeout: 272 seconds) |
| 07:37:51 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 07:38:08 | × | dsrt^ quits (~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) (Ping timeout: 268 seconds) |
| 07:38:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:38:59 | → | dsrt^ joins (~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) |
| 07:43:21 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 07:43:44 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:44:26 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:45:47 | → | kh0d joins (~kh0d@109.111.226.14) |
| 07:46:31 | → | alfiee joins (~alfiee@user/alfiee) |
| 07:50:18 | × | kh0d quits (~kh0d@109.111.226.14) (Ping timeout: 246 seconds) |
| 07:50:45 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 07:52:40 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 07:53:42 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 07:53:42 | ljdarj1 | is now known as ljdarj |
| 07:54:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:59:27 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 08:05:29 | → | kh0d joins (~kh0d@109.111.226.14) |
| 08:05:34 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 08:05:42 | × | Googulator88 quits (~Googulato@80-95-93-233.pool.digikabel.hu) (Ping timeout: 240 seconds) |
| 08:06:44 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 08:10:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 08:11:26 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 08:12:22 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 08:15:59 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 08:19:01 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 08:21:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 08:25:34 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Remote host closed the connection) |
| 08:25:34 | → | tzh_ joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 08:30:23 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 08:31:35 | → | alfiee joins (~alfiee@user/alfiee) |
| 08:32:52 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 08:35:55 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 08:44:52 | × | tzh_ quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:47:35 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 08:48:42 | <haskellbridge> | <Liamzee> Html () :( |
| 08:49:04 | <haskellbridge> | <Liamzee> so burn to bytestring, it'll get cached, but as a builder, which is afaik just a function pointer |
| 08:49:40 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 08:53:19 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 08:58:27 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 08:58:58 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 09:01:50 | → | __monty__ joins (~toonn@user/toonn) |
| 09:06:01 | → | krei-se- joins (~krei-se@p5dea1e73.dip0.t-ipconnect.de) |
| 09:06:25 | × | krei-se quits (~krei-se@p3ee0faf4.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 09:08:34 | <[exa]> | Liamzee: yap that's a builder, not cacheable |
| 09:09:55 | <[exa]> | but you can cache the prebuild piece (let it evaluate to something with runHtml or so?) and then just shove it into the other html builders? |
| 09:11:54 | <[exa]> | basically having the global value as this should do it: memoized = toLazyByteString ...someglue... runHtmlT $ mypage |
| 09:12:30 | → | forell joins (~forell@user/forell) |
| 09:12:39 | <[exa]> | `someglue` should be solvable by following a typehole |
| 09:15:22 | → | dhil joins (~dhil@2a0c:b381:52e:3600:dd6a:fa62:e132:ec11) |
| 09:16:59 | → | alfiee joins (~alfiee@user/alfiee) |
| 09:21:30 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 09:26:00 | × | califax quits (~califax@user/califx) (Ping timeout: 264 seconds) |
| 09:26:41 | → | califax joins (~califax@user/califx) |
| 09:30:07 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 09:36:09 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 260 seconds) |
| 09:39:48 | × | califax quits (~califax@user/califx) (Ping timeout: 264 seconds) |
| 09:41:14 | → | califax joins (~califax@user/califx) |
| 09:57:47 | <tomsmeding> | Athas: I have few insights regarding higher-order derivatives in general, let alone with `ad`. :P |
| 09:58:12 | <tomsmeding> | (Assuming you mean 2nd, etc. derivatives, not "AD of code containing (higher-order) functions") |
| 09:58:19 | <Athas> | tomsmeding: well, I got it working (albeit with undesirable boilerplate), but now it's just remarkably slow. |
| 09:58:29 | <tomsmeding> | Athas: which mode did you use? |
| 09:58:43 | <Athas> | Forward-over-forward. And it's slower than just hacking up your own dual numbers. |
| 09:59:03 | <tomsmeding> | forward in `ad` is just a dual number, so that's rather surprising |
| 09:59:28 | <tomsmeding> | did you try Numeric.AD.Mode.Tower(.Double)? It purports to be higher-order forward derivatives |
| 09:59:46 | <Athas> | Well, it's not so easy - I need actual nested AD. |
| 10:00:04 | <Athas> | I've realised I'm not good at fast Haskell. |
| 10:00:14 | <tomsmeding> | few people are |
| 10:00:34 | <tomsmeding> | can you share your code with the manual dual numbers? I'm curious to see what beats `ad` |
| 10:01:21 | <__monty__> | (I'd appreciate another recap of what AD is. It's not just a way to numerically compute derivatives of numerical functions, is it? Feel free to leave the recap for when the discussion is more or less over.) |
| 10:01:31 | <tomsmeding> | __monty__: it is |
| 10:01:49 | <tomsmeding> | the problem is that you can do so efficiently for a function of type R^n -> R, or for a function of type R -> R^n |
| 10:02:09 | <tomsmeding> | the typical dual-numbers formulation gives you the _latter_, whereas you usually (but not always) want the former |
| 10:02:25 | → | alfiee joins (~alfiee@user/alfiee) |
| 10:02:28 | <tomsmeding> | the former you get with reverse AD, which is more complicated |
| 10:02:35 | <tomsmeding> | does that help? |
| 10:04:14 | <Athas> | This is my code: https://github.com/gradbench/gradbench/blob/4fdb8cc00daaae42b99431fde3da7be1b1bbbc13/tools/haskell/src/GradBench/Particle.hs |
| 10:04:14 | <Athas> | This is the ad hoc version: https://engineering.purdue.edu/~qobi/stalingrad-examples2009/particle-FF-ghc.html |
| 10:04:26 | <Athas> | And the dual numbers: https://engineering.purdue.edu/~qobi/stalingrad-examples2009/common-ghc.html |
| 10:04:42 | <tomsmeding> | ooh, DatatypeContexts |
| 10:05:13 | <Athas> | Yes, it is aaaalmost working Haskell. |
| 10:05:18 | <Athas> | There are also n+k patterns. |
| 10:05:24 | <Athas> | But it is easy to fix. |
| 10:05:31 | <tomsmeding> | that will likely be faster if you `data Bundle = Bundle {-# UNPACK #-} !Double {-# UNPACK #-} !Double` |
| 10:05:41 | <tomsmeding> | but let me read |
| 10:05:42 | <Athas> | Sure, but it is already faster than 'ad'. |
| 10:05:45 | <tomsmeding> | lol |
| 10:06:10 | <tomsmeding> | 'ad' with Forward over Forward, or Forward over ForwardDouble? |
| 10:06:15 | <Athas> | Forward over Forward. |
| 10:06:38 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 10:07:05 | <tomsmeding> | I like this blast-to-the-past Haskell style |
| 10:08:36 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
| 10:10:48 | <tomsmeding> | Athas: I see a 'gradient' function that uses forward AD |
| 10:10:51 | <tomsmeding> | is that intentional? |
| 10:11:41 | <Athas> | tomsmeding: in which program? |
| 10:12:24 | <tomsmeding> | I was looking at the stalingrad example, but it seems you've implemented that with a proper reverse-mode gradient |
| 10:12:46 | <Athas> | I have done all variants in my 'ad' code. |
| 10:12:58 | <Athas> | The hand-written code only has forward-over-forward. |
| 10:13:01 | <tomsmeding> | oh, right |
| 10:13:08 | <tomsmeding> | the closest match is 'ff'? |
| 10:14:02 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds) |
| 10:14:08 | <Athas> | Yes. |
| 10:14:12 | <tomsmeding> | the input to f is also only length 2, so doing forward mode twice has a chance of being competitive with reverse AD |
| 10:15:04 | <tomsmeding> | I have no clue juts from looking at the code; I would perhaps profile to see if there's anything surprising, but it's bound to produce noise here |
| 10:15:13 | <Athas> | Yes, forward mode is better here, but it is still slow. |
| 10:16:33 | <tomsmeding> | the Forward in 'ad' is a sum type with special cases for zero (not sure why?) and constants |
| 10:16:53 | <tomsmeding> | oh, the zero is relevant if you're doing nested AD I guess |
| 10:17:16 | <tomsmeding> | perhaps that just introduces busywork here? I don't know |
| 10:17:50 | × | mniip quits (mniip@libera/staff/mniip) (Ping timeout: 604 seconds) |
| 10:18:11 | <tomsmeding> | Athas: if you haven't yet, I recommend implementing 'ff' by Forward over ForwardDouble, I suspect it'll help quite a bit |
| 10:20:41 | <Athas> | tomsmeding: I gave it a shot yesterday, but received some type errors I couldn't figure out. Maybe I will try again. |
| 10:22:48 | <ski> | that `stalingrad' code looks a bit weird |
| 10:22:56 | <haskellbridge> | <Liamzee> [exa]: so it's the fault of the person who made the servant lib |
| 10:22:57 | <haskellbridge> | <Liamzee> oh well |
| 10:23:44 | <Athas> | ski: it's written by Scheme programmers and specifically to resemble the style of a corresponding Scheme program. |
| 10:24:15 | <haskellbridge> | <Liamzee> erm, not the lib, but the adapter for the lib |
| 10:24:38 | <haskellbridge> | <Liamzee> will probably try to figure out how to get it to cache lucid later |
| 10:24:47 | × | synchromesh quits (~john@2406:5a00:24cf:bb00:19d8:9179:8622:bdf3) (Quit: WeeChat 4.1.1) |
| 10:25:23 | <ski> | (lot of use of `let'-`in', rather than `where'. some redundant brackets (e.g. when defining some infix operators, or sometimes around function calls, or even conses). incorrect `Show' instance (ought to use `showsPrec', not `show') |
| 10:25:39 | <ski> | mhm |
| 10:25:56 | <ski> | any relation to the Stalin Scheme implementation, Athas ? |
| 10:26:09 | <Athas> | ski: yeah, same people. |
| 10:26:14 | <ski> | ah |
| 10:26:51 | <Athas> | This is code from a benchmark suite to demonstrate how wonderful Stalingrad (an extension of Stalin) is. |
| 10:27:20 | <ski> | it calls out to Scheme code, from Haskell ? |
| 10:28:04 | <Athas> | No, it is a bunch of implementations of the same program in various languages, followed by a performance comparison. Stalingrad is by far the fastest. |
| 10:28:29 | → | mniip joins (mniip@libera/staff/mniip) |
| 10:28:32 | → | gmg joins (~user@user/gehmehgeh) |
| 10:28:54 | <ski> | ah |
| 10:30:31 | <Athas> | See https://www.bcl.hamilton.ie/~qobi/ad2016-benchmarks/ |
| 10:30:36 | <Athas> | Nice work, really! |
| 10:32:40 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 10:32:47 | <ski> | "Scheme->C" is a particular Scheme implementation ? |
| 10:32:53 | <ski> | can't recall hearing about that one, before |
| 10:34:06 | <ski> | yea, looks like a quite nice variety of different backend languages |
| 10:34:20 | <ski> | /implementations |
| 10:35:57 | <ski> | does any of those use source transformations ? |
| 10:36:14 | <sprout> | needs egel |
| 10:36:57 | <ski> | "three files that contain the code that is transformed zero, one, and two times" -- sounds like it, yea |
| 10:37:46 | <ski> | "We could not benchmark against ADIC because we were unsuccessful in getting ADIC to transform its own generated code." -- for higher derivatives ? |
| 10:39:01 | <ski> | "polyvariant submission" does sound like it suggests something like partial evaluation / program specialization, or related |
| 10:42:08 | → | alp joins (~alp@2001:861:8ca0:4940:1861:ecb2:15d3:3a1d) |
| 10:42:48 | × | AlexZenon quits (~alzenon@94.233.240.210) (Read error: Connection reset by peer) |
| 10:43:04 | → | AlexZenon joins (~alzenon@94.233.240.210) |
| 10:45:21 | × | Ekho quits (~Ekho@user/ekho) (Remote host closed the connection) |
| 10:47:46 | × | Fijxu quits (~Fijxu@user/fijxu) (Ping timeout: 248 seconds) |
| 10:48:43 | → | natto17 joins (~natto@129.154.243.159) |
| 10:49:32 | × | natto quits (~natto@129.154.243.159) (Ping timeout: 260 seconds) |
| 10:49:32 | × | noteness quits (~noteness@user/noteness) (Ping timeout: 260 seconds) |
| 10:49:32 | × | Hafydd quits (~Hafydd@user/hafydd) (Ping timeout: 260 seconds) |
| 10:49:33 | → | noteness_ joins (~noteness@user/noteness) |
| 10:50:29 | → | alfiee joins (~alfiee@user/alfiee) |
| 10:50:49 | → | Hafydd joins (~Hafydd@user/hafydd) |
| 10:51:04 | → | Fijxu_ joins (~Fijxu@user/fijxu) |
| 10:51:58 | × | ash3en quits (~Thunderbi@89.56.182.235) (Ping timeout: 252 seconds) |
| 10:54:45 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 11:00:19 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 11:00:46 | → | Ekho joins (~Ekho@user/ekho) |
| 11:06:20 | <Athas> | ski: yes, Scheme->C is a Scheme compiler (actually there seems to be several of that name, very confusing). I don't think any of them implement AD with source transformation. |
| 11:07:28 | <Athas> | ski: oh right, those Fortran things are source transformers. But they work terribly. |
| 11:07:40 | <Athas> | The authors actually wrote an entire paper about how none of those tools work. |
| 11:09:41 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 248 seconds) |
| 11:13:34 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 11:15:06 | → | euleritian joins (~euleritia@dynamic-176-006-132-178.176.6.pool.telefonica.de) |
| 11:24:58 | → | sprotte24 joins (~sprotte24@p200300d16f266c002dc4a2d25f2ad6fe.dip0.t-ipconnect.de) |
| 11:27:04 | × | euleritian quits (~euleritia@dynamic-176-006-132-178.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 11:27:22 | → | euleritian joins (~euleritia@95.90.214.149) |
| 11:27:48 | <merijn> | Athas: That sounds about right :p |
| 11:30:36 | → | xff0x joins (~xff0x@2405:6580:b080:900:74ac:a2fa:2f95:eb9f) |
| 11:35:00 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 11:35:33 | → | alfiee joins (~alfiee@user/alfiee) |
| 11:40:14 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 11:43:44 | × | euleritian quits (~euleritia@95.90.214.149) (Ping timeout: 260 seconds) |
| 11:44:10 | → | ^Dan joins (~xxx@89.136.142.218) |
| 11:45:16 | × | alecs quits (~alecs@nat16.software.imdea.org) (Quit: alecs) |
| 11:46:51 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 11:47:24 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 11:52:17 | × | ^Dan quits (~xxx@89.136.142.218) (Remote host closed the connection) |
| 12:01:42 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 12:03:42 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 12:03:45 | → | chele joins (~chele@user/chele) |
| 12:08:44 | × | ash3en quits (~Thunderbi@89.56.182.235) (Quit: ash3en) |
| 12:08:53 | × | alp quits (~alp@2001:861:8ca0:4940:1861:ecb2:15d3:3a1d) (Ping timeout: 248 seconds) |
| 12:08:53 | → | ash3en1 joins (~Thunderbi@89.56.182.235) |
| 12:09:46 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 12:10:17 | → | rvalue joins (~rvalue@user/rvalue) |
| 12:11:17 | ash3en1 | is now known as ash3en |
| 12:17:29 | × | amir quits (sid22336@user/amir) (Quit: Connection closed for inactivity) |
| 12:20:37 | → | alfiee joins (~alfiee@user/alfiee) |
| 12:23:18 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 12:24:16 | → | euleritian joins (~euleritia@95.90.214.149) |
| 12:25:30 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 12:34:44 | × | kh0d quits (~kh0d@109.111.226.14) (Remote host closed the connection) |
| 12:35:15 | × | ash3en quits (~Thunderbi@89.56.182.235) (Quit: ash3en) |
| 12:35:27 | → | ash3en1 joins (~Thunderbi@89.56.182.235) |
| 12:37:45 | ash3en1 | is now known as ash3en |
| 12:42:40 | → | kh0d joins (~kh0d@109.111.226.14) |
| 12:45:09 | × | loonycyborg_ quits (loonycybor@chat.chantal.wesnoth.org) (Ping timeout: 265 seconds) |
| 12:45:46 | → | tabaqui joins (~tabaqui@167.71.80.236) |
| 12:47:27 | → | loonycyborg joins (loonycybor@wesnoth/developer/loonycyborg) |
| 12:47:35 | × | hughjfchen quits (~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3) |
| 12:47:55 | → | hughjfchen joins (~hughjfche@vmi2417424.contaboserver.net) |
| 12:48:43 | × | kh0d quits (~kh0d@109.111.226.14) (Ping timeout: 245 seconds) |
| 12:49:30 | × | hughjfchen quits (~hughjfche@vmi2417424.contaboserver.net) (Client Quit) |
| 12:50:45 | → | dolio joins (~dolio@130.44.140.168) |
| 12:50:48 | → | hughjfchen joins (~hughjfche@vmi2417424.contaboserver.net) |
| 12:54:03 | → | jespada joins (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) |
| 12:54:44 | × | jespada quits (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Client Quit) |
| 12:55:41 | × | ash3en quits (~Thunderbi@89.56.182.235) (Quit: ash3en) |
| 12:55:50 | → | jespada joins (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) |
| 12:55:57 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 12:56:41 | → | kh0d joins (~kh0d@109.111.226.14) |
| 13:01:20 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 13:03:04 | × | ash3en quits (~Thunderbi@89.56.182.235) (Ping timeout: 260 seconds) |
| 13:04:08 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 13:05:42 | → | alfiee joins (~alfiee@user/alfiee) |
| 13:06:26 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 248 seconds) |
| 13:10:09 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 13:18:22 | → | alp joins (~alp@2001:861:8ca0:4940:ce87:6c75:c7a9:f360) |
| 13:23:37 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 13:29:01 | → | weary-traveler joins (~user@user/user363627) |
| 13:30:51 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 244 seconds) |
| 13:32:49 | → | Guest84 joins (~Guest84@14.139.38.105) |
| 13:36:19 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 260 seconds) |
| 13:42:58 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 13:43:02 | × | alp quits (~alp@2001:861:8ca0:4940:ce87:6c75:c7a9:f360) (Ping timeout: 272 seconds) |
| 13:43:14 | → | califax joins (~califax@user/califx) |
| 13:44:46 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 13:45:41 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 13:45:44 | × | Guest84 quits (~Guest84@14.139.38.105) (Quit: Client closed) |
| 13:50:45 | → | alfiee joins (~alfiee@user/alfiee) |
| 13:52:00 | × | sabathan quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 13:55:34 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 13:56:06 | → | sabathan joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 14:03:51 | × | poscat quits (~poscat@user/poscat) (Quit: Bye) |
| 14:11:22 | → | Digitteknohippie joins (~user@user/digit) |
| 14:11:40 | × | Digit quits (~user@user/digit) (Ping timeout: 244 seconds) |
| 14:11:50 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:12:36 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 14:15:26 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 14:17:20 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 14:20:16 | → | poscat joins (~poscat@user/poscat) |
| 14:21:02 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 272 seconds) |
| 14:24:03 | × | kh0d quits (~kh0d@109.111.226.14) (Remote host closed the connection) |
| 14:26:37 | → | kh0d joins (~kh0d@109.111.226.14) |
| 14:31:13 | × | kh0d quits (~kh0d@109.111.226.14) (Ping timeout: 245 seconds) |
| 14:31:14 | × | adamCS quits (~adamCS@pool-100-33-104-162.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 14:31:14 | × | doyougnu- quits (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Ping timeout: 252 seconds) |
| 14:31:23 | → | adamCS joins (~adamCS@pool-100-33-104-162.nycmny.fios.verizon.net) |
| 14:32:48 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 246 seconds) |
| 14:33:16 | → | doyougnu joins (~doyougnu@syn-045-046-170-068.res.spectrum.com) |
| 14:33:40 | Digitteknohippie | is now known as Digit |
| 14:35:33 | × | noteness_ quits (~noteness@user/noteness) (Ping timeout: 248 seconds) |
| 14:35:50 | → | alfiee joins (~alfiee@user/alfiee) |
| 14:36:39 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 252 seconds) |
| 14:37:51 | → | noteness joins (~noteness@user/noteness) |
| 14:38:17 | × | jespada quits (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 14:40:29 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 14:46:35 | → | jespada joins (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) |
| 14:49:02 | → | myme joins (~myme@2a01:799:d5e:5f00:69c6:1b0c:ff6d:bdea) |
| 14:49:15 | → | Buliarou1 joins (~gypsydang@46.232.210.139) |
| 14:49:51 | → | kh0d joins (~kh0d@109.111.226.14) |
| 14:50:06 | → | as__ joins (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) |
| 14:51:04 | → | SlackCoder joins (~SlackCode@64-94-63-8.ip.weststar.net.ky) |
| 14:52:53 | × | euleritian quits (~euleritia@95.90.214.149) (Read error: Connection reset by peer) |
| 14:54:42 | → | euleritian joins (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
| 14:57:03 | → | ft joins (~ft@p508db463.dip0.t-ipconnect.de) |
| 14:58:04 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 14:59:01 | × | euleritian quits (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 14:59:19 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 15:02:14 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 15:02:16 | → | notdabs joins (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) |
| 15:02:24 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 15:06:48 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 15:07:07 | → | euleritian joins (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
| 15:07:58 | × | euleritian quits (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:08:17 | → | euleritian joins (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
| 15:11:49 | × | as__ quits (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 244 seconds) |
| 15:12:25 | → | as___ joins (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) |
| 15:14:20 | → | berzerk joins (~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24) |
| 15:15:06 | × | bsima quits (~bsima@143.198.118.179) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:15:31 | → | bsima joins (~bsima@143.198.118.179) |
| 15:16:48 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 15:16:55 | <absence> | When using a constraint called Subset, which takes two type-level lists, I find myself having to use "Subset (x : list1) (x : list2) => ..." instead of just "Subset list1 list2". Is there a way to convince the type checker that the x is superfluous? |
| 15:17:53 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 15:18:44 | <tomsmeding> | absence: I have a feeling that this is an X-Y problem, and that the answer is a common-ish trick that I don't know a name for: define an associated type family to your class where the right-hand sides are precisely the instance contexts, then add that type family as a _superclass_ constraint to the class |
| 15:19:26 | <tomsmeding> | that allows ghc to, given an `instance C A => C T` not only infer `C T` from `C A`, but furthermore conclude from evidence of `C T` that `C A` must also hold |
| 15:19:35 | <tomsmeding> | the latter is normally _not_ what GHC does |
| 15:19:58 | <tomsmeding> | if you don't know what I'm talking about, or don't know how it applies to your case, you'll have to share the definition of that Subset thing |
| 15:20:11 | <absence> | Can I do that if the constraint and the function that needs it are defined in a third-party library? |
| 15:20:29 | <tomsmeding> | no |
| 15:20:33 | <tomsmeding> | you have to modify the class |
| 15:20:50 | <tomsmeding> | I'm not 100% sure this is what you are running into, but it has a similar "vibe" :p |
| 15:20:54 | → | alfiee joins (~alfiee@user/alfiee) |
| 15:21:17 | <absence> | Here's the constraint by the way: https://hackage.haskell.org/package/effectful-core-2.5.1.0/docs/src/Effectful.Internal.Effect.html#Subset |
| 15:21:38 | × | taktoa[c] quits (sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 244 seconds) |
| 15:22:45 | <tomsmeding> | ah, so `Subset list1 list2 => Subset (x : list1) (x : list2)` itself isn't even directly derivable |
| 15:22:57 | → | taktoa[c] joins (sid282096@id-282096.tinside.irccloud.com) |
| 15:23:29 | <absence> | Speaking of vibes, it feels vaguely similar to "(Monad (t m), Monad m, MonadTrans t) =>", so maybe something something QuantifiedConstraints...? |
| 15:23:42 | × | jackdk quits (sid373013@cssa/jackdk) (Ping timeout: 244 seconds) |
| 15:23:43 | × | aristid quits (sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 268 seconds) |
| 15:24:29 | <int-e> | Looks like Subset (x : list1) (x : list2) should simplify to Subset list1 (x : list2), but there's nothing that ensures that list1 doesn't contain another x... |
| 15:24:37 | <tomsmeding> | absence: Note that `Subset (x : list1) (x : list2)` is NOT equivalent to `Subset list1 list2`: the former allows elements of list1 to be equal to x, whereas the latter only allows that if x is in list2 |
| 15:24:44 | <tomsmeding> | that |
| 15:25:08 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 15:25:56 | → | jackdk joins (sid373013@cssa/jackdk) |
| 15:26:47 | → | aristid joins (sid1599@id-1599.uxbridge.irccloud.com) |
| 15:28:31 | × | berzerk quits (~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds) |
| 15:30:27 | × | as___ quits (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds) |
| 15:31:12 | <absence> | I'm not sure I see how adding an x to both of them breaks the subset relationship... |
| 15:31:36 | <tomsmeding> | absence: sure, Subset a b implies Subset (x:a) (x:b). But the other way round does not hold |
| 15:32:01 | <tomsmeding> | [1,1] is a subset of [1,2], but [1] is not a subset of [2] |
| 15:32:49 | <absence> | Oh right, that makes sense. |
| 15:33:18 | <tomsmeding> | Now, even the implication `Subset a b => Subset (x:a) (x:b)` is not directly inferrable from the given instances, but you could prove it perhaps, given singletons for those lists |
| 15:33:35 | <EvanR> | x = x ? |
| 15:33:54 | <tomsmeding> | > x == x |
| 15:33:55 | <lambdabot> | True |
| 15:33:57 | <tomsmeding> | seems so |
| 15:33:58 | <EvanR> | oh was reading : as "type off" |
| 15:34:00 | <EvanR> | er |
| 15:34:04 | <EvanR> | type O |
| 15:34:24 | <tomsmeding> | we're in #haskell, not in #agda ;) |
| 15:36:10 | <absence> | Proving things with singletons sounds like it will quickly escalate into "not worth it". :p |
| 15:37:14 | <tomsmeding> | also not particularly efficient. |
| 15:37:28 | <EvanR> | was just reading about "presets" which are setoids (a set that comes equipped with an equivalence relation) without the equivalence relation provided. And then it explained "a preset becomes a set if you give it a relation which.... is reflexive (x = x)" |
| 15:38:11 | <EvanR> | xD |
| 15:38:41 | <EvanR> | (and other properties but, they also involve "=") |
| 15:40:22 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 268 seconds) |
| 15:41:13 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 15:41:51 | × | jespada quits (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 15:42:54 | <EvanR> | ok I got confused, = is the relation being defined |
| 15:43:13 | × | euleritian quits (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:43:39 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 15:45:40 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 15:50:04 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 15:50:26 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 252 seconds) |
| 15:50:52 | → | euleritian joins (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
| 15:51:18 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 15:55:39 | → | vpan joins (~vpan@212.117.1.172) |
| 16:00:29 | <roconnor> | EvanR: PERs: Partial Equivalence Relations |
| 16:01:17 | <EvanR> | yes? |
| 16:03:14 | <roconnor> | Oh I misunderstood what your presets were. |
| 16:03:29 | <roconnor> | I though they were setoids without reflexivity. |
| 16:04:31 | <EvanR> | I actually veered off, the presets are "sets" without equality among the elements |
| 16:04:57 | <EvanR> | (yet) |
| 16:05:51 | <EvanR> | so x doesn't equal x because equal doesn't exist |
| 16:06:58 | → | alfiee joins (~alfiee@user/alfiee) |
| 16:07:55 | × | euleritian quits (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Ping timeout: 244 seconds) |
| 16:07:55 | → | Square joins (~Square@user/square) |
| 16:11:20 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 16:23:03 | × | notdabs quits (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) (Remote host closed the connection) |
| 16:23:06 | <haskellbridge> | <Bowuigi> How are those useful? I mean, order dependency is nice but do they make something more elegant? |
| 16:23:25 | → | notdabs joins (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) |
| 16:24:58 | <haskellbridge> | <Bowuigi> Quotients become central in proofs, that's nice |
| 16:26:29 | × | acidjnk quits (~acidjnk@p200300d6e71c4f937555fc5a67c80b19.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 16:27:09 | → | euleritian joins (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) |
| 16:27:37 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 16:28:33 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Client Quit) |
| 16:29:23 | <EvanR> | something about foundations https://ncatlab.org/nlab/show/preset |
| 16:30:05 | <EvanR> | it was the 60s, so maybe they were tripping AF |
| 16:31:49 | <EvanR> | also you could attempt to construe haskell's datatypes as presets because not all of them have a way to, at least decidably, know two values are equal |
| 16:32:20 | <EvanR> | either because there's no Eq instance or because more serious issues |
| 16:33:10 | <haskellbridge> | <Bowuigi> The concept of prefunction seems useful |
| 16:33:58 | <EvanR> | yes we have functions between types that might not agree with one or more notions of equality we have in mind on the domains |
| 16:34:03 | <haskellbridge> | <Bowuigi> Being able to ignore equality means that you can inspect the internal structure of something without that being in "normal form" |
| 16:35:25 | <EvanR> | or you could talk about, however you did it, any function you manage to define automatically preserves (a) notion of equality |
| 16:35:41 | <EvanR> | which we might take for granted and otherwise never had language for |
| 16:36:30 | <EvanR> | (automatically preserves equality, perhaps without using normal forms) |
| 16:36:42 | <haskellbridge> | <Bowuigi> That's usually called congruence I think |
| 16:37:58 | <EvanR> | sounds like a luxury to be able to pick a "real" equality relation so you can call other mappings congruence |
| 16:38:10 | <EvanR> | or homomorphism |
| 16:43:58 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 16:45:23 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 16:48:56 | × | vpan quits (~vpan@212.117.1.172) (Quit: Leaving.) |
| 16:49:50 | × | Square quits (~Square@user/square) (Ping timeout: 252 seconds) |
| 16:50:19 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 16:52:42 | → | alfiee joins (~alfiee@user/alfiee) |
| 16:56:34 | → | j1n37 joins (~j1n37@user/j1n37) |
| 16:56:59 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 16:57:27 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 17:10:09 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:11:14 | × | euleritian quits (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:11:33 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 17:11:36 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 17:12:31 | chiselfu1e | is now known as chiselfuse |
| 17:16:30 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 17:16:52 | → | euleritian joins (~euleritia@95.90.214.149) |
| 17:17:25 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:20:59 | × | euleritian quits (~euleritia@95.90.214.149) (Ping timeout: 252 seconds) |
| 17:21:55 | → | euleritian joins (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) |
| 17:24:29 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:25:41 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 17:26:44 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 17:27:28 | <EvanR> | so we can go from, imperative language with "functions" doesn't have real functions because they do side effects, or depend on invisible state, etc. to functional language with "functions" futhermore doesn't have functions because it doesn't preserve the equality xD |
| 17:27:34 | <EvanR> | no true function |
| 17:32:56 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 17:37:44 | → | jespada joins (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) |
| 17:38:46 | → | alfiee joins (~alfiee@user/alfiee) |
| 17:41:16 | <__monty__> | I'm not sure that's entirely rigorous. Nowhere do the definitions require that the notion of equality is part of the language of the functions, right? |
| 17:43:12 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 17:43:26 | <c_wraith> | No, though if you're strictly in math... If the objects in the pairs that make up a formal function can be compared for equality, then functions are equal if they contain the same set of pairs. |
| 17:43:41 | <c_wraith> | It gets much harder when you want equality to be computable |
| 17:43:59 | × | euleritian quits (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:44:03 | <EvanR> | if x = y then f(x) = f(y) can be |
| 17:44:22 | <EvanR> | derived from the usual definition of functions in set theory |
| 17:45:53 | <EvanR> | and is otherwise a pretty common rule to rely on |
| 17:45:54 | → | euleritian joins (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) |
| 17:46:09 | <EvanR> | even though it's wrong! |
| 17:46:45 | × | dhil quits (~dhil@2a0c:b381:52e:3600:dd6a:fa62:e132:ec11) (Ping timeout: 265 seconds) |
| 17:47:22 | × | euleritian quits (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:47:40 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 17:47:57 | <EvanR> | e.g. in a possible implementation of computable reals, you could have rational real which terminates and is easy to compute with, and another real which converges to the same rational, and causes the f to explode when applied to it |
| 17:48:38 | <EvanR> | (though now you might argue the f is not really a function after all, since it's observing a difference, which is the same point as above) |
| 17:52:23 | <haskellbridge> | <Bowuigi> It's only wrong from an undecidability/non-termination standpoint |
| 17:52:34 | <haskellbridge> | <Bowuigi> Even then, it holds for PERs IIRC |
| 17:53:04 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 17:53:37 | <haskellbridge> | <Bowuigi> Congruence is derivable in various type theories as well, even without identity types |
| 17:53:53 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 17:55:24 | <EvanR> | another example is treating zero and minus zero differently in floats. Another example is implementing rationals with two numbers, and mapping 1/2 and 2/4 to false and true respectively (assuming false and true are not equal) |
| 17:56:10 | <EvanR> | though in these cases indeed x = x, which is what got me started on this |
| 17:56:23 | <sim590> | foo |
| 17:56:29 | <EvanR> | except for NaN |
| 17:56:54 | → | xeno11 joins (~xeno11@c-69-140-170-168.hsd1.de.comcast.net) |
| 17:57:07 | <sim590> | test |
| 17:58:31 | <EvanR> | failed |
| 17:58:33 | <haskellbridge> | <Bowuigi> IEEE-754 floats are so weird |
| 17:58:43 | <sim590> | :) |
| 17:59:18 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 18:00:28 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 18:00:33 | <xeno11> | To anyone that can help/edit wiki... haskell wikibook main page was edited. It seems "Haskell is pure" was changed to "JEWS ARE THE BEST |
| 18:00:34 | <xeno11> | LIRON WAS THE CREATOR OF COMPUTERS" and other changes might have been made. |
| 18:01:20 | <xeno11> | https://en.wikibooks.org/wiki/Haskell |
| 18:01:20 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 18:01:21 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds) |
| 18:02:06 | → | euleritian joins (~euleritia@95.90.214.149) |
| 18:03:14 | <EvanR> | seems like the kind of thing the wiki infrastructure would flag automatically |
| 18:08:46 | → | tromp joins (~textual@2a02:a210:cba:8500:40b3:acb4:4579:83af) |
| 18:12:29 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:14:00 | × | kh0d quits (~kh0d@109.111.226.14) (Remote host closed the connection) |
| 18:20:59 | <haskellbridge> | <Bowuigi> Who's Liron and why did they create computers? |
| 18:22:01 | <dminuoso> | More importantly, why did they even name them computers and did they have the authority to do so? |
| 18:22:54 | → | acidjnk joins (~acidjnk@p200300d6e71c4f6518434db087d421fc.dip0.t-ipconnect.de) |
| 18:24:50 | → | alfiee joins (~alfiee@user/alfiee) |
| 18:25:31 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 18:28:56 | → | kh0d joins (~kh0d@212.200.65.86) |
| 18:29:12 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 18:30:13 | <EvanR> | In the beginning the Universe was created. |
| 18:30:13 | <EvanR> | This had made many people very angry and has been widely regarded as a bad move. |
| 18:31:36 | → | alp joins (~alp@2001:861:8ca0:4940:4f32:5e1f:632d:94e1) |
| 18:31:56 | Clint | golfclaps. |
| 18:43:13 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 18:44:08 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 18:44:57 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 18:45:22 | × | ash3en quits (~Thunderbi@89.56.182.235) (Ping timeout: 268 seconds) |
| 18:47:12 | <ski> | EvanR : "you could attempt to construe haskell's datatypes as presets because not all of them have a way to, at least decidably, know two values are equal" -- it's useful to consider an intended semantic equality, not necessarily decidable, on various Haskell data types |
| 18:47:16 | → | Pixi` joins (~Pixi@user/pixi) |
| 18:47:24 | <ski> | e.g. for `Set's and `Map's considering ones which have the same elements/associations, but represented differently internally, asb being "equal". also not including imbalanced representations as valid representations of the semantic values. leading to having an abstract data type that is intended to be a quotient type of a subset type of the representation type |
| 18:47:57 | <ski> | laws for `Eq' could be `x == y = True => x = y' and `x == y = False => x =/= y', where `=' is semantic equality (an equivalence relation on the representations), and `=/=' is semantic inrquality (an apartness relation on the representations) |
| 18:48:17 | <ski> | Mercury has (a bit) more explicit support for this, by allowing you to attach a user-defined equality (which is not just "another computable function", but is tied semantically to reasoning laws, and possibly used by some optimizations), causing the data constructor to become non-injective, matching on it is (committed-choice, .. |
| 18:48:38 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 18:48:50 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 18:48:50 | <ski> | .., the implementation arbitrarily choosed one representation) multi-deterministic (could semantically result in any one of one or more possible results), "tainting" the matching operation to be committed-choice multi-deterministic, .. |
| 18:48:56 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 272 seconds) |
| 18:49:00 | <ski> | .., until you at some point decide to use a `promise_equivalent_solutions' pragma (proof obligation) to claim that at this point you'll get the same result regardless of which representation was observed (or else you can let `main' be comitted-choice multi-deterministic, which you could also do for concurrency, with race conditions possibly affecting result) |
| 18:50:07 | × | Pixi` quits (~Pixi@user/pixi) (Read error: Connection reset by peer) |
| 18:56:56 | → | zzz joins (~z@user/zero) |
| 18:57:58 | × | yin quits (~z@user/zero) (Read error: Connection reset by peer) |
| 18:58:02 | zzz | is now known as yin |
| 19:00:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:00:03 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:47 | → | caconym joins (~caconym@user/caconym) |
| 19:01:06 | × | forell quits (~forell@user/forell) (Ping timeout: 252 seconds) |
| 19:04:46 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:06:30 | × | xeno11 quits (~xeno11@c-69-140-170-168.hsd1.de.comcast.net) (Ping timeout: 240 seconds) |
| 19:10:14 | → | alfiee joins (~alfiee@user/alfiee) |
| 19:13:30 | → | laurapigeon joins (~laura@205.124.7.51.dyn.plus.net) |
| 19:14:33 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 19:15:49 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:18:30 | <laurapigeon> | Hello! I hope this is the right place to troubleshoot build issues- I'm on a fork of arch linux with the following packages from the arch repos: ghc, cabal-install, stack, haskell-language-server. I can access ghci, import modules and load my own .hs files. But when I try to run `ghc --make helloworld` in a folder with hello world I get the following error. When I try to run ghc-pkg check I get a series of errors like the following, |
| 19:18:31 | <laurapigeon> | terminated by the following: https://paste.tomsmeding.com/akUj6oxa |
| 19:19:06 | <laurapigeon> | Sorry if this is the wrong place or way to ask, I'm new to IRC |
| 19:19:32 | <geekosaur> | arch and derivatives don't ship static libs, which ghc uses by default. add `-dynamic` |
| 19:20:31 | <geekosaur> | I think there's a package to get static libs for ghc bootlibs, but not for additional packages |
| 19:20:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:20:49 | <yushyin> | yeah, ghc-static |
| 19:20:56 | <laurapigeon> | Perfect- that worked, thanks a bunch |
| 19:22:03 | <laurapigeon> | getting ghc-static from extra made the original command work too, nice! |
| 19:22:30 | <yushyin> | laurapigeon: https://wiki.archlinux.org/title/Haskell#Static_linking for more information on the static approach |
| 19:23:37 | → | xeno11 joins (~xeno11@c-69-140-170-168.hsd1.de.comcast.net) |
| 19:24:34 | <laurapigeon> | oh a reading issue on my part, good to know this is here |
| 19:29:03 | → | Square joins (~Square@user/square) |
| 19:31:27 | <sim590> | I read on multiple posts on the Web that we categorize a function as "unpure" if it has side-effects and furturemore that when calling that function twice, if it doesn't produce the "same" ouptput for the both calls, then it is not pure. To me, this can only apply to IO and only IO is unpure. I read some places that people assume Monads are unpure, but to me it is not the case, because "side |
| 19:31:29 | <sim590> | effects" of monads are actually just behind the scene just like with the do operator, it is syntaxic sugar, but in the end, there were no side effects, just some computation abstracted away, but this doesn't mean that in two separate calls of a function that is wrapped in a monad that we supply the same argument because the monad actually hides the abstracted some of the arguments and both |
| 19:31:31 | <sim590> | function calls had indeed different arguments. Therefore, am I right to say that only IO is impure and that for example, the State monad or even the Maybe monad are not unpure. They are indeed pure? |
| 19:31:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:31:56 | <mauke> | <laurapigeon> [...] I'm new to IRC <- no worries, you're doing great so far |
| 19:34:00 | <mauke> | sim590: if you're taking that approach, then IO is pure, too |
| 19:34:15 | <EvanR> | sim590, an impure function is a function that's not pure. A pure function is a (something) which only depends on the input and has side effects (that you care about) |
| 19:34:50 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 19:34:54 | <EvanR> | IO actions don't have a function type in the first place |
| 19:35:03 | <EvanR> | so this doesn't directly apply |
| 19:35:13 | <mauke> | consider, for example: main1 = putStrLn "." >> putStrLn "." >> putStrLn "."; main2 = let x = putStrLn "." in x >> x >> x |
| 19:35:14 | <EvanR> | you don't give them input |
| 19:35:31 | <tomsmeding> | laurapigeon: I know it's convenient to be able to get haskell tooling from the system package manager, but do consider using ghcup ( https://www.haskell.org/ghcup/ ) instead, if you haven't already -- besides being the main supported way to get haskell tooling these days, it also gives you much more flexibility with versions etc. |
| 19:35:56 | <sim590> | EvanR, mauke: I'm not sure if I should understand that you are agreeing together or not. |
| 19:35:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:36:11 | <mauke> | putStrLn is "pure" in the sense that whenever you call it with a particular string, it returns an IO value that is equivalent to any other IO value returned from putStrLn with the same argument |
| 19:36:57 | <mauke> | we're not at odds, I think |
| 19:37:26 | <mauke> | I'm talking about the purity of functions like putStrLn, which is indeed a function, and not the purity of IO (), which is not a function |
| 19:38:05 | <sim590> | Of course, when i said I was talking about IO, I was talking about the function which are warapped inside IO. |
| 19:38:16 | <EvanR> | sim590, I'm trying to clarify your premise using traditional jargon |
| 19:38:30 | <EvanR> | "IO is/is not pure" doesn't fit this for categorical reasons |
| 19:38:31 | <mauke> | A -> IO B, I hope, not IO (A -> B) |
| 19:38:51 | <sim590> | mauke: indeed. |
| 19:38:57 | <EvanR> | sim590, there's not necessarily any IO wrapped inside IO |
| 19:39:02 | <EvanR> | alskdjf |
| 19:39:05 | <EvanR> | any function wrapped inside IO |
| 19:39:36 | <EvanR> | it's a big difference from imperative I/O code |
| 19:39:48 | <EvanR> | IO actions are first class values you can pass around and store in structures |
| 19:39:58 | <EvanR> | but they don't take any arguments or input |
| 19:40:07 | <EvanR> | it's just a thing that can be executed |
| 19:40:13 | <ski> | sim590 : "this can only apply to IO and only IO is unpure" -- no, things like e.g. internal state, indeterminacy, continuations, could also cause being side-effects, not just Input/Output communication with the OS |
| 19:40:18 | <EvanR> | and purity of functions is about... functions |
| 19:40:24 | <ski> | sim590 : "\"side effects\" of monads are actually just behind the scene just like with the do operator, it is syntaxic sugar" -- `do' is indeed syntactic sugar, but you can't invoke that to claim something about side-effects or not of monads |
| 19:40:32 | <sim590> | w`e mauke said is what I mean. Any function `f :: [[...] A -> ] IO a` if I can write it like that where `[]` means it's optional.. |
| 19:40:34 | <ski> | sim590 : "in the end, there were no side effects, just some computation abstracted away" -- you could perhaps phrase it like this, depending on what you mean by this. "calls of a function that is wrapped in a monad" is vague/confusing phrasing (specifically "wrapped in a monad", although also potentially "call") |
| 19:40:41 | <ski> | sim590 : "am I right to say that only IO is impure" -- `IO' is not impure |
| 19:41:06 | <EvanR> | sim590, well if you have putChar :: Char -> IO (), the important part here is the IO, not the -> |
| 19:41:10 | <EvanR> | that function is pure |
| 19:41:17 | <EvanR> | but you're calling the IO impure |
| 19:41:30 | <EvanR> | calling that function doesn't execute anything |
| 19:43:03 | <sim590> | ski: I'm not writing a scientific paper here. I'm discussing and I hope people can grasp what I mean, assuming that I have read and wrote Haskell for at least 5 years now. |
| 19:44:24 | × | laurapigeon quits (~laura@205.124.7.51.dyn.plus.net) (Quit: Konversation terminated!) |
| 19:44:25 | <sim590> | EvanR: I'm just saying that the set of functions that CAN be impure reside in the set that contains functions of the return type that is `IO a` where a could also be `()`. |
| 19:44:35 | <ski> | sim590 : yes. but it's important to try to better understand the relevant concepts and distinctions (and non-distinctions), and to that end it helps being more strict about terminology, for beginners, to understand what is being claimed and not claimed, to understand the essentials of the situaation, and to ensure that we have a common ground for further conversation |
| 19:44:45 | <sim590> | by "reside", I mean contained in. |
| 19:45:34 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 19:45:47 | <ski> | there is no "`IO' is side-effectful, but other monads are not". this is not a relevant distinction, in Haskell |
| 19:46:29 | <sim590> | I'm talking about the functions inside the set of functions why have a return type `IO a` where `a` can be `()` also. |
| 19:46:43 | <sim590> | s/why/which/ |
| 19:46:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:47:03 | <EvanR> | sim590, IO doesn't contain functions... I just get the feeling you're down the wrong path a few miles with the concepts |
| 19:47:10 | <sim590> | I'm not saying IO is a set |
| 19:47:12 | → | Pixi joins (~Pixi@user/pixi) |
| 19:47:19 | × | tv quits (~tv@user/tv) (Quit: derp) |
| 19:47:25 | <sim590> | I'm talkinga bout THE SET of functions which have a return type `IO a`. |
| 19:47:35 | <EvanR> | all those functions are pure |
| 19:47:36 | → | tv joins (~tv@user/tv) |
| 19:47:41 | <EvanR> | since all functions in haskell are pure |
| 19:47:55 | <EvanR> | it's purely functional |
| 19:48:13 | <ski> | "the set of functions that CAN be impure" -- there are zero such functions, in Haskell (unless you unsafe escape hatches like `unsafePerformIO', which comes with proof obligations for the programmer in order to use safely) (there is also an argument that non-termination (and partiality) can be viewed as a side-effect, albeit more "benign" than most other ones. if you want to, we could discuss this, but |
| 19:48:19 | <ski> | otherwise i'll assume we agree to disregard these) |
| 19:50:13 | <sim590> | EvanR: to me, IO functions have side effects. I can call some IO action which will act on a MVar value and at some point my program, it might terminate and at some other point it might not because another thread has not acted on that MVar value also. |
| 19:50:30 | <sim590> | This is the kind of side-effects which I see IO allowing. |
| 19:51:11 | × | jespada quits (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 19:52:14 | <sim590> | And depending on that circumstance, the function might return 0 or else 1. |
| 19:52:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 19:52:17 | <EvanR> | sim590, you're focusing on functions returning IO, but that's not how you get side effects |
| 19:52:18 | <sim590> | For e.g. |
| 19:52:22 | <ski> | sim590 : the main point here is that, unless in languages with side-effects, we have reasoning (including for refactoring) laws which doesn't have to take potential side-effects into account, can be more general ("aggressive"), you can "replace equals by equals". `let x = putStrLn "foo" in do x; x' is equal (equivalent) to `do putStrLn "foo"; putStrLn "foo";'. in C, `{ int n = puts("foo"); n; n }' is not |
| 19:52:28 | <ski> | equivalent to `{ puts("foo"); puts("foo") }' |
| 19:52:34 | <EvanR> | e.g. getChar :: IO Char will get a char, it's not a function |
| 19:53:03 | <EvanR> | meanwhile [putChar 'a', getChar, putChar 'b'] is a list constructed using such functions, but they don't cause side effects |
| 19:53:33 | <ski> | sim590 : it does not matter here, what happens "under the hood", whether you'd consider the implementation (not necessarily in Haskell) to "be side-effectful". what matters is how you can reason and observe about program fragments, "at the level of the language" |
| 19:53:47 | <EvanR> | but you can execute all three actions contained there in as its own IO action (with no -> involved at that point) |
| 19:55:59 | → | alfiee joins (~alfiee@user/alfiee) |
| 19:56:00 | <ski> | sim590 : "I can call some IO action which will act on a MVar value and at some point my program, it might terminate and at some other point it might not because another thread has not acted on that MVar value also." -- you're not calling it. calling is for functions. `IO'-actions are not functions. calling `putStrLn' as in the call `putStrLn "foo"' always gives the same result value (that value being an |
| 19:56:03 | <sim590> | EvanR: "getChar is not a function" .... "[putChar 'a', getChar, putChar 'b'] is a list constructed using such FUNCTIONS" .... I'm not sure I understand. |
| 19:56:06 | <ski> | `IO'-action, a "recipe" for what I/O operations to (possibly) later perform). later, you can invoke/run/perform this action, and that is what causes observable input/output interactions to happen |
| 19:56:17 | <EvanR> | sim590, well, putChar is one your functions |
| 19:56:22 | <EvanR> | that you think has side effects |
| 19:56:29 | <EvanR> | (it doesn't, this demonstrates why) |
| 19:56:49 | <EvanR> | getChar is in the same boat as the result of putChar, but is not a function |
| 19:57:03 | <EvanR> | these are counterexamples to your theory |
| 19:57:20 | <ski> | `IO'-actions (explicitly) express (Input/Output-) effects. the "explicitly" part is why this is not *side*-effects (which would be implicit) |
| 19:58:08 | <sim590> | EvanR: are you saying that `f :: a` is not a function ?& |
| 19:58:24 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 260 seconds) |
| 19:59:11 | <EvanR> | f :: a is not a function |
| 20:00:00 | <ski> | the type of a `getChar' expression is `IO Char', not `Char'. in C, the type of `getchar()' is `char'. so, in C, expressions of type char, when evaluated, may implicitly cause effects, on the *side* (not explicitly accounted for, in the interface of `getchar', being `int getchar(void);'). while in Haskell, evaluating `getChar' will not cause any effects, it will just compute a value of type `IO Char' (an |
| 20:00:06 | <ski> | `IO'-action) for you. only by running/executing/invoking this value (this action), will you get an actual `Char' to work on |
| 20:00:36 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 20:00:54 | <ski> | sim590 : all functions in Haskell take exactly one argument/parameter, have a type of the general shape `(...) -> (...)'. and all expressions of such type are functions, taking one input parameter/argument |
| 20:00:55 | <sim590> | To me, this is a "constant function". It just doesn't have a parameter. Just like you we call `f(x) = 5` a function in Math. |
| 20:01:11 | <ski> | if the type is not of the shape `(...) -> (...)', then it's not a function |
| 20:01:44 | <sim590> | I guess f(x)=5 has a parameter, but it's just not used. Fine. |
| 20:02:02 | <EvanR> | (\_ -> 5) :: () -> Int would be a function |
| 20:02:16 | <EvanR> | x :: Int is not a function |
| 20:02:19 | <EvanR> | big diff |
| 20:02:47 | <EvanR> | 5 :: Int to be concrete |
| 20:02:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:03:02 | <EvanR> | it's just a 5 |
| 20:03:19 | <EvanR> | there's no argument or input to be had |
| 20:03:46 | <EvanR> | you can "lambda wrap" any value you want to put another level of "function" around it though |
| 20:03:50 | <EvanR> | might be what you were thinking |
| 20:04:16 | <EvanR> | but while [5] or [[5]] are lists, 5 isn't a list |
| 20:04:24 | <ski> | in Haskell, the effects of `getChar' and `putChar' are accounted for, explicitly, in the interfaces (type signatures), by the `IO' in `getChar :: IO Char' and `putChar :: Char -> IO ()' (and by `IO T' being a distinct type from `T', you can't implicitly treat a value of one as being a value of the other). this separation (which is similar in spirit to the old idea of "separate user interface from internal |
| 20:04:31 | <ski> | machinery", but is enforced in Haskell) is what makes I/O effects explicit, not implicit, not on the side, not side-effects |
| 20:04:31 | <sim590> | Who says that `getChar :: IO Char` is not actually `getChar :: () -> IO Char` behind the scene and therefore, `getChar` is a function! |
| 20:04:43 | <EvanR> | :t getChar :: () -> IO Char |
| 20:04:44 | <lambdabot> | error: |
| 20:04:44 | <lambdabot> | • Couldn't match expected type ‘() -> IO Char’ |
| 20:04:44 | <lambdabot> | with actual type ‘IO Char’ |
| 20:04:48 | <EvanR> | the type checker said so |
| 20:04:56 | <sim590> | That's what HE says. |
| 20:05:11 | <sim590> | :D |
| 20:05:34 | <EvanR> | just like 0 doesn't equal 1, () -> IO Char doesn't match IO Char |
| 20:05:44 | <EvanR> | and if they did it would be bad |
| 20:05:48 | <ski> | "behind the scene" or "under the (implementation covers)" doesn't matter. what matters is the interface presented to you, at the level of the language, what can be observed there, what reasoning laws you have available that preserve observable behaviour |
| 20:06:09 | × | michalz quits (~michalz@185.246.207.193) (Remote host closed the connection) |
| 20:09:50 | <ski> | GHC happens to represent `IO Char' as something like `RealWorld -> (Char,RealWorld)', internally, but this is carefully set up, and easy to mess up (largely, but not only, because Haskell has no support for checking uniqueness, unlike Clean and Mercury. even if that was added, other aspects of `IO' (concurrency, exceptions, ..) is not accurately explicitly reflected here ..), internal representation (which, |
| 20:09:51 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 20:09:56 | <ski> | if you'd fool around with it, would allow you to express side-effecting computations, yes). this should be treated as an internal implementation detail, which just happens to be expressed in an internal language which happens to *look* like Haskell, for convenience |
| 20:10:33 | <ski> | and other Haskell implementations have internally represented `IO' in other ways (e.g. non-function ones, unlike the above) |
| 20:11:05 | <EvanR> | the RealWorld -> implementation is weird and not particular helpful to using IO normally |
| 20:11:18 | <ski> | yes |
| 20:11:19 | <EvanR> | but I see it comes up in the guts of low level I/O stuff |
| 20:12:19 | <ski> | sim590 : does this help ? |
| 20:13:36 | <ski> | @quote /bin/ls |
| 20:13:36 | <lambdabot> | shachaf says: getLine :: IO String contains a String in the same way that /bin/ls contains a list of files |
| 20:13:37 | <sim590> | ski: by that logic, I could say that a function `f :: Int -> State Int Int` which returns the value of the state + its input would be unpure because from what I CAN SEE, when I call `runState (f 0 >> put 1 >> f 0) 0`, `f` returned `0+0=1` the first time, while it returned `1+0=1` the second time. So, from what I can tell from the signature, it was given the same argument, but returned something |
| 20:13:39 | <sim590> | different both times, so `f` is impure. |
| 20:15:15 | <ski> | "which returns the value of the state + its input" -- it does not do this. `f' returns a value that is a `State Int'-action. the function `f' does not "returns the value of the state + its input". *invoking*/running/executing/performing this resulting action, will yield as a result "the value of the state + its input", yes |
| 20:16:13 | <ski> | i agree that if "which returns the value of the state + its input" was true, then it would be impure. but it doesn't do that, and so wouldn't need to be impure (and actually isn't) on these grounds |
| 20:16:23 | → | forell joins (~forell@user/forell) |
| 20:18:18 | <ski> | "`f` returned `0+0=1` the first time, while it returned `1+0=1` the second time" -- no. `f' returned the same action (being a recipe expressing "yield zero added to the current state"), in both calls. but *executing*/invokking/running/performing this action, twoce, yields different results, in this situation |
| 20:20:08 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 272 seconds) |
| 20:20:33 | <EvanR> | > let f n = put (n+1) >> return 0 in runState (f 0 >> put 1 >> f 0) 0 |
| 20:20:35 | <lambdabot> | (0,1) |
| 20:20:35 | <ski> | an action is a value, it is, on its own, just being, not peforming/doing/running/executing. only when an action is embedded in a larger action in a way that it'll get executed, when the larger one is, or when it's passed to a "run function" (like `runState') which executes the action, or (in the case of `IO') put as the definition of `main' (or entered into the interactor), does the action get executed |
| 20:20:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:21:19 | <EvanR> | I didn't write f right |
| 20:21:28 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 20:22:08 | <ski> | "it was given the same argument, but returned something different both times" -- no, for reasons i tried to explicate, above |
| 20:22:09 | <EvanR> | > let f n = get >>= \s -> return (n+s) in runState (f 0 >> put 1 >> f 0) 0 |
| 20:22:11 | <lambdabot> | (1,1) |
| 20:22:16 | <EvanR> | > let f n = get >>= \s -> return (n+s) in runState (f 0 >> put 1 >> f 0) 0 |
| 20:22:18 | <lambdabot> | (1,1) |
| 20:22:28 | → | ash3en joins (~Thunderbi@89.56.182.235) |
| 20:23:11 | <EvanR> | the f function is pure while the State action might be seen as "impure in context" |
| 20:23:21 | <EvanR> | again the functions don't cause any effects |
| 20:24:54 | <ski> | sim590 : you can think of a Haskell implementation as providing a run-time which consists of two main parts. (a) a part which evaluates expressions (typically lazily, but it only needs to be non-strict, so it's e.g. allowed to evaluate things ahead of time, speculatively, as long as some kind of time-out is used, and appropriate failure catching is applied, so that no behaviour difference can be noticed). |
| 20:25:00 | <ski> | for `main :: IO T', this means evaluating "what Input/Output operations/interactions to perform" |
| 20:25:17 | × | tabaqui quits (~tabaqui@167.71.80.236) (Quit: WeeChat 4.5.2) |
| 20:25:33 | <sim590> | EvanR: why would it be seen as impure? |
| 20:25:39 | <sim590> | The state action. |
| 20:25:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:25:55 | <ski> | sim590 : the other part being (b) an imperative interpreter, which inspects this the `main' recipe that we get by evaluating it, and actually performs the detailed I/O interactions |
| 20:25:58 | <EvanR> | sim590, in context |
| 20:26:09 | <sim590> | I don't get what that means. |
| 20:26:24 | <ski> | in practice, though, (a) evaluation and (b) `IO' execution are interleaved processes |
| 20:26:27 | <EvanR> | you could emulating being inside a stateful environment within the State program |
| 20:26:40 | <EvanR> | even though you're not and it's just a trick |
| 20:26:51 | <EvanR> | it just passes the state around |
| 20:27:28 | <EvanR> | but when writing a State program you think of there being an ambient state (temporarily) |
| 20:28:35 | <sim590> | Yes, you think "like" you benefit from a state, but it's actually just an abstraction. Like the previous signature of `f` was an abstraction for `f :: Int -> s -> (Int, s)`. |
| 20:28:51 | <sim590> | I guess, `s :: Int`. |
| 20:29:00 | <EvanR> | sure |
| 20:29:31 | <EvanR> | all those functions have no state though regardless |
| 20:30:03 | → | wildsalander joins (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 20:30:20 | <sim590> | That's why it's easy for me to tell that State is not impure. But, for IO, it's a bit harder. And there was a awful lot amount of text I got from both of you and I didn't understand all the explanations when I was interleaving the read from one person's explanation with the other's. |
| 20:30:37 | <EvanR> | well State action isn't a function |
| 20:31:16 | <sim590> | I know, you made that point earlier. |
| 20:31:26 | <EvanR> | so pure impure doesn't even apply |
| 20:31:31 | <EvanR> | according to my definition |
| 20:31:40 | <sim590> | I was talking about `f`. |
| 20:31:42 | <sim590> | ... |
| 20:31:58 | <EvanR> | f is a function, in Haskell, so it's pure |
| 20:32:24 | <EvanR> | same as putChar |
| 20:32:44 | <sim590> | That's a theorem of yours, but for now I'm only accepting the lemma about Monads such as State and others that are not IO. |
| 20:32:47 | <EvanR> | or put :: s -> State a () |
| 20:33:40 | <EvanR> | it's not even a monad thing |
| 20:33:49 | <EvanR> | you can access State or IO using Applicative |
| 20:33:59 | <sim590> | I know that this is a function-thing. |
| 20:33:59 | <EvanR> | you can build programs that way |
| 20:34:09 | <sim590> | But you can separate functions in subsets. |
| 20:34:46 | <EvanR> | are you still thinking that some functions are not pure? The ones that return IO ? |
| 20:35:04 | <sim590> | And I agree with the lemma that considers functions of the sets of all Haskell functions F minus the set of functions which have a return type `IO a` or `IO ()`. |
| 20:35:21 | <EvanR> | I'll take that as a yes |
| 20:36:07 | <sim590> | I would require to read something thourugh about it (not in a IRC chat where conversations are interleaving and hard to follow). Yet, I don't wish to read a scientific paper. Yet, I'd like it rigourous enough. |
| 20:36:13 | <sim590> | If that resource exists? |
| 20:36:27 | <EvanR> | you're making a mistake there, since A -> B and A -> IO () are the same kind of thing |
| 20:36:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:36:42 | <EvanR> | just returning different types |
| 20:36:58 | <EvanR> | same implementation behind the scenes |
| 20:37:04 | <EvanR> | same lack of side effects |
| 20:41:23 | → | alfiee joins (~alfiee@user/alfiee) |
| 20:41:27 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:41:35 | <ski> | "the State action might be seen as \"impure in context\"" -- this can be interpreted as meaning you can have a (state-)side-effectful language (perhaps you could have `main = let _ = f 0; _ = put 1 in f 0', which is compiled to the Haskell expresion, EvanR provided above |
| 20:42:20 | <sim590> | I don't understand how I can consider that functions in IO are pure while I see a lot on the Web people saying they try to "keep their code pure" by doing the less they can inside IO. Why would you try to do the less you can inside IO if ALL haskell functions are pure. It seems like those two statements are incompatible. |
| 20:42:37 | <EvanR> | they're using the jargon "pure" in a different sense |
| 20:42:47 | <EvanR> | in the sense of not having the IO type anywhere at all |
| 20:42:52 | <ski> | in this imperative language, you couldn't use the usual replacing-equals-by-equals reasoning that you'd do in Haskell, so it'd be side-effectful. but the implementation would compile it to (non-side-effectful) Haskell, that expresses the same effects (and behaviour in general) |
| 20:43:08 | <EvanR> | not in the sense of pure function |
| 20:45:39 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 20:45:59 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:46:14 | <EvanR> | I think whoever is saying "keep code as pure as possible" when referring to IO code, might also have similar issues if they had State everywhere |
| 20:46:34 | <EvanR> | so it's really expressing sentiment about imperative programming, not IO |
| 20:47:14 | <sim590> | EvanR: I don't believe that. Because, they can easily just do without the `do` operator and just use `>>=`. |
| 20:47:21 | <sim590> | and lambdas. |
| 20:47:29 | <EvanR> | that's just syntactic sugar |
| 20:47:34 | <sim590> | Exactly. |
| 20:47:41 | <ski> | "a lot on the Web people saying they try to \"keep their code pure\" by doing the less they can inside IO." -- what they really mean here is that they try to express a larger portion of the functionality/behaviour of the program, outside of (not entangled with) `IO'. or, another way to express it, imagining a side-effectful language (similar to the one i hinted at, for `State Int', above. having both |
| 20:47:47 | <ski> | side-effectful, and non-side-effectful functions, say), that compiles (the side-effectful functions to functions resulting in `IO' in Haskell, and the non-side-effectful functions to functions with other result types) |
| 20:47:49 | <EvanR> | using >>= and lambda will have the same issues because your pattern is still fundamentally imperative |
| 20:48:11 | <ski> | in terms of such a side-effectful language, what they mean is that they try to "keep their code pure", in that language |
| 20:48:17 | <EvanR> | you can even format it so the code doesn't look very much different from do |
| 20:48:31 | <sim590> | When you talk about Imperative programming, you talk about `do`, no ? Else, I don't see what you are talking about because there's no imperative instructions in Haskell other than the ones that are "imperative-like" thanks to the do operator. |
| 20:49:02 | <EvanR> | imperative programming means your writing sequences of statements to be executed in order |
| 20:49:08 | <sim590> | Yeah. |
| 20:49:10 | <EvanR> | whatever the syntax for that is |
| 20:49:19 | <EvanR> | formatted chain of >>= and lambda for example |
| 20:49:22 | <ski> | they're reasoning at multiple levels. (a) reasoning on the level of *evaluation* of Haskell expressions (which have no side-effects), and (b) reasoning on the level of *execution* of `IO'-actions (which you can, if you wish, think of as reasoning in a different, side-effectful, language, as sketched above) |
| 20:49:41 | <sim590> | You could say that lambdas inside lambdas are imperative programming which doesn't make sense. |
| 20:49:54 | <EvanR> | chained with >>= sure |
| 20:50:17 | <ski> | "they can easily just do without the `do` operator and just use `>>=`." -- whether they use `do' or not here is irrelevant. doesn't matter |
| 20:50:22 | <EvanR> | with semantics, execute the command, pass the result to the next function in the chain to get a new command >>= |
| 20:50:35 | <EvanR> | it's the same thing |
| 20:50:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 20:50:59 | <EvanR> | concrete syntax is besides the point |
| 20:51:31 | <ski> | "When you talk about Imperative programming, you talk about `do`, no ?" -- no. talking about reasoning where you have to think about implicit effects of computations, and where ordering (and possible duplication, and omisssion) of computations can have observable behavioural effects on the program |
| 20:52:00 | <EvanR> | cmd1 >>= \result1 -> cmd2 >>= \result2 -> ... return 0 |
| 20:52:30 | → | michalz joins (~michalz@185.246.207.203) |
| 20:53:00 | <ski> | if you write `main = getLine >>= putStrLn', then the value of `main' is an `IO'-action, a recipe, a "sequence of I/O instructions" (although "sequence" is, in general, a bit inaccurate), effectively in an imperative language. this is the imperative programming we're talking about here |
| 20:53:17 | <ski> | does not matter whether you express this with `do' or `>>=' |
| 20:55:07 | <ski> | the contents of the file `/bin/ls' on an Un*x system is not a list of files, but it's a set of instructions describing how to obtain a list of files, if/when executed (interacting with the OS) at some point |
| 20:55:59 | <ski> | the same holds for `main'. the value of `main' is a "set of instructions describing how to" interact with the OS, in order to effect some observable behaviour on the OS |
| 20:56:33 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 20:56:40 | <ski> | the value of `main' itself is inert, doesn't "do" anything. only when the run-time system interprets these imperative instructions, does any actual input/output behaviour commence |
| 20:58:16 | <sim590> | You are saying that `(\ x -> (\ y -> x + y) 1) 1` for example is imperative programming? |
| 20:58:18 | <ski> | "You could say that lambdas inside lambdas are imperative programming which doesn't make sense." -- yea, i don't think this would make any sense |
| 20:58:24 | <ski> | no |
| 20:58:51 | <ski> | that kind of lambda nesting can be used to express a kind of sequencing (from data-dependencies), yes |
| 20:58:59 | <EvanR> | imperative programming is a vibe, not a strict concrete thing |
| 20:59:07 | <ski> | but that's not how the imperative instructions here are being expressed |
| 21:00:08 | <ski> | (or the imperative programming, or the imperative behaviour, if you prefer) |
| 21:01:24 | <EvanR> | data Tele a = GetC (Char -> Tele a) | PutC Char (Tele a) | Done a |
| 21:01:27 | <EvanR> | PutC '?' >> GetC >>= \c -> PutC c >> PutC '!' >> Done () |
| 21:01:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:01:44 | <EvanR> | would be a possible imperative program in haskell, if you defined the right Monad instance |
| 21:01:55 | <EvanR> | :: Tele () |
| 21:02:09 | × | kimiamania8 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 21:02:17 | <EvanR> | no I messed it up |
| 21:02:26 | <EvanR> | I'm melting |
| 21:02:29 | <ski> | yes, something like that can be used to try to explain how `IO'-actions can be seen as inert instructions |
| 21:02:34 | → | kimiamania8 joins (~65804703@user/kimiamania) |
| 21:03:12 | <ski> | PutC '?' (GetC (\c -> PutC c (PutC '!' (Done ())))) |
| 21:03:27 | × | euleritian quits (~euleritia@95.90.214.149) (Ping timeout: 244 seconds) |
| 21:03:50 | <EvanR> | so it's not lambdas in lambdas there but just data, that happens to use a lambda in a place to get a result |
| 21:04:35 | <ski> | you can write a `runTele :: Tele a -> IO a' interpreter, and then calling `runTele' on a `Tele'-action, and then letting the run-time system interpret/execute the resulting `IO'-action, would be equivalent to letting the run-time system interpret/execute the corresponding equivalent `IO'-action directly |
| 21:05:39 | <sim590> | In any case, this whole conversation lasted too long already for me considering I should have been working. So, I'll go back to my employer's task I have to finish. I'll resume investigating purity later. Thanks for the conversation anyway! |
| 21:05:48 | <ski> | so, you can imagine that the run-time system is an imperative program (not written in Haskell), which interprets `IO'-actions similarly to how `runTele' interprets `Tele'-actions, and in addition actually interacts with the OS |
| 21:06:36 | <ski> | sim590 : yea, i think the best approach is to ponder it, sleep on it, do examples, think about how you can reason about (including refactoring) programs, come back later to this |
| 21:07:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 21:07:18 | <dminuoso> | I think plenty of confusion comes from decades of programming having (incorrectly) reused terminology like calling routines functions, and then attaching labels like "pure" and "impure" to differentiate things that should not be compared. |
| 21:07:22 | <ski> | it can take some times to be able to switch perspectives, to be able to see the relevant distinctions (which you're not used to drawing) |
| 21:07:31 | <ski> | yes, there is that too |
| 21:07:57 | <ski> | there's is a lot of bad "monad tutorials" out there (arguably, most of them are bad, to lesser or greater extents) |
| 21:08:44 | → | euleritian joins (~euleritia@dynamic-176-006-128-244.176.6.pool.telefonica.de) |
| 21:10:28 | <dminuoso> | Rather than asking "what the difference between pure and impure functions" is, we should rather re-learn the notion of "function" to mean something that is almost, but not quite , entirely unlike its cousin from traditional programming and compare that to "effect". Once you learn them as orthogonal things and advance, you can get into deeper ideas on how to encode one with the other (in both |
| 21:10:30 | <dminuoso> | directions!) |
| 21:11:54 | <ski> | there's two approaches a monad tutorial could take, i think. (a) one focused on concrete practicalities, how to express various intended imperative behaviours (effects), how to remove / factor out common kinds of related boiler-plate code (e.g. for state-threading, or short-circuiting of failure), identifying idioms/"patterns" for this |
| 21:12:23 | <ski> | and (b) a category-theoretic perspective, which explains what this has to do with monads as seen in category theory |
| 21:12:28 | <geekosaur> | e.g. "You could have invented monads" |
| 21:12:35 | <geekosaur> | (for (a)) |
| 21:12:47 | <dminuoso> | And as for "monad tutorials", Im still a firm believer that all we really need, is a Prelude.Simple module that exposes things like `thenIO :: IO a -> (a -> IO b) -> IO b`, `returnIO :: a -> IO a`, with some special tweakery to attach a `a ~ IO` constraint as a superclass to Monad a... |
| 21:12:53 | <ski> | for the practical programmer, (a) is of most use, (b) is more a curiosity, if one looks into it at all |
| 21:12:53 | <geekosaur> | also I'm not sure how much use (b) is for a Haskell programmer |
| 21:12:58 | <EvanR> | b 😱 |
| 21:13:07 | <dminuoso> | If we had that type of Prelude.Simple, we would not have any of these monad confusions. |
| 21:13:15 | <dminuoso> | Just people learning to program with a simple interface. |
| 21:13:22 | <dminuoso> | They can explore list comprehensions, IO code.. |
| 21:13:33 | <dminuoso> | And then we open the can of burritos. |
| 21:13:53 | <EvanR> | I am still waiting for the chapter of "category theory for programmers" gets to the part where there is anything related to programming in it xD |
| 21:14:22 | <ski> | indeed, geekosaur |
| 21:14:44 | <dminuoso> | EvanR: Hey, when I started Haskell I put it on pause, learned category theory, had a rough understanding of monoidal categories, went back to Haskell, and couldn't quite figure out how to write any simple ask/response beginner proggrams. :-) |
| 21:14:48 | <dminuoso> | Been there, done that! |
| 21:14:57 | <ski> | for a programming language semanticist, otoh, it could be useful |
| 21:14:58 | <dminuoso> | It was excruciatingly slow. |
| 21:15:11 | <dminuoso> | A bit unclear why I kept at it, was rather thick headed. |
| 21:15:32 | <EvanR> | it's like how useful is monoid theory, when you want to use Monoid in haskell |
| 21:15:42 | <EvanR> | xD |
| 21:16:04 | <dminuoso> | EvanR: The thing I keep saying in these discussions: You dont use Monad if you dont write code polymorphically over it. |
| 21:16:12 | <dminuoso> | If you dont, you're just using *instances* of it. |
| 21:16:34 | <dminuoso> | All these monad discussions and explanations are centered around the idea of what Monad abstracts over, when people are strugglyg with instances.. |
| 21:16:36 | <EvanR> | code polymorphic in Monad and no other assumptions |
| 21:16:40 | <EvanR> | I wonder xD |
| 21:16:47 | <dminuoso> | Similar story with Monoid. |
| 21:16:49 | <EvanR> | if it's as pointless as Monoid |
| 21:16:51 | <EvanR> | lol |
| 21:17:03 | <davean> | instances are for SPECIALIZE pragmas |
| 21:17:05 | <EvanR> | ok, the Monad library has a bunch of routines |
| 21:17:11 | <EvanR> | unlike Comonad |
| 21:17:15 | <dminuoso> | davean: Hey I'm special. |
| 21:17:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:17:38 | <ski> | you're using individual monads (individual types supporting the monadic opertions, in addition to other operations). but you're not using the monad concept in any non-trivial sense |
| 21:18:01 | <davean> | {-# SPECIALIZE dminuoso :: Special #-} |
| 21:18:13 | <dminuoso> | ski: Right, and attaching the label monad to that is as useful as calling adding numbers as "you're working with monoids" when teaching first graders some basic arithmatic. |
| 21:18:20 | <dminuoso> | Pedagogically you just dont do it. |
| 21:18:31 | <ski> | "when people are strugglyg with instances" -- which is why people generally need to learn to "shut up and learn individual instances" more |
| 21:19:00 | <EvanR> | that helps also in category theory xD |
| 21:19:29 | <EvanR> | without any examples it's a (large) pile of abstract nonsense |
| 21:19:38 | <dminuoso> | EvanR: I would argue its the exact opposite, even. |
| 21:19:41 | × | euleritian quits (~euleritia@dynamic-176-006-128-244.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 21:19:47 | <ski> | dminuoso : i think i largely agree with that |
| 21:20:04 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 21:20:14 | <ski> | (i also tend to view monoids (the concept) as expressing a notion of "sequencing") |
| 21:21:06 | <ski> | i suppose the question becomes "how to best help people to learn to shut up, and focus on the instances ?" |
| 21:22:37 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 21:23:31 | <dminuoso> | This is where my idea of some prelude and GHC mode comes from, to constrain users into a particular instance model. But that could only be useful within the scope of say a particular course or book that introduces Haskell subjects linearly. |
| 21:23:31 | × | euleritian quits (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 21:23:32 | <davean> | I found everything easier once I forgot about instances. Things like "hoist" were way more enlightening for me |
| 21:23:46 | <EvanR> | there was a really old monad ttorial which used 3 examples |
| 21:23:53 | → | euleritian joins (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 21:23:58 | <davean> | EvanR: "You could have invented monads"? |
| 21:24:04 | <EvanR> | maybe |
| 21:24:25 | <EvanR> | i recall 2 of the examples being basically the same thing (state and RNG) |
| 21:24:52 | <davean> | http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html |
| 21:25:12 | <EvanR> | it was like my first intro so I struggled to believe there was some non-state related applications xD |
| 21:25:28 | <davean> | Its not quite as I remembered |
| 21:27:07 | → | alfiee joins (~alfiee@user/alfiee) |
| 21:27:33 | <geekosaur> | yeh, I mentioned that earlier. still IMO the only monad tutorial worth anything |
| 21:27:47 | ski | didn't understand the "with some special tweakery to attach a `a ~ IO` constraint as a superclass to Monad a..." part |
| 21:29:47 | <dminuoso> | Hitchhiker's Guide to the Galaxy helpfully suggests that a Monad is 'just a monoid in the category of endofunctors,' which is technically true but about as useful as describing a spaceship as ‘just some metal arranged cleverly in space.’ |
| 21:30:08 | <dminuoso> | Now I finally found out what LLMs are good for. |
| 21:30:11 | <ski> | EvanR : "What the Hell are Monads?" by Noel Winstanley in 1999-02 at <https://web.archive.org/web/19991018214519/http://www.dcs.gla.ac.uk/~nww/Monad.html> ? |
| 21:30:34 | <dminuoso> | The Guide concludes that Haskell is ‘almost certainly very important,’ but advises against asking a Haskell programmer what a Monad really is, unless you have packed a towel, a week’s worth of supplies, and a sturdy escape plan." |
| 21:31:04 | <ski> | i consider this still one of the best monad tutorials (being the first one that was directed towards ordinary programmers, from what i know) |
| 21:31:25 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 21:31:25 | <ski> | but yes, that dpipono blag is also a good contender |
| 21:31:36 | <davean> | dminuoso: Its ok, I made sure to use a phantom type when I passed them to the lecture transformer. |
| 21:31:51 | <EvanR> | ski, they only have 2 examples! |
| 21:32:17 | <EvanR> | dminuoso, did you ask it to generate a bad monad tutorial |
| 21:32:30 | <EvanR> | it's gotta be better at that than good ones |
| 21:32:32 | <ski> | EvanR : `Maybe',`State s',`IO' |
| 21:32:48 | <EvanR> | hmmmmmmm. No RNG so it's not the one I'm thinking of |
| 21:33:09 | <ski> | mhm |
| 21:33:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:33:54 | <davean> | EvanR: Also there are totally non-state related applications, like reverse state. |
| 21:34:31 | <EvanR> | reverse state? |
| 21:34:32 | <mauke> | the anarchy monad |
| 21:35:01 | <EvanR> | it's florida by flipped around the Y axis |
| 21:35:06 | <EvanR> | but* |
| 21:35:15 | <ski> | i also like the (non-tutorial) short overview "Escaping Hell with Monads" by Philip Nillson in 2017-05-08 at <https://philipnilsson.github.io/Badness10k/escaping-hell-with-monads/> |
| 21:35:32 | <EvanR> | that's a good one |
| 21:36:05 | <EvanR> | I posted that in response to people in elixir who are trying to add specialized syntax for basically State monading |
| 21:36:31 | <EvanR> | if you're adding specialized syntax for State monading, then... it might not be that hard to just add monad syntax |
| 21:36:39 | <ski> | i didn't like shadowing of variables in Elixir |
| 21:37:09 | <EvanR> | is that the idiom where they keep "assigning" to the same variable over and over |
| 21:37:48 | <ski> | "State variables" <https://www.mercurylang.org/information/doc-latest/mercury_ref/Clauses.html#State-variables> in Mercury is a neat syntax, for threading state(s), though |
| 21:38:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:38:28 | <ski> | DCGs (Definite Clause Grammars) in Prolog systems can also be (ab)used to thread (a single) state, implicitly |
| 21:38:50 | <dminuoso> | Hey I have an idea how to resolve the monad debate. If we accept the idea that a single instance is better to start with, why not just introduce Cont. We skip the need to introduce any further instances. |
| 21:38:50 | <mauke> | > let f x | x <- x + 1, y <- x, x <- x * 2 = (x,y) in f 3 |
| 21:38:52 | <lambdabot> | (8,4) |
| 21:39:00 | <ski> | ("abused", because this relies on a particular implementation of DCGs, the transformation implementation being transparent, rather than opaque) |
| 21:39:06 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 21:39:40 | <ski> | yes, mauke |
| 21:40:06 | <ski> | EvanR : "keep \"assigning\" to the same variable over and over" -- yes |
| 21:40:47 | <ski> | Erlang doesn't permit this, will do matching on the second time in `X = foo(),X = bar(X,T)', to check that the two results are equal |
| 21:41:53 | <ski> | this coheres with the Prolog roots of Erlang, where `,' means conjunction, which is commutative (although Prolog, unlike e.g. Mercury, does have side-effecting logical formulae (goals), which break commutativity) |
| 21:42:30 | <ski> | dminuoso : well .. i kinda sorta approve .. |
| 21:44:05 | <ski> | (programming with `(>>=)' already is a kind of CPS, although commonly "nq") |
| 21:44:19 | <mauke> | https://www.gofundme.com/f/haskell-infrastructure-overhaul |
| 21:44:29 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 21:45:10 | <EvanR> | "nq" ? |
| 21:46:05 | <ski> | "not quite" |
| 21:46:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:47:19 | <EvanR> | mauke, I will forward my check from elon to this when I get it |
| 21:47:21 | → | gmg joins (~user@user/gehmehgeh) |
| 21:47:51 | <ski> | there is something called "nqCPS", which is related to composable/delimited/sub- continuations .. and also to Andrzej Filinski's notion of "monadic reflection", which allows you to turn any (computable) implementation of a monad (like we do in Haskell, e.g.), into an actual corresponding side-effect in the language, assuming only we have composable continuation side-effects (or, equivalently, ordinary |
| 21:47:57 | <ski> | (undelimited) continuation effects, and a single piece of mutable state) |
| 21:48:18 | → | j1n37 joins (~j1n37@user/j1n37) |
| 21:50:01 | <ski> | i recall at some point looking at an example of staged computation, in MetaML, which interpreted a description of a regex, matching on an input string. the staging on it walked over the description, converting it to a piece of code (not too dissimilar to `Expr' or `TExpr' in TH) that when executed would more efficiently match on input strings (without having to re-interpret the regex all the time) |
| 21:50:39 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 21:51:03 | → | califax joins (~califax@user/califx) |
| 21:51:21 | × | wildsalander quits (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 246 seconds) |
| 21:52:06 | <ski> | this example was written in CPS (success and failure continuation), but the staging of it became nqCPS, because of the inserted quasiquotation and unquotation, meaning that you often had to construct new code fragments, splicing recursive results into them, rather than doing tail-calls. however, MetaML also had support for composable continuations, so i converted the example into DS (Direct Style), with the |
| 21:52:12 | <ski> | ocasional call to `shift' and `reset' inserted, making the code more readable |
| 21:52:39 | <EvanR> | direct style? |
| 21:53:00 | <monochrom> | is when you don't use CPS :) |
| 21:53:16 | → | pavonia joins (~user@user/siracusa) |
| 21:53:26 | <ski> | yes. or when you don't use state-threading style. or you don't use short-circuiting |
| 21:53:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 21:53:35 | <ski> | or whichever "style" you're contrasting with |
| 21:53:55 | <ski> | (but in this context, it would be contrasting with CPS (or nqCPS)) |
| 21:54:14 | <mauke> | I wonder what kind of code gets more readable by the addition of shift/reset |
| 21:55:02 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 21:55:50 | <ski> | one could quite possibly have used instead `reify' and `reflect' primitives of Filinski's "Monadic Reflection", for a non-deterministic monad, in place of `shift' and `reset'. or `fail' and `amb' (disjunction, like `(<|>)') operations for the non-determinism monad, implemented in terms of `reflect' (`reify' (or a `collect' operation defined in terms of it) is used at the toplevel of the computation, to |
| 21:55:56 | <ski> | collect the results, delimiting the extent of the side-effects) |
| 21:57:18 | <ski> | nqCPS code, generally, mauke. `Codensity' does something similar (in terms of nqCPS) (albeit without side-effects), in Haskell |
| 21:57:19 | <mauke> | do any of those not break my brain? |
| 21:57:28 | <monochrom> | Oh I think the readable part comes from trying to be in direct style most of the time, rather than the shift-reset part. |
| 21:57:40 | <ski> | yes, exactly |
| 21:57:57 | <ski> | making the "special cases", when you resort to `reset' and `shift', stand out more |
| 21:59:00 | <ski> | rather than always be passing around continuations everywhere, and not as clearly being able to notice when they're being used "unconventionally". as well as the continuation-passing cluttering up (and turning inside-out) the code, in general |
| 22:06:39 | <monochrom> | But I have one readable use of shift-reset. If you accept that Python's yield is readable in some cases, then it's shift-reset when I do that in Haskell. :) |
| 22:07:05 | <monochrom> | https://www.vex.net/~trebla/haskell/cont.xhtml#yield |
| 22:07:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:08:01 | <mauke> | I don't believe in python |
| 22:10:48 | × | ash3en quits (~Thunderbi@89.56.182.235) (Quit: ash3en) |
| 22:10:51 | <ski> | for monadic reflection, see "Representing Monads" in 1994-01 and "Representing Layered Monads" in 1999-01, both by Andrzej Filinski, at <http://hjemmesider.diku.dk/~andrzej/papers/>. at some point, i typed in the code in the papers, which you can access at <https://0x0.st/HOHX.tar.gz>,<https://0x0.st/HOH8.tar.gz> (see `starting-points.txt' for how to run, using either SML/NJ directly, or its CM (Compilation |
| 22:10:57 | <ski> | Manager) (which might also work in MLton, i don't recall if i tried)) |
| 22:11:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 22:12:03 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 22:12:12 | ski | . o O ( "Yield: Mainstream Delimited Continuations" by Roshan P. James,Amr Sabry in 2009 (?) at <https://www.cs.indiana.edu/~sabry/papers/yield.pdf> ) |
| 22:13:31 | → | alfiee joins (~alfiee@user/alfiee) |
| 22:15:41 | <mauke> | monochrom: you say square_cps1 is mixing styles because (*) is not in CPS, but mul_cps is also mixing styles because currying |
| 22:17:53 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 22:19:48 | <mauke> | Integer -> ((Integer -> (Integer -> t) -> t) -> r) -> r ?? |
| 22:22:11 | <monochrom> | I am not taking currying seriously. |
| 22:22:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:27:14 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 22:27:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 22:38:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:39:42 | <ski> | there's "serious", and there's "trivial" currying. "serious" would be when the function does some actual computation (e.g. for sharing some preprocessing ("compilation") of early parameter(s)), before returning a function |
| 22:42:19 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 22:43:10 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 22:47:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:47:56 | → | kaskal- joins (~kaskal@2a02:8388:15bf:c200:a121:d904:3721:b9c6) |
| 22:48:04 | × | kaskal quits (~kaskal@84-115-231-2.cable.dynamic.surfer.at) (Ping timeout: 252 seconds) |
| 22:50:03 | × | xeno11 quits (~xeno11@c-69-140-170-168.hsd1.de.comcast.net) (Quit: Client closed) |
| 22:51:07 | <geekosaur> | yes |
| 22:51:29 | <geekosaur> | (whoops) |
| 22:53:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 23:00:16 | → | alfiee joins (~alfiee@user/alfiee) |
| 23:03:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:04:10 | <monochrom> | :) |
| 23:04:21 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 23:06:37 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 23:07:56 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:08:36 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 23:09:04 | <EvanR> | escaping hell with monads is so great |
| 23:09:33 | <EvanR> | I just wish there was an escaping hell with functor to go with it / before it |
| 23:10:39 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 23:19:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:24:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 23:35:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:38:12 | <monochrom> | Generally "escaping hell with function programming" is what we need to include all of the above and more. |
| 23:39:31 | <monochrom> | There is now a functional programming playing card deck. Some conference was handing out them to attendees. |
| 23:40:34 | <monochrom> | My student went and got one and showed me. He first let me randomly drew one card. I drew the monad card. (Other cards are like: GADT, Scheme macros, shift-reset, ...) |
| 23:41:23 | <monochrom> | I don't normally believe in Tarot cards, but FP cards seems to have better predictive power! |
| 23:42:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 23:46:00 | → | alfiee joins (~alfiee@user/alfiee) |
| 23:46:51 | ski | . o O ( "Ccard V2.0 - a category theory card game" <http://www.verify-it.de/sub/ccard/index.html> ) |
| 23:51:03 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 276 seconds) |
| 23:51:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:54:51 | <EvanR> | scheme macros |
| 23:54:55 | <EvanR> | is that all it says |
| 23:55:00 | <EvanR> | or is there flavor text at least |
| 23:56:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 23:58:07 | geekosaur | notes that ski's link doesn't seem to describe the same game |
| 23:58:30 | <geekosaur> | it appears to all be CT statements of increasing complexity |
| 23:59:26 | geekosaur | also wonders if the one monochrom is talking about is more like Tarot, or more like M:tG |
All times are in UTC on 2025-03-21.