The type scheme we have discussed so far-involving the primitive types and the type constructors outlined above-is usually referred to as Primitive Recursive Arithmetic. It is a theory that is considered very safe, and is widely accepted. We noted before that equality testing, for example, is decidable over types constructed using cross product and primitive types. This is true in general for the type theory we have discussed so far.
The next topic we discuss is much less safe: namely function space types. There are questions associated with this type that are undecidable.