[gugagore]

> people who like type systems tend to dislike Julia's type system.

This is true. As far as I understand it, there is not a type theory basis for Julia's design (type theory seems to have little to say about subtyping type lattices). Relatedly, another comment mentioned that Julia needs sum types.

[pjmlp]

It is the same type theory that has powered Common Lisp and Dylan.

[gugagore]

We're not using "type theory" the same way, I think. I'm thinking in terms of

    - simply typed lambda calculus
    - System F
    - dependent type theory (MLTT)
    - linear types
    - row types
    - and so on

But it's subtle to talk about. It's not like there is a single type theory that underlies Typescript or Rust, either. These practical languages have partial, (and somewhat post-hoc) formalizations of their systems.

[pjmlp]

For starters,

"On the use of LISP in implementing denotational semantics"

https://dl.acm.org/doi/10.1145/319838.319866

Type theory in CS isn't a synonymous with whatever Haskell happens to do.