Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added pointer to:
I have expanded the previous idea-section a fair bit (it used to just say that simple type theory has non-indexed type formation). Now it reads as follows:
Originally, “simple type theory” was the name of the type theory introduced by Church (1940) (therefore often and more informatively: “Church’s type theory” or similar). This type theory allowed function type-type formation (therefore often: “simply typed lambda-calculus”) based on two elementary types (a kind of type of natural numbers and a type of propositions).
In mild generalization, if one admits in addition product type-type formation then [e.g. Gunter (1992)] these are the type theories whose categorical semantics is in cartesian closed categories (see also at relation between category theory and type theory).
More generally, the term “simple type” has come to refer to any type theory whose type formations are not indexed, […]
Finally I added this reference:
added pointer to:
added reference
Anonymouse
1 to 6 of 6