------------------------------------------------------------------------
-- The Agda standard library
--
-- Simple combinators working solely on and with functions
------------------------------------------------------------------------
 
-- The contents of this module is also accessible via the `Function`
-- module. See `Function.Strict` for strict versions of these
-- combinators.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Function.Base where
 
open import Level using (Level)
 
private
  variable
    a b c d e : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e
 
------------------------------------------------------------------------
-- Some simple functions
 
id : A → A
id x = x
 
const : A → B → A
const x = λ _ → x
 
constᵣ : A → B → B
constᵣ _ = id
 
------------------------------------------------------------------------
-- Operations on dependent functions
 
-- These are functions whose output has a type that depends on the
-- value of the input to the function.
 
infixr  _∘_ _∘₂_
infixl  _ˢ_
infixl  _|>_
infix   case_return_of_
infixr -1 _$_
 
-- Composition
 
_∘_ : ∀ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)
{-# INLINE _∘_ #-}
 
_∘₂_ : ∀ {A₁ : Set a} {A₂ : A₁ → Set d}
         {B : (x : A₁) → A₂ x → Set b}
         {C : {x : A₁} → {y : A₂ x} → B x y → Set c} →
       ({x : A₁} → {y : A₂ x} → (z : B x y) → C z) →
       (g : (x : A₁) → (y : A₂ x) → B x y) →
       ((x : A₁) → (y : A₂ x) → C (g x y))
f ∘₂ g = λ x y → f (g x y)
 
-- Flipping order of arguments
 
flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y
{-# INLINE flip #-}
 
-- Application - note that _$_ is right associative, as in Haskell.
-- If you want a left associative infix application operator, use
-- RawFunctor._<$>_ from Effect.Functor.
 
_$_ : ∀ {A : Set a} {B : A → Set b} →
      ((x : A) → B x) → ((x : A) → B x)
f $ x = f x
{-# INLINE _$_ #-}
 
-- Flipped application (aka pipe-forward)
 
_|>_ : ∀ {A : Set a} {B : A → Set b} →
       (a : A) → (∀ a → B a) → B a
_|>_ = flip _$_
{-# INLINE _|>_ #-}
 
-- The S combinator - written infix as in Conor McBride's paper
-- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax
-- and evaluation".
 
_ˢ_ : ∀ {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} →
      ((x : A) (y : B x) → C x y) →
      (g : (x : A) → B x) →
      ((x : A) → C x (g x))
f ˢ g = λ x → f x (g x)
{-# INLINE _ˢ_ #-}
 
-- Converting between implicit and explicit function spaces.
 
_$- : ∀ {A : Set a} {B : A → Set b} → ((x : A) → B x) → ({x : A} → B x)
f $- = f _
{-# INLINE _$- #-}
 
λ- : ∀ {A : Set a} {B : A → Set b} → ({x : A} → B x) → ((x : A) → B x)
λ- f = λ x → f
{-# INLINE λ- #-}
 
-- Case expressions (to be used with pattern-matching lambdas, see
-- README.Case).
 
case_returning_of_ : ∀ {A : Set a} (x : A) (B : A → Set b) →
                  ((x : A) → B x) → B x
case x returning B of f = f x
{-# INLINE case_returning_of_ #-}
 
------------------------------------------------------------------------
-- Non-dependent versions of dependent operations
 
-- Any of the above operations for dependent functions will also work
-- for non-dependent functions but sometimes Agda has difficulty
-- inferring the non-dependency. Primed (′ = \prime) versions of the
-- operations are therefore provided below that sometimes have better
-- inference properties.
 
infixr  _∘′_ _∘₂′_
infixl  _|>′_
infix   case_of_
infixr -1 _$′_
 
-- Composition
 
_∘′_ : (B → C) → (A → B) → (A → C)
f ∘′ g = _∘_ f g
 
_∘₂′_ : (C → D) → (A → B → C) → (A → B → D)
f ∘₂′ g = _∘₂_ f g
 
-- Flipping order of arguments
 
flip′ : (A → B → C) → (B → A → C)
flip′ = flip
 
-- Application
 
_$′_ : (A → B) → (A → B)
_$′_ = _$_
 
-- Flipped application (aka pipe-forward)
 
_|>′_ : A → (A → B) → B
_|>′_ = _|>_
 
-- Case expressions (to be used with pattern-matching lambdas, see
-- README.Case).
 
case_of_ : A → (A → B) → B
case x of f = case x returning _ of f
{-# INLINE case_of_ #-}
 
------------------------------------------------------------------------
-- Operations that are only defined for non-dependent functions
 
infixl  _⟨_⟩_
infixl  _∋_
 
-- Binary application
 
_⟨_⟩_ : A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y
 
-- In Agda you cannot annotate every subexpression with a type
-- signature. This function can be used instead.
 
_∋_ : (A : Set a) → A → A
A ∋ x = x
 
-- Conversely it is sometimes useful to be able to extract the
-- type of a given expression.
 
typeOf : {A : Set a} → A → Set a
typeOf {A = A} _ = A
 
-- Construct an element of the given type by instance search.
 
it : {A : Set a} → {{A}} → A
it {{x}} = x
 
------------------------------------------------------------------------
-- Composition of a binary function with other functions
 
infixr  _-⟪_⟫-_ _-⟨_⟫-_
infixl  _-⟪_⟩-_
infixr  _-⟨_⟩-_ ∣_⟫-_ ∣_⟩-_
infixl  _on_ _on₂_ _-⟪_∣ _-⟨_∣
 
-- Two binary functions
 
_-⟪_⟫-_ : (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
f -⟪ _*_ ⟫- g = λ x y → f x y * g x y
 
-- A single binary function on the left
 
_-⟪_∣ : (A → B → C) → (C → B → D) → (A → B → D)
f -⟪ _*_ ∣ = f -⟪ _*_ ⟫- constᵣ
 
-- A single binary function on the right
 
∣_⟫-_ : (A → C → D) → (A → B → C) → (A → B → D)
∣ _*_ ⟫- g = const -⟪ _*_ ⟫- g
 
-- A single unary function on the left
 
_-⟨_∣ : (A → C) → (C → B → D) → (A → B → D)
f -⟨ _*_ ∣ = f ∘₂ const -⟪ _*_ ∣
 
-- A single unary function on the right
 
∣_⟩-_ : (A → C → D) → (B → C) → (A → B → D)
∣ _*_ ⟩- g = ∣ _*_ ⟫- g ∘₂ constᵣ
 
-- A binary function and a unary function
 
_-⟪_⟩-_ : (A → B → C) → (C → D → E) → (B → D) → (A → B → E)
f -⟪ _*_ ⟩- g = f -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
 
-- A unary function and a binary function
 
_-⟨_⟫-_ : (A → C) → (C → D → E) → (A → B → D) → (A → B → E)
f -⟨ _*_ ⟫- g = f -⟨ const ∣ -⟪ _*_ ⟫- g
 
-- Two unary functions
 
_-⟨_⟩-_ : (A → C) → (C → D → E) → (B → D) → (A → B → E)
f -⟨ _*_ ⟩- g = f -⟨ const ∣ -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
 
-- A single binary function on both sides
 
_on₂_ : (C → C → D) → (A → B → C) → (A → B → D)
_*_ on₂ f = f -⟪ _*_ ⟫- f
 
-- A single unary function on both sides
 
_on_ : (B → B → C) → (A → B) → (A → A → C)
_*_ on f = f -⟨ _*_ ⟩- f
 
 
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
 
-- Version 1.4
 
_-[_]-_ = _-⟪_⟫-_
{-# WARNING_ON_USAGE _-[_]-_
"Warning: Function._-[_]-_ was deprecated in v1.4.
Please use _-⟪_⟫-_ instead."
#-}
 
-- Version 2.0
 
case_return_of_ = case_returning_of_
{-# WARNING_ON_USAGE case_return_of_
"case_return_of_ was deprecated in v2.0.
Please use case_returning_of_ instead."
#-}