Isomorphic Reasoning: Counting with Types Part 1
summary
Claim: parametric polymorphism gives a hidden type arithmetic that lets one compute exact inhabitant counts (e.g. ∀a. a→a is unique, function types count as B^A). Tools: Yoneda lemma, representable/Naperian and container functors, products/coproduts, System F with de Bruijn indices. Built: a Haskell/Scala/Idris implementation with a minimal parser/printer that lifts searches into sequences of isomorphisms to enumerate inhabitants. Results: concrete enumeration works; improvements (fixpoints, double-negation, Fω) are listed.
AI-written summary · about
chapters (12)
- 0:00Start
- 14:21Techniques for Counting Types
- 18:23Identity of Indiscernibles
- 31:34What Is an Isomorphism
- 37:39Floating Point Numbers
- 40:32Unit Introduction
- 47:42Functions
- 1:20:42Preliminary Definitions
- 1:23:22Definition of Categories
- 1:28:50Associativity
- 1:33:47Concrete Categories
- 1:35:09Classifications of Categories
related talks
01h 12mTruth about Types
38mPropositions as Types for Beginners in Haskell
52mCategory-parametric Programming
58mMonoidal Catamorphisms
24mHigher order programming with probabilistic effects: A model of stochastic memo...
01h 11mHands on Chat About Categories
47mIntroduction to FP Using Haskell (Part 2)
01h 00mCategory Theory - Part 5 of 6