Logs: freenode/#haskell
| 2021-03-23 19:04:36 | × | MilkywayPirate quits (~user@178.157.255.8) (Remote host closed the connection) |
| 2021-03-23 19:05:02 | → | MilkywayPirate joins (~user@178.157.255.8) |
| 2021-03-23 19:05:11 | × | kmein quits (~weechat@static.173.83.99.88.clients.your-server.de) (Quit: ciao kakao) |
| 2021-03-23 19:05:25 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 2021-03-23 19:05:30 | → | kmein joins (~weechat@static.173.83.99.88.clients.your-server.de) |
| 2021-03-23 19:08:18 | × | Sathiana quits (~kath@185-113-98-38.cust.bredband2.com) (Quit: WeeChat 3.1) |
| 2021-03-23 19:08:26 | × | borne quits (~fritjof@200116b8640b5f00a6d9c1e30b1bd3ca.dip.versatel-1u1.de) (Ping timeout: 240 seconds) |
| 2021-03-23 19:08:44 | → | malumore joins (~malumore@151.62.117.161) |
| 2021-03-23 19:10:51 | × | Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 265 seconds) |
| 2021-03-23 19:11:02 | × | MilkywayPirate quits (~user@178.157.255.8) (Ping timeout: 260 seconds) |
| 2021-03-23 19:11:18 | → | ph88_ joins (~ph88@2a02:8109:9e00:7e5c:4978:201f:ec35:67e9) |
| 2021-03-23 19:11:18 | × | elliott_ quits (~elliott_@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 245 seconds) |
| 2021-03-23 19:11:35 | × | v01d4lph4 quits (~v01d4lph4@106.212.133.35) (Remote host closed the connection) |
| 2021-03-23 19:11:53 | → | MilkywayPirate joins (~user@178.157.255.8) |
| 2021-03-23 19:12:33 | <Gurkenglas> | Should WHNF for a function f be the WHNF of f ⊥? |
| 2021-03-23 19:12:47 | × | ph88^ quits (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2021-03-23 19:12:50 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-23 19:13:45 | <monochrom> | No. Not even the same type. |
| 2021-03-23 19:15:02 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 2021-03-23 19:15:02 | <Gurkenglas> | monochrom, yea but except for the not being the same type thing :P |
| 2021-03-23 19:15:07 | <monochrom> | In Haskell, especially because of seq, WHNF for function types is a lambda without any requirement on what's inside the lambda. IIRC this is the "weak" part. |
| 2021-03-23 19:15:08 | × | texasmynsted quits (~texasmyns@99.96.221.112) (Quit: ZNC - http://znc.in) |
| 2021-03-23 19:15:21 | → | atraii joins (~atraii@2601:681:8700:c471:182c:49ac:c430:1f21) |
| 2021-03-23 19:15:43 | <Gurkenglas> | aka, should seq f () apply f to ⊥ until f ⊥ reaches WHNF or the ⊥ is touched |
| 2021-03-23 19:15:52 | <dolio> | No. |
| 2021-03-23 19:15:58 | <Gurkenglas> | Why not? |
| 2021-03-23 19:16:08 | <dolio> | Why would it? |
| 2021-03-23 19:16:18 | × | MilkywayPirate quits (~user@178.157.255.8) (Ping timeout: 245 seconds) |
| 2021-03-23 19:16:26 | × | ph88_ quits (~ph88@2a02:8109:9e00:7e5c:4978:201f:ec35:67e9) (Ping timeout: 268 seconds) |
| 2021-03-23 19:16:37 | <Gurkenglas> | It would undefined and undefined . id observationally equivalent (right?). Would it open some other can of worms? |
| 2021-03-23 19:16:38 | <monochrom> | seq f () is () iff f is \x->something |
| 2021-03-23 19:16:47 | <monochrom> | even \x->bottom |
| 2021-03-23 19:16:50 | <Gurkenglas> | *would make |
| 2021-03-23 19:17:04 | <monochrom> | as said, "weak" means no one looks under the lambda. |
| 2021-03-23 19:17:17 | <Gurkenglas> | monochrom, you are saying it like it is, but i am asking how it should be |
| 2021-03-23 19:18:07 | <monochrom> | How it should be? There are only two choices. (\x->bottom) = bottom or (\x->bottom) ≠ bottom. |
| 2021-03-23 19:18:27 | <Gurkenglas> | right, i am arguing in favor of (\x->bottom) = bottom. Is there a reason against? |
| 2021-03-23 19:18:27 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:b09b:3609:dd4b:42c9) (Remote host closed the connection) |
| 2021-03-23 19:18:29 | <monochrom> | f bottom is highly irrelevant. |
| 2021-03-23 19:18:45 | <monochrom> | seq is a reason against. |
| 2021-03-23 19:19:13 | <Gurkenglas> | Why not make seq (\x->⊥) () = ⊥? |
| 2021-03-23 19:19:30 | <monochrom> | And seq is justified by "laziness can hurt space so we need something for manually kiling laziness" |
| 2021-03-23 19:19:32 | <dolio> | What is `seq id` supposed to do in this 'apply to ⊥' scenario? |
| 2021-03-23 19:19:46 | <Gurkenglas> | dolio, ⊥ |
| 2021-03-23 19:19:46 | <d34df00d> | Doesn't "weak" mean nobody looks under constructors, and not lambdas? |
| 2021-03-23 19:19:47 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-23 19:20:01 | <dolio> | Why would you want `seq id` to blow up? |
| 2021-03-23 19:20:10 | <Gurkenglas> | dolio, because id is strict |
| 2021-03-23 19:20:21 | <dolio> | What does that have to do with anything? |
| 2021-03-23 19:20:28 | <monochrom> | Huh, when was seq supposed to check function strictness? |
| 2021-03-23 19:20:34 | <d34df00d> | I thought "weak" means that, given `data Foo a = Foo a`, Foo undefined `seq` () is to () |
| 2021-03-23 19:20:41 | <Gurkenglas> | dolio, strict functions are exactly those which would make seq ⊥ |
| 2021-03-23 19:20:44 | × | vincenzopalazzo quits (~vincenzop@host-79-30-9-166.retail.telecomitalia.it) (Remote host closed the connection) |
| 2021-03-23 19:20:51 | <dolio> | No. |
| 2021-03-23 19:20:51 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-23 19:20:59 | → | vincenzopalazzo joins (~vincenzop@host-79-30-9-166.retail.telecomitalia.it) |
| 2021-03-23 19:21:09 | <Gurkenglas> | You mean they would not make seq ⊥, or they should not make seq ⊥? |
| 2021-03-23 19:21:39 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 2021-03-23 19:21:46 | <monochrom> | One of "weak" or "head" or both is going to refer to "don't look under lambda". There is also the possibility that the same word also covers "don't look under constructors". |
| 2021-03-23 19:22:06 | <Gurkenglas> | okay, how would you like to call the variant that does look under lambda? |
| 2021-03-23 19:22:09 | <dolio> | seq is supposed to be strict in both arguments. id is not bottom. |
| 2021-03-23 19:23:04 | <Gurkenglas> | dolio, seq could still be strict if it mapped id to the same as bottom |
| 2021-03-23 19:23:13 | <dolio> | It could, but it would be worthless. |
| 2021-03-23 19:23:40 | × | vincenzopalazzo quits (~vincenzop@host-79-30-9-166.retail.telecomitalia.it) (Remote host closed the connection) |
| 2021-03-23 19:23:57 | <monochrom> | "thoroughly analysing normal form" looks under lambdas. >:) |
| 2021-03-23 19:24:00 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-23 19:24:02 | → | MilkywayPirate joins (~user@178.157.255.8) |
| 2021-03-23 19:24:21 | <dolio> | The practical use of seq is to ensure some kind of evaluation, and blowing up when evaluating a strict function is pretty bad behavior. |
| 2021-03-23 19:24:22 | <Gurkenglas> | monochrom, why >:)? Will saying TANF confuse people? |
| 2021-03-23 19:24:24 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-23 19:24:32 | <monochrom> | I made it up. |
| 2021-03-23 19:25:02 | <monochrom> | But everyone tends to get my joke, so it is anything but confusing. |
| 2021-03-23 19:25:37 | <Gurkenglas> | you must still be joking |
| 2021-03-23 19:26:36 | × | MilkywayPirate quits (~user@178.157.255.8) (Read error: Connection reset by peer) |
| 2021-03-23 19:26:55 | <dolio> | Also, per the earlier remark, the 'weak' part is what signals not looking under lambda. 'Weak head normal form' was invented because 'head normal form' does some stuff under lambdas, which is not what actual implementations do. |
| 2021-03-23 19:27:04 | × | rj quits (~x@gateway/tor-sasl/rj) (Ping timeout: 268 seconds) |
| 2021-03-23 19:28:01 | <Gurkenglas> | dolio, you mean, people currently use seq to evaluate "let a = precompute datastrucutre in \x -> a x", and my change would break that? |
| 2021-03-23 19:28:33 | <dolio> | They could. |
| 2021-03-23 19:28:50 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2021-03-23 19:29:01 | <Gurkenglas> | I was hoping for arguments of form "even though this would make undefined observationally indistinguishable from undefined . id, it would introduce this other barrier from Hask being straightforwardly a category:" |
| 2021-03-23 19:29:27 | <ski> | (`\x -> let y = ..x.. in \z -> ..x..y..z..' is sometimes called "serious" currying. also see "run-time compilation") |
| 2021-03-23 19:29:38 | <dolio> | Being practically useless seems like a much better reason than some adherence to mathematical purity. |
| 2021-03-23 19:29:47 | <ski> | (as opposed to "trivial") |
| 2021-03-23 19:30:18 | × | son0p quits (~son0p@181.136.122.143) (Quit: Lost terminal) |
| 2021-03-23 19:30:51 | <ski> | (well, actually. imagine a `seq y' before the '\z -> ...' as well) |
| 2021-03-23 19:30:56 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-23 19:31:00 | <Gurkenglas> | dolio, it would fix my VeryLazyNaturals! Or would you call my usecase useless since it's not useful for any actual application? :P |
| 2021-03-23 19:31:04 | <dolio> | Your description is also type-directed, so might be impossible to actually implement. |
| 2021-03-23 19:31:51 | → | rj joins (~x@gateway/tor-sasl/rj) |
| 2021-03-23 19:32:43 | <monochrom> | Mathematical purity is just as artificial as practice anyway. |
| 2021-03-23 19:34:29 | → | Sornaensis joins (~Sornaensi@077213203030.dynamic.telenor.dk) |
| 2021-03-23 19:35:09 | × | raichoo quits (~raichoo@dslb-178-009-065-121.178.009.pools.vodafone-ip.de) (Quit: Lost terminal) |
| 2021-03-23 19:35:23 | → | Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 2021-03-23 19:35:30 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 2021-03-23 19:36:23 | × | Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 244 seconds) |
| 2021-03-23 19:36:23 | <dolio> | It's important to remember that math isn't always automatically right. If something actually behaves differently than the math, that might just mean the math is not modelling the actual thing correctly. |
| 2021-03-23 19:36:43 | × | carlomagno1 quits (~cararell@148.87.23.10) (Ping timeout: 245 seconds) |
| 2021-03-23 19:36:48 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2021-03-23 19:37:32 | <Gurkenglas> | I suppose instead of blowing up, seq f () could simply proceed to () when f touches its argument ⊥ (but not when f itself resolves to undefined) - this would still make undefined observationally identical to undefined . id, right? |
| 2021-03-23 19:38:19 | × | Sorny quits (~Sornaensi@79.142.232.102) (Ping timeout: 256 seconds) |
All times are in UTC.