Domain Equations

The domains 𝒟 σ form a "standard collection of domains for arithmetic" in PCF, written \(\mathcal D_\sigma\) in (Plotkin1977LCP). As PCF is a simply-typed language, the domains 𝒟 σ are not reflexive, so their embedding in Agda can use ordinary type definitions, not involving bijections.

{-# OPTIONS --rewriting --confluence-check --lossy-unification #-}

module Examples.PCF.Domain-Equations where

  open import Examples.PCF.Abstract-Syntax
  open import Notation.Domains
  open import Notation.Functions
  open import Notation.Flat.Booleans
  open import Notation.Flat.Naturals
  open import Notation.Updates
  open import Agda.Builtin.Nat renaming (_==_ to _==ᴺ_) public

  𝒟 : Types → Domain       -- standard domains
  𝒟 ι        = Nat⊥        -- natural numbers
  𝒟 o        = Bool⊥       -- truth-values
  𝒟 (σ ⇒ τ)  = 𝒟 σ →ᶜ 𝒟 τ  -- functions
  variable x y z : ⟪ 𝒟 σ ⟫

Environments ρ are type-preserving maps from variables to values. They are naturally modeled by a dependent type: Env σ consists of type-preserving maps from variables in Vars σ to their values in the domain 𝒟 σ. The environment ρ⊥ maps all variables to ⊥.

  Env = (σ : Types) → ⟪ Vars σ →ˢ 𝒟 σ ⟫  -- typed environments
  variable ρ : Env
  ρ⊥ : Env                               -- initial environment
  ρ⊥ _ _ = ⊥

Extension or overriding typed environments, written ρ [ v / x ]′ here, requires instances of the equality tests for both variables and types. The definition of the latter is somewhat tedious:

  _==ⱽ_ : Vars σ → Vars σ → Bool
  (α i σ ==ⱽ α i′ σ)  =  (i ==ᴺ i′)
  instance
    eqV : Eq (Vars σ)
    _==_ {{eqV}} = _==ⱽ_
  instance
    eqT : MaybeEq Types
    eqT ._==?_ ι ι = just refl
    eqT ._==?_ o o = just refl
    eqT ._==?_ (σ ⇒ τ) (σ₁ ⇒ τ₁) with σ ==? σ₁  | τ ==? τ₁
    eqT ._==?_ (σ ⇒ τ) (σ₁ ⇒ τ₁)    | just refl | just refl = just refl
    eqT ._==?_ (σ ⇒ τ) (σ₁ ⇒ τ₁)    | _         | _         = nothing
    eqT ._==?_ _ _ = nothing

  _[_/_]′ : Env → ⟪ 𝒟 σ ⟫ → Vars σ → Env
  -- ρ [ v / x ]′ maps x to v, and other x′ to ρ x′
  _[_/_]′ {σ} ρ x v = ρ [ σ ← ρ σ [ x / v ] ]