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,000