------------------------------------------------------------------------
-- Applicative structures
------------------------------------------------------------------------

module SimplyTyped.ApplicativeStructure where

open import SimplyTyped.TypeSystem

record ApplicativeStructure : Set1 where
  field
    -- Semantic domains.

    Dom : TmLike

    -- Interpretations of variables, abstractions and applications.

    Var : ∀ {Γ τ} → Γ ∋ τ → Dom Γ τ
    Lam : ∀ {Γ σ τ} → Dom (Γ ▻ σ) τ → Dom Γ (σ ⟶ τ)
    App : ∀ {Γ σ τ} → Dom Γ (σ ⟶ τ) → Dom Γ σ → Dom Γ τ

  -- Given an applicative structure a term can easily be interpreted.
  -- (Yes, this module just encodes a fold.)

  ⟦_⟧ : ∀ {Γ τ} → Γ ⊢ τ → Dom Γ τ
  ⟦ var x   ⟧ = Var x
  ⟦ ƛ t     ⟧ = Lam ⟦ t ⟧
  ⟦ t₁ · t₂ ⟧ = App ⟦ t₁ ⟧ ⟦ t₂ ⟧