Which of these is "a monad"?
6
117
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"?
Get Ṁ200 play money
Related questions
Sort 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.
Related questions
Which of the following is a dumpling [resolves to poll]?
Which of these four events will happen first? #1
Which of these four events will happen first? #3
Dd
50% chance
Which computational universe do we live in?
Which of the following will I do first?
Which interpretation of Quantum Mechanics is closest to the truth?
Which of these options is the most conscious, or the most likely to be conscious?
POLL
Which is better?
POLL
Which is better?
POLL