juvix icon indicating copy to clipboard operation
juvix copied to clipboard

Add builtin Functor / Applicative / Monad

Open janmasrovira opened this issue 1 year ago • 1 comments

  • 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.

janmasrovira avatar Sep 12 '23 10:09 janmasrovira