Hacker News new | comments | show | ask | jobs | submit login

> Note that it does not have to be a type-theoretic type system! This is precisely the source of the confusion.

What do you mean by "type theoretic"? Once you have a formal system where your objects are divided into sorts and your syntactic expressions are constrained by those sorts such that expressions may be ill-formed when the sorts are mismatched (by some definition), then you have a type theory on your hands.

> the properties can be checked by syntax-guided computation

Not all type systems can be checked by computation (some are undecidable).

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact