Hacker News new | ask | show | jobs
by igravious 2668 days ago
It's type theory, so the `objects' in question are either systems of terms and/or types. See where it says:

    terms allowed to depend on types, corresponding to polymorphism.
    types depending on terms, corresponding to dependent types.
    types depending on types, corresponding to type operators.
So I think they're using the word `objects' either loosely (as in, they could have said `things' but maybe that's too informal?) or they're using it as a shorthand for `type-theoretic objects', in which case they're talking about languages of a certain constrained expressive power: the language which features polymorphism, the language which features dependent types, the language which features type operator.

`object' here refers neither to the objects of object-oriented programming nor to object in common lisp object system.

edit: IANATT