Peter's early work on parametricity, and why it still matters to me
summary
Argues that Peter H.'s categorical account of relational parametricity (using reflexive graphs and naturality) gives a formal semantics that validates surprising equivalences of local-state code — e.g., two implementations of a counter whose increments and reads are sign-flipped are observationally equal under the parametricity relation. Applies that framework to deep learning's fixed-input-dimension problem by treating networks as uniform families and shows prior work (Lebin and Diaz) exploits a finite-extension property where, for uniform linear maps, a finite witness n0 = 2 for linear maps determines the whole family.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:21Key messages on Peter’s work
- 2:26Higher-order imperative languages
- 4:09Parametricity and local variables
- 8:03Relational parametricity and state
- 10:51Categorical framework
- 13:18Fixed input dimension problem
- 15:47Uniform family approach
- 18:16Compatibility and equivariance
- 20:47Finite representability
- 22:14Connection to parametricity
- 23:21References and thanks
related talks
52mCategory-parametric Programming
07mOn the Reparameterisation Gradient for Non-Differentiable but Continuous Models
16mSensitivity by Parametricity
01h 39mIsomorphic Reasoning: Counting with Types Part 1
49mSemantic Foundations for Probabilistic Programming
41mWar Time Proofs and Futuristic Programs
22mReasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence
01h 01mCategory Theory - Part 2 of 6