------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous N-ary Functions: basic types and operations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Nary.NonDependent.Base where
------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------
open import Level using (Level; 0ℓ; _⊔_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_)
open import Data.Unit.Polymorphic.Base
open import Function.Base using (_∘′_; _$′_; const; flip)
private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
------------------------------------------------------------------------
-- Type Definitions
-- We want to define n-ary function spaces and generic n-ary operations on
-- them such as (un)currying, zipWith, alignWith, etc.
-- We want users to be able to use these seamlessly whenever n is concrete.
-- In other words, we want Agda to infer the sets `A₁, ⋯, Aₙ` when we write
-- `uncurryₙ n f` where `f` has type `A₁ → ⋯ → Aₙ → B`. For this to happen,
-- we need the structure in which these Sets are stored to effectively
-- η-expand to `A₁, ⋯, Aₙ` when the parameter `n` is known.
-- Hence the following definitions:
------------------------------------------------------------------------
-- First, a "vector" of `n` Levels (defined by induction on n so that it
-- may be built by η-expansion and unification). Each Level will be that
-- of one of the Sets we want to take the n-ary product of.
Levels : ℕ → Set
Levels zero = ⊤
Levels (suc n) = Level × Levels n
-- The overall Level of a `n` Sets of respective levels `l₁, ⋯, lₙ` will
-- be the least upper bound `l₁ ⊔ ⋯ ⊔ lₙ` of all of the Levels involved.
-- Hence the following definition of n-ary least upper bound:
⨆ : ∀ n → Levels n → Level
⨆ zero _ = Level.zero
⨆ (suc n) (l , ls) = l ⊔ (⨆ n ls)
-- Second, a "vector" of `n` Sets whose respective Levels are determined
-- by the `Levels n` input.
Sets : ∀ n (ls : Levels n) → Set (Level.suc (⨆ n ls))
Sets zero _ = ⊤
Sets (suc n) (l , ls) = Set l × Sets n ls
-- Third, a function type whose domains are given by a "vector" of `n` Sets
-- `A₁, ⋯, Aₙ` and whose codomain is `B`. `Arrows` forms such a type of
-- shape `A₁ → ⋯ → Aₙ → B` by induction on `n`.
Arrows : ∀ n {r ls} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
Arrows zero _ b = b
Arrows (suc n) (a , as) b = a → Arrows n as b
-- We introduce a notation for this definition
infixr 0 _⇉_
_⇉_ : ∀ {n ls r} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
_⇉_ = Arrows _
------------------------------------------------------------------------
-- Operations on Sets
-- Level-respecting map
infixr -1 _<$>_
_<$>_ : (∀ {l} → Set l → Set l) →
∀ {n ls} → Sets n ls → Sets n ls
_<$>_ f {zero} as = _
_<$>_ f {suc n} (a , as) = f a , (f <$> as)
-- Level-modifying generalised map
lmap : (Level → Level) → ∀ n → Levels n → Levels n
lmap f zero ls = _
lmap f (suc n) (l , ls) = f l , lmap f n ls
smap : ∀ f → (∀ {l} → Set l → Set (f l)) →
∀ n {ls} → Sets n ls → Sets n (lmap f n ls)
smap f F zero as = _
smap f F (suc n) (a , as) = F a , smap f F n as
------------------------------------------------------------------------
-- Operations on Functions
-- mapping under n arguments
mapₙ : ∀ n {ls} {as : Sets n ls} → (B → C) → as ⇉ B → as ⇉ C
mapₙ zero f v = f v
mapₙ (suc n) f g = mapₙ n f ∘′ g
-- compose function at the n-th position
infix 1 _%=_⊢_
_%=_⊢_ : ∀ n {ls} {as : Sets n ls} → (A → B) → as ⇉ (B → C) → as ⇉ (A → C)
n %= f ⊢ g = mapₙ n (_∘′ f) g
-- partially apply function at the n-th position
infix 1 _∷=_⊢_
_∷=_⊢_ : ∀ n {ls} {as : Sets n ls} → A → as ⇉ (A → B) → as ⇉ B
n ∷= x ⊢ g = mapₙ n (_$′ x) g
-- hole at the n-th position
holeₙ : ∀ n {ls} {as : Sets n ls} → (A → as ⇉ B) → as ⇉ (A → B)
holeₙ zero f = f
holeₙ (suc n) f = holeₙ n ∘′ flip f
-- function constant in its n first arguments
-- Note that its type will only be inferred if it is used in a context
-- specifying what the type of the function ought to be. Just like the
-- usual const: there is no way to infer its domain from its argument.
constₙ : ∀ n {ls r} {as : Sets n ls} {b : Set r} → b → as ⇉ b
constₙ zero v = v
constₙ (suc n) v = const (constₙ n v)