open import 1Lab.Type

open import Meta.Idiom

module Meta.Bind where

Primitive: do syntaxπŸ”—

record Bind (M : Effect) : Typeω where
  private module M = Effect M
  field
    _>>=_ : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ M.β‚€ A β†’ (A β†’ M.β‚€ B) β†’ M.β‚€ B
    ⦃ Idiom-bind ⦄ : Idiom M

  _>>_ : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ M.β‚€ A β†’ M.β‚€ B β†’ M.β‚€ B
  _>>_ f g = f >>= Ξ» _ β†’ g

  infixl 1 _>>=_

  _=<<_ : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ (A β†’ M.β‚€ B) β†’ M.β‚€ A β†’ M.β‚€ B
  _=<<_ f x = x >>= f

  infixr 1 _=<<_

open Bind ⦃ ... ⦄ public