Scott.agda

-- type-in-type is unlikely to be necessary, but it does make my life easier.
{-# OPTIONS --type-in-type         #-}

module Scott where

open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Data.Unit
open import Data.Nat

-- A proof of correctness for Scott-encoded datatypes.
-- The proof is organized as follows: we define a type ADT of algebraic datatypes
-- and give two semantics of it in Agda: a straightforward one where e.g. products are interpreted
-- as Agda products and a Scott-encoded one. We then show that these are isomorphic.

postulate extensionality' : ∀ {A} {B : A → Set} {f : ∀ (x : A) → B x} {g : ∀ (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g
extensionality : ∀ {A B} {f : A → B} {g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
extensionality = extensionality'

-- A definition of an isomorphism between two (Agda) sets.
record Iso (A : Set) (B : Set) : Set where
  field
    left : A → B
    right : B → A
    iso₁ : ∀ {x} → right (left x) ≡ x
    iso₂ : ∀ {y} → left (right y) ≡ y

_≅_ = Iso
infix 10 _≅_

-- iso₁e and iso₂e aren't strictly necessary, only a convenient shortcut.
iso₁e : ∀ {A B} → (i : A ≅ B) → Iso.right i ∘ Iso.left i ≡ id
iso₁e = extensionality ∘ (λ i x → Iso.iso₁ i {x})

iso₂e : ∀ {A B} → (i : A ≅ B) → Iso.left i ∘ Iso.right i ≡ id
iso₂e = extensionality ∘ (λ i x → Iso.iso₂ i {x})

Iso-refl : ∀ {A} → A ≅ A
Iso-refl = record { left = id; right = id; iso₁ = refl; iso₂ = refl}

Iso-comp : ∀ {A B C} → B ≅ C → A ≅ B → A ≅ C
Iso-comp i2 i1 = record
  { left = λ z → Iso.left i2 (Iso.left i1 z)
  ; right = λ z → Iso.right i1 (Iso.right i2 z)
  ; iso₁ = trans (cong (Iso.right i1) (Iso.iso₁ i2)) (Iso.iso₁ i1)
  ; iso₂ = trans (cong (Iso.left i2) (Iso.iso₂ i1)) (Iso.iso₂ i2)
  }

_⊚_ = Iso-comp
infixr 4 _⊚_

Iso-sym : ∀ {A B} → A ≅ B → B ≅ A
Iso-sym i = record { left = Iso.right i; right = Iso.left i; iso₁ = Iso.iso₂ i; iso₂ = Iso.iso₁ i }

-- Essentially: "every function of type ∀ Q → (A → Q) → Q is a natural transformation"
postulate naturality : ∀ {A B C} {f : ∀ (Q : Set) → (A → Q) → Q} {g : B → C} → g ∘ f B ≡ f C ∘ (g ∘_)

-- The Yoneda lemma, internal to Agda.
-- This is essential to correctness of Scott encodings.
yoneda : ∀ {A} → A ≅ (∀ (Q : Set) → (A → Q) → Q)
yoneda {A} = record
  { left  = λ a Q cont → cont a
  ; right = λ cps → cps A id
  ; iso₁  = refl
  ; iso₂  = λ {y : (Q : Set) → (A → Q) → Q} →
    extensionality' λ Q → extensionality λ cont →
      begin
        cont (y A id)
      ≡⟨ refl ⟩
        (cont ∘ (y A)) (λ z → z)
      ≡⟨ cong-app (naturality {_} {_} {_} {y} {cont}) id ⟩
        y Q cont
      ∎
  }

-- A description of a (non-recursive) algebraic datatype with free variables in some set V
data Factor : {V : Set} → Set where
  𝟙   : ∀ {V} → Factor {V}
  _⊗_ : ∀ {V} → V → Factor {V} → Factor {V}

data ADT : {V : Set} → Set where
  𝟘   : ∀ {V} → ADT {V}
  _⊕_ : ∀ {V} → Factor {V} → ADT {V} → ADT {V}

infixr 5 _⊕_
infixr 4 _⊗_

⟦_⊢_⟧* : ∀ {V} → (V → Set) → Factor {V} → Set
⟦ Γ ⊢ 𝟙 ⟧*       = ⊤
⟦ Γ ⊢ a ⊗ p ⟧* = (Γ a) × ⟦ Γ ⊢ p ⟧*

-- We give a "standard" semantics of an algebraic datatype in terms of Agda types and constructs
⟦_⊢_⟧ : ∀ {V} → (V → Set) → ADT {V} → Set
⟦ Γ ⊢ 𝟘 ⟧    = ⊥
⟦ Γ ⊢ f ⊕ a ⟧ = ⟦ Γ ⊢ f ⟧* ⊎ ⟦ Γ ⊢ a ⟧

-- We prove now that the standard semantics is functorial on its free variables (essentially, that we can
-- derive an instance of Functor for every ADT).

-- Covariant functors on an I-indexed family of arguments.
record Functor+ {I} (F : (I → Set) → Set) : Set where
  constructor functor+
  field
    fmap : ∀ {a b : I → Set} → (∀ (i : I) → a i → b i) → F a → F b
    fmap-id : ∀ {a} {x} → fmap {a} (λ i → id) x ≡ x
    fmap-∘  : ∀ {a b c} {f g} {x} → (fmap {b} {c} g ∘ fmap f) x ≡ fmap {a} {c} (λ i → g i ∘ f i) x

-- Contravariant functors (necessary because the Scott-encoded semantics of a factor is in fact contravariant).
record Functor- {I} (F : (I → Set) → Set) : Set where
  constructor functor-
  field
    fmap : ∀ {a b : I → Set} → (∀ (i : I) → a i → b i) → F b → F a
    fmap-id : ∀ {a} {x} → fmap {a} (λ i → id) x ≡ x
    fmap-∘  : ∀ {a b c} {f g} {x} → (fmap {a} {b} g ∘ fmap f) x ≡ fmap {a} {c} (λ i → f i ∘ g i) x

⟦⟧*-Functor : ∀ {V} → (τ : Factor {V}) → Functor+ (λ Γ → ⟦ Γ ⊢ τ ⟧*)
⟦⟧*-Functor 𝟙 = functor+ (λ _ z → z) refl refl
⟦⟧*-Functor (a ⊗ τ) = record
  { fmap = λ { f (ai , τi) → (f a ai , Functor+.fmap (⟦⟧*-Functor τ) f τi) }
  ; fmap-id = λ { {a} {ai , τi} → cong (λ z → ai , z) (Functor+.fmap-id (⟦⟧*-Functor τ)) }
  ; fmap-∘ = λ { {_} {_} {_} {f} {g} {ai , τi}
               → cong (λ z → g a (f a ai) , z) (Functor+.fmap-∘ (⟦⟧*-Functor τ))
               }
  }

-- Functoriality of the standard semantics
⟦⟧-Functor : ∀ {V} → (τ : ADT {V}) → Functor+ (λ Γ → ⟦ Γ ⊢ τ ⟧)
⟦⟧-Functor 𝟘 = functor+ (λ _ z → z) refl refl
⟦⟧-Functor (p ⊕ τ) = record
  { fmap = λ f → [ inj₁ ∘ Functor+.fmap (⟦⟧*-Functor p) f
                 , inj₂ ∘ Functor+.fmap (⟦⟧-Functor τ) f ]′
  ; fmap-id = λ { {_} {inj₁ a} → cong inj₁ (Functor+.fmap-id (⟦⟧*-Functor p))
                ; {_} {inj₂ b} → cong inj₂ (Functor+.fmap-id (⟦⟧-Functor τ)) }
  ; fmap-∘ = λ {_} {_} {_} {f} {g}
             → λ { {inj₁ a} → cong inj₁ ((Functor+.fmap-∘ (⟦⟧*-Functor p)))
                 ; {inj₂ b} → cong inj₂ (Functor+.fmap-∘ (⟦⟧-Functor τ)) }
  }

scottFactor : ∀ {V} → (V → Set) → Factor {V} → Set → Set
scottFactor Γ 𝟙 Q       = Q
scottFactor Γ (a ⊗ f) Q = (Γ a) → scottFactor Γ f Q

scott1 : ∀ {V} → (V → Set) → ADT {V} → Set → Set
scott1 Γ 𝟘 Q       = Q
scott1 Γ (f ⊕ a) Q = scottFactor Γ f Q → scott1 Γ a Q

-- Scott-encoded semantics of a non-recursive algebraic datatype
⟦_⊢_⟧s : ∀ {V} → (V → Set) → ADT {V} → Set
⟦ Γ ⊢ t ⟧s = ∀ Q → scott1 Γ t Q

sf-Functor : ∀ {Q} {V} → (τ : Factor {V}) → Functor- (λ Γ → scottFactor Γ τ Q)
sf-Functor 𝟙 = functor- (λ _ z → z) refl refl
sf-Functor (i ⊗ τ) = record
  { fmap = λ f τi → Functor-.fmap (sf-Functor τ) f ∘ τi ∘ f i
  ; fmap-id = extensionality (λ ai → Functor-.fmap-id (sf-Functor τ))
  ; fmap-∘ = λ {_} {_} {_} {f} {g} → extensionality (λ ai → Functor-.fmap-∘ (sf-Functor τ))
  }

scott-Functor : ∀ {Q} {V} → (τ : ADT {V}) → Functor+ (λ Γ → scott1 Γ τ Q)
scott-Functor {Q} 𝟘 = functor+ (λ _ z → z) refl refl
scott-Functor {Q} (x ⊕ τ) = record
  { fmap = λ f τi →  Functor+.fmap (scott-Functor τ) f ∘ τi ∘ (Functor-.fmap (sf-Functor x) f)
  ; fmap-id = λ {a τi} → extensionality (λ ai
                       → trans (Functor+.fmap-id (scott-Functor τ))
                         (cong τi (Functor-.fmap-id (sf-Functor x))))
  ; fmap-∘ = λ {_} {_} {_} {f} {g} {τi} → extensionality (λ xi
                                        → trans (Functor+.fmap-∘ (scott-Functor τ))
                                                (cong (Functor+.fmap (scott-Functor τ) (λ i → g i ∘ f i) ∘ τi)
                                                      (Functor-.fmap-∘ (sf-Functor x))))
  }

-- Functoriality of the Scott semantics w.r.t. its arguments
⟦⟧s-Functor : ∀ {V} → (τ : ADT {V}) → Functor+ (λ Γ → ⟦ Γ ⊢ τ ⟧s)
⟦⟧s-Functor τ = record
  { fmap = λ f τi Q → Functor+.fmap (scott-Functor τ) f (τi Q)
  ; fmap-id = extensionality' (λ Q → Functor+.fmap-id (scott-Functor τ))
  ; fmap-∘ = extensionality' (λ Q → Functor+.fmap-∘ (scott-Functor τ) )
  }

-- A couple of useful lemmas stating obvious isomorphisms - iterating these is what gets us correctness
Iso-curry : ∀ {A B C} → (A → B → C) ≅ (A × B → C)
Iso-curry = record
  { left  = λ curried pair → curried (proj₁ pair) (proj₂ pair)
  ; right = λ uncurried a b → uncurried (a , b)
  ; iso₁  = refl
  ; iso₂  = λ {y} → extensionality (λ x → cong y refl)
  }
Iso-sum : ∀ {A B C} → ((A → C) × (B → C)) ≅ (A ⊎ B → C)
Iso-sum = record
  { left  = λ pf → [ proj₁ pf , proj₂ pf ]′
  ; right = λ case → (case ∘ inj₁ , case ∘ inj₂)
  ; iso₁  = refl
  ; iso₂  = extensionality λ
            { (inj₁ a) → refl
            ; (inj₂ b) → refl
            }
  }

-- Covariant and contravariant Hom-functors
-- Not useful by themselves, but these allow one to derive (A' → B' ≅ A → B) from A' ≅ A and B' ≅ B
Hom+ : ∀ {A} → Functor+ (λ B → A → B tt)
Hom+ = functor+ (λ z z₁ x → z tt (z₁ x)) refl refl
Hom- : ∀ {B} → Functor- (λ A → A tt → B)
Hom- = functor- (λ z z₁ x → z₁ (z tt x)) refl refl

_⟫_ : ∀ {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_⟫_ = trans
infixr -10 _⟫_

-- Propagating isomorphisms through an (indexed) functor.
-- Note that one needs to provide an isomorphism for every index.
Iso-Functor+ : ∀ {I} {A B} {F : (I → Set) → Set} → Functor+ F → (∀ (i : I) → A i ≅ B i) → F A ≅ F B
Iso-Functor+ ft ii = record
  { left = Functor+.fmap ft (λ v → Iso.left (ii v))
  ; right = Functor+.fmap ft (λ v → Iso.right (ii v))
  ; iso₁ = λ {x} → Functor+.fmap-∘ ft
                   ⟫ cong (λ f → Functor+.fmap ft f x)
                          (extensionality' λ v → iso₁e (ii v))
                   ⟫ Functor+.fmap-id ft
  ; iso₂ = λ {x} → Functor+.fmap-∘ ft
                   ⟫ cong (λ f → Functor+.fmap ft f x)
                          (extensionality' λ v → iso₂e (ii v))
                   ⟫ Functor+.fmap-id ft
  }

Iso-Functor- : ∀ {I} {A B} {F : (I → Set) → Set} → Functor- F → (∀ (i : I) → A i ≅ B i) → F A ≅ F B
Iso-Functor- ft ii = record
  { left = Functor-.fmap ft (λ v → Iso.right (ii v))
  ; right = Functor-.fmap ft (λ v → Iso.left (ii v))
  ; iso₁ = λ {x} → Functor-.fmap-∘ ft
                   ⟫ cong (λ f → Functor-.fmap ft f x)
                          (extensionality' λ v → iso₁e (ii v))
                   ⟫ Functor-.fmap-id ft
  ; iso₂ = λ {x} → Functor-.fmap-∘ ft
                   ⟫ cong (λ f → Functor-.fmap ft f x)
                          (extensionality' λ v → iso₂e (ii v))
                   ⟫ Functor-.fmap-id ft
  }

-- Propagating isomorphism through function and polymorphic types
Iso-fun : ∀ {A B A' B'} → A ≅ A' → B ≅ B' → (A → B) ≅ (A' → B')
Iso-fun ia ib = Iso-Functor+ Hom+ (λ {tt → ib}) ⊚ Iso-Functor- Hom- λ {tt → ia}
Iso-forall : ∀ {A B : Set → Set} → (∀ x → A x ≅ B x) → (∀ x → A x) ≅ (∀ x → B x)
Iso-forall i = record
  { left  = λ z x → Iso.left (i x) (z x)
  ; right = λ z x → Iso.right (i x) (z x)
  ; iso₁  = extensionality' (λ x₁ → Iso.iso₁ (i x₁))
  ; iso₂  = extensionality' (λ y₁ → Iso.iso₂ (i y₁))
  }

-- Trivial isomorphisms
Iso-unit : ∀ {A} → A ≅ (⊤ → A)
Iso-unit = record
  { left  = λ a tt → a
  ; right = λ fa → fa tt
  ; iso₁  = refl
  ; iso₂  = λ {y} → extensionality λ x → cong y refl
  }
Iso-bot : ∀ {A} → ⊤ ≅ (⊥ → A)
Iso-bot = record
  { left  = λ tt → λ ()
  ; right = λ u → tt
  ; iso₁  = refl
  ; iso₂  = extensionality λ ()
  }

factorCurry : ∀ {V} {Γ : V → Set} t Q → (scottFactor Γ t Q) ≅ (⟦ Γ ⊢ t ⟧* → Q)
factorCurry 𝟙 Q = Iso-unit
factorCurry (A ⊗ t) Q = Iso-curry ⊚ Iso-fun Iso-refl (factorCurry t Q)

scottCurry : ∀ {V} {Γ : V → Set} t Q → (scott1 Γ t Q) ≅ ((⟦ Γ ⊢ t ⟧ → Q) → Q)
scottCurry 𝟘 Q = Iso-fun Iso-bot Iso-refl ⊚ Iso-unit
scottCurry (x ⊕ t) Q = Iso-fun Iso-sum Iso-refl ⊚ (Iso-curry ⊚ Iso-fun (factorCurry x Q) (scottCurry t Q))

-- Correctness of the Scott encoding for non-recursive datatypes.
-- The idea goes as follows: we show that, for every Q, the Scott-encoded type is
-- isomorphic to (⟦ Γ ⊢ τ ⟧ → Q) → Q (by iterating the ×, ⊎ isomorphisms) and then
-- we apply Yoneda
nonrec-scott-correct : ∀ {V} {Γ : V → Set} (t : ADT {V}) → ⟦ Γ ⊢ t ⟧s ≅ ⟦ Γ ⊢ t ⟧
nonrec-scott-correct t = Iso-sym yoneda ⊚ Iso-forall (scottCurry t) ⊚ Iso-refl

-- Type-level (parametric) fixed point combinator. Note that we want to do simultaneous induction on
-- an E-indexed family of mutually-recursive types.
{-# NO_POSITIVITY_CHECK #-}
data pFix {E : Set} (f : (E → Set) → (E → Set)) (e : E) : Set where
  into : f (λ e' → pFix f e') e → pFix f e

-- "Correctness" for pFix
pFix-Iso : ∀ {E : Set} (f : (E → Set) → (E → Set)) (e : E) → pFix f e ≅ f (pFix f) e
pFix-Iso f e = record
  { left  = λ { (into p) → p}
  ; right = into
  ; iso₁  = λ { {into p} → refl }
  ; iso₂  = refl }

data Recur : Set where
  recur : Recur

self : ∀ {V} → V ⊎ Recur
self = inj₂ recur

var : ∀ {V} → V → V ⊎ Recur
var = inj₁

-- A recursive datatype that refers to E recursive types and V free type variables is
-- precisely a (non) recursive datatype that refers to V ⊎ E free type variables
Recursive : ∀ {V : Set} → Set → Set
Recursive {V} R = ADT {V ⊎ R}

-- Partially applying an indexed functor gives a functor
partial : ∀ {V E} {F} → Functor+ {V ⊎ E} F → (V → Set) → (E → Set) → Set
partial {_} {_} {F} ft Γ Σ = F [ Γ , Σ ]′

partial-Functor : ∀ {V E} {F} → (Γ : V → Set) → (ft : Functor+ {V ⊎ E} F) → Functor+ {E} (partial ft Γ)
partial-Functor Γ ft = record
  { fmap = λ f → Functor+.fmap ft (λ {(inj₁ a) → id; (inj₂ b) → f b})
  ; fmap-id = λ {_} {x} → cong (λ f → Functor+.fmap ft f x)
                               (extensionality' (λ {(inj₁ a) → refl; (inj₂ b) → refl}))
                          ⟫ Functor+.fmap-id ft
  ; fmap-∘ = λ {_} {_} {_} {_} {_} {x} → Functor+.fmap-∘ ft
                                         ⟫ cong (λ f → Functor+.fmap ft f x)
                                                (extensionality' λ {(inj₁ a) → refl; (inj₂ b) → refl})
  }

-- (sem1/sem1s) separates the fixed and the recursive variables in a (normal/Scott-encoded) ADT
sem1 : ∀ {V E} → Recursive {V} E → (V → Set) → (E → Set) → Set
sem1 = partial ∘ ⟦⟧-Functor

sem1-Functor : ∀ {V E} → (τ : Recursive {V} E) → (Γ : V → Set) → Functor+ (sem1 τ Γ)
sem1-Functor τ Γ = partial-Functor Γ (⟦⟧-Functor τ)

sem1s : ∀ {V E} → Recursive {V} E → (V → Set) → (E → Set) → Set
sem1s = partial ∘ ⟦⟧s-Functor

sem1s-Functor : ∀ {V E} → (τ : Recursive {V} E) → (Γ : V → Set) → Functor+ (sem1s τ Γ)
sem1s-Functor τ Γ = partial-Functor Γ (⟦⟧s-Functor τ)

-- Recursive semantics for E-indexed families of mutually recursive datatypes.
-- These are obtained by partially applying these (i.e. giving concrete values for all the free type
-- variables in V) and taking the parametric fixed point with respect to the recursive variables in E.
⟦_⊢_⟧r : ∀ {V E} → (V → Set) → (E → Recursive {V} E) → E → Set
⟦ Γ ⊢ τ ⟧r e = pFix (λ Σ e' → sem1 (τ e') Γ Σ) e

⟦_⊢_⟧rs : ∀ {V E} → (V → Set) → (E → Recursive {V} E) → E → Set
⟦ Γ ⊢ τ ⟧rs e = pFix (λ Σ e' → sem1s (τ e') Γ Σ) e

-- The proof for correctness goes as follows:
-- Let F (resp. sF) be the normal (resp. Scott-encoded) semantics of some type. Then:
-- Fix(F) ≅ F (Fix(F)) ≅ F (Fix(G)) ≅ G (Fix(G)) ≅ Fix(G)
{-# TERMINATING #-}
scott-encoding-correct : ∀ {V E} (τ : E → Recursive {V} E) (Γ : V → Set) → ∀ e → ⟦ Γ ⊢ τ ⟧r e ≅ ⟦ Γ ⊢ τ ⟧rs e
scott-encoding-correct τ Γ e =  (Iso-sym (pFix-Iso (λ Σ e' → sem1s (τ e') Γ Σ) e))
                                ⊚ Iso-sym (nonrec-scott-correct (τ e))
                                ⊚ Iso-Functor+ (sem1-Functor (τ e) Γ) (scott-encoding-correct τ Γ)
                                ⊚ pFix-Iso (λ Σ e' → sem1 (τ e') Γ Σ) e