Reference on standard types

This question is about what I presume is a basic construction in type theory.

The finite types are defined as follows: 0 is a finite type; if $\sigma, \tau$ are finite types, then so is $\sigma\rightarrow \tau$; and the set of finite types is the smallest set satisfying those two properties. The interpretation of these types which I am currently using is: objects of type 0 are natural numbers, and objects of type $\sigma\rightarrow\tau$ are funtions from the set of objects of type $\sigma$ to the set of objects of type $\tau$.

Now, amongst the finite types are the so-called standard types: $0$, $0\rightarrow 0$, $(0\rightarrow 0)\rightarrow 0$, etc. These are identified with natural numbers: $0\rightarrow 0$ is abbreviated by 1, and $n\rightarrow 0$ is abbreviated by $n+1$. Given a finite type $\sigma$, we can associate to $\sigma$ a standard type, the height of $\sigma$, given by $$ht(0)=0, ht(\sigma\rightarrow \tau)=\max\{ht(\sigma)+1, ht(\tau)\}.$$

Now intuitively, it is clear that, "morally speaking," all objects can be represented by objects of standard type. For example, given an object $F$ of type $0\rightarrow 1$, we can represent $F$ by the type-1 functional $$ G: \langle x, y\rangle\mapsto Fxy,$$ where $\langle\cdot,\cdot\rangle$ is your favorite pairing function on $\mathbb{N}$. Now, inductively we can carry this out through all the finite types, in a somewhat-messy-to-write-out but still fairly natural way: to each object $F$ of type $\sigma$ we associate an object $st(F)$ of type $ht(\sigma)$ in such a way that $F$ can be "recovered" from $st(F)$ and $\sigma$. (Morally, that recovered ought to mean something like "recovered computably.")

My question is the following: I've seen this alluded to in a number of sources, but I've never seen it worked out in detail. I've written out a procedure for encoding arbitrary objects of finite type by standard-type objects, but it's long and messy, I'm sure it can be made shorter, and I'm not totally certain it's correct; moreover, I'd like to see how it's been done in the past. So my question is:

Can someone recommend for me a source where this encoding is written out explicitly?

Solution 1:

This seemed like a fun exercise in formal verification, so here’s a verified implementation in Agda. encode converts an object to standard type, decode recovers the original object, and decode-encode witnesses that you always get back the same object.

import Level
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality

-- Assume functional extensionality

postulate ext : Extensionality Level.zero Level.zero

-- Assume we have a pairing function (exercise for the reader)

postulate pair : ℕ × ℕ → ℕ
postulate unpair : ℕ → ℕ × ℕ
postulate unpair-pair : ∀ p → unpair (pair p) ≡ p

-- Definitions

data ty : Set where
  N : ty
  _⇒_ : ty → ty → ty

tySet : ty → Set
tySet N = ℕ
tySet (σ ⇒ τ) = tySet σ → tySet τ

ht : ty → ℕ
ht N = 0
ht (σ ⇒ τ) = suc (pred (ht τ) ⊔ ht σ)

natSet : ℕ → Set
natSet 0 = ℕ
natSet (suc n) = natSet n → ℕ

-- Implementation

dummy : ∀ n → natSet n
dummy zero = 0
dummy (suc _) _ = 0

combine : (n₁ n₂ : ℕ) → natSet n₁ × natSet n₂ → natSet (n₂ ⊔ n₁)
separate : (n₁ n₂ : ℕ) → natSet (n₂ ⊔ n₁) → natSet n₁ × natSet n₂

combine zero zero = pair
combine zero (suc n₂) (f₁ , f₂) g₂ = pair (f₁ , f₂ g₂)
combine (suc n₁) zero (f₁ , f₂) g₁ = pair (f₁ g₁ , f₂)
combine (suc n₁) (suc n₂) (f₁ , f₂) g with separate n₁ n₂ g
... | g₁ , g₂ = pair (f₁ g₁ , f₂ g₂)
separate zero zero = unpair
separate zero (suc n₂) f = proj₁ (unpair (f (dummy n₂))) , proj₂ ∘ unpair ∘ f
separate (suc n₁) zero f = proj₁ ∘ unpair ∘ f , proj₂ (unpair (f (dummy n₁)))
separate (suc n₁) (suc n₂) f =
  proj₁ ∘ unpair ∘ f ∘ combine n₁ n₂ ∘ (_, dummy n₂) ,
  proj₂ ∘ unpair ∘ f ∘ combine n₁ n₂ ∘ (dummy n₁ ,_)

encode : (σ : ty) → tySet σ → natSet (ht σ)
decode : (σ : ty) → natSet (ht σ) → tySet σ

encode N n = n
encode (σ ⇒ N) f g = f (decode σ g)
encode (σ ⇒ (τ ⇒ φ)) f g with separate (ht σ) (pred (ht φ) ⊔ ht τ) g
... | g₁ , g₂ = encode (τ ⇒ φ) (f (decode σ g₁)) g₂
decode N n = n
decode (σ ⇒ N) f g = f (encode σ g)
decode (σ ⇒ (τ ⇒ φ)) f g =
  decode (τ ⇒ φ) (f ∘ combine (ht σ) (pred (ht φ) ⊔ ht τ) ∘ (encode σ g ,_))

-- Proof

separate-combine : ∀ n₁ n₂ p → separate n₁ n₂ (combine n₁ n₂ p) ≡ p
separate-combine₁ : ∀ n₁ n₂ f₁ f₂ g₁ →
  proj₁ (separate (suc n₁) n₂ (combine (suc n₁) n₂ (f₁ , f₂))) g₁ ≡ f₁ g₁
separate-combine₂ : ∀ n₁ n₂ f₁ f₂ g₂ →
  proj₂ (separate n₁ (suc n₂) (combine n₁ (suc n₂) (f₁ , f₂))) g₂ ≡ f₂ g₂

separate-combine zero zero = unpair-pair
separate-combine zero (suc n₂) (f₁ , f₂)
  rewrite unpair-pair (f₁ , f₂ (dummy n₂)) | ext (separate-combine₂ zero n₂ f₁ f₂) = refl
separate-combine (suc n₁) zero (f₁ , f₂)
  rewrite ext (separate-combine₁ n₁ zero f₁ f₂) | unpair-pair (f₁ (dummy n₁) , f₂) = refl
separate-combine (suc n₁) (suc n₂) (f₁ , f₂)
  rewrite ext (separate-combine₁ n₁ (suc n₂) f₁ f₂) | ext (separate-combine₂ (suc n₁) n₂ f₁ f₂)
  = refl
separate-combine₁ n₁ zero f₁ f₂ g₁
  rewrite unpair-pair (f₁ g₁ , f₂) = refl
separate-combine₁ n₁ (suc n₂) f₁ f₂ g₁
  rewrite separate-combine n₁ n₂ (g₁ , dummy n₂) | unpair-pair (f₁ g₁ , f₂ (dummy n₂)) = refl
separate-combine₂ zero n₂ f₁ f₂ g₂
  rewrite unpair-pair (f₁ , f₂ g₂) = refl
separate-combine₂ (suc n₁) n₂ f₁ f₂ g₂
  rewrite separate-combine n₁ n₂ (dummy n₁ , g₂) | unpair-pair (f₁ (dummy n₁) , f₂ g₂) = refl

decode-encode : ∀ σ f → decode σ (encode σ f) ≡ f
decode-encode⇒ : ∀ σ τ f g → decode (σ ⇒ τ) (encode (σ ⇒ τ) f) g ≡ f g
encode-combine : ∀ σ τ φ f g h →
  encode (σ ⇒ (τ ⇒ φ)) f (combine (ht σ) (pred (ht φ) ⊔ ht τ) (encode σ g , h)) ≡
  encode (τ ⇒ φ) (f g) h

decode-encode N i = refl
decode-encode (σ ⇒ τ) f = ext (decode-encode⇒ σ τ f)
decode-encode⇒ σ N f g
  rewrite decode-encode σ g = refl
decode-encode⇒ σ (τ ⇒ φ) f g
  rewrite ext (encode-combine σ τ φ f g) = decode-encode (τ ⇒ φ) (f g)
encode-combine σ τ φ f g h
  rewrite separate-combine (ht σ) (pred (ht φ) ⊔ ht τ) (encode σ g , h) | decode-encode σ g
  = refl