IRCBrowse

2026/03/12

Newest at the top

2026-03-12 19:07:19 +0100 <ski> for natural numbers (and subsets), the latter is actually an equality
2026-03-12 19:06:58 +0100 <ski> (n + o) ∸ o ≤ n
2026-03-12 19:06:44 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:06:44 +0100 <ski> and
2026-03-12 19:06:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:06:42 +0100 <ski> m ≤ (m ∸ o) + o
2026-03-12 19:06:27 +0100 <ski> two consequences (unit & counit) of that galois connection / adjunction are
2026-03-12 19:06:26 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 244 seconds)
2026-03-12 19:06:20 +0100Wygulmage(~Wygulmage@user/Wygulmage) Wygulmage
2026-03-12 19:06:02 +0100 <haskellbridge> <ijouw> Seems useful
2026-03-12 19:06:01 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:06:00 +0100 <ski> in words, ⌜m ∸ o⌝ is the least ⌜n⌝ such that ⌜m ≤ n + o⌝ (⌜n⌝ added to ⌜m⌝ is at least ⌜o⌝)
2026-03-12 19:05:38 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:05:34 +0100Wygulmage4(~Wygulmage@user/Wygulmage) (Quit: Client closed)
2026-03-12 19:05:06 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:04:46 +0100 <ski> ⇔ m ≤ n + o
2026-03-12 19:04:45 +0100 <ski> m ∸ o ≤ n
2026-03-12 19:03:53 +0100merijn(~merijn@77.242.116.146) (Ping timeout: 248 seconds)
2026-03-12 19:03:29 +0100 <ski> <https://en.wikipedia.org/wiki/Monus>
2026-03-12 19:03:05 +0100 <ski> no
2026-03-12 19:03:01 +0100 <haskellbridge> <ijouw> monus >> minus?
2026-03-12 19:03:01 +0100 <ski> galois connections / adjunctions
2026-03-12 19:02:16 +0100 <Wygulmage4> ski: Is there any formal relation between a monoid (or semigroup) with monus and a residuated lattice (or residuated semilattice)? They seem to be doing similar things w.r.t. generalized division and subtraction.
2026-03-12 19:02:08 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:01:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:01:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:00:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:00:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:59:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:56:48 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 18:56:12 +0100chewybread(~chewybrea@user/chewybread) (Ping timeout: 264 seconds)
2026-03-12 18:56:05 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 18:56:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:55:22 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 18:54:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:54:55 +0100 <yahb2> [(Foo," Bar")]
2026-03-12 18:54:55 +0100 <ski> % (reads :: ReadS FooBar) "Foo Bar"
2026-03-12 18:54:44 +0100 <yahb2> []
2026-03-12 18:54:44 +0100 <ski> % (reads :: ReadS FooBar) "foo bar"
2026-03-12 18:54:26 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:54:18 +0100 <gentauro> nice
2026-03-12 18:54:16 +0100 <yahb2> Just Foo
2026-03-12 18:54:16 +0100 <gentauro> % readFoobar "foo"
2026-03-12 18:54:13 +0100 <yahb2> <no output>
2026-03-12 18:54:13 +0100 <gentauro> % readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar)
2026-03-12 18:53:58 +0100 <yahb2> <interactive>:61:1: error: [GHC-39999] ; • No instance for ‘Show Ghci8.FooBar’ ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; There are instances for similar types: ; ...
2026-03-12 18:53:58 +0100 <gentauro> % readFoobar "foo"
2026-03-12 18:53:56 +0100 <yahb2> <no output>
2026-03-12 18:53:56 +0100 <gentauro> % data FooBar = Foo | Bar deriving (Read, Show)
2026-03-12 18:53:47 +0100 <yahb2> <interactive>:57:1: error: [GHC-39999] ; • No instance for ‘Show FooBar’ ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; • In a stmt of an interactive GHCi command: ; Yah...