------------------------------------------------------------------------
-- Simple combinators working solely on and with functions
------------------------------------------------------------------------

module Data.Function where

infixr  _∘_ _∘′_ _∘₀_ _∘₁_
infixl  _on_ _on₁_
infixl  _⟨_⟩_ _⟨_⟩₁_
infixr  _-[_]₁-_ _-[_]-_ _$_
infix   _∶_ _∶₁_

------------------------------------------------------------------------
-- Types

-- Unary functions on a given set.

Fun₁ : Set → Set
Fun₁ a = a → a

-- Binary functions on a given set.

Fun₂ : Set → Set
Fun₂ a = a → a → a

------------------------------------------------------------------------
-- Functions

_∘_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

_∘′_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘′ g = _∘_ f g

_∘₀_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set₁} →
       (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
       ((x : A) → C (g x))
f ∘₀ g = λ x → f (g x)

_∘₁_ : {A : Set₁} {B : A → Set₁} {C : {x : A} → B x → Set₁} →
       (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
       ((x : A) → C (g x))
f ∘₁ g = λ x → f (g x)

id : {a : Set} → a → a
id x = x

id₁ : {a : Set₁} → a → a
id₁ x = x

const : {a b : Set} → a → b → a
const x = λ _ → x

const₁ : {a : Set₁} {b : Set} → a → b → a
const₁ x = λ _ → x

flip : {A B : Set} {C : A → B → Set} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ x y → f y x

flip₁ : {A B : Set} {C : A → B → Set₁} →
        ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip₁ f = λ x y → f y x

-- Note that _$_ is right associative, like in Haskell. If you want a
-- left associative infix application operator, use
-- Category.Functor._<$>_, available from
-- Category.Monad.Identity.IdentityMonad.

_$_ : {a : Set} {b : a → Set} → ((x : a) → b x) → ((x : a) → b x)
f $ x = f x

_⟨_⟩_ : {a b c : Set} → a → (a → b → c) → b → c
x ⟨ f ⟩ y = f x y

_⟨_⟩₁_ : {a b : Set} → a → (a → b → Set) → b → Set
x ⟨ f ⟩₁ y = f x y

_on_ : {a b c : Set} → (b → b → c) → (a → b) → (a → a → c)
_*_ on f = λ x y → f x * f y

_on₁_ : {a b : Set} {c : Set₁} → (b → b → c) → (a → b) → (a → a → c)
_*_ on₁ f = λ x y → f x * f y

_-[_]-_ : {a b c d e : Set} →
          (a → b → c) → (c → d → e) → (a → b → d) → (a → b → e)
f -[ _*_ ]- g = λ x y → f x y * g x y

_-[_]₁-_ : {a b : Set} →
           (a → b → Set) → (Set → Set → Set) → (a → b → Set) →
           (a → b → Set)
f -[ _*_ ]₁- g = λ x y → f x y * g x y

-- In Agda you cannot annotate every subexpression with a type
-- signature. This function can be used instead.
--
-- You should think of the colon as being mirrored around its vertical
-- axis; the type comes first.

_∶_ : (A : Set) → A → A
_ ∶ x = x

_∶₁_ : (A : Set₁) → A → A
_ ∶₁ x = x