2025/03/21

Newest at the top

2025-03-21 22:15:32 +0100 <EvanR> it's like how useful is monoid theory, when you want to use Monoid in haskell
2025-03-21 22:15:11 +0100 <dminuoso> A bit unclear why I kept at it, was rather thick headed.
2025-03-21 22:14:58 +0100 <dminuoso> It was excruciatingly slow.
2025-03-21 22:14:57 +0100 <ski> for a programming language semanticist, otoh, it could be useful
2025-03-21 22:14:48 +0100 <dminuoso> Been there, done that!
2025-03-21 22:14:44 +0100 <dminuoso> EvanR: Hey, when I started Haskell I put it on pause, learned category theory, had a rough understanding of monoidal categories, went back to Haskell, and couldn't quite figure out how to write any simple ask/response beginner proggrams. :-)
2025-03-21 22:14:22 +0100 <ski> indeed, geekosaur
2025-03-21 22:13:53 +0100 <EvanR> I am still waiting for the chapter of "category theory for programmers" gets to the part where there is anything related to programming in it xD
2025-03-21 22:13:33 +0100 <dminuoso> And then we open the can of burritos.
2025-03-21 22:13:22 +0100 <dminuoso> They can explore list comprehensions, IO code..
2025-03-21 22:13:15 +0100 <dminuoso> Just people learning to program with a simple interface.
2025-03-21 22:13:07 +0100 <dminuoso> If we had that type of Prelude.Simple, we would not have any of these monad confusions.
2025-03-21 22:12:58 +0100 <EvanR> b 😱
2025-03-21 22:12:53 +0100 <geekosaur> also I'm not sure how much use (b) is for a Haskell programmer
2025-03-21 22:12:53 +0100 <ski> for the practical programmer, (a) is of most use, (b) is more a curiosity, if one looks into it at all
2025-03-21 22:12:47 +0100 <dminuoso> And as for "monad tutorials", Im still a firm believer that all we really need, is a Prelude.Simple module that exposes things like `thenIO :: IO a -> (a -> IO b) -> IO b`, `returnIO :: a -> IO a`, with some special tweakery to attach a `a ~ IO` constraint as a superclass to Monad a...
2025-03-21 22:12:35 +0100 <geekosaur> (for (a))
2025-03-21 22:12:28 +0100 <geekosaur> e.g. "You could have invented monads"
2025-03-21 22:12:23 +0100 <ski> and (b) a category-theoretic perspective, which explains what this has to do with monads as seen in category theory
2025-03-21 22:11:54 +0100 <ski> there's two approaches a monad tutorial could take, i think. (a) one focused on concrete practicalities, how to express various intended imperative behaviours (effects), how to remove / factor out common kinds of related boiler-plate code (e.g. for state-threading, or short-circuiting of failure), identifying idioms/"patterns" for this
2025-03-21 22:10:30 +0100 <dminuoso> directions!)
2025-03-21 22:10:28 +0100 <dminuoso> Rather than asking "what the difference between pure and impure functions" is, we should rather re-learn the notion of "function" to mean something that is almost, but not quite , entirely unlike its cousin from traditional programming and compare that to "effect". Once you learn them as orthogonal things and advance, you can get into deeper ideas on how to encode one with the other (in both
2025-03-21 22:08:44 +0100euleritian(~euleritia@dynamic-176-006-128-244.176.6.pool.telefonica.de)
2025-03-21 22:07:57 +0100 <ski> there's is a lot of bad "monad tutorials" out there (arguably, most of them are bad, to lesser or greater extents)
2025-03-21 22:07:31 +0100 <ski> yes, there is that too
2025-03-21 22:07:22 +0100 <ski> it can take some times to be able to switch perspectives, to be able to see the relevant distinctions (which you're not used to drawing)
2025-03-21 22:07:18 +0100 <dminuoso> I think plenty of confusion comes from decades of programming having (incorrectly) reused terminology like calling routines functions, and then attaching labels like "pure" and "impure" to differentiate things that should not be compared.
2025-03-21 22:07:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-03-21 22:06:36 +0100 <ski> sim590 : yea, i think the best approach is to ponder it, sleep on it, do examples, think about how you can reason about (including refactoring) programs, come back later to this
2025-03-21 22:05:48 +0100 <ski> so, you can imagine that the run-time system is an imperative program (not written in Haskell), which interprets `IO'-actions similarly to how `runTele' interprets `Tele'-actions, and in addition actually interacts with the OS
2025-03-21 22:05:39 +0100 <sim590> In any case, this whole conversation lasted too long already for me considering I should have been working. So, I'll go back to my employer's task I have to finish. I'll resume investigating purity later. Thanks for the conversation anyway!
2025-03-21 22:04:35 +0100 <ski> you can write a `runTele :: Tele a -> IO a' interpreter, and then calling `runTele' on a `Tele'-action, and then letting the run-time system interpret/execute the resulting `IO'-action, would be equivalent to letting the run-time system interpret/execute the corresponding equivalent `IO'-action directly
2025-03-21 22:03:50 +0100 <EvanR> so it's not lambdas in lambdas there but just data, that happens to use a lambda in a place to get a result
2025-03-21 22:03:27 +0100euleritian(~euleritia@95.90.214.149) (Ping timeout: 244 seconds)
2025-03-21 22:03:12 +0100 <ski> PutC '?' (GetC (\c -> PutC c (PutC '!' (Done ()))))
2025-03-21 22:02:34 +0100kimiamania8(~65804703@user/kimiamania) kimiamania
2025-03-21 22:02:29 +0100 <ski> yes, something like that can be used to try to explain how `IO'-actions can be seen as inert instructions
2025-03-21 22:02:26 +0100 <EvanR> I'm melting
2025-03-21 22:02:17 +0100 <EvanR> no I messed it up
2025-03-21 22:02:09 +0100kimiamania8(~65804703@user/kimiamania) (Quit: PegeLinux)
2025-03-21 22:01:55 +0100 <EvanR> :: Tele ()
2025-03-21 22:01:44 +0100 <EvanR> would be a possible imperative program in haskell, if you defined the right Monad instance
2025-03-21 22:01:42 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 22:01:27 +0100 <EvanR> PutC '?' >> GetC >>= \c -> PutC c >> PutC '!' >> Done ()
2025-03-21 22:01:24 +0100 <EvanR> data Tele a = GetC (Char -> Tele a) | PutC Char (Tele a) | Done a
2025-03-21 22:00:08 +0100 <ski> (or the imperative programming, or the imperative behaviour, if you prefer)
2025-03-21 21:59:07 +0100 <ski> but that's not how the imperative instructions here are being expressed
2025-03-21 21:58:59 +0100 <EvanR> imperative programming is a vibe, not a strict concrete thing
2025-03-21 21:58:51 +0100 <ski> that kind of lambda nesting can be used to express a kind of sequencing (from data-dependencies), yes
2025-03-21 21:58:24 +0100 <ski> no