Given a typical popular programming language, its native type theory is a dependent type theory which describes invariants, preconditions, predicates, and other generalizations of typical type-system features. The title says it all: what are some strong examples of popular languages which have a type system that can't be (naturally?) embedded into their native type theory?

For what it's worth, I can't think of any examples whatsoever. Static types can be embedded. Object protocols and duck-typed constraints can be embedded too. Hoare logic can be embedded as well.

("Strong" here means that I'm not asking for a completely open listing, just well-known or easy-to-express examples which could possibly serve as canonical counterexamples.)

  • 1
    $\begingroup$ Probably any language which is not type safe... like Java (cis.upenn.edu/~bcpierce/courses/629/papers/…) $\endgroup$
    – cody
    Commented Jul 22, 2022 at 20:30
  • $\begingroup$ I think non-type-safe languages are fine too. Haskell's unsound type system embeds into Haskell's native type theory, for example. I would love to read a specific strong example of how Java's type system can't be embedded into Java's native type theory. $\endgroup$
    – Corbin
    Commented Jul 22, 2022 at 22:39
  • $\begingroup$ The question is, what is the meaning of "embed"? If you map Java's int into int + exception + undefined behavior + segfault then you're probably going to be successful (since AFAIKT the "native type theory" is just a logic of the operational semantics of the language) $\endgroup$
    – cody
    Commented Jul 25, 2022 at 15:53
  • 1
    $\begingroup$ I'll accept any of the definitions used in this nLab article; I'm not picky. I suppose I'm asking for examples of popular programming languages whose operational semantics don't line up with their type systems. $\endgroup$
    – Corbin
    Commented Jul 28, 2022 at 4:11


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.