Logs: liberachat/#haskell
| 2025-11-14 17:20:44 | <comerijn> | dolio: It's not "somewhat unspecified" it's explicitly undefined |
| 2025-11-14 17:24:10 | <haskellbridge> | <Zemyla> You wouldn't have to de/reconstruct the digits. |
| 2025-11-14 17:24:14 | <jreicher> | dolio: No, I'm not sure they are inherently effectful. From what I can see you can still have church-rosser for delimited continuations |
| 2025-11-14 17:25:31 | × | acidjnk quits (~acidjnk@p200300d6e717192040ac95c287188d84.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2025-11-14 17:28:46 | × | tromp quits (~textual@2001:1c00:3487:1b00:f8db:b16d:6074:eae9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-11-14 17:30:28 | → | tromp joins (~textual@2001:1c00:3487:1b00:f8db:b16d:6074:eae9) |
| 2025-11-14 17:30:41 | → | Googulator89 joins (~Googulato@team.broadbit.hu) |
| 2025-11-14 17:32:43 | <dolio> | reset ((shift _. 1) + (shift _. 2)) |
| 2025-11-14 17:32:49 | <dolio> | Is that 1 or 2? |
| 2025-11-14 17:33:47 | × | Googulator85 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-14 17:35:18 | <haskellbridge> | <Zemyla> Also, I'm wondering if you'd get any kind of significant savings by having sized :: Sized a => a -> Int# instead of a -> Int. |
| 2025-11-14 17:36:05 | <Leary> | loonycyborg: When an exception is raised, it prevents further execution. As such, there will only ever be one exception to handle. The issue is that it's undefined /which/ exception that will be. |
| 2025-11-14 17:36:30 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-11-14 17:38:04 | <haskellbridge> | <loonycyborg> It's not necessarily true for particular runtime. They still can evaluate other parts of complex value even if got exception from one of the parts |
| 2025-11-14 17:38:09 | <jreicher> | dolio: I don't know, but I can see in the literature references to delimited continuations with church-rosser. I'm trying to figure out how they work now. They build on lambda-mu, but even lambda-mu doesn't have church-rosser I think. |
| 2025-11-14 17:39:24 | <haskellbridge> | <loonycyborg> You can implement exceptions as any type implicitly becoming Either |
| 2025-11-14 17:40:06 | × | tromp quits (~textual@2001:1c00:3487:1b00:f8db:b16d:6074:eae9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-11-14 17:41:43 | <haskellbridge> | <loonycyborg> That's the whole deal with "pure" exceptions, all parts of evaluation chain exist no matter what. But runtime can evaluate them in any order |
| 2025-11-14 17:42:03 | <dolio> | The only ways I know of off hand to fix this are 1) enforce linear use of continuations and 2) fix an evaluation order so that Church-Rosser is a vacuous property. |
| 2025-11-14 17:42:13 | <haskellbridge> | <loonycyborg> if runtime picks just one exception among them then whole calculation isn't pure anymore |
| 2025-11-14 17:42:34 | <haskellbridge> | <loonycyborg> but if it takes all in no particular order it still can be pure |
| 2025-11-14 17:42:41 | <dolio> | But maybe there are others. |
| 2025-11-14 17:43:08 | → | tromp joins (~textual@2001:1c00:3487:1b00:f8db:b16d:6074:eae9) |
| 2025-11-14 17:43:46 | <haskellbridge> | <loonycyborg> Like exceptions will be as deterministic as non-exceptional values |
| 2025-11-14 17:45:21 | → | haltingsolver joins (~cmo@2604:3d09:207f:8000::d1dc) |
| 2025-11-14 17:45:35 | × | acarrico1 quits (~acarrico@pppoe-209-99-223-51.greenmountainaccess.net) (Ping timeout: 244 seconds) |
| 2025-11-14 17:45:54 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2025-11-14 17:48:26 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-11-14 17:52:50 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-11-14 17:55:47 | → | Googulator43 joins (~Googulato@team.broadbit.hu) |
| 2025-11-14 17:57:24 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-11-14 17:58:55 | × | Googulator89 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-14 18:01:03 | <haskellbridge> | <Zemyla> In practice, how much does it matter that exceptions are non-deterministic? If they show up in a pure computation, then that computation was hosed anyway. If they show up in non-parallel IO, then it's deterministic. And if they show up in parallel IO, then you either handled them incorrectly or it was hosed. |
| 2025-11-14 18:02:50 | <davean> | wait who said it was deterministic if it showed up in non-parallel IO? |
| 2025-11-14 18:03:01 | <davean> | and what do you mean that the computation for pure computation was hosed anyway? |
| 2025-11-14 18:03:11 | <davean> | You could just rerun it and not get the exception. |
| 2025-11-14 18:03:29 | <haskellbridge> | <Zemyla> If you have quot 1 0 + quot minBound (-1), does it really matter whether it threw a division by zero or an overflow? |
| 2025-11-14 18:04:05 | <davean> | Yes, that says something about what type you're in. More importantly thoguh it matters a LOT if what it threw was OutOfMemory |
| 2025-11-14 18:04:23 | <davean> | or AsyncException |
| 2025-11-14 18:04:26 | <davean> | or ... |
| 2025-11-14 18:06:03 | → | Googulator78 joins (~Googulato@team.broadbit.hu) |
| 2025-11-14 18:08:26 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-11-14 18:09:19 | × | Googulator43 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-14 18:09:34 | × | tromp quits (~textual@2001:1c00:3487:1b00:f8db:b16d:6074:eae9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-11-14 18:10:32 | → | eron joins (~eron@187.56.155.181) |
| 2025-11-14 18:10:47 | → | Googulator15 joins (~Googulato@team.broadbit.hu) |
| 2025-11-14 18:14:05 | × | Googulator78 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-14 18:16:02 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-11-14 18:20:38 | → | myxos joins (~myxos@2001:579:8380:f20:e1c:e3b9:dc1a:668f) |
| 2025-11-14 18:22:17 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-11-14 18:23:04 | × | myxokephale quits (~myxos@2001:579:8380:f20:bec3:508e:c208:bae7) (Ping timeout: 246 seconds) |
| 2025-11-14 18:23:21 | <dolio> | Zemyla: The problem is catching them. |
| 2025-11-14 18:25:20 | <jreicher> | dolio: I think the problem in your example is that the "handler" is given in the shift operator. The problem is solved if it's given in the reset operator. Then there can be only one handler per capture scope. |
| 2025-11-14 18:25:39 | → | Googulator53 joins (~Googulato@team.broadbit.hu) |
| 2025-11-14 18:26:07 | <jreicher> | Doesn't mean there aren't still other problems though |
| 2025-11-14 18:26:34 | <dolio> | Algebraic effects have handlers that let you handle the effects, but then you need the effects to have a deterministic order to get deterministic handler results. |
| 2025-11-14 18:27:55 | <jreicher> | That's what I would expect. I'm still thinking it through, and I'm still trying to figure out how the different calculi and operator designs relate. |
| 2025-11-14 18:28:49 | × | Googulator15 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-14 18:28:55 | <jreicher> | Have to head off for a bit. Thanks heaps for your thoughts; helps a lot. |
| 2025-11-14 18:30:55 | <dolio> | My example is just using shift/reset to implement exceptions. |
| 2025-11-14 18:31:18 | <dolio> | The exact same problem happens if you use algebraic effects for them. |
| 2025-11-14 18:31:55 | <dolio> | handle (raise 1 + raise 2) with cases {r} -> r ; {raise n -> _} -> n |
| 2025-11-14 18:34:05 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2025-11-14 18:39:16 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 2025-11-14 18:46:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-14 18:48:45 | × | Googulator53 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-14 18:48:56 | → | humasect_ joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-11-14 18:49:39 | → | humasec__ joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-11-14 18:49:49 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 260 seconds) |
| 2025-11-14 18:54:06 | × | eron quits (~eron@187.56.155.181) (Quit: Client closed) |
| 2025-11-14 18:54:35 | → | polykernel joins (~polykerne@user/polykernel) |
| 2025-11-14 18:55:04 | × | humasec__ quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 256 seconds) |
| 2025-11-14 18:56:16 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2025-11-14 19:00:08 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 2025-11-14 19:04:09 | <haskellbridge> | <loonycyborg> davean: I don't think you'd be ever able to handle out of memory error as a pure exception. Because if results are determined by something other than values themselves(like where are they stored) then things are most definitely not pure anymore. |
| 2025-11-14 19:04:47 | <haskellbridge> | <loonycyborg> While something like integer overflow can be handled as a pure exception. Because same calculation with same values will always cause overflow |
| 2025-11-14 19:06:11 | <haskellbridge> | <loonycyborg> Basically if same calculation gives different results when repeated then it's not pure. |
| 2025-11-14 19:09:34 | <haskellbridge> | <loonycyborg> If you have a tuple with two values that both cause some overflow exception or other deterministic condition like that then you still can get a deterministic list of those exceptions and entire thing will be pure because it depends only on input values |
| 2025-11-14 19:09:42 | <davean> | Leary: you can't handle them in the pure code, but you CAN handle them in the IO and then retry |
| 2025-11-14 19:10:15 | <haskellbridge> | <loonycyborg> while memory overflow handling depends on other parameters that we don't track so it cannot ever be pure |
| 2025-11-14 19:12:43 | <haskellbridge> | <loonycyborg> I guess we could track memory as extra value(s) and make things pure that way but that would be just excessively complex :P |
| 2025-11-14 19:14:16 | <davean> | I mean you can see it failed, free memory, and then try again |
| 2025-11-14 19:15:45 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 2025-11-14 19:18:38 | → | Square3 joins (~Square@user/square) |
| 2025-11-14 19:21:40 | × | humasect_ quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-11-14 19:21:55 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-11-14 19:24:51 | <haskellbridge> | <loonycyborg> This will have to be done in IO monad in any case. |
| 2025-11-14 19:25:21 | <haskellbridge> | <loonycyborg> Unless runtime handles it transparently for the program. |
| 2025-11-14 19:25:24 | × | haltingsolver quits (~cmo@2604:3d09:207f:8000::d1dc) (Ping timeout: 260 seconds) |
| 2025-11-14 19:27:33 | <haskellbridge> | <loonycyborg> Handling out-of-memory conditions is notoriously hard problem. In this OOM state you can't rely on any functions that allocate more memory for any reason. |
| 2025-11-14 19:27:49 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 2025-11-14 19:31:30 | × | notzmv quits (~umar@user/notzmv) (Ping timeout: 244 seconds) |
| 2025-11-14 19:32:18 | <haskellbridge> | <loonycyborg> In practice any OOM handlers don't get much workout either. If PC runs out of memory OS either moves things to swapfile or kills some processes with signal that can't be trapped |
| 2025-11-14 19:32:46 | <davean> | Actually there is a clear signal if you don't have overcommit, you get an alloc fail |
| 2025-11-14 19:34:03 | <davean> | Lots of quality software handles these signals. Thats not the point though, the point is that exceptions in pure code *are not deterministic* |
| 2025-11-14 19:36:24 | <haskellbridge> | <loonycyborg> Some of them most definitely aren't |
| 2025-11-14 19:38:21 | <haskellbridge> | <loonycyborg> And trying to handle them purely would violate all sort of things like referential transparency :P |
| 2025-11-14 19:39:10 | <haskellbridge> | <loonycyborg> But things like integer overflow and divide by zero are deterministic and can be considered separate form of resulting value. |
| 2025-11-14 19:39:43 | → | eron joins (~eron@187.56.155.181) |
| 2025-11-14 19:40:31 | × | mreh quits (~matthew@host86-146-25-125.range86-146.btcentralplus.com) (Quit: Lost terminal) |
All times are in UTC.