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;