[Agda] Dealing with HOAS

[Darin Morrison]

On Thu, Sep 24, 2009 at 8:36 PM, Vag Vagoff <vag.vagoff at gmail.com> wrote:
> How to express syntax of Simply Type Lambda Calculus using HOAS?
>
> This encoding gives an error about Exp on left side of ->:
>
> data Typ : Set where
> _⟶_ : Typ → Typ → Typ
> type : String → Typ
>
> data Val : Typ → Set where
> num : ℕ → Val Int
>
> data Exp : Typ → Set where
> val : ∀ {t} → Val t → Exp t
> lam : ∀ {t₁ t₂} → (Exp t₁ → Exp t₂) → Exp (t₁ ⟶ t₂)
> app : ∀ {t₁ t₂} → Exp (t₁ ⟶ t₂) → Exp t₂ → Exp t₁
>
> How to hack this representation to get rid of error?

What are you trying to do with this representation?

If you want to write a simple interpreter, one way you can achieve
this is to use a well-scoped deBruijn representation to write the
terms and then interpret the terms into a fragment of Agda for
normalisation.

For the most part this works pretty well and well-scoped deBruijn
indices are actually not that painful to work with.  The downside is
that it's much more difficult to convert interpreted terms back to the
deBruijn representation if you need that functionality.  In that case,
you will have to investigate normalisation by evaluation and interpret
the terms via what amounts to a Kripke model for intuitionistic
propositional logic.

Below I've included code for the first part I described.

Cheers,
Darin

---

module Exp where

open import Data.Unit

-- Types
infixr 0 _⇒_
data Type : Set where
 unit : Type
 _⇒_  : Type → Type → Type

-- Contexts
infixl 1 _▸_
data Ctx : Set where
 ε   : Ctx
 _▸_ : Ctx → Type → Ctx

-- Variables
infix 0 _∋_
data _∋_ : Ctx → Type → Set where
 vz : ∀ {Γ τ}     → Γ ▸ τ ∋ τ
 vs : ∀ {Γ τ₁ τ₂} → Γ ∋ τ₁ → Γ ▸ τ₂ ∋ τ₁

-- Terms (well-scoped deBruijn)
infix 0 _⊢_
data _⊢_ : Ctx → Type → Set where
 t   : ∀ {Γ}       → Γ ⊢ unit
 var : ∀ {Γ τ}     → Γ ∋ τ → Γ ⊢ τ
 _·_ : ∀ {Γ τ₁ τ₂} → Γ ⊢ τ₁ ⇒ τ₂ → Γ ⊢ τ₁ → Γ ⊢ τ₂
 ƛ_  : ∀ {Γ τ₁ τ₂} → Γ ▸ τ₁ ⊢ τ₂ → Γ ⊢ τ₁ ⇒ τ₂

-- Interpreted Types
⟪_⟫ : Type → Set
⟪ unit    ⟫ = ⊤
⟪ τ₁ ⇒ τ₂ ⟫ = ⟪ τ₁ ⟫ → ⟪ τ₂ ⟫

-- Environments
data Env : Ctx → Set where
 ε   : Env ε
 _▸_ : ∀ {Γ τ} → Env Γ → ⟪ τ ⟫ → Env (Γ ▸ τ)

lookup : ∀ {Γ τ} → Γ ∋ τ → Env Γ → ⟪ τ ⟫
lookup vz     (ρ ▸ v) = v
lookup (vs x) (ρ ▸ v) = lookup x ρ

-- Terms (deBruijn) to interpreted Terms
⟦_⟧ : ∀ {Γ τ} → Γ ⊢ τ → Env Γ → ⟪ τ ⟫
⟦ t       ⟧ ρ = tt
⟦ var x   ⟧ ρ = lookup x ρ
⟦ e₁ · e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ (⟦ e₂ ⟧ ρ)
⟦ ƛ e     ⟧ ρ = λ x → ⟦ e ⟧ (ρ ▸ x)

-- The identity function on unit in deBruijn representation
id : ε ⊢ unit ⇒ unit
id = ƛ var vz

id′ : ⟪ unit ⇒ unit ⟫
id′ = ⟦ id ⟧ ε

foo : ε ⊢ unit
foo = (ƛ var vz) · t

-- evaluating this in agda-mode yields tt
foo′ : ⟪ unit ⟫
foo′ = ⟦ foo ⟧ ε