# Notes on W Types and Inductive Types

## 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)
``````