Logs on 2025-08-08 (liberachat/#haskell)
| 00:03:24 | × | bryanv quits (~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10) (Server closed connection) |
| 00:03:27 | <Leary> | energizer: I don't know, but it follows from (half of) homomorphism (for all xs, ys. h (xs <> ys) = h xs <> h ys) and will hold for any `foldMap f`. |
| 00:03:36 | → | bryanv joins (~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10) |
| 00:03:51 | × | Ranhir quits (~Ranhir@157.97.53.139) (Remote host closed the connection) |
| 00:07:24 | × | acidjnk quits (~acidjnk@p200300d6e7171956e90dafb18b04e6cb.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 00:08:07 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 00:10:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:13:13 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 00:14:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 00:16:58 | × | vetkat quits (~vetkat@user/vetkat) (Quit: So long, and thanks for all the fish) |
| 00:21:45 | → | vetkat joins (~vetkat@user/vetkat) |
| 00:25:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:30:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 00:31:41 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 00:36:24 | × | iteratee_ quits (~kyle@199.119.84.78) (Server closed connection) |
| 00:36:31 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 00:36:38 | → | iteratee joins (~kyle@199.119.84.78) |
| 00:41:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:45:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 00:50:32 | → | weary-traveler joins (~user@user/user363627) |
| 00:50:50 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
| 00:56:24 | × | xff0x quits (~xff0x@2405:6580:b080:900:b6cd:f0c8:c2fb:2237) (Ping timeout: 276 seconds) |
| 00:56:30 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:57:29 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 01:01:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 01:05:29 | → | chewybread joins (~chewybrea@user/chewybread) |
| 01:05:50 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:06:08 | → | weary-traveler joins (~user@user/user363627) |
| 01:07:20 | × | chewybread quits (~chewybrea@user/chewybread) (Remote host closed the connection) |
| 01:11:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:13:18 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 01:15:09 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 01:17:59 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 260 seconds) |
| 01:18:24 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Server closed connection) |
| 01:18:35 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 01:18:59 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 01:30:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:35:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 01:36:44 | × | trickard quits (~trickard@cpe-49-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 01:36:58 | → | trickard_ joins (~trickard@cpe-49-98-47-163.wireline.com.au) |
| 01:40:42 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 01:45:24 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:50:21 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 01:53:43 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 01:55:35 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 01:58:31 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 02:00:49 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:07:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 02:10:59 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 02:15:24 | × | Kamuela quits (sid111576@id-111576.tinside.irccloud.com) (Server closed connection) |
| 02:15:35 | → | Kamuela joins (sid111576@id-111576.tinside.irccloud.com) |
| 02:16:36 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 02:17:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:20:54 | × | Square quits (~Square@user/square) (Ping timeout: 276 seconds) |
| 02:21:00 | × | davidlbowman quits (~dlb@user/davidlbowman) (Quit: WeeChat 4.1.1) |
| 02:22:42 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 02:29:55 | → | Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 02:33:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:36:44 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 02:37:41 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 02:48:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:55:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 02:58:36 | × | jespada quits (~jespada@r179-25-206-34.dialup.adsl.anteldata.net.uy) (Ping timeout: 276 seconds) |
| 03:00:17 | → | jespada joins (~jespada@r179-25-146-183.dialup.adsl.anteldata.net.uy) |
| 03:06:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:07:46 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:08:02 | → | weary-traveler joins (~user@user/user363627) |
| 03:11:22 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 03:22:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:27:07 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 03:29:45 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
| 03:31:01 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 03:32:52 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 03:37:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:41:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 03:42:50 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 03:43:04 | → | califax joins (~califax@user/califx) |
| 03:52:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:57:37 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 04:03:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:08:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 04:16:54 | × | fr33domlover quits (~fr33domlo@towards.vision) (Server closed connection) |
| 04:17:17 | → | fr33domlover joins (~fr33domlo@towards.vision) |
| 04:19:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:23:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 04:27:24 | × | Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 260 seconds) |
| 04:31:47 | → | fgarcia joins (~lei@user/fgarcia) |
| 04:34:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:36:24 | × | drlkf quits (~drlkf@chat-1.drlkf.net) (Server closed connection) |
| 04:36:48 | → | drlkf joins (~drlkf@chat-1.drlkf.net) |
| 04:40:22 | → | euphores joins (~SASL_euph@user/euphores) |
| 04:41:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 04:44:41 | × | haritz quits (~hrtz@user/haritz) (Remote host closed the connection) |
| 04:52:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:54:21 | → | michalz joins (~michalz@185.246.207.218) |
| 04:57:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 05:01:58 | × | fgarcia quits (~lei@user/fgarcia) (Ping timeout: 240 seconds) |
| 05:02:45 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 276 seconds) |
| 05:04:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:09:04 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 05:09:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 05:10:54 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Server closed connection) |
| 05:11:10 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 05:20:12 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:20:36 | → | ubert joins (~Thunderbi@91.141.76.34.wireless.dyn.drei.com) |
| 05:24:36 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 05:33:41 | × | ubert quits (~Thunderbi@91.141.76.34.wireless.dyn.drei.com) (Ping timeout: 248 seconds) |
| 05:35:35 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:40:27 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 05:40:36 | → | Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 05:42:47 | → | fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi) |
| 05:43:18 | → | tromp joins (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) |
| 05:46:44 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 260 seconds) |
| 05:50:48 | × | Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 05:51:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:55:23 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 05:59:06 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 06:05:37 | × | eldfrb^ quits (~eldfrb@99-73-20-238.lightspeed.tukrga.sbcglobal.net) (Remote host closed the connection) |
| 06:05:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:08:24 | → | takuan joins (~takuan@d8D86B9E9.access.telenet.be) |
| 06:10:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 06:14:45 | × | hc quits (~hc@mail.hce.li) (Read error: Connection reset by peer) |
| 06:18:33 | → | hc joins (~hc@mail.hce.li) |
| 06:19:55 | × | ft quits (~ft@p3e9bcd7f.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:21:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:23:07 | × | YoungFrog quits (~youngfrog@2a02:a03f:ca07:f900:4407:d5e8:2b8d:2dc6) (Ping timeout: 252 seconds) |
| 06:27:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 06:39:03 | → | YoungFrog joins (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) |
| 06:39:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:41:16 | → | chele joins (~chele@user/chele) |
| 06:41:20 | → | jackdk joins (uid373013@cssa/life/jackdk) |
| 06:43:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 06:43:57 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 06:49:03 | × | tromp quits (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:52:33 | → | tromp joins (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) |
| 06:54:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:57:11 | → | talisman` joins (~user@2601:644:937c:ed10::ae5) |
| 06:58:18 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 06:59:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 07:00:02 | × | caconym747 quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:42 | → | caconym747 joins (~caconym@user/caconym) |
| 07:00:49 | × | talismanick quits (~user@2601:644:937c:ed10::ae5) (Ping timeout: 260 seconds) |
| 07:03:39 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:06:38 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:09:24 | × | peutri quits (~peutri@bobo.desast.re) (Server closed connection) |
| 07:09:33 | → | peutri joins (~peutri@bobo.desast.re) |
| 07:10:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 07:12:40 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 07:17:56 | → | acidjnk joins (~acidjnk@p200300d6e717192225dcf845b9904c0e.dip0.t-ipconnect.de) |
| 07:18:22 | → | FANTOM joins (~fantom@87.74.59.94) |
| 07:21:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:25:36 | × | tromp quits (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:29:05 | → | poscat0x04 joins (~poscat@user/poscat) |
| 07:30:35 | → | SlackCoder joins (~SlackCode@64-94-63-8.ip.weststar.net.ky) |
| 07:30:35 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 252 seconds) |
| 07:41:28 | → | dextaa joins (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) |
| 07:43:31 | × | dextaa quits (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) (Remote host closed the connection) |
| 07:43:50 | → | dextaa joins (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) |
| 07:45:01 | × | dextaa quits (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) (Remote host closed the connection) |
| 07:46:04 | → | dextaa joins (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) |
| 07:46:31 | × | dextaa quits (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) (Remote host closed the connection) |
| 07:46:50 | → | dextaa joins (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) |
| 07:47:32 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 07:49:37 | × | SlackCoder quits (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Ping timeout: 248 seconds) |
| 07:53:40 | × | poscat0x04 quits (~poscat@user/poscat) (Remote host closed the connection) |
| 07:54:22 | → | poscat joins (~poscat@user/poscat) |
| 07:54:24 | × | mfc_kbs quits (~keibisoft@mail.keibisoft.com) (Server closed connection) |
| 07:54:42 | → | mfc_kbs joins (~keibisoft@2a06:1fc0:0:1::1cd) |
| 07:56:51 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 08:09:05 | → | __monty__ joins (~toonn@user/toonn) |
| 08:16:47 | × | dextaa quits (~dan@200116b82dca98000e5d5dfc8d68d582.dip.versatel-1u1.de) (Ping timeout: 252 seconds) |
| 08:21:44 | AlexNoo_ | is now known as AlexNoo |
| 08:22:24 | → | dextaa joins (~dan@200116b82dca980033c93e9a50267820.dip.versatel-1u1.de) |
| 08:30:48 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 08:42:16 | × | phma quits (~phma@host-67-44-208-38.hnremote.net) (Read error: Connection reset by peer) |
| 08:44:01 | → | phma joins (phma@2001:5b0:215a:b978:b6f0:b4c6:edfd:8a6a) |
| 08:45:45 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 252 seconds) |
| 08:55:17 | → | rembo10_ joins (~rembo10@main.remulis.com) |
| 08:57:07 | × | rembo10 quits (~rembo10@main.remulis.com) (Ping timeout: 252 seconds) |
| 08:58:12 | → | gmg joins (~user@user/gehmehgeh) |
| 09:01:21 | → | ubert joins (~Thunderbi@91.141.76.34.wireless.dyn.drei.com) |
| 09:11:22 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 09:16:54 | × | sudden quits (~cat@user/sudden) (Server closed connection) |
| 09:17:09 | → | sudden joins (~cat@user/sudden) |
| 09:18:57 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 09:21:29 | × | dextaa quits (~dan@200116b82dca980033c93e9a50267820.dip.versatel-1u1.de) (Quit: Leaving) |
| 09:25:28 | × | aforemny_ quits (~aforemny@i59F4C627.versanet.de) (Ping timeout: 240 seconds) |
| 09:26:36 | → | aforemny joins (~aforemny@2001:9e8:6cf7:6c00:9f22:b1e:aec8:ecc9) |
| 09:44:34 | → | Guest84 joins (~Guest84@2401:4900:1c52:d1bb:cc6f:4e7c:df27:efc5) |
| 09:50:48 | → | kuribas joins (~user@ptr-17d51emw6dvgxl0n7oc.18120a2.ip6.access.telenet.be) |
| 09:51:55 | × | oxapentane quits (~oxapentan@user/oxapentane) (Remote host closed the connection) |
| 09:52:27 | → | oxapentane joins (~oxapentan@user/oxapentane) |
| 09:52:44 | <kuribas> | If I implement a type system and type checker, would the progress and preservation properties garantee it is implemented correctly? |
| 09:52:53 | <kuribas> | For example, would it catch bugs in substitution? |
| 09:54:13 | <Guest84> | A smart C++ programmer recommend me that I learn haskell to get better at C++. |
| 09:54:14 | <Guest84> | I do have a background with C++ for 10 years but I cant say I ever like OOPS. |
| 09:55:24 | <Guest84> | Where do I start with ? |
| 09:55:46 | <Guest84> | I even have some (read as very little) experience of functional style c++ and lisp. |
| 09:56:32 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 09:58:15 | <mauke> | Guest84: it's been a long time since I started learning haskell, but have you seen https://www.haskell.org/get-started/ ? |
| 10:00:20 | <haskellbridge> | <sm> and more stuff: https://joyful.com/Haskell+minimap |
| 10:00:30 | <kuribas> | I can recommend https://www.seas.upenn.edu/~cis1940/spring13/ |
| 10:00:55 | <mauke> | sm: I love looking at blank pages |
| 10:01:51 | <[exa]> | Guest84: there are various parts of many programming languages that help. Myself I'd recommend prolog first (so that you're able to code in templates easily) and Haskell helps with the "correct by construction" feeling (which is kinda present in C++ as the "keep all local state consistent" approach...more of a soft-skill imo.) |
| 10:01:52 | <mauke> | for a "halfway step" (static types, type inference, mostly functional, algebraic types, currying) without laziness (or type classes), you could look at ocaml |
| 10:02:17 | <mauke> | but after using haskell, ocaml's syntax feels weird |
| 10:02:53 | <kuribas> | Isn't rust closer to C++ though? Haskell is more high level than C++. It doesn't give you much control about memory layout and allocation though. |
| 10:03:31 | × | trickard_ quits (~trickard@cpe-49-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 10:03:45 | → | trickard_ joins (~trickard@cpe-49-98-47-163.wireline.com.au) |
| 10:03:52 | <mauke> | sm: sorry, not entirely blank. there is a single animated svg on it, spinning endlessly |
| 10:14:16 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 10:15:34 | <int-e> | mauke: https://publish-01.obsidian.md/access/599da60310a78cfd30ea6fd228437374/Haskell%20minimap.md is human readable ;) |
| 10:15:36 | → | img joins (~img@user/img) |
| 10:16:21 | <kuribas> | If I mess up the substitution for forall, the type system may be still sound, but reject valid programs. |
| 10:17:12 | trickard_ | is now known as trickard |
| 10:17:51 | <[exa]> | kuribas: if I got the question right, you're asking on whether having (quickcheck?) tests on the 2 properties passing implies that the internal "tools" in the typesystem (substitution) are working as intended? |
| 10:20:47 | <[exa]> | (I'd say that would work just right, but given the sheer spectrum of stupid bugs that may happen in unification I wouldn't bet on it formally) |
| 10:24:47 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 244 seconds) |
| 10:25:16 | × | Guest84 quits (~Guest84@2401:4900:1c52:d1bb:cc6f:4e7c:df27:efc5) (Quit: Client closed) |
| 10:27:39 | → | sprotte24 joins (~sprotte24@p200300d16f43d3003d43dd3d16486e1e.dip0.t-ipconnect.de) |
| 10:28:40 | <kuribas> | I was more thinking about formal proofs, but the idea is the same. |
| 10:29:41 | <kuribas> | If "forall a b. a -> b" has a substitution error, so checks as "forall a. a -> a", it would still be sound, but reject valid programs. |
| 10:30:06 | <kuribas> | So there would need to be some completeness property that prevents this, however most typesystems aren't complete. |
| 10:32:12 | × | michalz quits (~michalz@185.246.207.218) (Remote host closed the connection) |
| 10:32:49 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 248 seconds) |
| 10:33:51 | <haskellbridge> | <sm> mauke: yikes, thanks for letting me know. You have js disabled ? |
| 10:34:45 | → | michalz joins (~michalz@185.246.207.201) |
| 10:35:10 | <mauke> | not specifically, but I have ublock origin configured to block all third-party scripts by default |
| 10:35:51 | <haskellbridge> | <sm> aha |
| 10:38:39 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 10:38:49 | haskellbridge | sm needs to find a better setup that's similarly convenient |
| 10:39:08 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:39:14 | → | poscat joins (~poscat@user/poscat) |
| 10:39:30 | × | ubert quits (~Thunderbi@91.141.76.34.wireless.dyn.drei.com) (Ping timeout: 272 seconds) |
| 10:43:43 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 10:44:14 | → | poscat joins (~poscat@user/poscat) |
| 10:46:56 | → | SlackCoder joins (~SlackCode@64-94-63-8.ip.weststar.net.ky) |
| 10:47:15 | × | athan quits (~athan@syn-047-132-161-157.res.spectrum.com) (Ping timeout: 276 seconds) |
| 10:48:30 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 10:48:58 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 10:51:51 | → | poscat joins (~poscat@user/poscat) |
| 10:52:17 | → | poscat0x04 joins (~poscat@user/poscat) |
| 10:54:55 | × | CalimeroTeknik quits (~calimero@ctkarch.org) (Changing host) |
| 10:54:55 | → | CalimeroTeknik joins (~calimero@user/calimeroteknik) |
| 10:56:21 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 248 seconds) |
| 10:56:45 | × | trickard quits (~trickard@cpe-49-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 10:56:59 | → | trickard_ joins (~trickard@cpe-49-98-47-163.wireline.com.au) |
| 10:57:58 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 240 seconds) |
| 11:04:14 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 11:05:09 | trickard_ | is now known as trickard |
| 11:09:45 | <jcarpenter2> | Quick question. I've got a value of type "[MaybeT m a]" and I want to convert it to a "MaybeT m [a]" by taking all of the Just values. Just like catMaybes, but for MaybeT instead of for Maybe. I can do this with the code "liftMaybeT . fmap catMaybes . traverse runMaybeT" but I'm wondering if there's a more elegant / algebraic way such that I don't have to use runMaybeT and liftMaybeT in my code. Any ideas? |
| 11:10:52 | <jcarpenter2> | My code works perfectly fine as-is, but I'd like to know if there's a neat higher-level function I could use. |
| 11:12:15 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 11:13:27 | → | fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi) |
| 11:15:05 | × | jackdk quits (uid373013@cssa/life/jackdk) (Quit: Connection closed for inactivity) |
| 11:16:24 | → | Square joins (~Square@user/square) |
| 11:18:42 | × | zfnmxt quits (~zfnmxt@user/zfnmxt) (Ping timeout: 248 seconds) |
| 11:21:00 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 11:21:06 | × | poscat0x04 quits (~poscat@user/poscat) (Remote host closed the connection) |
| 11:21:38 | → | poscat joins (~poscat@user/poscat) |
| 11:21:44 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 11:22:10 | → | poscat joins (~poscat@user/poscat) |
| 11:22:34 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 272 seconds) |
| 11:23:16 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 11:27:51 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 11:32:48 | × | jaror quits (~jaror@5070ACC7.static.ziggozakelijk.nl) (Quit: The Lounge - https://thelounge.chat) |
| 11:33:25 | → | jaror joins (~jaror@5070ACC7.static.ziggozakelijk.nl) |
| 11:47:13 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 11:51:30 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 11:51:41 | → | poscat joins (~poscat@user/poscat) |
| 11:52:08 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:55:15 | → | athan joins (~athan@syn-047-132-161-157.res.spectrum.com) |
| 11:56:50 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 11:57:16 | → | poscat joins (~poscat@user/poscat) |
| 11:58:35 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 11:59:20 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 11:59:41 | → | poscat joins (~poscat@user/poscat) |
| 12:02:16 | × | trickard quits (~trickard@cpe-49-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 12:02:29 | → | trickard_ joins (~trickard@cpe-49-98-47-163.wireline.com.au) |
| 12:05:53 | × | bcksl quits (~bcksl@user/bcksl) (Quit: \) |
| 12:05:54 | × | end quits (~end@user/end/x-0094621) (Quit: end) |
| 12:06:11 | <kuribas> | [exa]: So I can make a system, proof it consistent, and have an inference algorithm for that system that I can prove is complete. If I want more garantees, like universal quantification, I'll need more theorems for it. |
| 12:10:21 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 12:13:02 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 12:13:02 | ljdarj1 | is now known as ljdarj |
| 12:24:22 | → | bcksl joins (~bcksl@user/bcksl) |
| 12:24:41 | <kuribas> | However I could prove that for every monotype b, if "x : forall a. e", then "x : e[b/a]". In that case a substitution error would give a contradiction, if "a -> b" must work with distinc types, it would fail if substution makes them equal. |
| 12:29:32 | → | end joins (~end@user/end/x-0094621) |
| 12:30:08 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Quit: fp) |
| 12:30:25 | → | fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi) |
| 12:31:36 | trickard_ | is now known as trickard |
| 12:40:54 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 12:43:36 | → | xff0x joins (~xff0x@2405:6580:b080:900:3038:cd69:f604:d295) |
| 12:44:09 | → | euandreh joins (~Thunderbi@2804:d59:892b:6600:cfc9:47d1:96e8:b32d) |
| 12:45:09 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 12:47:36 | × | AlexZenon quits (~alzenon@178.34.162.188) (Quit: ;-) |
| 12:48:16 | × | AlexNoo quits (~AlexNoo@178.34.162.188) (Quit: Leaving) |
| 12:48:51 | → | weary-traveler joins (~user@user/user363627) |
| 12:50:55 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 12:52:38 | → | davidlbowman joins (~dlb@user/davidlbowman) |
| 12:55:04 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds) |
| 13:00:24 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
| 13:02:58 | → | haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 13:02:58 | × | haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 13:02:58 | → | haritz joins (~hrtz@user/haritz) |
| 13:05:35 | → | statusfailed joins (~statusfai@statusfailed.com) |
| 13:21:02 | → | AlexNoo joins (~AlexNoo@178.34.162.188) |
| 13:21:57 | × | Vajb quits (~Vajb@n4ff0xajgx7huazq3a1-1.v6.elisa-mobile.fi) (Ping timeout: 248 seconds) |
| 13:22:40 | → | AlexZenon joins (~alzenon@178.34.162.188) |
| 13:22:41 | × | dyniec quits (~dyniec@dybiec.info) (Remote host closed the connection) |
| 13:23:18 | → | dyniec joins (~dyniec@dybiec.info) |
| 13:24:17 | × | sprotte24 quits (~sprotte24@p200300d16f43d3003d43dd3d16486e1e.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 13:36:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 13:37:59 | ← | statusfailed parts (~statusfai@statusfailed.com) () |
| 13:39:04 | × | jespada quits (~jespada@r179-25-146-183.dialup.adsl.anteldata.net.uy) (Quit: Textual IRC Client: www.textualapp.com) |
| 13:47:30 | → | jespada joins (~jespada@2800:a4:2228:2400:e5a0:dd56:e91c:d25b) |
| 13:48:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 13:51:24 | × | smiesner quits (b0cf5acf8c@user/smiesner) (Server closed connection) |
| 13:51:31 | → | smiesner joins (b0cf5acf8c@user/smiesner) |
| 13:58:23 | → | Cale joins (~cale@2607:fea8:995f:f126:15c3:35a5:81ac:187c) |
| 14:02:52 | → | ft joins (~ft@p3e9bcd7f.dip0.t-ipconnect.de) |
| 14:14:11 | × | ttybitnik quits (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 14:14:50 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:27:17 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 14:33:23 | → | fgarcia joins (~lei@user/fgarcia) |
| 14:34:28 | × | AlexZenon quits (~alzenon@178.34.162.188) (Ping timeout: 240 seconds) |
| 14:34:55 | → | AlexNoo_ joins (~AlexNoo@94.233.240.26) |
| 14:34:57 | × | AlexNoo quits (~AlexNoo@178.34.162.188) (Ping timeout: 248 seconds) |
| 14:36:59 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 14:37:38 | → | AlexNoo__ joins (~AlexNoo@94.233.240.26) |
| 14:37:50 | AlexNoo__ | is now known as AlexNoo |
| 14:40:04 | × | AlexNoo_ quits (~AlexNoo@94.233.240.26) (Ping timeout: 260 seconds) |
| 14:43:30 | → | AlexZenon joins (~alzenon@94.233.240.26) |
| 14:46:54 | × | pointlessslippe1 quits (~pointless@62.106.85.17) (Server closed connection) |
| 14:49:01 | → | pointlessslippe1 joins (~pointless@62.106.85.17) |
| 15:00:44 | → | vpan joins (~vpan@212.117.1.172) |
| 15:01:02 | vpan | is now known as Guest7277 |
| 15:01:10 | Guest7277 | is now known as vpan |
| 15:01:14 | × | cptaffe quits (~cptaffe@user/cptaffe) (Ping timeout: 265 seconds) |
| 15:03:10 | × | davidlbowman quits (~dlb@user/davidlbowman) (Ping timeout: 265 seconds) |
| 15:07:49 | × | jespada quits (~jespada@2800:a4:2228:2400:e5a0:dd56:e91c:d25b) (Ping timeout: 276 seconds) |
| 15:10:47 | → | jespada joins (~jespada@2800:a4:234e:1000:35fb:ac29:3d39:de58) |
| 15:16:03 | → | karenw joins (~karenw@dudl-15-b2-v4wan-170016-cust2909.vm31.cable.virginm.net) |
| 15:16:17 | → | euphores joins (~SASL_euph@user/euphores) |
| 15:16:27 | karenw | is now known as Guest1731 |
| 15:31:54 | × | sprout quits (~sprout@84-80-106-227.fixed.kpn.net) (Server closed connection) |
| 15:32:08 | → | sprout joins (~sprout@84-80-106-227.fixed.kpn.net) |
| 15:33:10 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 15:44:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 15:49:48 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:50:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 15:52:11 | × | arahael quits (~arahael@user/arahael) (Ping timeout: 252 seconds) |
| 16:01:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 16:06:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 16:11:12 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 16:13:47 | × | phma quits (phma@2001:5b0:215a:b978:b6f0:b4c6:edfd:8a6a) (Read error: Connection reset by peer) |
| 16:13:49 | × | ouilemur quits (~jgmerritt@user/ouilemur) (Ping timeout: 252 seconds) |
| 16:14:06 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 16:15:02 | → | phma joins (phma@2001:5b0:215d:dff8:8beb:c012:2554:46c7) |
| 16:15:15 | × | SlackCoder quits (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 16:15:51 | → | ouilemur joins (~jgmerritt@user/ouilemur) |
| 16:17:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 16:22:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 16:24:24 | × | Yumemi quits (~Yumemi@chamoin.net) (Server closed connection) |
| 16:25:13 | → | Yumemi joins (~Yumemi@chamoin.net) |
| 16:30:42 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 16:32:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 16:37:18 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 16:47:01 | × | kuribas quits (~user@ptr-17d51emw6dvgxl0n7oc.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 16:48:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 16:52:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 16:55:37 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 16:56:34 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 260 seconds) |
| 16:58:57 | × | vpan quits (~vpan@212.117.1.172) (Quit: Leaving.) |
| 16:59:54 | × | Guest1731 quits (~karenw@dudl-15-b2-v4wan-170016-cust2909.vm31.cable.virginm.net) (Ping timeout: 260 seconds) |
| 17:03:30 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:08:06 | → | davidlbowman joins (~dlb@user/davidlbowman) |
| 17:08:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 17:14:58 | <jcarpenter2> | Trying to figure out why this program crashes... https://gitlab.com/-/snippets/4878869 |
| 17:15:59 | <jcarpenter2> | This reproduces an error I just had in a larger program. In that program, I just had some divergent code, and I've put an "undefined" here to represent that. |
| 17:16:34 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 248 seconds) |
| 17:17:14 | <jcarpenter2> | Basically there's a value here called "runFunction", and if I run it once it's fine but if I run it twice the program crashes. The output here is "Running once", "Just ()", "Running twice", and then a crash. |
| 17:17:40 | <jcarpenter2> | It seems like the "undefined" value is getting forced somehow, but I'm not sure how that happens. |
| 17:18:10 | <Lycurgus> | crash |
| 17:18:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:19:10 | <jcarpenter2> | The crash goes away if (1) I switch from the State monad to the Reader monad (that's shown here with 3 commented lines that replace the lines immediately above), or (2) I replace "do_return" just with "return" on line 20 |
| 17:19:57 | <jcarpenter2> | The thing is, msum should just return the good value, which is the first value in the array. Somehow the rest of the array seems to be getting forced, even though msum has already found a good value. |
| 17:20:06 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
| 17:20:08 | <jcarpenter2> | Anyway, I'd appreciate any help understanding this! |
| 17:20:37 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 17:21:27 | <mauke> | I don't know, but here's a live demo: https://play.haskell.org/saved/MvGY0Szb |
| 17:22:04 | <jcarpenter2> | Oh, thank you for that! |
| 17:25:41 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 17:26:18 | × | phma quits (phma@2001:5b0:215d:dff8:8beb:c012:2554:46c7) (Read error: Connection reset by peer) |
| 17:27:29 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 260 seconds) |
| 17:27:45 | → | phma joins (~phma@host-67-44-208-41.hnremote.net) |
| 17:30:48 | <int-e> | jcarpenter2: the second `get` depends on the state that would be left by the undefined `do_return undefined` call. This can be demonstrated by defining do_return _ = put [] instead |
| 17:33:21 | <int-e> | (writing `do_return ()` makes the function strict in its argument, even in the case when there's only one possible value to match) |
| 17:43:03 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 17:43:55 | <jcarpenter2> | ohhhhhhhhhhh |
| 17:44:12 | <jcarpenter2> | I knew it was something |
| 17:44:21 | <jcarpenter2> | thank you very much |
| 17:45:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:46:24 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 17:49:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 17:52:14 | <mauke> | int-e++ |
| 17:58:14 | → | poscat0x04 joins (~poscat@user/poscat) |
| 17:58:27 | <jcarpenter2> | If I simplify down to just the 2 lines "units <- get" and "msum $ fmap do_return units" I don't get a crash either, which is interesting. Seems like the "traverse" is what makes the second "get" depend on the first "do_return undefined" call, since that causes the whole list to be iterated. |
| 17:58:55 | <jcarpenter2> | with an fmap, the state would be updated independently for each list element |
| 17:59:58 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 245 seconds) |
| 18:00:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:02:12 | × | Athas quits (athas@2a01:7c8:aaac:1cf:c58b:c964:cf04:bf1d) (Quit: ZNC 1.9.1 - https://znc.in) |
| 18:02:23 | → | Athas joins (athas@149.210.169.107) |
| 18:02:51 | <int-e> | jcarpenter2: it may be helpful to give `do_return` an explicit type signature for each of those experiments; you'll find that the type changes |
| 18:05:19 | <int-e> | hmm, or not? |
| 18:05:22 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 18:05:43 | <jcarpenter2> | no, I was just doing that :) |
| 18:06:13 | <jcarpenter2> | I'm trying to find some way to reproduce the issue without using "runMaybeT" etc. |
| 18:06:30 | <int-e> | Ah but the `traverse` forces full sequencing inside the wrapped `State [()]` monad while the plain `msum` shortcuts inside the MaybeT |
| 18:08:24 | → | tromp joins (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) |
| 18:14:37 | → | fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi) |
| 18:15:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:20:07 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 18:23:05 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 18:30:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:34:31 | <jcarpenter2> | Okay, I think I see what you're saying. The "traverse runMaybeT" sequences a bunch of values in the State monad, and in order to get those values it has to run "do_return" on each list element, including the undefined one. |
| 18:35:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 18:36:28 | <c_wraith> | Well, more importantly... traverse is in terms of Applicative |
| 18:36:39 | <c_wraith> | And Applicative can't short-circuit |
| 18:36:58 | <c_wraith> | At least, not in that sense. |
| 18:39:42 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 18:40:00 | <int-e> | > runMaybeT $ traverse id [empty, undefined] |
| 18:40:01 | <lambdabot> | error: |
| 18:40:02 | <lambdabot> | Variable not in scope: runMaybeT :: f0 [b0] -> t |
| 18:40:12 | <int-e> | @let import Control.Monad.Trans.Maybe |
| 18:40:13 | <lambdabot> | Defined. |
| 18:40:15 | <int-e> | > runMaybeT $ traverse id [empty, undefined] |
| 18:40:16 | <lambdabot> | error: |
| 18:40:16 | <lambdabot> | • Ambiguous type variables ‘m0’, |
| 18:40:17 | <lambdabot> | ‘b0’ arising from a use of ‘show_M38876083433... |
| 18:40:22 | <int-e> | meh |
| 18:40:31 | <int-e> | @undef |
| 18:40:31 | <lambdabot> | Undefined. |
| 18:41:01 | <int-e> | with enough defaulting that would evaluate to `Nothing` |
| 18:41:39 | <c_wraith> | but what about when you give it (empty:undefined) as an argument? |
| 18:41:58 | <c_wraith> | that's the part traverse can't escape |
| 18:42:22 | <int-e> | it still evaluates to `Nothing` |
| 18:42:37 | <int-e> | the whole recursive `traverse id undefined` is never touched |
| 18:43:02 | <monochrom> | > runMaybeT $ traverse id (Nothing : undefined) |
| 18:43:03 | <lambdabot> | error: |
| 18:43:03 | <lambdabot> | Variable not in scope: runMaybeT :: Maybe [b0] -> t |
| 18:43:15 | <monochrom> | > runMaybeT $ traverse id ((Nothing :: Maybe Int): undefined) |
| 18:43:16 | <lambdabot> | error: |
| 18:43:16 | <lambdabot> | Variable not in scope: runMaybeT :: Maybe [Int] -> t |
| 18:43:43 | <c_wraith> | Oh right. MaybeT smuggles a monad requirement in |
| 18:44:11 | <c_wraith> | that's actually kind of a cute trick |
| 18:45:59 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:50:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 18:51:37 | × | phma quits (~phma@host-67-44-208-41.hnremote.net) (Read error: Connection reset by peer) |
| 18:53:36 | → | phma joins (phma@2001:5b0:210d:1aa8:aefa:72b1:7a70:bfa2) |
| 18:53:44 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 18:57:12 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 18:58:41 | → | sprotte24 joins (~sprotte24@p200300d16f43d300b160c6115250e1c1.dip0.t-ipconnect.de) |
| 18:58:59 | → | werneta joins (~werneta@syn-071-083-160-242.res.spectrum.com) |
| 18:59:01 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 248 seconds) |
| 19:00:04 | × | caconym747 quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:43 | → | caconym747 joins (~caconym@user/caconym) |
| 19:01:23 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:01:26 | → | fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi) |
| 19:04:06 | <jcarpenter2> | okay, thanks guys! |
| 19:04:32 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:04:39 | <jcarpenter2> | I understand this a lot better, and found a way to refactor my code so that I don't need to evaluate and re-form the MaybeT transformer |
| 19:05:47 | <jcarpenter2> | (well, except in one place where I actually do want *every* successful computation in a list, not just the first one) |
| 19:06:59 | → | MudEater85 joins (~MudEater@102.219.153.100) |
| 19:08:05 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 19:08:28 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 240 seconds) |
| 19:10:44 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 19:18:24 | × | MudEater85 quits (~MudEater@102.219.153.100) (Quit: Client closed) |
| 19:19:26 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:21:24 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 19:24:21 | <jcarpenter2> | really appreciate all your insight |
| 19:24:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 19:25:54 | × | op_4 quits (~tslil@user/op-4/x-9116473) (Server closed connection) |
| 19:26:07 | → | op_4 joins (~tslil@user/op-4/x-9116473) |
| 19:34:49 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:38:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 19:46:12 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Quit: fp) |
| 19:47:34 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
| 19:50:12 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:54:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:59:01 | × | poscat0x04 quits (~poscat@user/poscat) (Remote host closed the connection) |
| 19:59:21 | → | gorignak joins (~gorignak@user/gorignak) |
| 19:59:32 | → | poscat joins (~poscat@user/poscat) |
| 20:00:23 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 20:00:32 | → | poscat joins (~poscat@user/poscat) |
| 20:02:21 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 276 seconds) |
| 20:05:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:10:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 20:21:12 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:25:40 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:33:20 | × | tromp quits (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:34:25 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 248 seconds) |
| 20:35:21 | → | tt12310978324354 joins (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) |
| 20:36:35 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:41:25 | → | tromp joins (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) |
| 20:42:24 | × | ringo_ quits (~ringo@157.230.117.128) (Server closed connection) |
| 20:42:43 | → | ringo_ joins (~ringo@157.230.117.128) |
| 20:43:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 20:47:07 | → | fp joins (~Thunderbi@2001-14ba-6e24-3000--19a.rev.dnainternet.fi) |
| 20:51:51 | × | YoungFrog quits (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Quit: ZNC 1.7.x-git-3-96481995 - https://znc.in) |
| 20:52:11 | → | YoungFrog joins (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) |
| 20:54:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:59:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 21:00:04 | → | pavonia joins (~user@user/siracusa) |
| 21:01:55 | → | nitrix_ joins (~nitrix@user/meow/nitrix) |
| 21:03:09 | × | nitrix quits (~nitrix@user/meow/nitrix) (Ping timeout: 260 seconds) |
| 21:10:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:15:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 21:24:46 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 252 seconds) |
| 21:25:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:27:45 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 248 seconds) |
| 21:29:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 21:40:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:45:42 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 21:49:48 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 21:56:11 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:57:23 | × | michalz quits (~michalz@185.246.207.201) (Remote host closed the connection) |
| 22:00:41 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 22:01:16 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 22:04:01 | × | fp quits (~Thunderbi@2001-14ba-6e24-3000--19a.rev.dnainternet.fi) (Ping timeout: 248 seconds) |
| 22:06:31 | × | tromp quits (~textual@2001:1c00:3487:1b00:fc99:7338:6c62:cab) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:07:04 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 276 seconds) |
| 22:11:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:12:32 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 22:18:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 22:30:22 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 22:32:36 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:36:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 22:43:15 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 22:47:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:52:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 23:03:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:08:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 23:09:54 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 23:11:45 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:18:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:25:29 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 23:34:23 | × | sprotte24 quits (~sprotte24@p200300d16f43d300b160c6115250e1c1.dip0.t-ipconnect.de) (Quit: Leaving) |
| 23:36:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:40:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 23:43:34 | × | athan quits (~athan@syn-047-132-161-157.res.spectrum.com) (Quit: Konversation terminated!) |
| 23:51:39 | <haskellbridge> | <orenty7> Hello everyone, |
| 23:51:39 | <haskellbridge> | I started diving into GHC recently and, as a result, stumble upon dependent types discussions a lot. Apparently there's a lot of effort to make haskell dependently-typed, so the question is: why it wasn't from the beginning? |
| 23:51:51 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:56:19 | <EvanR> | complexity increases a lot, for the user and the compiler |
| 23:56:53 | <Leary> | Haskell was born from a committee of academics working on /lazy/ functional languages. The type system was secondary. Also, this was like thirty years ago; was there even precedent? |
| 23:56:59 | <EvanR> | a lot of haskell people report not wanting to use dependent types |
| 23:57:11 | × | ttybitnik quits (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 23:58:41 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
All times are in UTC on 2025-08-08.