Parametricity for Nested Types and GADTs

Introduction

List

List(A) ≡ μX. 1 + A × X.λA. A → (A → A → A) → A.

PTree

data PTree (A : Set) : Set where pleaf A : X pnode PTree (A × A) : XH(F)(A) ≡ (A → F(A)) → (F(A × A) → F(A)) → F(A).PTree(A) ≡ (μφ. λX. X + φ (X × X)) A, PTree(A) ≡ μX. A + A × A, λF.(λA. A → F(A)) → (λA. F(A × A) → F(A)) → λA. F(A).

PForest

PForest(A) ≡ μX. 1 + A × PTree(X).

Bush

data Bush (A : Set) : Set where bnil : X bcons A, Bush (Bush A) : XBush(A) = (μφ. λX. 1 + X × φ (φX)) A. Bush(A) = μX. 1 + A × φ (X).

The Calculus

Interpreting Types

The Identity Extension Lemma

Naturality and the Abstraction Theorem

Parametricity for GADTs

Conclusion and Directions for Future Work