Post AcSd4I2TGziB2WrIrA by MartinEscardo@mathstodon.xyz
 (DIR) More posts by MartinEscardo@mathstodon.xyz
 (DIR) Post #AcSd40ITEloY0wCpIO by MartinEscardo@mathstodon.xyz
       2023-12-01T19:08:02Z
       
       0 likes, 0 repeats
       
       {- I think I am going to teach Haskell monads like this next year. -}{-# Language UndecidableInstances #-}{- Original definition of Haskell monad. -}class Monad' m where return' :: a -> m a bind'   :: m a -> (a -> m b) -> m b{- Nonsense new definition. -}{-class Functor f where fmap :: (a -> b) -> f a -> f bclass Functor f => Applicative f where pure  :: a -> f a (<*>) :: f (a -> b) -> f a -> f bclass Applicative m => Monad m where return :: a -> m a (>>=)  :: m a -> (a -> m b) -> m b return = pure-}{- We get a Monad from a Monad'. -}instance Monad' m => Monad m where (>>=) = bind'{- This is because we can always define Functor and Applicative as follows. -}instance Monad' m => Functor m where fmap f xm = do              x <- xm              pure (f x)instance Monad' m => Applicative m where pure = return' fm <*> xm = do              f <- fm              x <- xm              pure (f x){- Example. An economic definition of the Maybe monad. -}data Maybe' a = Nothing' | Just' ainstance Monad' Maybe' where return' = Just' bind' Nothing'  f = Nothing' bind' (Just' x) f = f x{- To test this, define a function using Monad rather than Monad'. -}fibm :: Monad m => Integer -> m Integerfibm 0 = pure 0fibm 1 = pure 1fibm n = do          x <- fibm (n-2)          y <- fibm (n-1)          pure (x+y){- We can use it with the Maybe' Monad automatically derived from the Maybe' Monad'. -}fib11 :: Maybe' Integerfib11 = fibm 111/
       
 (DIR) Post #AcSd41TqpwVngWXQfo by MartinEscardo@mathstodon.xyz
       2023-12-01T19:12:36Z
       
       0 likes, 0 repeats
       
       It was already difficult to teach monads to 2nd year functional programming students, and the new definition seems to be designed to make them deliberately incomprehensible. 2/
       
 (DIR) Post #AcSd42eAV4MJIoNBOS by MartinEscardo@mathstodon.xyz
       2023-12-01T19:24:37Z
       
       1 likes, 0 repeats
       
       The whole point of monads presented as Kleisli triples, which is what Monad' amounts to, is to avoid having to define and prove functoriality and naturality. The new Haskell definition misses this point.Moreover, "Applicative" is a distraction. It is used sometimes, but only very occasionally, and, more importantly, it is hardly at the core of the definition of monad. In fact, here we have it only because our monads (in either form) are internally defined and hence automatically strong as we are working in something that looks more or less like a cartesian closed category (but it really isn't a cartesian closed category, as the universal property of exponentials for function types doesn't really hold (meaning that it fails).)3/
       
 (DIR) Post #AcSd48tHHo0gfPUKmG by MartinEscardo@mathstodon.xyz
       2023-12-01T19:28:29Z
       
       0 likes, 0 repeats
       
       So there are two big mistakes in the new definition.(1) It has got the mathematics wrong.(2) It makes it incredibly hard to teach to programmers.What a pity, because it is a really useful mathematical abstraction with useful uses in programming.4/
       
 (DIR) Post #AcSd4BquH4tbqvOyzw by MartinEscardo@mathstodon.xyz
       2023-12-01T20:41:33Z
       
       0 likes, 0 repeats
       
       Epilogue.The people who advocate the new Monad as opposed to the original Monad' should be sentenced to teach Monads for ever to undergrad students in their after-life.And should avoid claiming that Haskell is informed by mathematics and tries to make it easier to reason about programs.🙂 Good night.5/5
       
 (DIR) Post #AcSd4I2TGziB2WrIrA by MartinEscardo@mathstodon.xyz
       2023-12-03T19:45:00Z
       
       0 likes, 0 repeats
       
       Let me elaborate a bit further.While it is true that `Functor` and `Applicative` are useful type classes in Haskell, it is also the case that for Haskell `Monad`s we don't really have a choice for what its functorial and applicative parts are, if we are to obey the functorial, applicative and monad laws.Moreover for monads (in Kleisli form as in Haskell) we don't need to understand `Functor` and `Applicative first in order to understand the original Haskell definitionclass Monad m where return :: a -> m a (>>=)  :: m a -> (a -> m b) -> m bForcing to define `Functor` as a pre-requisite to define `Monad` is OK-ish, but still inelegant from both mathematical and computational points of view, because we don't really have a choice, up to (observational program) equivalence. But forcing to define `Applicative` as a prerequisite for `Monad` goes too far in terms of cognitive overload. Like functoriality, the applicativity of a Haskell monad is uniquely determined for *all* monads. Hence having to define it every time for every monad is a disservice to (mathematical and computational) simplicity and a source of boilerplate.In particular, how do you explain to students that (1) yes, they have to define `Functor` and `Applicative`, but (2) no, they don't really have a choice, other than maybe writing more efficient code, but in any case there is default code that is required to be equivalent to their more efficient code.In light of (1) and (2), I don't consider reasonable to define `Monad` in Haskell in the current way.6/5
       
 (DIR) Post #AcSd4LtOwepizYe7H6 by MartinEscardo@mathstodon.xyz
       2023-12-03T19:47:07Z
       
       0 likes, 0 repeats
       
       Of course, there is an alternative way to support the current Haskell definition of Monad.We can teach 2nd-year computer-science undergrad students category theory first, and in particular cartesian closed categories, and then explain monads, internally defined monads, monads in Kleisli form, and then show that internally-defined monads in Kleisli form are automatically functorial and applicative (as well as natural).And then, digression, we can discuss categorical models of Haskell, and point out that, actually, none of them can possibly be cartesian closed, because currying-uncurrying doesn't really satisfy the required property for cartesian closed categories, namely that they are inverses of each other in Haskell, because they are not in Haskell (they are in Miranda).7/5
       
 (DIR) Post #AcSd4R39lobizGFTfs by MartinEscardo@mathstodon.xyz
       2023-12-03T20:02:40Z
       
       0 likes, 0 repeats
       
       Further, monads in Haskell are automatically, strong. But luckily nobody so far has had the brilliant idea of creating a type class `StrongFunctor` as an additional prerequite to define Haskell monads. (I hope this post is not considered as an invitation, but, if it is, you may further consider monoidal monad as an intermediate step, as the strength is a particular case of the (automatic) monoidality of Haskell monads.) As you can see, we are going in the direction of applied nonsense, where the so-called abstract nonsense teaches that none of this is necessary as we have it for free. 8/5
       
 (DIR) Post #AcSd4W8eqmykllrRRY by MartinEscardo@mathstodon.xyz
       2023-12-03T20:15:27Z
       
       0 likes, 0 repeats
       
       I promise to stop. But don't take my word for it.The summary is that the current definition of Haskell monad adds consequences of the original definition as part of the new definition.Consider this question seriously: why do that? 9/5
       
 (DIR) Post #AcSdAQcQHoG7O4bNeS by jesper@agda.club
       2023-12-03T20:30:11.481469Z
       
       1 likes, 0 repeats
       
       @MartinEscardo I must say I'm a bit surprised by all this hate for Applicative. It's true that it's annoying to have to define the Functor and Applicative instances first before you can define Monad, but this seems like a limitation of Haskell rather than a problem with the concepts themselves.I have been teaching monads in Haskell to 3rd year students in Delft for three years now, and I always found Applicative to be a useful intermediate step going from Functor to Monad. But I do admit I am taking more of a programmer perspective than a mathematician perspective in my lectures.At the risk of saying things you probably already know, Applicative was introduced to Haskell because it gives a useful interface to writing things like parsers with a *first-order* interface rather than the intrinsically higher-order interface of Monad. This is useful because it leaves a lot more room for optimizations.I would call Haskell a mathematically-inspired language rather than a mathematically-based language. To me this makes sense, since as programmers we do sometimes need to care about intentional properties of our functions, and trying to capture *everything* about a program's behavior in its type is a fool's errand.