inductive types: Nonlinear Function
Created: January 13, 2022
Modified: January 13, 2022

inductive types

This page is from my personal notes, and has not been specifically reviewed for public consumption. It might be incomplete, wrong, outdated, or stupid. Caveat lector.
  • Talia Ringer says that these are one of the most beautiful, foundational ideas in programming languages: https://twitter.com/TaliaRinger/status/1481845588224266240
  • What is an inductive type? My lay conception is that it's something like the natural numbers, or the Haskell list type. It's a set that's defined inductively, so that you can define operations on this set recursively. But that doesn't immediately reveal why you'd consider them beautiful, on top of whatever beauty already exists in the concept of recursion.