Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→ 1,790,502 events total
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.