Dingle Dangle. We can piggy-back onto Agda's built-in normalization by providing an interpreter of terms in our syntax into Agda terms. It would be nice to include our own real normalizer in the future, but the point right now is to demonstrate that heads (such as `◎`) can do interesting things to compute trees.

gistfile1.hs

module dingle where
  open import Data.String using (String)
  open import Relation.Binary.PropositionalEquality using (_≡_; refl)

  module Theory (rep : Set) where

    infixr 0 _⇒_
    data * : Set where
      ⟨_⟩ : rep → *
      _⇒_ : * → * → *

    data Cx : Set where
      E : Cx
      _,_ : Cx → * → Cx

    infixr 0 _⊢_
    infixr 0 _∋_
      
    data _∋_ : Cx → * → Set where
      top : ∀ {Γ τ} → Γ , τ ∋ τ
      pop : ∀ {Γ σ τ} → Γ ∋ τ → Γ , σ ∋ τ
          
    infixl 70 _%_
    infix  70 !_ 
    infixr 70 _>>_
     
    data _⊢_ (Γ : Cx) : * → Set where
      var : {τ : *} → Γ ∋ τ → Γ ⊢ τ
      ƛ_ : {σ τ : *} → Γ , σ ⊢ τ → Γ ⊢ σ ⇒ τ
      _%_ : {σ τ : *} → Γ ⊢ σ ⇒ τ → Γ ⊢ σ → Γ ⊢ τ
      
      !_ : {φ : rep} → String → Γ ⊢ ⟨ φ ⟩
      _>>_ : {φ ψ : rep} → Γ ⊢ ⟨ φ ⟩ → Γ ⊢ ⟨ ψ ⟩ → Γ ⊢ ⟨ φ ⟩
      
    data Tree : Set where
      !_ : String → Tree
      _>>_ : Tree → Tree → Tree
      
    ⟦_⟧* : * → Set
    ⟦ ⟨ x ⟩ ⟧* = Tree
    ⟦ σ ⇒ τ ⟧* = ⟦ σ ⟧* → ⟦ τ ⟧*


    data Env : Cx → Set where
      E : Env E
      _,_ : ∀ {Γ τ} → Env Γ → ⟦ τ ⟧* → Env (Γ , τ)
      
    ⟦_⟧_ : ∀ {Γ τ} → Γ ⊢ τ → Env Γ → ⟦ τ ⟧*
    ⟦ var top ⟧ (_ , x) = x
    ⟦ var (pop i) ⟧ (γ , _) = ⟦ var i ⟧ γ
    ⟦ ƛ t ⟧ γ = λ z → ⟦ t ⟧ (γ , z)
    ⟦ t % t₁ ⟧ γ = (⟦ t ⟧ γ) (⟦ t₁ ⟧ γ)
    ⟦ ! x ⟧ γ = ! x
    ⟦ t >> t₁ ⟧ γ = (⟦ t ⟧ γ) >> (⟦ t₁ ⟧ γ)

  data cat : Set where
    N D V P : cat
  
  open Theory cat

  eis : E ⊢ ⟨ D ⟩ ⇒ ⟨ P ⟩
  eis = ƛ !"εἰς" >> var top

  tosouton : E ⊢ ⟨ N ⟩ ⇒ ⟨ D ⟩
  tosouton = ƛ !"τοσοῦτον" >> var top

  eleutherias : E ⊢ ⟨ N ⟩
  eleutherias = !"ἐλευθερίας"

  hkomen : E ⊢ ⟨ P ⟩ ⇒ ⟨ V ⟩
  hkomen = ƛ !"ἥκομεν" >> var top

  -- The function composition combinator head
  ◎ : ∀ {A B C} → E ⊢ (B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C)
  ◎ = ƛ ƛ ƛ var (pop (pop top)) % (var (pop top) % var top)

  -- Whilst syntactically ex₁ and ex₂ differ, they both evaluate to
  -- the same normal form. Such differences may be used to generate
  -- various surface word orders.
  ex₁ ex₂ : E ⊢ ⟨ V ⟩
  ex₁ = hkomen % (eis % (tosouton % eleutherias))
  ex₂ = hkomen % (◎ % eis % tosouton % eleutherias)

  spec : ⟦ ex₁ ⟧ E ≡ ⟦ ex₂ ⟧ E
  spec = refl