{-# OPTIONS --no-positivity-check #-}
{-# OPTIONS --no-termination-check #-}
{-# OPTIONS --universe-polymorphism #-}
module AlgIR where
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Function
open import Level
open import Data.Sum
{- 1. Families, the families monad and morphisms of families -}
{- families form a large functor -}
Fam : Set1 -> Set1
Fam D = Σ Set (λ A -> (A → D))
Fam₁ : {D D' : Set1} -> (D -> D') -> Fam D -> Fam D'
Fam₁ g (A , f) = (A , g ∘ f)
{- first and second projection of a family -}
π₀ : {D : Set1} -> Fam D -> Set
π₀ (U , T) = U
π₁ : {D : Set1} -> (P : Fam D) -> π₀ P → D
π₁ (U , T) = T
{- monadic structure of Families -}
η : {I : Set1} -> I -> Fam I
η i = (⊤ , const i)
μ : {D : Set1} -> Fam (Fam D) → Fam D
μ {D} (A , B) = (Σ A (π₀ ∘ B) , g)
where g : Σ A (π₀ ∘ B) -> D
g (a , k) = π₁ (B a) k
{- morphisms between families with the same index -}
_⇒_ : ∀ {a b} -> {I : Set} →
(P : I -> Set a) -> (Q : I -> Set b) -> Set (a ⊔ b)
P ⇒ Q = ∀ {i} → P i → Q i
{- 2 Inductive-recursive definitions by Dybjer and Setzer -}
{- the Dybjer Setzer codes -}
data IR (D : Set₁) : Set₁ where
ι : D → IR D
σ : (A : Set) → (A → IR D) → IR D
δ : (A : Set) → ((A → D) → IR D) → IR D
{- and their semantics which maps a family to a family. The first part
of the semantics computes the index -}
⟦_⟧₀ : {D : Set₁} → IR D → Fam D → Set
⟦ ι _ ⟧₀ P = ⊤
⟦ σ A f ⟧₀ P = Σ A (λ a → ⟦ f a ⟧₀ P)
⟦ δ A F ⟧₀ (U , T) = Σ (A → U) (λ f → ⟦ F (T ∘ f) ⟧₀ (U , T))
{- the second part of the semantics computes the decoding function -}
⟦_⟧₁ : {D : Set₁} → (c : IR D) → (P : Fam D) → ⟦ c ⟧₀ P → D
⟦ ι d ⟧₁ P _ = d
⟦ σ A f ⟧₁ P (s , x) = ⟦ f s ⟧₁ P x
⟦ δ A F ⟧₁ (U , T) (g , x) = ⟦ F (T ∘ g) ⟧₁ (U , T) x
{- and the family inductively defined by a code -}
mutual
data U {D : Set1} (c : IR D) : Set where
C : ⟦ c ⟧₀ (P c) → U c
T : {D : Set1} → (c : IR D) → U c → D
T c (C a) = ⟦ c ⟧₁ (P c) a
P : {D : Set1} → (c : IR D) → Fam D
P γ = (U γ , T γ)
{- 3 A Different presentation of IR using Fam, mixed variance and folds -}
{- while a family indexes by elements of a set, a large family indexes
by a (tuple) of large types. Note we separate out positive and
negative occurrences to make LFam take two inputs. This is where mixed variance starts -}
LFam : Set1 → Set1 → Set1
LFam I O = Σ Set (λ A → (A → I) → O)
{- as with Fam, LFam is functorial in its second component. We could
not express this functoriality without separating out the variance as
we did above into I and O -}
LFam₁ : {I X Y : Set1} → (X -> Y) -> LFam I X -> LFam I Y
LFam₁ f (A , F) = (A , f ∘ F)
{- localisation for LFam. This is the key concept which makes IR tick
.. the rest is plumbing. Localisation shows that given a small family
then we can turn any element of a large family into a small family by
"localising it" -}
ρ : {I O : Set1} -> Fam I -> LFam I O -> Fam O
ρ (U , T) (A , F) = ((A → U) , \g -> F ( T ∘ g ))
{- Mixed variant IR as an inductive (large) type -}
data IR2 (I O : Set1) : Set1 where
ι : O → IR2 I O
σ : Fam (IR2 I O) → IR2 I O
δ : LFam I (IR2 I O) → IR2 I O
{- fold oeprator for IR2 -}
iter : {I O X : Set1} ->
(O -> X) -> (Fam X -> X) -> (LFam I X -> X) -> IR2 I O -> X
iter α β γ (ι o) = α o
iter α β γ (σ f) = β (Fam₁ (iter α β γ) f)
iter α β γ (δ F) = γ (LFam₁ (iter α β γ) F)
{- decoding an IR2 code using fold. Not the use of the monadic structure of Fam allows us to do this -}
⟦_⟧' : {I O : Set1} -> IR2 I O -> Fam I → Fam O
⟦ c ⟧' m = iter η μ (μ ∘ ρ m) c
{- we can extract the index and decoding function if we want -}
⟦_⟧'₀ : {I O : Set1} -> IR2 I O -> Fam I → Set
⟦ c ⟧'₀ = π₀ ∘ ⟦ c ⟧'
⟦_⟧'₁ : {I O : Set1} -> (c : IR2 I O) -> (m : Fam I) → ⟦ c ⟧'₀ m -> O
⟦ c ⟧'₁ = π₁ ∘ ⟦ c ⟧'
{- IR2 families: -}
mutual
data U' {D : Set1} (c : IR2 D D) : Set where
C' : ⟦ c ⟧'₀ (P' c) → U' c
T' : {D : Set1} → (c : IR2 D D) → U' c → D
T' c (C' a) = ⟦ c ⟧'₁ (P' c) a
P' : {D : Set1} → (c : IR2 D D) → Fam D
P' c = (U' c , T' c)
{- IR2 is mixed variant -}
_✫_ : {I I' O : Set₁} -> IR2 I O -> (I' -> I) -> IR2 I' O
(ι d) ✫ f = ι d
(σ (A , g)) ✫ f = σ (A , λ a -> g a ✫ f)
(δ (A , F)) ✫ f = δ (A , \k -> F (f ∘ k) ✫ f)
_✯_ : {I O O' : Set₁} -> (O -> O') -> IR2 I O -> IR2 I O'
f ✯ (ι d) = ι (f d)
f ✯ (σ (A , g)) = σ (A , \a -> f ✯ (g a))
f ✯ (δ (A , F)) = δ (A , \k -> f ✯ F k)
{- 4 Containers and Container based IR-}
{- Containers ... a theory of simple data types -}
Cont : Set1
Cont = Fam Set
{- Containers represent functors -}
[_]₀ : ∀ {a} -> Cont -> Set a → Set a
[ (S , P) ]₀ X = Σ S (λ s -> (P s → X))
[_]₁ : ∀ {a b} -> ∀ {X : Set a} -> ∀ {Y : Set b} ->
(H : Cont) -> (X -> Y) -> [ H ]₀ X -> [ H ]₀ Y
[ (S , P) ]₁ f (s , g) = (s , f ∘ g)
{- Large Container Families and their localisation -} {- We make use
of the abstract structure highlighted above to define the semantics of
Container based IR codes -}
{- first large contioaner families -}
LCFam : Set1 -> Set1 -> Set1
LCFam I O = Σ Cont (λ H -> [ H ]₀ I -> O)
LCFam₁ : {I X Y : Set1} ->
(X -> Y) -> LCFam I X -> LCFam I Y
LCFam₁ f (H , F) = (H , f ∘ F)
{- then localisation for them -}
ρC : {I O : Set1} -> Fam I -> LCFam I O -> Fam O
ρC (B , f) (H , F) = ([ H ]₀ B , F ∘ [ H ]₁ f)
{- Container IR codes and their decoding -}
{- Note that ContIR I is the free monad on LCFam I, which shows that
we are in free monad land, just as we build terms from signatures -}
data ContIR (I O : Set1) : Set1 where
ι : O → ContIR I O
σδ : LCFam I (ContIR I O) → ContIR I O
{- fold for the type ContIR -}
iterC : {I O X : Set1} ->
(O -> X) -> (LCFam I X -> X) -> ContIR I O -> X
iterC α β (ι o) = α o
iterC α β (σδ F) = β (LCFam₁ (iterC α β) F)
{- using fold to define the decoding function -}
⟦_⟧C : {I O : Set1} -> ContIR I O -> Fam I → Fam O
⟦ c ⟧C m = iterC η (μ ∘ ρC m) c
{- extracting index and decoding function -}
⟦_⟧C₀ : {I O : Set1} -> ContIR I O -> Fam I → Set
⟦ c ⟧C₀ = π₀ ∘ ⟦ c ⟧C
⟦_⟧C₁ : {I O : Set1} -> (c : ContIR I O) -> (m : Fam I) → ⟦ c ⟧C₀ m -> O
⟦ c ⟧C₁ = π₁ ∘ ⟦ c ⟧C
{-5. Indexed Containers -}
{- an indexed contianer has positions indexed by a set -}
data ContC (I : Set) : Set1 where
contC : (S : Set) → (P : S → I -> Set) → ContC I
{- an indexed contianer maps I-indexed sets to sets -}
⟦_⟧I₀ : ∀ {a} -> {I : Set} -> ContC I -> (I -> Set a) -> Set a
⟦ contC S P ⟧I₀ X = Σ S (λ s -> P s ⇒ X)
{- and is functorial -}
⟦_⟧I₁ : ∀ {a b} -> {I : Set} -> (H : ContC I)
-> {P : I -> Set a} -> {Q : I -> Set b}
-> (f : P ⇒ Q) -> ⟦ H ⟧I₀ P → ⟦ H ⟧I₀ Q
⟦ contC S T ⟧I₁ f (s , g) = (s , λ x -> f (g x))
{-3. Large Indexed Container Families and their reflection -}
{- we capitalise on previous work by following the algorithm ... define large
indexed contianer families and their locaisation -}
LICFam : {I : Set} -> (D : I -> Set1) -> Set1 -> Set1
LICFam {I} D E = Σ (ContC I) (λ H -> ⟦ H ⟧I₀ D -> E)
LICFam₁ : {I : Set} -> {D : I -> Set1} -> {X Y : Set1} ->
(X -> Y) -> LICFam D X -> LICFam D Y
LICFam₁ f (H , F) = (H , f ∘ F)
{- products of families -}
data Π {a} (A : Set) (B : A → Set a) : Set a where
λ' : ( (a : A) → B a ) → Π A B
ρI : {I : Set} -> {D : I -> Set1} -> {E : Set1} ->
Π I (Fam ∘ D) -> LICFam D E → Fam E
ρI {I} {D} {E} (λ' Φ) (H , F) = (⟦ H ⟧I₀ V , F ∘ ⟦ H ⟧I₁ W)
where V : I → Set
V = π₀ ∘ Φ
W : V ⇒ D
W {i} = π₁ (Φ i)
{-4. Container IIR codes, their fold and their decoding -}
{- Indexed codes IIR D is again the free monad on LICFam D -}
data IIR {I : Set} (D : I -> Set1) (E : Set1) : Set1 where
ιI : E → IIR D E
σδI : LICFam D (IIR D E) → IIR D E
{- again a fold -}
iterI : {I : Set} -> {D : I -> Set1} -> {E : Set1} -> {X : Set1} ->
(E -> X) -> (LICFam D X -> X) -> IIR D E -> X
iterI α β (ιI e) = α e
iterI α β (σδI F) = β (LICFam₁ (iterI α β) F)
{- and again a decoding function given by a fold -}
⟦_⟧I : {I : Set} -> {D : I -> Set1} -> {E : Set1} ->
IIR D E -> Π I (Fam ∘ D) → Fam E
⟦ c ⟧I m = iterI η (μ ∘ ρI m) c
{- Fully Indexed contianers -}
{- Here we index input and output by sets -}
ICont : Set -> Set -> Set1
ICont I J = J -> ContC I
{- and hence get functors that map I -indexed sets to J-indexed sets -}
⟨_⟩₀ : ∀ {a} {I J : Set} -> ICont I J -> (I -> Set a) -> (J -> Set a)
⟨ Φ ⟩₀ X j = ⟦ Φ j ⟧I₀ X
{- in a functorial way -}
⟨_⟩₁ : ∀ {a b} -> {I J : Set} -> (H : ICont I J)
-> {P : I -> Set a} -> {Q : I -> Set b}
-> (f : P ⇒ Q) -> ⟨ H ⟩₀ P ⇒ ⟨ H ⟩₀ Q
⟨ Φ ⟩₁ f {j} = ⟦ Φ j ⟧I₁ f
{- Fully Indexed IR -}
{- same pattern -}
IIIR : {I J : Set} -> (D : I -> Set1) -> (E : J -> Set1) -> Set1
IIIR {I} {J} D E = (j : J) -> IIR {I} D (E j)
⟨_⟩ : {I J : Set} -> {D : I -> Set1} -> {E : J -> Set1} ->
IIIR D E -> Π I (Fam ∘ D) → Π J (Fam ∘ E)
⟨ Φ ⟩ m = λ' (λ j -> ⟦ Φ j ⟧I m)