An explanation of polynomial functors

Polynomial.agda

{-# OPTIONS --postfix-projections #-}
open import Agda.Primitive
open import Data.Product
module Polynomial where

variable
  X I O : Set

record Poly : Set₁ where
  -- A polynomial is an expression
  --   ∑[i] X^e(i)
  -- where i : Ind is from an index set, and
  -- e(i) is the exponent.
  field
    Ind : Set
    Exp : Ind → Set

-- We can realize this polynomial as a functor
⟦_⟧ : Poly → Set → Set
⟦ p ⟧ X = Σ[ i ∈ Ind ] (Exp i → X)
  where open Poly p
-- The part that proves it is a functor is left to the reader.

-- Some examples
module Example where
  -- Trivial examples left to the reader:
  --   the polynomials X ↦ X, X ↦ 1 + X, X ↦ X² etc.
  -- They can be easily constructed.

  -- An interesting example is the List functor.
  -- It is schematically
  --   List(X) = 1 + X + X² + X³ + ⋯
  -- So our `Ind` type should be `ℕ`, and the exponent
  -- should be `Fin n`.
  open import Data.Nat
  open import Data.Fin
  open import Data.List
  open import Data.Vec.Functional

  𝕃 : Poly
  𝕃 .Poly.Ind = ℕ
  𝕃 .Poly.Exp = Fin

  -- Let's demonstrate that this indeed gives the
  -- list functor. These are just converting between
  -- `Fin n → X` and `List X`.

  ⟦𝕃⟧→List : ⟦ 𝕃 ⟧ X → List X
  ⟦𝕃⟧→List (_ , xs) = toList xs

  List→⟦𝕃⟧ : List X → ⟦ 𝕃 ⟧ X
  List→⟦𝕃⟧ xs = _ , fromList xs

-- More generally, we can allow multiple variables
-- and multiple outputs. Here the input variables
-- are labelled with the type I, and the output
-- with the type O. `Poly` is simply `MPoly ⊤ ⊤`.
record MPoly (I O : Set) : Set₁ where
  field
    Ind : O → Set
    Exp : (o : O) → Ind o → I → Set

-- `(I → Set)` represents the input of I-many
-- variables of type `Set`.
⟦_⟧ₘ : MPoly I O → (I → Set) → (O → Set)
⟦ p ⟧ₘ X[_] o = Σ[ j ∈ Ind o ] (∀ i → Exp o j i → X[ i ])
  where open MPoly p

variable
  P Q : MPoly I O

-- What should the morphisms be? We would like
-- the morphisms to induce a natural transformation
-- on the functor `⟦ p ⟧ₘ`. So for the indices,
-- we should have a forward map. But the exponent
-- should have a backward map for contravariance.

record _⟶_ (P Q : MPoly I O) : Set₁ where
  module P = MPoly P
  module Q = MPoly Q
  field
    ind : ∀ o → P.Ind o → Q.Ind o
    exp : ∀ o j i → Q.Exp o (ind o j) i → P.Exp o j i

-- This is the induced natural transformation.
[_] : P ⟶ Q → ∀ X o
  → ⟦ P ⟧ₘ X o → ⟦ Q ⟧ₘ X o
[ F ] X o (j , a) = ind o j , λ i e → a i (exp o j i e)
  where open _⟶_ F
-- Naturality omitted.

open import Data.Sum
open MPoly

-- What operation can we have on polynomials?
-- As endofunctors, we should be able to compose them.
-- (...)

-- Also, we can add them.
_⊕_ : MPoly I O → MPoly I O → MPoly I O
(F ⊕ G) .Ind o = F .Ind o ⊎ G .Ind o
  -- Their terms are simply put together
(F ⊕ G) .Exp o (inj₁ x) j = F .Exp o x j
(F ⊕ G) .Exp o (inj₂ y) j = G .Exp o y j
  -- Their exponents are unchanged

-- We can multiply them, remember we have
-- distributivity of multiplication over addition.
_⊗_ : MPoly I O → MPoly I O → MPoly I O
(F ⊗ G) .Ind o = F .Ind o × G .Ind o
  -- By distributivity, the terms are paired together
(F ⊗ G) .Exp o (x , y) j = F .Exp o x j ⊎ G .Exp o y j
  -- Their exponents are added

-- We leave for the reader to prove that they are indeed
-- products and sums when considered categorically.

-- For exponentials, let's think about
-- the single variable case again. In the category
-- Functor(𝒞, 𝒞), the exponents should be
--   [P^Q](X) = Hom(よX, P^Q)
--            = Hom(よX × Q, P).
-- If Q is representable as よB, then
--        ... = Hom(よX × よB, P)
--            = Hom(よ(X + B), P)
--            = P(X+B)
-- Any general Q can be expressed as a sum of
-- representables.