This is lifted from McBride’s W-types: good news and bad news. See the link in the footnote to follow along. Probably as I make progress I’ll update here. But also maybe not.
data Bool : Set where
true : Bool
false : Bool
data W (S : Set) (P : S → Set) : Set where
_◂_ : (s : S) (f : P s → W S P) → W S P
natf : Bool → Set
natf true = ⊤
natf false = ⊥
ℕ : Set
ℕ = W Bool natf
zero : ℕ
zero = false ◂ λ ()
succ : ℕ → ℕ
succ n = true ◂ (λ _ → n)Turns out this probably isn’t possible. I didn’t take it as far as McBride did, but I think his conclusion is relevant here:
W-types are a powerful conceptual tool, but they’re no basis for an implementation of recursive datatypes in decidable type theories. To encode a first-order structure by a function space is to throw away canonical choice of representation. When you care about what things are (because they show up in types), not just what they do (when you run them), that price isn’t worth paying.
(emphasis mine)
_+_ : ℕ → ℕ → ℕ
(false ◂ _) + m = m
(t ◂ f) + m = succ (n + m)
where
n = f {!!}