| ▲ | TimorousBestie 2 hours ago | |
Instead of spending time beating one’s head against Russell and Whitehead, I would advise reading Homotopy Type Theory (aka the HoTT Book). Dependent types are cool and mind-expanding, but higher inductive types are downright mind-altering. The Little Schemer/Typer could be used as a preparatory text to gear one up for HoTT. It also has the advantage of being a bit more applicable to functional programming languages, maybe even more so than Mac Lane’s Categories for the Working Mathematician (which I sometimes see suggested to mathematically-inclined Haskell novices). | ||