Logs: liberachat/#haskell
| 2026-02-24 09:44:31 | <__monty__> | dminuoso: I think they're talking about lattices. |
| 2026-02-24 09:44:33 | <tomsmeding> | "lattice" implies that such upper bounds (and lower bounds) are unique |
| 2026-02-24 09:44:57 | <tomsmeding> | so Bounded is not a "bounded lattice", it's a "partial order with minimal and maximal elements" |
| 2026-02-24 09:45:07 | <tomsmeding> | which... we knew 10 minutes ago already |
| 2026-02-24 09:45:08 | <dminuoso> | tomsmeding: Trying to understand what "maximal element of the entire set" would mean, if it was not a unique smallest supremum of any subset of the set. |
| 2026-02-24 09:45:20 | <tomsmeding> | welcome to math where there are unintuitive counterexamples |
| 2026-02-24 09:45:27 | <dminuoso> | Oh hold on. |
| 2026-02-24 09:45:35 | <dminuoso> | The favourite person in a group could work I suppose. |
| 2026-02-24 09:46:10 | <jreicher> | tomsmeding: clopen is my favourite |
| 2026-02-24 09:46:44 | <dminuoso> | Hold on what I just said makes no sense. |
| 2026-02-24 09:46:52 | <jreicher> | dminuoso: are you wondering what the difference between lattice and having max and min is? |
| 2026-02-24 09:47:06 | <dminuoso> | The uniqueness is not of any subset, but a *pair* of elements. |
| 2026-02-24 09:47:11 | <jreicher> | Yes |
| 2026-02-24 09:47:18 | <jreicher> | (But I'm still not sure what the initial question was) |
| 2026-02-24 09:47:24 | <tomsmeding> | (which are, in particular, subsets) |
| 2026-02-24 09:47:29 | <tomsmeding> | jreicher: I think yes |
| 2026-02-24 09:47:46 | <tomsmeding> | do you have an example of a bounded partial order that is not a lattice? |
| 2026-02-24 09:47:51 | → | fp joins (~Thunderbi@wireless-86-50-141-0.open.aalto.fi) |
| 2026-02-24 09:47:53 | <tomsmeding> | (I don't) |
| 2026-02-24 09:48:02 | <Leary> | dminuoso: Maximal means nothing else is bigger than it, though perhaps the /greatest/ element is a better notion for a bound, in which case its bigger than everything. |
| 2026-02-24 09:48:22 | <int-e> | I'm confused; Bounded just defined two points called minBound and maxBound? So it would work for partial orders too (and thus, lattices) |
| 2026-02-24 09:48:44 | <tomsmeding> | int-e: the original original question was why Bounded does not have Ord as a superclass, which had answer "partial orders are a thing" |
| 2026-02-24 09:48:45 | <Leary> | tomsmeding: You can just contrive a small finite partial order on paper. |
| 2026-02-24 09:48:58 | <Leary> | It's not hard to make a counterexample. |
| 2026-02-24 09:49:03 | <int-e> | tomsmeding: Ah. I see, lack of context strikes again. |
| 2026-02-24 09:49:08 | <tomsmeding> | int-e: then we thought "but is Bounded then a bounded lattice?", to which the answer is no, as no unique joins/meets are required |
| 2026-02-24 09:49:16 | <tomsmeding> | now we want an example of that :p |
| 2026-02-24 09:49:54 | <jreicher> | tomsmeding: by "bounded" do we just mean the entire set (rather than any pair) as an infimum and supremum? |
| 2026-02-24 09:49:59 | <tomsmeding> | yes |
| 2026-02-24 09:50:02 | <tomsmeding> | or at least, I do |
| 2026-02-24 09:50:11 | <__monty__> | dminuoso: If you're looking for any example of it whatsoever I think the one tomsmeding mentioned is the easiest. Take any set with more than one element and all subsets of that set, the partial order relation is subset-of, the minBound would be the empty set, the maxBound the set you started with, some pairs of subsets won't satisfy the subset-of relation in either order. So this can implement Bounded |
| 2026-02-24 09:50:17 | <__monty__> | but not Ord. |
| 2026-02-24 09:50:30 | <jreicher> | Then just "duplicate" a meet or join. It will no longer be a lattice. |
| 2026-02-24 09:50:48 | <tomsmeding> | __monty__: yes, we figured that out, but we're already at the next question: that thing is clearly a lattice, but we want a not-lattice that is nevertheless a bounded partial order |
| 2026-02-24 09:51:04 | <int-e> | Is it okay if it's? 0 < 1,2 < 3,4 < 5 has minimal and maximal elements but 3,4 have no infimum and 1,2 have no supremum |
| 2026-02-24 09:51:29 | <tomsmeding> | but there's no unique maximum |
| 2026-02-24 09:51:30 | <__monty__> | tomsmeding: The conversation has moved on but I'm not sure it's not leaving dminuoso behind ; ) |
| 2026-02-24 09:51:42 | <tomsmeding> | ah :p |
| 2026-02-24 09:51:43 | <int-e> | tomsmeding: 5 is the unique maximal element here |
| 2026-02-24 09:51:47 | <Leary> | tomsmeding: https://gist.github.com/LSLeary/c52be6739f5815d13a6774d46dcbde75 |
| 2026-02-24 09:51:53 | <tomsmeding> | int-e: no, because 2 !< 5 |
| 2026-02-24 09:52:00 | <int-e> | tomsmeding: it's transitive |
| 2026-02-24 09:52:07 | <tomsmeding> | oh notation |
| 2026-02-24 09:52:14 | <tomsmeding> | yes |
| 2026-02-24 09:52:27 | <tomsmeding> | yes perfect |
| 2026-02-24 09:52:36 | <jreicher> | I think int-e and I are thinking the same. 0 is one end and 5 is the other. The join of 1 and 2 is not unique |
| 2026-02-24 09:52:37 | tomsmeding | closes the image editor |
| 2026-02-24 09:52:41 | <int-e> | tomsmeding: sorry, I'm trying to cast a Hesse diagram in ASCII here |
| 2026-02-24 09:52:51 | <int-e> | the translation is a bit lossy ;) |
| 2026-02-24 09:52:55 | <jreicher> | int-e: have I understood you correctly? |
| 2026-02-24 09:53:18 | <tomsmeding> | Leary: that notation in your gist is a bit ambiguous, what do the /\ on line 4 mean :p |
| 2026-02-24 09:53:19 | <int-e> | Hasse diagram, meh. |
| 2026-02-24 09:54:13 | <dminuoso> | Leary: Did you mean it like https://paste.tomsmeding.com/ayvscggm ? |
| 2026-02-24 09:54:34 | <__monty__> | I'm also interested in kind of the reverse question, are there structures that can implement Ord but not Bounded? Something like a cyclical ordering? I suppose only if we put the "laws" of the class aside. |
| 2026-02-24 09:54:43 | <dminuoso> | Or well, maybe without that x even |
| 2026-02-24 09:54:51 | <merijn> | __monty__: Clearly we need a PartialOrd superclass of Ord that implement "a -> a -> Maybe Ordering" |
| 2026-02-24 09:54:53 | <dminuoso> | Not sure if it makes it less or more ambiguous |
| 2026-02-24 09:54:55 | <tomsmeding> | dminuoso: the x must be a crossing of lines without a node, yes |
| 2026-02-24 09:55:11 | <tomsmeding> | __monty__: Integer? |
| 2026-02-24 09:56:14 | <jreicher> | __monty__: if the order is transitive and antisymmetric it can't be cyclical |
| 2026-02-24 09:56:24 | <Leary> | tomsmeding: Cross connections. Bit hard in slapdash asci. I revised it with an X if that's clearer. |
| 2026-02-24 09:56:52 | <tomsmeding> | yes, which is also what dminuoso made of it |
| 2026-02-24 09:57:21 | <__monty__> | tomsmeding: Oh, obviously, darn, less interesting than I thought. |
| 2026-02-24 09:59:28 | <int-e> | tomsmeding: here is what it looks like properly: https://int-e.eu/~bf3/tmp/hapo.png |
| 2026-02-24 10:01:03 | <__monty__> | TIL, min and max can return a value that is distinct from their arguments, as long as it is == to one of their arguments. |
| 2026-02-24 10:01:25 | <__monty__> | I assume that's for some sort of canonicalization? |
| 2026-02-24 10:01:58 | <tomsmeding> | int-e: yes |
| 2026-02-24 10:02:13 | <Leary> | __monty__: `==` values aren't supposed to be distinguishable in the first place. |
| 2026-02-24 10:02:35 | tomsmeding | has a meeting -> afk |
| 2026-02-24 10:08:00 | → | xdminsy joins (~xdminsy@112.10.231.192) |
| 2026-02-24 10:08:16 | <__monty__> | Leary: But things like Arg exist and they exist because they are useful, I assume. |
| 2026-02-24 10:08:35 | → | morj joins (~morj@user/morj) |
| 2026-02-24 10:11:25 | <Leary> | It's occasionally pragmatic to break the law, yes. `Arg` actually wouldn't be useful if people always remembered to write `fooBy` instead of just `foo :: Ord a => ...`. |
| 2026-02-24 10:11:52 | <Leary> | At least, not useful enough to justify its existence. |
| 2026-02-24 10:13:02 | → | petrichor joins (~jez@user/petrichor) |
| 2026-02-24 10:13:29 | × | xdminsy quits (~xdminsy@112.10.231.192) (Quit: Konversation terminated!) |
| 2026-02-24 10:16:01 | → | morj_away joins (~morj@user/morj) |
| 2026-02-24 10:16:37 | × | morj quits (~morj@user/morj) (Ping timeout: 272 seconds) |
| 2026-02-24 10:17:10 | <int-e> | `fooBy` is awful when you have data structures with invariants (consider an implementation of containers that implements Data.Map using Data.Set with `Arg k v` elements) |
| 2026-02-24 10:18:20 | <int-e> | (So it's not just programmer laziness.) |
| 2026-02-24 10:20:38 | × | morj_away quits (~morj@user/morj) (Client Quit) |
| 2026-02-24 10:20:56 | int-e | ponders extending this argument to saying that type classes are useles; people could just pass around the right operations explicitly. :-P |
| 2026-02-24 10:21:57 | <Leary> | Even in such a case, `Arg` should be handrolled in the guts of containers, not exposed from base. |
| 2026-02-24 10:23:43 | <Leary> | Re the extended argument, it's really about typeclasses with laws being used to implement operations that /don't require/ those laws and are useful in their absence; the typeclass method merely being a default choice. |
| 2026-02-24 10:26:50 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-02-24 10:27:05 | → | divlamir joins (~divlamir@user/divlamir) |
| 2026-02-24 10:29:22 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 252 seconds) |
| 2026-02-24 10:31:16 | × | hsw quits (~hsw@106.104.102.45) (Remote host closed the connection) |
| 2026-02-24 10:31:37 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2026-02-24 10:32:21 | → | hsw joins (~hsw@106.104.102.45) |
| 2026-02-24 10:49:08 | → | mange joins (~mange@user/mange) |
| 2026-02-24 10:53:35 | → | Enrico63 joins (~Enrico63@host-79-19-156-232.retail.telecomitalia.it) |
| 2026-02-24 10:57:55 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-02-24 10:59:31 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 2026-02-24 11:07:22 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Quit: WeeChat 4.8.1) |
| 2026-02-24 11:10:10 | × | tromp quits (~textual@2001:1c00:3487:1b00:7955:9591:6018:7ef9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-02-24 11:12:42 | → | Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 2026-02-24 11:14:03 | × | fp quits (~Thunderbi@wireless-86-50-141-0.open.aalto.fi) (Ping timeout: 268 seconds) |
| 2026-02-24 11:14:06 | → | xdminsy joins (~xdminsy@112.10.231.192) |
| 2026-02-24 11:16:47 | × | xdminsy quits (~xdminsy@112.10.231.192) (Client Quit) |
All times are in UTC.