Iowa Type Theory Commute

The curious case of exponentiation in simply typed lambda calculus


Listen Later

Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC).  But surprisingly, the type is non-uniform.  If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A.  The second argument needs to have type at strictly higher order than the first argument.  This has the fascinating consequence that we cannot define self-exponentiation, \ x . exp x x.  That term would reduce to \ x . x x, which is provably not typable in STLC.  

...more
View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

19 ratings


More shows like Iowa Type Theory Commute

View all
The Changelog: Software Development, Open Source by Changelog Media

The Changelog: Software Development, Open Source

289 Listeners

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas by Sean Carroll | Wondery

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas

4,174 Listeners

Interesting Times with Ross Douthat by New York Times Opinion

Interesting Times with Ross Douthat

7,217 Listeners

Tech Won't Save Us by Paris Marx

Tech Won't Save Us

571 Listeners

Dwarkesh Podcast by Dwarkesh Patel

Dwarkesh Podcast

507 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

16,019 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

13 Listeners

Software Unscripted by Richard Feldman

Software Unscripted

29 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

63 Listeners