8 ms·
> 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 desig
by gugagore 11mo ago
> 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 11mo agoIt is the same type theory that has powered Common Lisp and Dylan.
- gugagore 11mo agoWe'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 11mo agoFor starters, "On the use of LISP in implementing denotational semantics" https://dl.acm.org/doi/10.1145/319838.319866 https://dl.acm.org/doi/10.1145/319838.319866 Type theory in CS isn't a synonymous with whatever Haskell happens to do.