Which of these is "a monad"?
6
Never closes
`[1, 2, 3] : List Nat`
`List Nat : Type`
`List.{u} : Type u -> Type u`
`List.instMonad : Monad List`
`Monad List : Type (max (u + 1) v)`
`Monad.{u, v} : (m : Type u → Type v) -> Type (max (u + 1) v)`
`List.instLawfulMonad : LawfulMonad List`
`@LawfulMonad List : [inst : Monad List] -> Type (max (u + 1) v)`
`LawfulMonad List : Type (max (u + 1) v)`
`LawfulMonad.{u, v} : (m : Type u → Type v) -> [inst : Monad m] -> Prop`
The concept of monads is important in functional programming. But what actually is a monad?
The options above give various terms in the (dependently-typed) Lean programming language, along with their type ascriptions. Which of these terms can best be termed "a monad"?
This question is managed and resolved by Manifold.
Get 
1,000 to start trading!
1,000Sort by:
I picked List.instMonad because you can have many viable instances for the same type. This is less of an issue for Monad, but with Applicative List (for example), both zipping and Cartesian product can be used.
In Haskell, where instances are coherent and unnameable, I would be ok with Monad List instead.