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

The confusion stems from the popular usage of type system, which Benjamin Pierce defines thus, "A type system is a syntactic method for enforcing levels of abstraction in programs." [0] Note that it does not have to be a type-theoretic type system! This is precisely the source of the confusion.

Bit patterns don't have to matter. There are languages like Haskell which have type-theoretic type systems and no bit patterns specified [1]. There are also languages like C, which has non-type-theoretic type systems and lots of things to say about bits, and languages like ANS FORTH, which has no type system at all and could reinterpret bit patterns.

There are also languages which have features generally referred to as type systems, and which fit Pierce's definition, but which are not just not type-theoretic, but don't resemble any kind of system which discriminates values based on membership in a set. For example, Pony and Rust both have syntactic forms for adding memory semantics to values, and their type-checking routines check the memory semantics oblivious to the bits being stored. Pony additionally can check certain causality properties. Monte has auditors, which are syntactically-specified objects which enforce semantic properties of other objects by examining their ASTs [2].

In summary, "type system" means what Pierce says it means: there is syntax, the syntax describes abstract properties of the program, the properties can be checked by syntax-guided computation, and programs can be rejected as invalid if the check fails.

[0] https://www.cis.upenn.edu/~bcpierce/tapl/

[1] https://www.haskell.org/onlinereport/basic.html

[2] http://monte.readthedocs.io/en/latest/auditors.html




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


Then again, apart from the explicit (like bitwise operations and bitfields), even C tries to be hands-off about the encoding of its types.

The reason for the infamous undefinedness of signed integer overflow is precisely that C tries to be agnostic about their encoding (which mostly comes down to two's complement vs sign bit).


In fact, I think the data format ("sequence of bits") is actually something totally unrelated to the type system, which deals in an abstract idea of types. Type-checking doesn't get involved with encodings of values.




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

Search: