module Stdlib.Trait.Applicative;

import Stdlib.Data.Fixity open;
import Stdlib.Function open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Data.Nat.Base open;
import Stdlib.Data.List.Base open;
import Stdlib.Data.Unit.Base open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait.Foldable.Polymorphic open;
import Stdlib.Data.Unit.Base open;

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
  };

open Applicative public;

--- Sequences computations.
--- Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.
applicativeSeq
  {f : Type -> Type}
  {{Applicative f}}
  {A B : Type}
  (fa : f A)
  (fb : f B)
  : f B := ap (map λ {_ b := b} fa) fb;

--- lifts a binary function to ;Applicative;
liftA2
  {f : Type -> Type}
  {{Applicative f}}
  {A B C}
  (fun : A -> B -> C)
  : f A -> f B -> f C := map fun >> ap;

syntax iterator mapA_ {init := 0; range := 1};
mapA_
  {t : Type -> Type}
  {f : Type -> Type}
  {A B}
  {{Foldable t}}
  {{Applicative f}}
  (fun : A -> f B)
  (l : t A)
  : f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc};

replicateA {f : Type -> Type} {A} {{Applicative f}} : Nat -> f A -> f (List A)
  | zero _ := pure []
  | (suc n) x := liftA2 (::) x (replicateA n x);

when {f : Type -> Type} {{Applicative f}} : Bool -> f Unit -> f Unit
  | false _ := pure unit
  | true a := a;