A start on formalisation of STLC + type synonyms and newtype

localdefs.agda

module localdefs where

mutual
  data ty-ctx : Set where
    ε    : ty-ctx
    _,-_ : (Δ : ty-ctx) → defn Δ → ty-ctx

  data defn : ty-ctx → Set where
    synonym : ∀ {Δ} → ty Δ → defn Δ
    newtype : ∀ {Δ} → ty Δ → defn Δ

  data ty : ty-ctx → Set where
    wk    : ∀ {Δ τ} → ty Δ → ty (Δ ,- τ)
    defd  : ∀ {Δ τ} → ty (Δ ,- τ)
    bit   : ∀ {Δ}   → ty Δ
    _⇒_  : ∀ {Δ}   → ty Δ → ty Δ → ty Δ

infixl 10 _,-_

data _≅ty_ : ∀ {Δ} → ty Δ → ty Δ → Set where
  expand   : ∀ {Δ τ} →
             defd{Δ}{synonym τ} ≅ty wk τ

  wk-bit   : ∀ {Δ τ}       → wk{Δ}{τ}        bit ≅ty bit
  wk-⇒    : ∀ {Δ τ σ₁ σ₂}  → wk{Δ}{τ} (σ₁ ⇒ σ₂) ≅ty (wk{Δ}{τ} σ₁ ⇒ wk σ₂)

  cong-wk  : ∀ {Δ τ σ₁ σ₂}              → σ₁ ≅ty σ₂ → wk{Δ}{τ} σ₁ ≅ty wk{Δ}{τ} σ₂
  cong-⇒  : ∀ {Δ}{σ₁ σ₁' σ₂ σ₂' : ty Δ} → σ₁ ≅ty σ₂ → σ₁' ≅ty σ₂' → (σ₁ ⇒ σ₁') ≅ty (σ₂ ⇒ σ₂')

  ≅ty-refl  : ∀ {Δ}{τ : ty Δ} → τ ≅ty τ
  ≅ty-trans : ∀ {Δ}{τ₁ τ₂ τ₃ : ty Δ} →
              τ₁ ≅ty τ₂ → τ₂ ≅ty τ₃ → τ₁ ≅ty τ₃
  ≅ty-symm  : ∀ {Δ}{τ₁ τ₂ : ty Δ} →
              τ₁ ≅ty τ₂ →
              τ₂ ≅ty τ₁

-- looking up newtypes
data _⊢tydef_≡_ : (Δ : ty-ctx) → ty Δ → ty Δ → Set where
  zero : ∀ {Δ τ}     →                   (Δ ,- newtype τ) ⊢tydef defd ≡ wk τ
  suc  : ∀ {Δ τ x σ} → Δ ⊢tydef x ≡ τ → (Δ ,- σ) ⊢tydef wk x ≡ wk τ

-- typing contexts
data ctx (Δ : ty-ctx) : Set where
  ε : ctx Δ
  _,-_ : ctx Δ → ty Δ → ctx Δ

data _/_⊢v_ : (Δ : ty-ctx) → ctx Δ → ty Δ → Set where
  zero : ∀ {Δ Γ τ} →                 Δ / Γ ,- τ ⊢v τ
  suc  : ∀ {Δ Γ τ σ} → Δ / Γ ⊢v τ → Δ / Γ ,- σ ⊢v τ

data _/_⊢_ : (Δ : ty-ctx) → ctx Δ → ty Δ → Set where
  `_  : ∀ {Δ Γ τ} →
        Δ / Γ ⊢v τ →
        Δ / Γ ⊢ τ

  ƛ   : ∀ {Δ Γ σ τ} →
        Δ / Γ ,- σ ⊢ τ →
        Δ / Γ ⊢ (σ ⇒ τ)
  _·_ : ∀ {Δ Γ σ τ} →
        Δ / Γ ⊢ (σ ⇒ τ) →
        Δ / Γ ⊢ σ →
        Δ / Γ ⊢ τ

  `0 `1 : ∀ {Δ Γ} →
          Δ / Γ ⊢ bit

  mk    : ∀ {Δ Γ τ σ} →
          Δ ⊢tydef τ ≡ σ →
          Δ / Γ ⊢ σ →
          Δ / Γ ⊢ τ
  proj  : ∀ {Δ Γ τ σ} →
          Δ ⊢tydef τ ≡ σ →
          Δ / Γ ⊢ τ →
          Δ / Γ ⊢ σ

  conv : ∀ {Δ Γ τ₁ τ₂} →
         τ₁ ≅ty τ₂ →
         Δ / Γ ⊢ τ₁ →
         Δ / Γ ⊢ τ₂

------------------------------------------------------------------------------

-- A context that is like the Haskell:
--
--      newtype A = A Bit
--      type B = Bit
Δ : ty-ctx
Δ = ε ,- newtype bit ,- synonym bit

-- type synonyms are resolved by expanding definitions within the
-- 'conv' rule.
synonym-seethrough : Δ / ε ⊢ (defd ⇒ bit)
synonym-seethrough = ƛ (conv (≅ty-trans expand wk-bit) (` zero))

-- newtypes need explicit 'proj' constructors to be inserted.
newtype-not-seethrough : Δ / ε ⊢ (wk defd ⇒ bit)
newtype-not-seethrough = ƛ (conv (≅ty-trans (cong-wk wk-bit) wk-bit) (proj (suc zero) (` zero)))