Open janmasrovira opened 1 year ago
Possible syntaxes discussed during the call:
Option 1
trait
type Monad (M : Type -> Type) :=
mkMonad {{applicative : Applicative M}} {
bind : {A B : Type} -> M A -> (A -> M B) -> M B;
};
Option 2
trait
type Monad (M : Type -> Type) :=
mkMonad {
{{applicative : Applicative M}};
bind : {A B : Type} -> M A -> (A -> M B) -> M B;
};
Option 3
trait
type Monad (M : Type -> Type) :=
mkMonad {
applicative : {{Applicative M}};
bind : {A B : Type} -> M A -> (A -> M B) -> M B;
};
Suggested Juvix implementation:
I've not included
return
in theMonad
trait because it's redundant.