Proposed terminological change: Replace “Inductive Type” with “Free Type”

The elimination axiom for natural numbers, surreal numbers, lists, and trees can all be properly called induction. However, I don’t think the expression if b then x else y is an example of recursion, and so I don’t think 2 should be called an inductive type. Similarly, I don’t like how the term inductive type is used for dependent sums, unit and null types, and the various new types of homotopy type theory. What all these types share in common is that they have a set of constructors and an elimination axiom which essentially says that these constructors are the only way to obtain an element of these types. A better terminology would be such a type is the free type over a set of
constructors, and to call such a type a free type.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s