Logs: liberachat/#haskell
| 2021-07-03 19:08:44 | → | beka_ joins (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-03 19:10:02 | <zzz> | i have no idea. i'm not on my usual machine, i think it was a right-click paste from vim to irssi |
| 2021-07-03 19:10:30 | → | yauhsien joins (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) |
| 2021-07-03 19:10:49 | <zzz> | i must have touched the trackpad with my palm |
| 2021-07-03 19:11:27 | × | beka quits (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 268 seconds) |
| 2021-07-03 19:12:20 | × | cheater quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 19:12:21 | × | zeenk quits (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) (Read error: Connection reset by peer) |
| 2021-07-03 19:12:48 | → | cheater joins (~Username@user/cheater) |
| 2021-07-03 19:13:39 | → | zeenk joins (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) |
| 2021-07-03 19:15:12 | × | yauhsien quits (~yauhsien@61-231-45-160.dynamic-ip.hinet.net) (Ping timeout: 265 seconds) |
| 2021-07-03 19:16:05 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 19:19:16 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 19:20:52 | → | hexfive joins (~eric@50.35.83.177) |
| 2021-07-03 19:21:04 | × | beka_ quits (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 272 seconds) |
| 2021-07-03 19:21:19 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 2021-07-03 19:21:36 | × | HotblackDesiato quits (~HotblackD@gateway/tor-sasl/hotblackdesiato) (Ping timeout: 244 seconds) |
| 2021-07-03 19:21:43 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-03 19:22:23 | → | HotblackDesiato joins (~HotblackD@gateway/tor-sasl/hotblackdesiato) |
| 2021-07-03 19:23:20 | × | hexfive quits (~eric@50.35.83.177) (Read error: Connection reset by peer) |
| 2021-07-03 19:23:23 | → | hexfifty joins (~eric@50.35.83.177) |
| 2021-07-03 19:23:30 | × | hexfifty quits (~eric@50.35.83.177) (Client Quit) |
| 2021-07-03 19:25:14 | → | sm joins (~user@plaintextaccounting/sm) |
| 2021-07-03 19:25:21 | → | stevenxl joins (~stevenlei@68.235.43.93) |
| 2021-07-03 19:29:30 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-07-03 19:29:49 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-03 19:30:34 | × | stevenxl quits (~stevenlei@68.235.43.93) (Ping timeout: 268 seconds) |
| 2021-07-03 19:30:44 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 2021-07-03 19:34:44 | → | Schrostfutz joins (~Schrostfu@p5de88aa6.dip0.t-ipconnect.de) |
| 2021-07-03 19:35:08 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 256 seconds) |
| 2021-07-03 19:36:35 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-03 19:36:47 | <rawles> | Is Agda a natural next step for someone who enjoys Haskell programming and wants to explore dependent types? Are there other clear options? |
| 2021-07-03 19:37:33 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-07-03 19:38:08 | × | natechan quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Quit: WeeChat 2.9) |
| 2021-07-03 19:38:41 | <dolio> | There's also Idris, which is a bit more programming oriented. |
| 2021-07-03 19:41:02 | <rawles> | Ah, so Idris has a proof assistant but the syntax looks more familiar. I guess I can try both and see which feels right. I like the Ivor the Engine reference! |
| 2021-07-03 19:41:36 | <dolio> | Agda generally has more fancy type theoretic features, which can be interesting to learn about. |
| 2021-07-03 19:42:30 | <dolio> | Like, a view of what might be useful for programming eventually, even if not currently. |
| 2021-07-03 19:42:34 | <rawles> | I don't have any specific goal in mind, only to development my understanding of types by dipping my toe in languages with these kind of features. |
| 2021-07-03 19:42:42 | <rawles> | *develop |
| 2021-07-03 19:42:55 | <rawles> | That's really useful. Thanks, dolio. |
| 2021-07-03 19:44:28 | <tomsmeding> | if I'm not mistaken, an example of a thing that agda has and that idris doesn't is copattern matching |
| 2021-07-03 19:44:45 | <tomsmeding> | but my search-fu may just be fooling me |
| 2021-07-03 19:45:02 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 19:45:08 | <dolio> | Oh, that may be. That's an example of something that would be useful right now. It's quite nice. |
| 2021-07-03 19:45:45 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 2021-07-03 19:47:54 | × | xwx quits (~george@user/george) (Ping timeout: 240 seconds) |
| 2021-07-03 19:50:48 | → | xwx joins (~george@user/george) |
| 2021-07-03 19:53:23 | × | azeem quits (~azeem@176.200.221.91) (Ping timeout: 265 seconds) |
| 2021-07-03 19:53:32 | → | chrysanthematic joins (~chrysanth@user/chrysanthematic) |
| 2021-07-03 19:57:15 | → | azeem joins (~azeem@176.200.221.91) |
| 2021-07-03 19:57:26 | × | dunkeln quits (~dunkeln@188.70.10.165) (Ping timeout: 252 seconds) |
| 2021-07-03 19:58:16 | × | pricly_yellow quits (~pricly_ye@2a01:620:c04d:b00::339) (Remote host closed the connection) |
| 2021-07-03 20:00:06 | <zzz> | is performance something you care about? |
| 2021-07-03 20:01:52 | <rawles> | zzz: Me? No, not really, I'm after a 'learning by doing' experience, at least at first. |
| 2021-07-03 20:02:23 | <zzz> | go for agda then |
| 2021-07-03 20:05:28 | × | juhp quits (~juhp@128.106.188.66) (Ping timeout: 265 seconds) |
| 2021-07-03 20:06:38 | → | beka joins (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-03 20:06:54 | <rawles> | Great, thanks. |
| 2021-07-03 20:08:27 | → | juhp joins (~juhp@128.106.188.66) |
| 2021-07-03 20:08:34 | × | peterhil quits (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Ping timeout: 272 seconds) |
| 2021-07-03 20:10:53 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-03 20:12:14 | → | GIANTWORLDKEEPER joins (~pjetcetal@128-71-13-182.broadband.corbina.ru) |
| 2021-07-03 20:13:52 | <qrpnxz> | is there a way to specify on a field that you only want to allow one of the sum type options in the field rather than any of them? So for example, only allow Right values instead of Either? |
| 2021-07-03 20:14:36 | → | akhileshs joins (~user@c-73-63-166-39.hsd1.ca.comcast.net) |
| 2021-07-03 20:14:37 | <monochrom> | No. |
| 2021-07-03 20:14:39 | → | GIANTWORLDKEEPR_ joins (~pjetcetal@128-71-13-182.broadband.corbina.ru) |
| 2021-07-03 20:14:41 | <qrpnxz> | ty |
| 2021-07-03 20:17:19 | → | dunkeln joins (~dunkeln@188.70.10.165) |
| 2021-07-03 20:18:39 | → | sh9 joins (~sh9@softbank060116136158.bbtec.net) |
| 2021-07-03 20:19:57 | <qrpnxz> | is there syntax sugar for creating Data.Text type text? Or do i have to pass strings to pack every time? |
| 2021-07-03 20:20:40 | <geekosaur> | OverloadedStrings, for literals only |
| 2021-07-03 20:20:56 | <geekosaur> | you must use pack for computed ones |
| 2021-07-03 20:21:43 | <qrpnxz> | nice thanks |
| 2021-07-03 20:22:39 | <qrpnxz> | works! |
| 2021-07-03 20:22:45 | <maerwald> | qrpnxz: quasiquoters too |
| 2021-07-03 20:23:04 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 20:23:07 | <maerwald> | with neat interpolation even |
| 2021-07-03 20:23:26 | <qrpnxz> | dunno how to do that |
| 2021-07-03 20:23:53 | ← | akhileshs parts (~user@c-73-63-166-39.hsd1.ca.comcast.net) (ERC (IRC client for Emacs 26.3)) |
| 2021-07-03 20:23:54 | <maerwald> | https://hackage.haskell.org/package/string-interpolate |
| 2021-07-03 20:24:32 | <qrpnxz> | okay, this is epic |
| 2021-07-03 20:24:42 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 20:25:33 | → | jess joins (~jess@libera/staff/jess) |
| 2021-07-03 20:26:04 | × | dunkeln quits (~dunkeln@188.70.10.165) (Ping timeout: 268 seconds) |
| 2021-07-03 20:26:29 | → | fengctor joins (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) |
| 2021-07-03 20:27:45 | <rawles> | Oh yeah that's really neat. |
| 2021-07-03 20:29:20 | × | cheater quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2021-07-03 20:29:49 | → | cheater joins (~Username@user/cheater) |
| 2021-07-03 20:30:21 | × | cheater quits (~Username@user/cheater) (Client Quit) |
| 2021-07-03 20:30:54 | → | cheater joins (~Username@user/cheater) |
| 2021-07-03 20:31:30 | <fengctor> | hey all! just wondering if repeated modifications on the same optic get fused, or as an example in case my terminology isn't right: does |
| 2021-07-03 20:31:30 | <fengctor> | v & l1 . l2 %~ f & l1 . l2 %~ g |
| 2021-07-03 20:31:30 | <fengctor> | produce the intermediary structure from the first modification, or does it behave as |
| 2021-07-03 20:31:30 | <fengctor> | v & l1 . l2 %~ g . f & l1 . l2 %~ g |
| 2021-07-03 20:31:57 | → | dunkeln_ joins (~dunkeln@188.70.10.165) |
| 2021-07-03 20:31:58 | <fengctor> | sorry, as v & l1 . l2 %~ g . f |
| 2021-07-03 20:32:40 | → | jneira_ joins (~jneira_@217.red-81-39-172.dynamicip.rima-tde.net) |
| 2021-07-03 20:34:05 | × | fengctor quits (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) (Remote host closed the connection) |
| 2021-07-03 20:35:41 | <c_wraith> | I doubt that'd be reduced |
| 2021-07-03 20:35:50 | → | fengctor joins (~fengctor@bras-base-ngflon0508w-grc-11-76-68-2-143.dsl.bell.ca) |
All times are in UTC.