Logs: liberachat/#haskell
| 2026-03-12 17:51:09 | <gentauro> | > :i (+) |
| 2026-03-12 17:51:11 | <lambdabot> | <hint>:1:1: error: parse error on input `:' |
| 2026-03-12 17:51:20 | <gentauro> | > import Text.Read |
| 2026-03-12 17:51:21 | <lambdabot> | <hint>:1:1: error: parse error on input `import' |
| 2026-03-12 17:51:24 | <ski> | residuated lattices reminds me of ordered (intuitionistic) logic (see "Ordered Linear Logic and Applications" by Jeffrey E. Polakow in 2001-08 at <https://www.cs.cmu.edu/~jpolakow/diss.ps>,(draft) <https://web.archive.org/web/20010614031936/http://www.cs.cmu.edu:80/~jpolakow/diss.pdf>) |
| 2026-03-12 17:51:28 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 17:51:32 | <ski> | @let import Text.Read |
| 2026-03-12 17:51:33 | <lambdabot> | Defined. |
| 2026-03-12 17:51:54 | <gentauro> | > :i readMaybe |
| 2026-03-12 17:51:55 | <lambdabot> | <hint>:1:1: error: parse error on input `:' |
| 2026-03-12 17:51:57 | <gentauro> | :| |
| 2026-03-12 17:52:04 | <ski> | @type readMaybe |
| 2026-03-12 17:52:05 | <lambdabot> | Read a => String -> Maybe a |
| 2026-03-12 17:52:09 | <EvanR> | :i readMaybe |
| 2026-03-12 17:52:30 | <ski> | (there is no `@info' with lambdabot) |
| 2026-03-12 17:52:47 | <gentauro> | ski: got it |
| 2026-03-12 17:53:00 | × | dhil quits (~dhil@5.151.29.139) (Ping timeout: 244 seconds) |
| 2026-03-12 17:53:11 | <ski> | % :set -XLambdaCase |
| 2026-03-12 17:53:11 | <yahb2> | <no output> |
| 2026-03-12 17:53:16 | <gentauro> | :o |
| 2026-03-12 17:53:20 | <ski> | % let readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 17:53:20 | <yahb2> | <interactive>:51:59: error: [GHC-88464] ; Variable not in scope: toUpper :: a -> Char ; ; <interactive>:51:75: error: [GHC-88464] ; Variable not in scope: toLower :: a -> Char |
| 2026-03-12 17:53:32 | <ski> | % :m + Data.Char |
| 2026-03-12 17:53:32 | <yahb2> | <no output> |
| 2026-03-12 17:53:35 | <ski> | % let readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 17:53:35 | <yahb2> | <no output> |
| 2026-03-12 17:53:47 | <gentauro> | % readFoobar "foo" |
| 2026-03-12 17:53:47 | <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... |
| 2026-03-12 17:53:56 | <gentauro> | % data FooBar = Foo | Bar deriving (Read, Show) |
| 2026-03-12 17:53:56 | <yahb2> | <no output> |
| 2026-03-12 17:53:58 | <gentauro> | % readFoobar "foo" |
| 2026-03-12 17:53:58 | <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 17:54:13 | <gentauro> | % readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 17:54:13 | <yahb2> | <no output> |
| 2026-03-12 17:54:16 | <gentauro> | % readFoobar "foo" |
| 2026-03-12 17:54:16 | <yahb2> | Just Foo |
| 2026-03-12 17:54:18 | <gentauro> | nice |
| 2026-03-12 17:54:26 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 17:54:44 | <ski> | % (reads :: ReadS FooBar) "foo bar" |
| 2026-03-12 17:54:44 | <yahb2> | [] |
| 2026-03-12 17:54:55 | <ski> | % (reads :: ReadS FooBar) "Foo Bar" |
| 2026-03-12 17:54:55 | <yahb2> | [(Foo," Bar")] |
| 2026-03-12 17:54:58 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 17:55:22 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 17:56:02 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 17:56:05 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 17:56:12 | × | chewybread quits (~chewybrea@user/chewybread) (Ping timeout: 264 seconds) |
| 2026-03-12 17:56:48 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 17:59:46 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:00:18 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:00:42 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:01:22 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:01:25 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:02:08 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:02:16 | <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 18:03:01 | <ski> | galois connections / adjunctions |
| 2026-03-12 18:03:01 | <haskellbridge> | <ijouw> monus >> minus? |
| 2026-03-12 18:03:05 | <ski> | no |
| 2026-03-12 18:03:29 | <ski> | <https://en.wikipedia.org/wiki/Monus> |
| 2026-03-12 18:03:53 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2026-03-12 18:04:45 | <ski> | m ∸ o ≤ n |
| 2026-03-12 18:04:46 | <ski> | ⇔ m ≤ n + o |
| 2026-03-12 18:05:06 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:05:34 | × | Wygulmage4 quits (~Wygulmage@user/Wygulmage) (Quit: Client closed) |
| 2026-03-12 18:05:38 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:06:00 | <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 18:06:01 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:06:02 | <haskellbridge> | <ijouw> Seems useful |
| 2026-03-12 18:06:20 | → | Wygulmage joins (~Wygulmage@user/Wygulmage) |
| 2026-03-12 18:06:26 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-03-12 18:06:27 | <ski> | two consequences (unit & counit) of that galois connection / adjunction are |
| 2026-03-12 18:06:42 | <ski> | m ≤ (m ∸ o) + o |
| 2026-03-12 18:06:42 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:06:44 | <ski> | and |
| 2026-03-12 18:06:44 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:06:58 | <ski> | (n + o) ∸ o ≤ n |
| 2026-03-12 18:07:19 | <ski> | for natural numbers (and subsets), the latter is actually an equality |
| 2026-03-12 18:07:37 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:07:54 | <ski> | for natural numbers, monus is also called cut-off / saturated / truncated subtraction |
| 2026-03-12 18:07:55 | → | arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 18:07:55 | × | arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 18:07:55 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-03-12 18:08:42 | <Wygulmage> | And conveniently it's closed for natural numbers, unlike subtraction. |
| 2026-03-12 18:08:47 | <ski> | (and ⌜m ∸ o⌝ can be described as ⌜max 0 (m − o)⌝) |
| 2026-03-12 18:09:12 | → | jeremyn joins (~jeremy@user/jeremyn) |
| 2026-03-12 18:10:19 | <ski> | in total programming environments, people often use monus, instead of minus, just to get it totally defined |
| 2026-03-12 18:10:26 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:10:41 | <Wygulmage> | But of course it doesn't work for `Int`. |
| 2026-03-12 18:10:42 | <ski> | (i've seen people define "reciprocal" of zero as zero, for similar reasons ..) |
| 2026-03-12 18:10:51 | <Wygulmage> | *shudder* |
| 2026-03-12 18:10:58 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:11:08 | <ski> | yea, i was thinking of stuff like recursive functions (a la Kleene) |
| 2026-03-12 18:11:22 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:12:02 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:12:05 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:12:20 | <ski> | exercise for the reader : figure out an appropriate galois connection for division in relational algebra, and determine what the result of dividing by the empty relation here amounts to |
| 2026-03-12 18:13:07 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:13:17 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-03-12 18:15:46 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:16:18 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
All times are in UTC.