Let's say that "objects" are untyped, and "elements" are typed, by definition. These are semantic entities. Nuprl's (closed) terms are untyped in that you are allowed to think of them as objects. You can also think of them as elements. This is not the same. I'd like to distance Nuprl, based on PERs, from set theory. In set theory, objects are given their final meaning by the universe, and sets are types only in the most boring possible sense that you gather up objects and call them elements. In Nuprl, terms obtain their computational meaning as objects, but their mathematical meaning as elements. Interpreted as PERs, Nuprl's types let you ask whether two objects implement the same element. Equality of elements is not equality of objects, and the way you think about objects and elements is different. A variable has a declared type, and it denotes an arbitrary element of that type. It is meaningless to think of it as an object (unless the declared type is a subtype of the type of objects).

You are right that you don't need to explain elements in terms of objects. That doesn't necessarily make it a bad idea.

Each PER indicates how its elements are implemented by objects. There's no requirement that an object will have a unique type. Each type can be thought of as an abstract view of certain objects.

Constructions in Nuprl are heavily based on types, as in any strong type system. You wouldn't bother with a strong type system if you weren't going to do that. You can construct elements using the usual sorts of rules. Because Nuprl also has objects, you also have the option of constructing objects and then proving they implement elements of one or more types. If you've never felt at all constrained by a strong type system, great; you don't have to do that. But for many people, the intrinsically untyped approach is sometimes helpful. An element is an element; it doesn't matter whether it's an element by construction, or a verified object. I see this as a tremendous benefit for strongly typed programming.

On Monday, February 11, 2019 at 1:17:25 PM UTC-5, Thorsten Altenkirch wrote:

I have got something else against NuPRL. It explains Type Theory via untyped objects which are then typed. In  my view there is no reason why we need to explain typed things via untyped objects. When we talk about mathematical objects we think about typed entities, and the formalism of type theory should reflect this. It is not that we find an untyped object on the street and then try to find out which type it has. We are thinking of a type first and then we construct an element.

Thorsten