Notes on W Types and Inductive Types

03 Apr 2022 • Type Theory

Table of Contents

Well-Founded Trees

data W (A : 𝒰) (B : A β†’ 𝒰) : 𝒰 where
  sup : βˆ€ a β†’ (B a β†’ W A B) β†’ W A B

A selects the constructor as well as providing the constructor’s nonrecursive arguments. B then selects the recursive element as well as providing the recursive element’s arguments.

Example: Ordinals with a twist

data Ord (A : 𝒰) : 𝒰 where
  Z : A β†’ Ord A
  S : Ord A β†’ Ord A
  L : (β„• β†’ Ord A) β†’ Ord A

Ord A = W (A + πŸ™ + πŸ™) B
  where
  B (in1 a) = 𝟘
  B (in2 βˆ—) = πŸ™
  B (in3 βˆ—) = β„•
Z a = sup (in1 a) absurd
S o = sup (in2 βˆ—) (Ξ» _ β†’ o)
L f = sup (in3 βˆ—) f

Indexed Well-Founded Trees

data IW (I : 𝒰)
        (A : I β†’ 𝒰)
        (B : βˆ€ i β†’ A i β†’ 𝒰)
        (d : βˆ€ i β†’ (a : A i) β†’ B i a β†’ I) :
        I β†’ 𝒰 where
  isup : βˆ€ i β†’ (a : A i) β†’
         ((b : B i a) β†’ IW I A B d (d i a b)) β†’
         IW I A B d i

The indexed W type can be seen as either encoding an inductive type with nonuniform parameters or as encoding mutual inductive types, which are indexed inductive types anyway. I selects the nonuniform parameters, which I’ll call the index for now A selects the constructor, B selects the recursive element, and d returns the index of that recursive element.

Example: Mutual inductives β€” even and odd naturals

data Even : 𝒰 where
  Z : Even
  Sβ‚‘ : Odd β†’ Even
data Odd : 𝒰 where
  Sβ‚’ : Even β†’ Odd

EvenOdd = IW 𝟚 A B d
  where
  Even = in1 βˆ—
  Odd  = in2 βˆ—
  A Even = 𝟚  -- Even has two constructors
  A Odd  = πŸ™  -- Odd  has one constructor
  B Even (in1 βˆ—) = 𝟘  -- Z  has no  recursive elements
  B Even (in2 βˆ—) = πŸ™  -- Sβ‚‘ has one recursive element
  B Odd  βˆ— = πŸ™        -- Sβ‚’ has one recursive element
  d Even (in1 βˆ—) = absurd
  d Even (in2 βˆ—) βˆ— = Odd
  d Odd  βˆ—       βˆ— = Even
Z = isup Even (in1 βˆ—) absurd
Sβ‚‘ o = isup Even (in2 βˆ—) (Ξ» _ β†’ o)
Sβ‚’ e = isup Odd βˆ— (Ξ» _ β†’ e)

Example: Nonuniformly parametrized inductive β€” accessibility predicate

variable
  T : 𝒰
  _<_ : T β†’ T β†’ 𝒰

data Acc (t : T) : 𝒰 where
  acc : (βˆ€ s β†’ s < t β†’ Acc s) β†’ Acc t

Acc t = IW T (Ξ» _ β†’ πŸ™) (Ξ» t βˆ— β†’ βˆƒ[ s ] s < t) (Ξ» t βˆ— (s , _) β†’ s) t

Example: Nonuniformly parametrized inductive β€” perfect trees

data PTree (A : 𝒰) : 𝒰 where
  leaf : A β†’ PTree A
  node : PTree (A Γ— A) β†’ PTree A

PTree = IW 𝒰 (Ξ» A β†’ A + πŸ™) B d
  where
  B A (in1 a) = 𝟘
  B A (in2 βˆ—) = πŸ™
  d A (in1 a) = absurd
  d A (in2 βˆ—) βˆ— = A Γ— A
leaf A a = isup A (in1 a) absurd
node A t = isup A (in2 βˆ—) (Ξ» _ β†’ t)

Indexed Inductives and Fording

So far, (nonuniformly) parametrized inductives and mutual inductives can be encoded. Indexed inductives can be encoded as well by first going through a round of fording to turn them into nonuniformly parametrized inductives. Meanwhile, mutual inductives can also be represented as nonuniform parametrized inductives by first turning them into indexed inductives.

Example: Function images

variable
  A B : 𝒰

data Image (f : A β†’ B) : B β†’ 𝒰 where
  image : βˆ€ x β†’ Image f (f x)

-- Forded image type
data Image' (f : A β†’ B) (b : B) : 𝒰 where
  image' : βˆ€ x β†’ b ≑ f x β†’ Image f b

Image' f b = W (βˆƒ[ x ] b ≑ f x) 𝟘
image' x p = sup (x , p) absurd

Example: The finite sets

data Fin : β„• β†’ 𝒰 where
  FZ : βˆ€ n β†’ Fin (S n)
  FS : βˆ€ n β†’ Fin n β†’ Fin (S n)

-- Forded finite sets type
data Fin' (m : β„•) : 𝒰 where
  FZ' : βˆ€ n β†’ m ≑ S n β†’ Fin m
  FS' : βˆ€ n β†’ m ≑ S n β†’ Fin n β†’ Fin m

Fin' = IW β„• (Ξ» m β†’ 𝟚 Γ— βˆƒ[ n ] m ≑ S n) B d
  where
  B m (in1 βˆ— , n , p) = 𝟘
  B m (in2 βˆ— , n , p) = πŸ™
  d m (in1 βˆ— , n , p) = absurd
  d m (in2 βˆ— , n , p) βˆ— = n
FZ' m n p     = isup m (in1 βˆ— , n , p) absurd
FS' m n p fin = isup m (in2 βˆ— , n , p) (Ξ» _ β†’ fin)

Nested Inductives

Nested inductive types, when represented as recursive ΞΌ types, have nested type binders. Nonindexed inductive types potentially with nonuniform parameters, on the other hand, are single ΞΌ types.

Ord A = ΞΌX: 𝒰. A + X + (β„• β†’ X)
EvenOdd = ΞΌX: 𝟚 β†’ 𝒰. Ξ» { in1 βˆ— β†’ πŸ™ + X (in2 βˆ—) ; in2 βˆ— β†’ X (in1 βˆ—) }
Acc = ΞΌX: T β†’ 𝒰. Ξ» t β†’ βˆ€ s β†’ s < t β†’ X s
PTree = ΞΌX: 𝒰 β†’ 𝒰. Ξ» A β†’ A + X (A Γ— A)
Fin' m = ΞΌX: β„• β†’ 𝒰. (βˆƒ[ n ] m ≑ S n) + (βˆƒ[ n ] (m ≑ S n) Γ— X n)

Nested inductives, when not nested within themselves, can be defunctionalized into indexed inductives, which can then be forded into nonuniformly parametrized inductives, which can finally be encoded as indexed W types.

Example: Finitely-branching trees

data FTree : 𝒰 where
  ftree : List FTree β†’ FTree

FTree = ΞΌX: 𝒰. List X = ΞΌX: 𝒰. ΞΌY: 𝒰. πŸ™ + X Γ— Y

data I : 𝒰 where
  Tree : I
  List : I β†’ I

data Eval : I β†’ 𝒰 where
  nil : Eval (List Tree)
  cons : Eval Tree β†’ Eval (List Tree) β†’ Eval (List Tree)
  ftree : Eval (List Tree) β†’ Eval Tree

data Eval' (i : I) : 𝒰 where
  nil'  : i ≑ List Tree β†’ Eval' i
  cons' : i ≑ List Tree β†’ Eval' Tree β†’ Eval' (List Tree) β†’ Eval' i
  ftree : i ≑ Tree β†’ Eval' (List Tree) β†’ Eval' i

Eval' = IW I A B d
  where
  A i = i ≑ List Tree + i ≑ List Tree + i ≑ Tree
  B _ (in1 _) = 𝟘
  B _ (in2 _) = 𝟚
  B _ (in3 _) = πŸ™
  d _ (in1 _) = absurd
  d _ (in2 _) (in1 βˆ—) = Tree
  d _ (in2 _) (in2 βˆ—) = List Tree
  d _ (in3 _) βˆ— = List Tree

Non-example: Truly nested inductive β€” bushes

It’s unclear how this might be encoded either as indexed inductives or as an indexed W type.

data Bush (A : 𝒰) : 𝒰 where
  bnil : Bush A
  bcons : A β†’ Bush (Bush A) β†’ Bush A

Bush = ΞΌX: 𝒰 β†’ 𝒰. Ξ» A β†’ πŸ™ + A Γ— X (X A)

Inductive–Inductives

While mutual inductives allow the types of constructors of multiple inductives to refer to one another, inductive–inductives further allow one inductive to be a parameter or index of another.

data A : 𝒰 where
  …
data B : A β†’ 𝒰 where
  …

Example: Intrinsically well-formed contexts and types

That is, the entries of a context must be well formed under the correct context, while the context under which types are well formed must themselves be well formed.

data Ctxt : 𝒰 where
  Β· : Ctxt
  _∷_ : βˆ€ Ξ“ β†’ Type Ξ“ β†’ Ctxt

data Type : Ctxt β†’ 𝒰 where
  U : βˆ€ Ξ“ β†’ Type Ξ“
  Var : βˆ€ Ξ“ β†’ Type (Ξ“ ∷ U Ξ“)
  Pi : βˆ€ Ξ“ β†’ (A : Type Ξ“) β†’ Type (Ξ“ ∷ A) β†’ Type Ξ“

To encode this inductive–inductive type, it’s split into two mutual inductives: an β€œerased” one with the type interdependency removed (i.e. Type' does not have a Ctxt' parameter), and one describing the relationship between the two.

data Ctxt' : 𝒰 where
  Β· : Ctxt'
  _∷_ : Ctxt β†’ Type β†’ Ctxt

data Type' : 𝒰 where
  U : Ctxt' β†’ Type'
  Var : Ctxt' β†’ Type'
  Pi : Ctxt' β†’ Type' β†’ Type' β†’ Type'

data Ctxt-wf : Ctxt' β†’ 𝒰 where
  Β·-wf : Ctxt-wf Β·
  ∷-wf : βˆ€ {Ξ“} {A} β†’ Ctxt-wf Ξ“ β†’ Type-wf Ξ“ A β†’ Ctxt-wf (Ξ“ ∷ A)

data Type-wf : Ctxt' β†’ Type' β†’ 𝒰 where
  U-wf : βˆ€ {Ξ“} β†’ Ctxt-wf Ξ“ β†’ Type-wf Ξ“ (U Ξ“)
  Var-wf : βˆ€ {Ξ“} β†’ Ctxt-wf Ξ“ β†’ Type-wf (Ξ“ ∷ U Ξ“) (Var Ξ“)
  Pi-wf : βˆ€ {Ξ“} {A B} β†’ Ctxt-wf Ξ“ β†’ Type-wf Ξ“ A β†’
          Type-wf (Ξ“ ∷ A) B β†’ Type-wf Ξ“ (Pi Ξ“ A B)

In other words, Ctxt' and Type' describe the syntax, while Ctxt-wf and Type-wf describe the well-formedness rules.

Ξ“ β©΄ Β· | Ξ“ ∷ A            (Ctxt')
A, B β©΄ U | Var | Ξ  A B   (Type' with Ctxt' argument omitted)

─── Β·-wf
⊒ ·

⊒ Ξ“  Ξ“ ⊒ A
────────── ∷-wf
⊒ Ξ“ ∷ A

⊒ Ξ“
────────── U-wf
Ξ“ ⊒ U type

⊒ Ξ“
──────────────── Var-wf
Ξ“ ∷ U ⊒ Var type

⊒ Ξ“  Ξ“ ⊒ A  Ξ“ ∷ A ⊒ B
───────────────────── Pi-wf
Ξ“ ⊒ Ξ  A B type

The final encoding of a context or a type is then the erased type paired with its well-formedness.

Ctxt = Ξ£[ Ξ“ ∈ Ctxt' ] Ctxt-wf Ξ“
Type (Ξ“ , Ξ“-wf) = Ξ£[ A ∈ Type' ] Type-wf Ξ“ A

Β· = Β· , Β·-wf
(Ξ“ , Ξ“-wf) ∷ (A , A-wf) = Ξ“ ∷ A , ∷-wf Ξ“-wf A-wf
U (Ξ“ , Ξ“-wf) = U Ξ“ , U-wf Ξ“-wf
Var (Ξ“ , Ξ“-wf) = Var Ξ“ , Var-wf Ξ“-wf
Pi (Ξ“ , Ξ“-wf) (A , A-wf) (B , B-wf) = Pi Ξ“ A B , Pi-wf Ξ“-wf A-wf B-wf

These indexed mutual inductives can then be transformed into a single indexed inductive with an additional index, then into a nonuniformly parametrized inductive, and finally into an indexed W type. The same technique can be applied to generalized inductive–inductives, e.g. β€œinfinitary” Pi.

data Type' : 𝒰 where
  …
  Pi∞ : Ctxt' β†’ (β„• β†’ Type') β†’ Type'

data Type-wf : Ctxt' β†’ Type' β†’ 𝒰 where
  …
  Pi∞-wf : βˆ€ {Ξ“} {T : β„• β†’ Type'} β†’ Ctxt-wf Ξ“ β†’
          (βˆ€ n β†’ Type-wf Ξ“ (T n)) β†’ Type-wf Ξ“ (Pi∞ Ξ“ T)

Pi∞ (Ξ“ , Ξ“-wf) TT-wf = Pi∞ Ξ“ (fst ∘ TT-wf) , Pi∞-wf Ξ“-wf (snd ∘ TT-wf)

Inductive–Recursives

You can’t encode these as W types apparently.

Indexed Well-Founded Trees as Canonized Well-Founded Trees

This section is lifted from Dan Doel’s encoding of indexed W types as W types following the canonical construction from Why Not W? by Jasper Hugunin.

An indexed W type can be encoded as an unindexed one by first storing the index together with the A type as in IW' below. Then, define the canonical predicate to assert that, given some index selector d as would be found in an indexed well-founded tree, not only is the current index the one we expect, but the index of all recursive elements are the ones dictated by d. That is, f b gives the actual recursive element from which we can extract the index, while d i a b gives the expected index, and we again assert their equality. Finally, an encoded indexed W type EIW is a IW' type such that the index is canonical.

variable
  I : 𝒰
  A : I β†’ 𝒰
  B : βˆ€ i β†’ A i β†’ 𝒰
  d : βˆ€ i β†’ (a : A i) β†’ B i a β†’ I

IW' (I : 𝒰) β†’
    (A : I β†’ 𝒰) β†’
    (B : βˆ€ i β†’ A i β†’ 𝒰) β†’ 𝒰
IW' I A B = W (βˆƒ[ i ] A i) (Ξ» (i , a) β†’ B i a)

canonical : (βˆ€ i β†’ (a : A i) β†’ B i a β†’ I) β†’ IW' I A B β†’ I β†’ 𝒰
canonical d (sup (i , a) f) i' = (i ≑ i') Γ— (βˆ€ b β†’ canonical d (f b) (d i a b))

EIW : (I : 𝒰) β†’
      (A : I β†’ 𝒰) β†’
      (B : βˆ€ i β†’ A i β†’ 𝒰) β†’
      (d : βˆ€ i β†’ (a : A i) β†’ B i a β†’ I) β†’ I β†’ 𝒰
EIW I A B d i = Σ[ w ∈ IW' I A B ] (canonical d w i)

isup : (i : I) β†’ (a : A i) β†’ ((b : B i a) β†’ EIW I A B d (d i a b)) β†’ EIW I A B d i
isup i a f = sup (i , a) (fst ∘ f) , refl i , (snd ∘ f)
 W type  well-founded trees  inductive types  type theory