Newest at the top
| 2025-12-28 08:18:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 08:13:20 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-12-28 08:06:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-28 08:02:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 07:45:19 +0100 | <hololeap> | are there any language extensions now days that can let you write a Functor instance for Set? some way to inject a constraint requirement into an existing function, or something? |
| 2025-12-28 07:42:24 +0100 | <iqubic> | But this mathematical theory has little to do with Haskell at this point and I have gotten my orginal design question answered already. |
| 2025-12-28 07:40:54 +0100 | <iqubic> | Except, it's more like a DAG, because there might be multiple possible ways to get from the current state to some future state. |
| 2025-12-28 07:40:06 +0100 | <iqubic> | Essentially, if a level of my tree has N members, then all children there should have strictly less than N descendants, except for the root. |
| 2025-12-28 07:36:46 +0100 | synchromesh | (~john@2406:5a00:2412:2c00:7842:6802:4767:2e5b) synchromesh |
| 2025-12-28 07:35:20 +0100 | synchromesh | (~john@2406:5a00:2412:2c00:7842:6802:4767:2e5b) (Read error: Connection reset by peer) |
| 2025-12-28 07:34:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-12-28 07:29:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 07:18:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-28 07:13:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 07:11:02 +0100 | <ski> | ah, okay |
| 2025-12-28 07:10:47 +0100 | <ski> | (there's not even a need for the branching to be finite, it could still be well-founded. although, possibly, in your case, you're only interested in finite branching) |
| 2025-12-28 07:10:16 +0100 | <iqubic> | Yeah. But in my case, I want you to always have strictly less moves as you go along. That's the main case I'm interested in exploring. |
| 2025-12-28 07:09:53 +0100 | <ski> | you could have the branching explode, and still have finite depth for every path |
| 2025-12-28 07:09:17 +0100 | <ski> | the important part is that each state is getting closer to a minimal element (a leaf, one which has zero successors), on each step |
| 2025-12-28 07:08:22 +0100 | <ski> | a tree that at each node at depth `n' has either zero or `n' branches of that node could still be well-founded |
| 2025-12-28 07:08:21 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2025-12-28 07:07:06 +0100 | <ski> | not necessarily |
| 2025-12-28 07:03:55 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-12-28 07:03:27 +0100 | <iqubic> | Basically, if you keep iterating nextMoves function, you should keep getting less and less options. |
| 2025-12-28 07:02:51 +0100 | <iqubic> | Or something like that. |
| 2025-12-28 07:02:39 +0100 | <iqubic> | forall a. let a' = nextMoves a in all [ length (nextMoves opt) < length a' | opt <- nextMoves a] |
| 2025-12-28 07:02:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-12-28 07:00:53 +0100 | <ski> | in terms of `nextMoves', instead of `forall y. y < x -> P y', we'd say `forall y. elem y (nextMoves x) = True -> P y'. iow, assuming that it holds for all the possible next states, it should be able to show it holds for the current state |
| 2025-12-28 06:59:14 +0100 | <iqubic> | Right I see. |
| 2025-12-28 06:58:38 +0100 | <ski> | for a strict order relation `<', a property like `forall P. (forall x. (forall y. y < x -> P y) -> P x) -> forall x. P x'. if we were talking about natural numbers, this would be called "strong induction" : you can prove a property `P' holds for all `x', if you can prove it holds for all `x', under the assumption it holds for all `y' that are strictly less than `x' |
| 2025-12-28 06:58:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 06:55:43 +0100 | <iqubic> | What do you mean by well-foundedness? |
| 2025-12-28 06:55:20 +0100 | <ski> | (iow, you don't need more than one operation, to be able to have a law) |
| 2025-12-28 06:55:01 +0100 | <ski> | in any case, even without an explicit order relation (computationally irrelevant or not), you should still be able to express a well-foundedness law for `nextMoves' |
| 2025-12-28 06:54:30 +0100 | <iqubic> | ski: Currently my planned API doesn't need a way to tell which states are smaller. |
| 2025-12-28 06:54:08 +0100 | <iqubic> | I agree. Because different games with completely different rules might want to use similar state representations. |
| 2025-12-28 06:53:45 +0100 | <ski> | (you could put the order relation as a second operation in the record .. but perhaps you have no use for it, at all, at run-time) |
| 2025-12-28 06:53:12 +0100 | <ski> | yep. the latter seems more reasonable |
| 2025-12-28 06:52:47 +0100 | <iqubic> | But my main question was "Do I model this as a typeclass with one function or a record of one function"? |
| 2025-12-28 06:52:30 +0100 | <ski> | (that is well-founded) |
| 2025-12-28 06:52:02 +0100 | <ski> | yea, some arbitrary partial order |
| 2025-12-28 06:51:33 +0100 | <iqubic> | ski: For some definition of "strictly less", yeah. |
| 2025-12-28 06:51:17 +0100 | <haskellbridge> | <slack1256> Data* |
| 2025-12-28 06:51:17 +0100 | <iqubic> | Basically, I've been reading the book "Winning Ways For Your Mathematical Plays" by Berlekamp, Guy, and Conway, and I want to implement some of these things in Haskell. |
| 2025-12-28 06:51:12 +0100 | <ski> | all the outputs of `nextMoves' are presumably strictly less than the input |
| 2025-12-28 06:51:06 +0100 | <haskellbridge> | <slack1256> Multiple implementations for that in no way related to the days structure to give an instance |
| 2025-12-28 06:49:33 +0100 | <ski> | some kind of well-founded order thing |
| 2025-12-28 06:49:23 +0100 | <iqubic> | Correct. I'm only interested in finite games here. |
| 2025-12-28 06:48:54 +0100 | <ski> | presumably iterating `nextMoves' is meant to lead to a tree where no path is infinite ? |
| 2025-12-28 06:47:42 +0100 | <haskellbridge> | <slack1256> Right, which is also a non obvious function |