(Deep) Induction Rules for GADTs

Introduction

Rose trees.

Rose(A) ≡ μX. 1 + A × List(X)∀ (A : 𝒰) (P : Rose A → 𝒰) → P(empty) → (∀(a : A) (ts : List(Rose(A))) → P(node(a)(ts))) → ∀(x : Rose(A)) → P(x)∀ (A : 𝒰) (P : Rose A → 𝒰) (Q : A → 𝒰) → P empty → (∀ (a : A) (ts : List (Rose A)) → Q a → List∧(Rose A) P ts → P (node a ts)) → ∀ (x : Rose A) → Rose∧ A Q x → P xSeq : 𝒰 → 𝒰 ≡ μX. const : A → Seq(A) pair : Seq(A) → Seq(B) → Seq (A × B)

Deep Induction for ADTs and Nested Types

∀(A : 𝒰) (P : List(A) → 𝒰) → P(nil) → ∀(a : A) (as : List(A)) → P(as) → P (cons a as) → ∀(as : List(A)) → P a∀(A : 𝒰) (P : List(A) → 𝒰) (Q : A → 𝒰) → P(nil) → ∀(a : A) (as : List(A)) → Q a → P(as) → P (cons a as) → ∀(as : List(A)) → List∧ A Q as → Pdata PTree : 𝒰 → 𝒰 where pleaf : A → PTree(A) pnode : PTree(A × A) → PTree∀(P : ∀(A : 𝒰) → PTree(A) → 𝒰) → ∀(A : 𝒰) (a : A) → P A (pleaf a) → ∀(A : 𝒰) (pp : PTree (A × A)) → P(A × A) pp → P A (pnode pp) → ∀(A : 𝒰) (p : PTree(A)) → Pdata Bush : 𝒰 → 𝒰 where bnil : Bush(A) bcons : A → Bush (Bush(A)) → Bush(A)Bush∧ : ∀(A : 𝒰) → (A → 𝒰) → Bush(A) → 𝒰Bush∧ A Q bnil = ⊤ Bush∧ A Q (bcons a bb) = Q a × Bush∧ (Bush(A)) (Bush∧ A Q) A Q

(Deep) GADTs

Figure 1. Deep induction rules for perfect trees and bushes

data Equal : 𝒰 → 𝒰 → 𝒰 where refl : ∀❴A : 𝒰❵ → Equal A Adata Seq : 𝒰 → 𝒰 where const : ∀❴A : 𝒰❵ → A → Seq(A) pair : ∀❴A : 𝒰❵ → ∀(B, C : 𝒰) → Equal(A)(B × C) → Seq(B) → Seq(C) → Seq(A)

(Deep) Induction for GADTs

(Deep) Induction for Equal

Figure 2. The LType and LTerm data types

(Deep) Induction for Seq

Figure 3. Deep induction rule for Seq

(Deep) Induction for LTerm

The General Framework

Truly Nested GADTs Need Not Admit Deep Induction Rules

data G : 𝒰 → 𝒰 where c : ∀❴A : 𝒰❵ → G (G A) → G (A × A)

Case Study: Extracting Types of Lambda Terms

GetType : ∀ (A : 𝒰) → LTerm A → 𝒰 GetType A t = Maybe (LType A)

Conclusion