Newest at the top
| 2025-10-08 19:37:36 +0200 | <EvanR> | implicitly at some point dealing with non empty lists and so the restriction of head on that domain is total |
| 2025-10-08 19:37:04 +0200 | <tomsmeding> | i.e. the opposite of what you're saying :p |
| 2025-10-08 19:36:56 +0200 | <tomsmeding> | doesn't that amount to an (unstated) proof that it isn't actually partial |
| 2025-10-08 19:36:48 +0200 | <EvanR> | yeah ideally you can prove it |
| 2025-10-08 19:36:26 +0200 | <__monty__> | What I really mean is that the lists often end up never being empty where I call head. |
| 2025-10-08 19:36:19 +0200 | <EvanR> | this is all avoided if you can structure it so the compiler checks all the cases for you |
| 2025-10-08 19:35:41 +0200 | <tomsmeding> | intentionally partial, you mean? |
| 2025-10-08 19:34:28 +0200 | <__monty__> | I don't mind spending time on cases that aren't actually partial but there's lots of cases that are. |
| 2025-10-08 19:34:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-10-08 19:32:16 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b551:deec:8ee1:7922) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-10-08 19:32:01 +0200 | <EvanR> | murphy's law corrolary, if you don't have the proof then it will crash |
| 2025-10-08 19:31:27 +0200 | <EvanR> | ain't that something |
| 2025-10-08 19:30:16 +0200 | <__monty__> | Sometimes I don't have proof but there's also absence of proof of the contrary. |
| 2025-10-08 19:28:39 +0200 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2025-10-08 19:27:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-10-08 19:26:25 +0200 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 264 seconds) |
| 2025-10-08 19:23:57 +0200 | <EvanR> | in your case control F for last and check for proof |
| 2025-10-08 19:23:08 +0200 | <EvanR> | which is often not that hard to come up with, it's just that it's invisible |
| 2025-10-08 19:22:46 +0200 | <EvanR> | every use of tail or last etc has to come with a possibly invisible proof that the list isn't empty |
| 2025-10-08 19:22:04 +0200 | <EvanR> | unless the objective is to crash your program in a potentially hard to explain way |
| 2025-10-08 19:15:39 +0200 | Googulator65 | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 19:15:37 +0200 | Googulator10 | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-08 19:04:12 +0200 | MelodyOwO | (~MelodyOwO@user/MelodyOwO) (Quit: Leaving.) |
| 2025-10-08 19:01:10 +0200 | Googulator60 | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 19:00:47 +0200 | Googulator65 | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-08 18:59:03 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-10-08 18:55:38 +0200 | Googulator60 | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-08 18:55:37 +0200 | Googulator | (~Googulato@193-226-241-224.pool.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 18:48:37 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-10-08 18:35:46 +0200 | Googulator | (~Googulato@193-226-241-224.pool.digikabel.hu) |
| 2025-10-08 18:35:39 +0200 | Googulator | (~Googulato@193-226-241-224.pool.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 18:30:39 +0200 | Googulator | (~Googulato@193-226-241-224.pool.digikabel.hu) |
| 2025-10-08 18:30:27 +0200 | Googulator | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 18:27:27 +0200 | Tuplanolla | (~Tuplanoll@91-159-187-167.elisa-laajakaista.fi) Tuplanolla |
| 2025-10-08 18:08:14 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b551:deec:8ee1:7922) |
| 2025-10-08 18:07:22 +0200 | <haskellbridge> | <sm> for this reason ? Suppress them if you must |
| 2025-10-08 18:05:58 +0200 | <__monty__> | But the all the warnings about head and tail et al. are so noisy : ( |
| 2025-10-08 18:05:21 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2025-10-08 18:00:51 +0200 | Googulator | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-08 18:00:43 +0200 | Googulator | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 17:58:03 +0200 | Googulator45 | Googulator |
| 2025-10-08 17:55:50 +0200 | <haskellbridge> | <sm> bwe: 100%, removing such partial code from your program is the best when possible |
| 2025-10-08 17:55:42 +0200 | Googulator | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-08 17:55:42 +0200 | Googulator45 | (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-08 17:54:45 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-10-08 17:54:36 +0200 | ft | (~ft@p4fc2a207.dip0.t-ipconnect.de) ft |
| 2025-10-08 17:54:28 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-10-08 17:50:59 +0200 | trickard_ | trickard |
| 2025-10-08 17:48:19 +0200 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2025-10-08 17:41:45 +0200 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) |