Phoas in Agda. (Coq version http://adam.chlipala.net/cpdt/html/Hoas.html)

Phoas.agda

module PhoasEx where
data One : Set where
     one : One
        
data type : Set where
     Nat Unit : type
     _⇒_ : type -> type -> type
     
Value : type -> Set
Value Nat = ℕ
Value Unit = One
Value (n ⇒ m) = Value n -> Value m

module Phoas (var : type -> Set) where
     data exp : type -> Set where
          Var : ∀ {t : type} → (var t → exp t )
          Const : ℕ -> exp Nat
          _●_ : ∀ {dom ran} → exp (dom ⇒ ran) → exp dom → exp ran
          Abs : ∀ {dom ran} → (var dom → exp ran) → exp (dom ⇒ ran)     

module Ex1 where
     -- interpret the types into Agda types
     open Phoas Value

     id : exp (Nat ⇒ Nat)
     id = Abs λ (n : ℕ) → Var n

     n : exp Nat
     n = Const' 7

     ex : exp Nat
     ex = id ● n

     eval : {ty : type} → exp ty → Value ty
     eval (Var x) = x
     eval (Const x) = x
     eval (e ● e₁) = (eval e) (eval e₁)
     eval (Abs x) = λ z → eval (x z)
          
     _ : eval ((Abs λ (n : ℕ) → Var n) ● Const 7) ≡ (λ (n : ℕ) → n) 7
     _ = refl

module Ex2 where
     open Phoas (λ _ → One)
     
     countVars : {A : type} → exp A → ℕ
     countVars (Var x) = 1
     countVars (Const x) = 0
     countVars (x ● x₁) = Data.Nat._+_ (countVars x) (countVars x₁)
     countVars (Abs x) = countVars (x one) -- here is where we use the interpretation, 
                                               -- provide the constructor of type One