juvix
juvix copied to clipboard
Add builtin Functor / Applicative / Monad
- Depends on #2351.
Suggested Juvix implementation:
trait
type Functor (F : Type -> Type) :=
mkFunctor {fmap : {A B : Type} -> (A -> B) -> F A -> F B};
trait
type Applicative (F : Type -> Type) :=
mkApplicative {
functor : Functor F;
pure : {A : Type} -> A -> F A;
ap : {A B : Type} -> F (A -> B) -> F A -> F B;
};
trait
type Monad (M : Type -> Type) :=
mkMonad {
applicative : Applicative M;
bind : {A B : Type} -> M A -> (A -> M B) -> M B;
};
I've not included return
in the Monad
trait because it's redundant.