Logs: freenode/#haskell
| 2021-04-13 15:35:54 | <ski> | however, for terminating computations, it does get closer to the result. often one would prove a computation is terminating, by introducing some kind of "size" measure, and show that it decreases (discretely) in each step (towards zero) |
| 2021-04-13 15:36:02 | × | geekosaur quits (930099da@rrcs-147-0-153-218.central.biz.rr.com) (Ping timeout: 240 seconds) |
| 2021-04-13 15:36:33 | → | kiweun joins (~kiweun@2607:fea8:2a62:9600:483b:ac14:a41e:28c4) |
| 2021-04-13 15:36:34 | <ski> | (e.g. in some cases, one might operate on trees, and get wider, but shallower, trees, in each step) |
| 2021-04-13 15:37:29 | <fiedlr> | Yeah I know what you mean... I meant more like when it is used with "expansion" in the same text. But I couldn't think of a better alternative :-( I guess I'll stick to that. |
| 2021-04-13 15:37:47 | <fiedlr> | Especially when the "size" measure is not clearly stated. |
| 2021-04-13 15:37:59 | → | myShoggoth joins (~myShoggot@97-120-72-12.ptld.qwest.net) |
| 2021-04-13 15:39:37 | <dolio> | Well, in the case of β, there is not really a canonical choice of 'expansion' either, so it is ill behaved in that way, too. |
| 2021-04-13 15:39:46 | <dolio> | Unlike η, where the term is actually used. |
| 2021-04-13 15:41:05 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:483b:ac14:a41e:28c4) (Ping timeout: 258 seconds) |
| 2021-04-13 15:41:55 | → | usr25 joins (~usr25@unaffiliated/usr25) |
| 2021-04-13 15:41:58 | <ski> | η-expansion for sum types would also be more open-ended, iirc |
| 2021-04-13 15:42:26 | → | alexm_ joins (~alexm_@161.8.254.229) |
| 2021-04-13 15:42:27 | <dolio> | Which is also not done. |
| 2021-04-13 15:42:47 | → | porygon2 joins (~porygon2@178.239.168.171) |
| 2021-04-13 15:43:00 | <fiedlr> | Of course, in general it is ill-defined. That's why I talked about a particular computation branch. |
| 2021-04-13 15:43:02 | <ski> | mm. i suppose η-long form doesn't use that (?) |
| 2021-04-13 15:43:43 | ski | . o O ( normalization-by-evaluation, reflection & reification via delimited continuations ) |
| 2021-04-13 15:44:54 | hololeap_ | is now known as hololeap |
| 2021-04-13 15:45:33 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2021-04-13 15:46:12 | → | geekosaur joins (930099da@rrcs-147-0-153-218.central.biz.rr.com) |
| 2021-04-13 15:46:14 | → | ep1ctetus joins (~epictetus@ip72-194-54-201.sb.sd.cox.net) |
| 2021-04-13 15:46:29 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.1) |
| 2021-04-13 15:48:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-13 15:49:32 | × | alexm_ quits (~alexm_@161.8.254.229) (Ping timeout: 240 seconds) |
| 2021-04-13 15:50:11 | → | KeyJoo joins (~KeyJoo@62.176.30.171) |
| 2021-04-13 15:50:32 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 2021-04-13 15:52:07 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-04-13 15:52:25 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) |
| 2021-04-13 15:52:33 | × | Major_Biscuit quits (~Major_Bis@wlan-145-94-219-47.wlan.tudelft.nl) (Ping timeout: 240 seconds) |
| 2021-04-13 15:53:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-13 15:57:15 | → | idhugo joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-04-13 15:58:37 | × | grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-04-13 15:58:52 | × | chele quits (~chele@78.128.94.174) (Ping timeout: 240 seconds) |
| 2021-04-13 15:59:33 | × | finn_elija quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Ping timeout: 240 seconds) |
| 2021-04-13 16:00:17 | × | Haskman[m] quits (haskmanmat@gateway/shell/matrix.org/x-sdpzurestintfxkz) (Quit: Idle for 30+ days) |
| 2021-04-13 16:01:40 | → | finn_elija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) |
| 2021-04-13 16:01:49 | → | Lycurgus joins (~niemand@98.4.118.65) |
| 2021-04-13 16:03:55 | → | danso joins (~dan@23-233-111-52.cpe.pppoe.ca) |
| 2021-04-13 16:04:19 | → | Rudd0 joins (~Rudd0@185.189.115.108) |
| 2021-04-13 16:07:05 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 2021-04-13 16:09:56 | × | kritzefitz quits (~kritzefit@2003:5b:203b:200::10:49) (Ping timeout: 245 seconds) |
| 2021-04-13 16:11:12 | → | pfurla_ joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-04-13 16:11:14 | × | coot quits (~coot@37.30.50.130.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2021-04-13 16:11:40 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 2021-04-13 16:16:18 | → | Benzi-Junior joins (~BenziJuni@dsl-149-64-251.hive.is) |
| 2021-04-13 16:21:11 | → | rond_ joins (5940206b@89-64-32-107.dynamic.chello.pl) |
| 2021-04-13 16:22:19 | × | xff0x quits (~xff0x@2001:1a81:52e3:ed00:8d58:e974:e293:f3fe) (Ping timeout: 250 seconds) |
| 2021-04-13 16:23:06 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 2021-04-13 16:23:22 | → | xff0x joins (~xff0x@2001:1a81:52e3:ed00:16c4:781d:2418:6176) |
| 2021-04-13 16:23:52 | × | Lycurgus quits (~niemand@98.4.118.65) (Quit: Exeunt) |
| 2021-04-13 16:24:13 | → | supercoven joins (~Supercove@dsl-hkibng31-58c384-213.dhcp.inet.fi) |
| 2021-04-13 16:24:14 | × | supercoven quits (~Supercove@dsl-hkibng31-58c384-213.dhcp.inet.fi) (Max SendQ exceeded) |
| 2021-04-13 16:24:19 | × | _ashbreeze_ quits (~mark@64.85.214.234.reverse.socket.net) (Remote host closed the connection) |
| 2021-04-13 16:24:28 | → | supercoven joins (~Supercove@dsl-hkibng31-58c384-213.dhcp.inet.fi) |
| 2021-04-13 16:25:37 | → | _ashbreeze_ joins (~mark@64.85.214.234.reverse.socket.net) |
| 2021-04-13 16:26:50 | → | raichoo joins (~raichoo@dslb-088-077-025-199.088.077.pools.vodafone-ip.de) |
| 2021-04-13 16:28:07 | × | kini quits (~kini@unaffiliated/kini) (Remote host closed the connection) |
| 2021-04-13 16:29:24 | → | kini joins (~kini@unaffiliated/kini) |
| 2021-04-13 16:30:03 | × | jonatan quits (~nate@h77-53-70-163.cust.a3fiber.se) (Remote host closed the connection) |
| 2021-04-13 16:34:39 | → | neiluj joins (~jco@91-167-203-101.subs.proxad.net) |
| 2021-04-13 16:34:43 | × | neiluj quits (~jco@91-167-203-101.subs.proxad.net) (Changing host) |
| 2021-04-13 16:34:43 | → | neiluj joins (~jco@unaffiliated/neiluj) |
| 2021-04-13 16:37:41 | → | bitmagie joins (~Thunderbi@200116b8065a8100544220815d2d2bde.dip.versatel-1u1.de) |
| 2021-04-13 16:38:13 | × | bitmagie quits (~Thunderbi@200116b8065a8100544220815d2d2bde.dip.versatel-1u1.de) (Client Quit) |
| 2021-04-13 16:40:37 | → | Sorny joins (~Sornaensi@79.142.232.102) |
| 2021-04-13 16:40:40 | × | malumore_ quits (~malumore@151.62.122.89) (Remote host closed the connection) |
| 2021-04-13 16:41:38 | → | malumore joins (~malumore@151.62.122.89) |
| 2021-04-13 16:41:39 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2021-04-13 16:42:06 | → | grimpeux joins (~textual@modemcable153.12-178-173.mc.videotron.ca) |
| 2021-04-13 16:42:20 | × | fiedlr quits (~fiedlr@83.148.33.254) (Remote host closed the connection) |
| 2021-04-13 16:43:11 | × | Sorna quits (~Sornaensi@077213203030.dynamic.telenor.dk) (Ping timeout: 240 seconds) |
| 2021-04-13 16:44:11 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-04-13 16:44:39 | × | kuribas quits (~user@ptr-25vy0i8g2c6vaifvwgm.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-04-13 16:45:26 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 246 seconds) |
| 2021-04-13 16:45:59 | → | ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-13 16:47:12 | × | grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-04-13 16:47:44 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-04-13 16:48:22 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-13 16:49:40 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-04-13 16:50:30 | → | kw joins (d4662d5d@212.102.45.93) |
| 2021-04-13 16:50:42 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 2021-04-13 16:51:06 | <kw> | Is there a conventional way of naming traversals? Like how folks add 'L' to the names of lenses? |
| 2021-04-13 16:51:41 | → | fendor_ joins (~fendor@91.141.2.26.wireless.dyn.drei.com) |
| 2021-04-13 16:52:06 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-04-13 16:52:25 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) |
| 2021-04-13 16:53:13 | × | elfets_ quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 240 seconds) |
| 2021-04-13 16:53:37 | → | geowiesnot joins (~user@87-89-181-157.abo.bbox.fr) |
| 2021-04-13 16:54:11 | × | fendor quits (~fendor@77.119.130.199.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 2021-04-13 16:54:16 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 2021-04-13 16:55:23 | → | ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-13 16:55:48 | → | alexm_ joins (~alexm_@161.8.254.229) |
| 2021-04-13 16:56:20 | <tapas> | not really kw. I tend to name those similarly to any other traverse-based functionality |
| 2021-04-13 16:57:26 | <kw> | My problem is that the obvious names are already taken by less obvious functions. I'm thinking of tacking an 'A' or 'T' to the end. |
| 2021-04-13 16:59:04 | × | geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 268 seconds) |
| 2021-04-13 17:00:07 | × | alexm_ quits (~alexm_@161.8.254.229) (Ping timeout: 252 seconds) |
| 2021-04-13 17:00:21 | × | norsxa quits (uid494793@gateway/web/irccloud.com/x-qcpmzqxcuhseltht) (Quit: Connection closed for inactivity) |
| 2021-04-13 17:01:46 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 252 seconds) |
| 2021-04-13 17:05:18 | × | dhil quits (~dhil@80.208.56.181) (Quit: Leaving) |
| 2021-04-13 17:06:35 | × | kw quits (d4662d5d@212.102.45.93) (Quit: Connection closed) |
All times are in UTC.