Logs: freenode/#haskell
| 2020-09-17 12:16:30 | <enikar> | :t loeb |
| 2020-09-17 12:16:32 | <lambdabot> | Functor f => f (f a -> a) -> f a |
| 2020-09-17 12:17:44 | <ski> | (named after some kind of analogy with <https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem>,<https://en.wikipedia.org/wiki/L%C3%B6b's_paradox>) |
| 2020-09-17 12:17:49 | <Uniaika> | rally racing has made its way into Haskell! |
| 2020-09-17 12:17:58 | <ski> | racing ? |
| 2020-09-17 12:18:28 | <Uniaika> | https://en.wikipedia.org/wiki/S%C3%A9bastien_Loeb |
| 2020-09-17 12:18:28 | <phadej> | https://en.wikipedia.org/wiki/S%C3%A9bastien_Loeb |
| 2020-09-17 12:18:29 | <Uniaika> | :) |
| 2020-09-17 12:18:34 | <phadej> | (: |
| 2020-09-17 12:18:35 | <Uniaika> | haha, raced, phadej! |
| 2020-09-17 12:18:42 | <ski> | hm, never heard about him |
| 2020-09-17 12:18:54 | <Uniaika> | oh don't worry, I know him because I'm french |
| 2020-09-17 12:19:01 | <phadej> | finns know rally too |
| 2020-09-17 12:19:24 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-17 12:19:33 | <ski> | kuribas : anyway, can you follow that example, or would you like a hint ? |
| 2020-09-17 12:21:05 | → | bicho_rastrero joins (~cerdito@154.85-87-39.dynamic.clientes.euskaltel.es) |
| 2020-09-17 12:21:33 | <phadej> | eh, 9 consecutive championships |
| 2020-09-17 12:21:42 | <phadej> | might been a bit boring at the end |
| 2020-09-17 12:22:17 | <kuribas> | ski: more or less... I'll study it another time |
| 2020-09-17 12:22:58 | <phadej> | "Loeb is a tarmac expert, having won all but three of the WRC rallies on that surface in which he has participated between 2005 and 2013." |
| 2020-09-17 12:24:12 | <ski> | kuribas : basically, that example works sortof like a spreadsheet. every "cell" can refer to the value of all the other "cells" |
| 2020-09-17 12:24:32 | → | p-core joins (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) |
| 2020-09-17 12:24:37 | <kuribas> | ski: a comonad? |
| 2020-09-17 12:24:59 | × | gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2020-09-17 12:25:02 | <Unhammer> | so split-sections on windows gives "ld.exe: blah.o: too many sections", "file is too big", when compiling blazehtml |
| 2020-09-17 12:25:17 | <Unhammer> | too bad |
| 2020-09-17 12:25:28 | <ski> | this `loeb' only requires a functor (and general recursion) |
| 2020-09-17 12:26:11 | <Unhammer> | works great on my other project that doesn't need windows though :) 30M → 9.9M |
| 2020-09-17 12:26:14 | <ski> | (if you pick `Identity', you get the usual `fix') |
| 2020-09-17 12:26:34 | <kuribas> | indeed |
| 2020-09-17 12:26:36 | <kuribas> | pretty neat |
| 2020-09-17 12:26:53 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 246 seconds) |
| 2020-09-17 12:27:00 | <ski> | so, you can easily chase your own tail, with this `loeb' |
| 2020-09-17 12:27:32 | <ski> | but if you only provided access to some other cells, in some well-founded order, say .. |
| 2020-09-17 12:27:52 | <ski> | > foldr (\f as -> f as : as) [] (replicate 4 (succ . sum)) |
| 2020-09-17 12:27:55 | <lambdabot> | [8,4,2,1] |
| 2020-09-17 12:27:58 | <ski> | @type foldr (\f as -> f as : as) [] |
| 2020-09-17 12:28:00 | <lambdabot> | Foldable t => t ([a] -> a) -> [a] |
| 2020-09-17 12:28:24 | <ski> | in this case, each cell only gets access to the values of the cells after it |
| 2020-09-17 12:28:39 | <ski> | and so, it's in some sense "like `fix'", but doesn't get you general recursion |
| 2020-09-17 12:29:17 | <kuribas> | ski: but you just showed it is like fix? |
| 2020-09-17 12:29:22 | <kuribas> | with Identity |
| 2020-09-17 12:29:31 | <ski> | no, that was the `loeb' i just defined, above |
| 2020-09-17 12:30:17 | <kuribas> | ah right... |
| 2020-09-17 12:30:19 | <ski> | the original Löb's theorem, can be interpreted to be about staged computation, and in that case also doesn't give you general recursion |
| 2020-09-17 12:30:31 | <kuribas> | and if instead of cell you take datatype fields... that may work |
| 2020-09-17 12:30:37 | <ski> | (also related to quines) |
| 2020-09-17 12:31:06 | <ski> | you have to avoid cycles. so you need to pick some well-founded order |
| 2020-09-17 12:32:49 | × | p-core quits (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) (Quit: p-core) |
| 2020-09-17 12:33:05 | <ski> | (or if you don't, you'd need to ensure that each step is productive. that's my "larger" suggestion from above) |
| 2020-09-17 12:33:08 | → | p-core joins (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) |
| 2020-09-17 12:34:02 | → | mirrorbird joins (~psutcliff@2a00:801:44b:8959:8d6c:276b:332b:1c71) |
| 2020-09-17 12:34:43 | → | sQVe joins (~sQVe@unaffiliated/sqve) |
| 2020-09-17 12:35:27 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-17 12:36:12 | × | sQVe quits (~sQVe@unaffiliated/sqve) (Client Quit) |
| 2020-09-17 12:36:22 | → | wavemode joins (~wavemode@097-070-075-143.res.spectrum.com) |
| 2020-09-17 12:36:46 | → | sQVe joins (~sQVe@unaffiliated/sqve) |
| 2020-09-17 12:37:05 | × | sQVe quits (~sQVe@unaffiliated/sqve) (Client Quit) |
| 2020-09-17 12:37:31 | × | mmohammadi9812 quits (~mmohammad@5.238.164.128) (Quit: I quit (╯°□°）╯︵ ┻━┻) |
| 2020-09-17 12:38:35 | × | george_____t quits (5c094cd5@host-92-9-76-213.as43234.net) (Remote host closed the connection) |
| 2020-09-17 12:40:08 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-17 12:40:59 | → | sQVe joins (sQVe@gateway/vpn/mullvad/sqve) |
| 2020-09-17 12:41:30 | × | sQVe quits (sQVe@gateway/vpn/mullvad/sqve) (Client Quit) |
| 2020-09-17 12:41:56 | → | fendor_ joins (~fendor@t204-126.demo.tuwien.ac.at) |
| 2020-09-17 12:42:01 | → | sQVe joins (sQVe@gateway/vpn/mullvad/sqve) |
| 2020-09-17 12:43:44 | × | fendor quits (~fendor@e237-037.eduroam.tuwien.ac.at) (Ping timeout: 256 seconds) |
| 2020-09-17 12:44:03 | × | Unhammer quits (~Unhammer@gateway/tor-sasl/unhammer) (Ping timeout: 240 seconds) |
| 2020-09-17 12:44:29 | × | p-core quits (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) (Quit: p-core) |
| 2020-09-17 12:44:48 | → | p-core joins (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) |
| 2020-09-17 12:46:24 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-sjkqhkuufbqwprbm) |
| 2020-09-17 12:47:17 | → | Achylles joins (~Achylles@201-27-79-1.dsl.telesp.net.br) |
| 2020-09-17 12:48:46 | → | Unhammer joins (~Unhammer@gateway/tor-sasl/unhammer) |
| 2020-09-17 12:50:32 | × | p-core quits (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) (Quit: p-core) |
| 2020-09-17 12:50:53 | → | p-core joins (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) |
| 2020-09-17 12:52:19 | × | akegalj_ quits (~akegalj@93-142-93-99.adsl.net.t-com.hr) (Remote host closed the connection) |
| 2020-09-17 12:52:27 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:bce9:b254:2a4:39d4) |
| 2020-09-17 12:53:14 | → | jchia__ joins (~jchia@45.32.62.73) |
| 2020-09-17 12:53:57 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 2020-09-17 12:54:57 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 2020-09-17 12:55:45 | → | jchia__ joins (~jchia@58.32.37.220) |
| 2020-09-17 12:56:15 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-17 12:57:43 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:bce9:b254:2a4:39d4) (Ping timeout: 272 seconds) |
| 2020-09-17 12:58:00 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 2020-09-17 12:58:57 | × | sQVe quits (sQVe@gateway/vpn/mullvad/sqve) (Quit: Bye!) |
| 2020-09-17 12:59:04 | × | alp_ quits (~alp@88.126.45.36) (Ping timeout: 260 seconds) |
| 2020-09-17 13:00:56 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-17 13:01:06 | <exarkun> | Anyone want to recommend a prometheus library (I guess they're "prometheus client" libraries? for publishing metrics)? I see a lot of options out there. |
| 2020-09-17 13:02:24 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection) |
| 2020-09-17 13:06:55 | → | hyperisco joins (~hyperisco@d192-186-117-226.static.comm.cgocable.net) |
| 2020-09-17 13:11:08 | <exarkun> | oops no there's only one in my stack resolver so I guess that's easy |
| 2020-09-17 13:11:39 | × | Rudd0 quits (~Rudd0@185.189.115.98) (Ping timeout: 260 seconds) |
| 2020-09-17 13:12:27 | × | bicho_rastrero quits (~cerdito@154.85-87-39.dynamic.clientes.euskaltel.es) (Remote host closed the connection) |
| 2020-09-17 13:12:41 | × | ALM49 quits (7bc007ac@123-192-7-172.dynamic.kbronet.com.tw) (Remote host closed the connection) |
| 2020-09-17 13:13:40 | → | eric_ joins (~eric@2804:431:c7d4:b75:19f7:ea85:5be8:4c8e) |
| 2020-09-17 13:13:59 | → | jedws joins (~jedws@101.184.189.58) |
| 2020-09-17 13:15:43 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) |
| 2020-09-17 13:16:47 | → | mmohammadi9812 joins (~mmohammad@5.238.164.128) |
| 2020-09-17 13:17:10 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-17 13:17:14 | × | gxt quits (~gxt@gateway/tor-sasl/gxt) (Remote host closed the connection) |
| 2020-09-17 13:17:56 | → | gxt joins (~gxt@gateway/tor-sasl/gxt) |
All times are in UTC.