Odersky et al.'s $\nu Obj$ calculus [1] adds just enough dependent typeness on top of object oriented programming to express interfaces that define types (and consequently module systems and other fanciness). Although still undecidable, it seems to have proven itself practical as the base of a language without the need for interactive theorem proving.

I am curious about non-objected oriented type systems which are (1) at least as expressive as $\nu Obj$, in the sense that $\nu Obj$ can be embedded within them and (2) not "too much" more expressive (left intentionally vague), and therefore hopefully more tractable from a type inference / checking perspective.

For example, a sufficiently powerful non-objected system should be able to type the vtable concept, and then express "objects" as tuples the first element of which is a vtable. Unfortunately, the obvious way to do this requires existential types, which I (perhaps naively) think of as more complicated than $\nu Obj$. So, I suppose my question splits into three parts:

  1. Are existential types on top of basic Hindley-Milner sufficient to express $\nu Obj$?
  2. Am I correct that existentials are harder to deal with than $\nu Obj$ ("too much more expessive")?
  3. Is there something weaker than existentials that still captures $\nu Obj$, without an object oriented focus?

[1] Odersky et al. 2003, A nominal theory of objects with dependent types.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.