parametric higher-order abstract syntax
A variant of higher-order abstract syntax. It has some advantages over “regular” HOAS.
- It only uses strictly positive datatypes, so it can be encoded in proof assistants.
- It can rule out exotic terms via parametricity.
We demonstrate how to use PHOAS to encode the simply-typed lambda calculus in Agda. First, we define a universe of types.
data Ty : Set where
_⟶_ : Ty → Ty → Ty
variable
a b : Ty
Now we define the syntax of terms. In “regular” HOAS, a term with a free variable is represented by a function from terms to terms. In PHOAS, we parameterize terms by a variable representation; i.e., a function rep of type Ty → Set. Then a variable of (object language) type a is represented by a value of (metalanguage) type rep a, and a term of (object language) type b with a free variable of (object language) type a is represented by a function of (metalanguage) type rep a → Tm b.
module _ (rep : Ty → Set) where
data Tm : Ty → Set where
` : rep a → Tm a
ƛ : (rep a → Tm b) → Tm (a ⟶ b)
_$_ : Tm (a ⟶ b) → Tm a → Tm b
Finally, “proper” terms can be identified as terms that are valid for all possible variable representations.
Term : Ty → Set
Term a = ∀ {rep} → Tm rep a
Due to parametricity, a value of type Term a cannot “know” anything about the way variables are represented, so they are essentially uninterpreted symbols.
Ty⟦_⟧ : Ty → Set
Ty⟦ a ⟶ b ⟧ = Ty⟦ a ⟧ → Ty⟦ b ⟧
Tm⟦_⟧ : Tm Ty⟦_⟧ a → Ty⟦ a ⟧
Tm⟦ ` x ⟧ = x
Tm⟦ ƛ f ⟧ = λ x → Tm⟦ f x ⟧
Tm⟦ t₁ $ t₂ ⟧ = Tm⟦ t₁ ⟧ Tm⟦ t₂ ⟧
1. in Haskell
PHOAS is harder to encode in Haskell than in a proof assistant.
Representing the syntax of types and terms is straightforward.
{-# LANGUAGE DataKinds, GADTs, TypeFamilies #-}
import Data.Kind
data Ty :: Type = (:->) Ty Ty
data Tm (rep :: Ty -> Type) :: Ty -> Type where
Var :: rep a -> Tm rep a
Abs :: (rep a -> Tm rep b) -> Tm rep (a :-> b)
App :: Tm rep (a :-> b) -> Tm rep a -> Tm rep b
From here, it would be natural to implement the type interpretation function (Ty⟦_⟧ above) as a type family. And, indeed, we can do this.
type family BadEval (a :: Ty) where
BadEval (a :-> b) = BadEval a -> BadEval b
Now we want to write eval :: Tm BadEval a -> BadEval a. The problem is that Haskell doesn't allow type synonyms to be partially applied, so we can't even write this type down. Therefore, we instead need to encode the type interpretation function as a datatype.
data Eval :: Ty -> Type where
EvalArr :: (Eval a -> Eval b) -> Eval (a :-> b)
Then the evaluation function produces values of type Eval.
eval :: Tm Eval a -> Eval a
eval (Var x) = x
eval (Abs f) = EvalArr (\x -> eval (f x))
eval (App t1 t2) = case eval t1 of
EvalArr f -> f (eval t2)