Logs: liberachat/#haskell
| 2025-12-28 05:39:17 | <iqubic> | Essentially, I'm trying to model simple combinatorial games like "nim" where I can write a function like "nextMoves :: a -> [a]", but then I realized that different games might have the type for the state variable. |
| 2025-12-28 05:39:28 | <ski> | yea, sounds like record of operations is more sensible, then |
| 2025-12-28 05:40:43 | × | rekahsoft quits (~rekahsoft@70.51.99.245) (Remote host closed the connection) |
| 2025-12-28 05:40:46 | <ski> | btw, sometimes it makes sense to make a function from a record-of-operations, to another (possibly existential) record-of-operations. this being one way to do something similar to the parameterized modules in the module system of the MLs (SML,OCaml) (cf. Backpack) |
| 2025-12-28 05:41:11 | <iqubic> | Yeah, I get what you mean. |
| 2025-12-28 05:41:16 | → | rekahsoft joins (~rekahsoft@70.51.99.245) |
| 2025-12-28 05:41:29 | <haskellbridge> | <slack1256> I liked backpack... |
| 2025-12-28 05:42:16 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 05:42:45 | <ski> | you'd open the returned record in a scope, bringing the skolem into scope, and then use the operations directly. this is a way to do Abstract Data Types |
| 2025-12-28 05:43:03 | <iqubic> | In the basic game of "nim" you have a bunch of distinct piles, and each pile has a bunch of objects. Players take turns removing any amount of objects from a single pile. The winner is the player to make the last valid move. In other words, if you can't make a move, you lose. |
| 2025-12-28 05:43:34 | <ski> | (unlike doing OO via existentials, where you'd open the record, apply an operation to the current state, and then rewrap new state with the operations again, every time) |
| 2025-12-28 05:44:52 | <iqubic> | I can model this as with a state of [Int]. But if I want a similar game, but with the constraint of "after each move, the piles must all have a coprime number of objects", that's also a state of type "[Int]" but a different "nextMoves :: a -> [a]" function. |
| 2025-12-28 05:45:16 | <iqubic> | BTW, Conway et al. call that version "prim", I think. |
| 2025-12-28 05:45:41 | <haskellbridge> | <slack1256> These combinatorial games are not related in anyway right? They just happen to implement a nextMoves function, the lack of laws pushes you to record of functions |
| 2025-12-28 05:46:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-28 05:46:56 | <iqubic> | Yeah, correct. |
| 2025-12-28 05:47:12 | <iqubic> | It's mainly just the "nextMoves" function that relates them. |
| 2025-12-28 05:47:24 | <iqubic> | And I have no laws, because I have just the one function. |
| 2025-12-28 05:47:42 | <haskellbridge> | <slack1256> Right, which is also a non obvious function |
| 2025-12-28 05:48:54 | <ski> | presumably iterating `nextMoves' is meant to lead to a tree where no path is infinite ? |
| 2025-12-28 05:49:23 | <iqubic> | Correct. I'm only interested in finite games here. |
| 2025-12-28 05:49:33 | <ski> | some kind of well-founded order thing |
| 2025-12-28 05:51:06 | <haskellbridge> | <slack1256> Multiple implementations for that in no way related to the days structure to give an instance |
| 2025-12-28 05:51:12 | <ski> | all the outputs of `nextMoves' are presumably strictly less than the input |
| 2025-12-28 05:51:17 | <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 05:51:17 | <haskellbridge> | <slack1256> Data* |
| 2025-12-28 05:51:33 | <iqubic> | ski: For some definition of "strictly less", yeah. |
| 2025-12-28 05:52:02 | <ski> | yea, some arbitrary partial order |
| 2025-12-28 05:52:30 | <ski> | (that is well-founded) |
| 2025-12-28 05:52:47 | <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 05:53:12 | <ski> | yep. the latter seems more reasonable |
| 2025-12-28 05:53:45 | <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 05:54:08 | <iqubic> | I agree. Because different games with completely different rules might want to use similar state representations. |
| 2025-12-28 05:54:30 | <iqubic> | ski: Currently my planned API doesn't need a way to tell which states are smaller. |
| 2025-12-28 05:55:01 | <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 05:55:20 | <ski> | (iow, you don't need more than one operation, to be able to have a law) |
| 2025-12-28 05:55:43 | <iqubic> | What do you mean by well-foundedness? |
| 2025-12-28 05:58:01 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 05:58:38 | <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 05:59:14 | <iqubic> | Right I see. |
| 2025-12-28 06:00:53 | <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:02:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-12-28 06:02:39 | <iqubic> | forall a. let a' = nextMoves a in all [ length (nextMoves opt) < length a' | opt <- nextMoves a] |
| 2025-12-28 06:02:51 | <iqubic> | Or something like that. |
| 2025-12-28 06:03:27 | <iqubic> | Basically, if you keep iterating nextMoves function, you should keep getting less and less options. |
| 2025-12-28 06:03:55 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-12-28 06:07:06 | <ski> | not necessarily |
| 2025-12-28 06:08:21 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2025-12-28 06:08:22 | <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 06:09:17 | <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 06:09:53 | <ski> | you could have the branching explode, and still have finite depth for every path |
| 2025-12-28 06:10:16 | <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 06:10:47 | <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 06:11:02 | <ski> | ah, okay |
| 2025-12-28 06:13:25 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 06:18:24 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-28 06:29:12 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 06:34:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-12-28 06:35:20 | × | synchromesh quits (~john@2406:5a00:2412:2c00:7842:6802:4767:2e5b) (Read error: Connection reset by peer) |
| 2025-12-28 06:36:46 | → | synchromesh joins (~john@2406:5a00:2412:2c00:7842:6802:4767:2e5b) |
| 2025-12-28 06:40:06 | <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 06:40:54 | <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 06:42:24 | <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 06:45:19 | <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:02:17 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 07:06:57 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-28 07:13:20 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-12-28 07:18:05 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 07:23:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-12-28 07:29:18 | → | euphores joins (~SASL_euph@user/euphores) |
| 2025-12-28 07:31:12 | × | sroso quits (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2025-12-28 07:33:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 07:38:22 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-28 07:45:32 | <[exa]> | hololeap: you can wrap the set in a newtype that imposes the constraint, with similar tradeoffs like with other newtype wraps (inconvenient but coerces well) and typeclass constraints on data types (generally hated) |
| 2025-12-28 07:49:00 | <[exa]> | iqubic: people usually have these "operation records" for various backend implementations for whatever, e.g. here: https://hackage-content.haskell.org/package/tls-2.1.13/docs/Network-TLS.html#t:Backend or here: https://hackage.haskell.org/package/selda-0.5.2.0/docs/Database-Selda-Backend.html#t:SeldaBackend . TBH quite easy to go that way, and very easy to slap on a typeclass later, in case you |
| 2025-12-28 07:49:02 | <[exa]> | decide you want to infer which backend to use where. |
| 2025-12-28 07:49:15 | <hololeap> | hm, ok. I was looking into a different instance of Apply for Map (different than the one defined in semigroupoids) and ultimately it requires (Ord k, Semigroup a) => Map k a |
| 2025-12-28 07:49:19 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 07:50:04 | <hololeap> | but Apply is a class for Type -> Type |
| 2025-12-28 07:50:19 | <[exa]> | hololeap: why though (kinda curious, and also usually this has been a common instance of xyz issues) |
| 2025-12-28 07:51:15 | <hololeap> | mostly just out of curiosity. the current Apply instance feels very niche since it uses Map.intersectionWith under the hood |
| 2025-12-28 07:53:26 | <hololeap> | I was looking into an instance that would use something like Map.unionWith (<>) |
| 2025-12-28 07:53:39 | <hololeap> | though not exactly that |
| 2025-12-28 07:53:47 | <Leary> | That sounds like `Semigroup` instance instead. |
| 2025-12-28 07:53:58 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-28 07:54:39 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 2025-12-28 07:55:04 | <[exa]> | hololeap: that can't do applicative though, right? (you'd need a default function and default parameter) |
| 2025-12-28 07:55:26 | <hololeap> | right, Apply is Applicative sans `pure`, |
| 2025-12-28 07:55:30 | <[exa]> | so yeah that would be a (specialized) semigroup |
| 2025-12-28 07:55:47 | <hololeap> | just the <*> part of Applicative |
| 2025-12-28 07:55:50 | <[exa]> | no in this case even `ap` would require the defaults |
| 2025-12-28 07:56:47 | → | ystael joins (~ystael@user/ystael) |
| 2025-12-28 07:57:06 | <hololeap> | anyway, this wasn't really a problem I needed to solve, just an exploration of ideas |
| 2025-12-28 07:58:58 | <hololeap> | @hackage quickcheck-classes -- makes it easy to verify the Apply laws |
| 2025-12-28 07:58:58 | <lambdabot> | https://hackage.haskell.org/package/quickcheck-classes -- makes it easy to verify the Apply laws |
| 2025-12-28 08:00:01 | × | tt1231607 quits (~tt1231@75.185.104.199) (Quit: The Lounge - https://thelounge.chat) |
| 2025-12-28 08:03:17 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-28 08:05:33 | → | tt1231607 joins (~tt1231@75.185.104.199) |
| 2025-12-28 08:08:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-28 08:19:04 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
All times are in UTC.