Library Prelude.Control.Function

From Coq Require Import Basics FunctionalExtensionality.
From Prelude Require Import Control Equality.

#[local]
Open Scope prelude_scope.

Definition func (a b : Type) := a -> b.

Bind Scope monad_scope with func.
Bind Scope function_scope with func.

Definition map_func {a b c} (f : b -> c) (g : func a b) : func a c :=
  fun (x : a) => f (g x).

#[program]
Instance func_Functor (a : Type) : Functor (func a) :=
  { map := @map_func a
  }.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Definition func_apply {a b c} (f : func a (b -> c)) (g : func a b) : func a c :=
  fun (x : a) => f x (g x).

Definition func_pure {a b} (x : b) : func a b :=
  fun (_ : a) => x.

#[program]
Instance func_Applicative (a: Type) : Applicative (func a) :=
  { pure := @func_pure a
  ; apply := @func_apply a
  }.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Definition func_bind {a b c} (f : func a b) (g : b -> func a c) : func a c :=
  fun (x : a) => g (f x) x.

#[program]
Instance func_Monad (a : Type) : Monad (func a) :=
  { bind := @func_bind a
  }.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.