------------------------------------------------------------------------
-- 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.Base 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)