Definitions Of Types

We should replace this page with a guide/roadmap for the novices and less than novices. What definitions are useful and in what contexts? What are the current achievements in type theory for programming languages and how far or how close are they from having desired engineering properties so that they may have a real practical impact in programming.

From lots of type definitions some are useless regardless of context, some have very limited contexts, for example some type theories are minimal and designed not for practical use but for proving some technical results in the domain generically named as "foundations of mathematics". Those definitions will typically confuse beginner into thinking they would get useful insights from there (it is possible but not directly, just like you won't get such insights from actually programming turing machines). Other definitions may be useful in some programming domains, but not in others. Other people may get almost dizzy by things like CurryHowardIsomorphism. It is a spectacular (from an esthetic standpoint) result, but for a programmer, we can safely say that he will be no lesser a programmer if he doesn't know it. In comparison, a good programmer could use some basic things about lambda calculus.

We already have a page named WhatAreTypes. I see no compelling reason to rename a reference to that existing page just to make a slightly more formal name. However WikiGnomes are welcome to refactor the reference if compelled.

See DefinitionsOfTypesInPublications.