Hacker News Reader

Comment by gugagore | Hacker News Reader

> 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.

View on HN

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

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.

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.

Reply on news.ycombinator.com