DagTypes.agda

DagTypes.agda

module DagTypes where

data Unit : Set where
  * : Unit

data Void : Set where

data Sum (A B : Set) : Set where
  inl : A → Sum A B
  inr : B → Sum A B
_+_ = Sum

postulate
   -- The intended meaning of F ◦ G is, supposing F and G are regular types,
   -- i.e. F(α) = Σ_n c_n × α^n
   --      G(α) = Σ_n d_n × α^n
   -- that F ◦ G = Σ_n (c_n × d_n)
   -- This can be thought of analytically as saying that F ◦ G
   -- is the *coefficient of x^0* in the power series
   --      F(x)G(1/x)
  _◦_ : (Set → Set) → (Set → Set) → Set

  -- Type derivative
  D : (Set → Set) → (Set → Set)

-- Use these operations in recursive type definitions
{-# POLARITY D ++ #-}
{-# POLARITY _◦_ ++ ++ #-}

-- A "referential type" F is a type parameterized over two
-- type arguments:
-- F π ρ expresses data with π * ⋯ at every "place" that
-- can be referred to, and ρ for pieces of data that can
-- be external references.
Ref : Set₁
Ref = (π ρ : Set) → Set

-- Given F(π), return λ h →  (1 + hπ D_π + (hπ D_π)^2 + (hπ D_π)^3 + ⋯)F
data DerivList (F : (Set → Set)) : (Set → Set → Set) where
  dlnil : (h π : Set) → F π → DerivList F h π
  dlcons : (h π : Set) → h → π → D (DerivList F h) π → DerivList F h π

-- This type operator creates the referential type
-- F ◁ G which is "some data of type F, and some data of type G,
-- but the latter is allowed to have its references connect up
-- to places in the former".
_◁_ : Ref → Ref → Ref
(F ◁ G) π ρ = (λ h → DerivList (λ π → F π ρ) h π ) ◦ (λ h → G π (ρ + h))

-- rDag α π ρ = Binary directed acyclic graph with α at the leaves, with
-- eligible reference targets π, with ρ external references
data rDag (α : Set) : Ref where
  ref : (π ρ : Set) → ρ → rDag α π ρ
  leaf : (π ρ : Set) → π → α → rDag α π ρ
  node : (π ρ : Set) → π → (rDag α ◁ rDag α) π ρ → rDag α π ρ

-- Dag α = Binary dags with α at leaves
Dag : Set → Set
Dag α = rDag α Unit Void