module Stdlib.Trait.Monad;

import Stdlib.Data.Fixity open;
import Stdlib.Trait.Applicative open;

trait
type Monad (m : Type -> Type) :=
  mkMonad {
    {{applicative}} : Applicative m;
    builtin monad-bind
    bind : {A B : Type} -> m A -> (A -> m B) -> m B
  };

open Monad public;

syntax operator >>= seq;
>>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B :=
  bind x g;

syntax operator >=> seq;
>=>
  {A B C}
  {f : Type -> Type}
  {{Monad f}}
  (h : A -> f B)
  (g : B -> f C)
  (a : A)
  : f C := h a >>= g;