A Primer on Type Systems
cs.uaf.edu
A Primer on Type Systems
1–10 of 35 posts
Re: A Primer on Type Systems
#2> There does not seem to be any equivalent of the notion of soundness in the world of dynamic typing. However, we can still talk about whether a dynamic type system strictly enforces type safety.
My understanding is that there are well understood definitions of soundness for dynamically typed languages. The soundness theorem will generally be weaker ("your program will evaluate to a value or abort on a type confusion") but it is certainly possible to be sure a given dynamically typed language definition will never make mistakes like confusing an integer for a pointer. Though in the scheme of things such theorems are not much weaker than what you get for a statically typed language with exceptions ("your program will evaluate to a value with the given type or throw some exception").
Re: A Primer on Type Systems
#3I really liked this brief overview of type systems overall, but I especially liked that the author took the effort to move away from the terms "strongly typed" and "weakly typed". Too often these terms cause confusion. Even worse is when people confuse them for "statically typed" and "dynamically typed" (respectively), leading to people making claims like "Python is weakly typed" and "C is strongly typed" (which, depending on your definitions, are not true statements).
This material wasn't covered in my core curriculum for my CS degrees, which I think is a shame. Some students might find this stuff interesting, and I think introducing it to undergrads at least a little bit and saying "By the way, this is a thing you can research" could help some students with breaking into the academic side of CS.
Re: A Primer on Type Systems
#4I found this article helpful. Since C is a "strongly typed" language it helps to review what is meant by type. In addition, like #DonaldPShimoda, I liked that the author challenged to the existing notions of type. Good read.
Re: A Primer on Type Systems
#5I really liked this brief overview of type systems overall, but I especially liked that the author took the effort to move away from the terms "strongly typed" and "weakly typed". Too often these terms cause confusion. Even worse is when people confuse them for "statically typed" and "dynamically typed" (respectively), leading to people making claims like "Python is weakly typed" and "C is strongly typed" (which, dep…
It's more interesting to answer two questions:
1. Can I easily subvert this type system?
2. Can I make this type system map to concepts in the problem domain?
In C, the answer to 1 is "yes" and the answer to 2 is "to a limited extent". In fact, in C, you can subvert the type system so easily that it's considered impossible not to, to the extent that using the standard library requires throwing type information away, by using pointers-to-void or generic "char" buffers, and as for the second... well, Apps Hungarian notation exists for a reason. (Systems Hungarian exists for a reason, too, but I'll try to keep the insults out of this post.)
https://en.wikipedia.org/wiki/Hungarian_notation
The first question is interesting because it tells you if the type system can be used to enforce invariants, and the second question is interesting because it tells you if those invariants will be worth enforcing. If you're writing in Standard Pascal, and your type system enforces array length as a part of array type, well, to quote a metal album: "So Far, So Good... So What?" What does that tell me about whether my program is semantically correct as regards the problem domain? Similarly with enforcing size specification types: Differentiating between a short, an int, and a long tells me Sweet Fanny Adams about what values of those sizes mean in my program. Typing isn't "strong" if it's enforcing rules which ultimately make no sense, and if it's "sound", well, mathematical proofs of something I'm not interested in are themselves uninteresting.
Re: A Primer on Type Systems
#6[deleted]
Re: A Primer on Type Systems
#7This is an excellent article.
The only thing I'd want to see added to it is a section on gradual typing, a la Perl 6.
Re: A Primer on Type Systems
#8Interestingly "statically typed" and "dynamically typed" are becoming less exclusive, there are code sniffers that can run static analysis of code to detect potential type incompatibilities during inspection and PHP even now has a group of parse errors that will be raised if incompatible classes definitions are detected i.e.
class Foo { function do(): int { return 1; } }
class Bar extends Foo { function do(): string { return 'a'; } }
So I pretty strongly disagree that typing systems can either be static or dynamic, because I think the separation of manifest vs. implicit is a false one, lots of languages (again) support partially explicit type declarations while allowing some sort of support for a generic declaration.
Re: A Primer on Type Systems
#9I really liked this brief overview of type systems overall, but I especially liked that the author took the effort to move away from the terms "strongly typed" and "weakly typed". Too often these terms cause confusion. Even worse is when people confuse them for "statically typed" and "dynamically typed" (respectively), leading to people making claims like "Python is weakly typed" and "C is strongly typed" (which, dep…
It's more interesting to answer two questions: 1. Can I easily subvert this type system? 2. Can I make this type system map to concepts in the problem domain? In C, the answer to 1 is "yes" and the answer to 2 is "to a limited extent". In fact, in C, you can subvert the type system so easily that it's considered impossible not to, to the extent that using the standard library requires throwing type information away,…
I'd extend 1 to include "can I easily avoid subverting this type system?" Guarantees are better, but as long as I can get help that's enough for a tool to be useful assuming 2.
Regarding 2, I've long complained that the conception of types embedded in many systems (and many heads) is very representational and most of the time we don't actually care about representation. The exceptions I typically mention are where we care a lot about performance, and at system boundaries. We can fit those into your analysis by asserting (reasonably, I think) that in those instances representation starts to be a part of your problem domain.
Re: A Primer on Type Systems
#10I really liked this brief overview of type systems overall, but I especially liked that the author took the effort to move away from the terms "strongly typed" and "weakly typed". Too often these terms cause confusion. Even worse is when people confuse them for "statically typed" and "dynamically typed" (respectively), leading to people making claims like "Python is weakly typed" and "C is strongly typed" (which, dep…
It's more interesting to answer two questions: 1. Can I easily subvert this type system? 2. Can I make this type system map to concepts in the problem domain? In C, the answer to 1 is "yes" and the answer to 2 is "to a limited extent". In fact, in C, you can subvert the type system so easily that it's considered impossible not to, to the extent that using the standard library requires throwing type information away,…
>"well, Apps Hungarian notation exists for a reason. (Systems Hungarian exists for a reason, too, but I'll try to keep the insults out of this post.)"
Can you elaborate? I read the wiki page on Apps Hungarian. I am not following. How does/would this address issues with the type system in C?
>"Can I make this type system map to concepts in the problem domain?"
I didn't really follow your Pascal example explanation of this, you first mentioned "because it tells you if the type system can be used to enforce invariants." But the went on to talk about array lengths. How does whether or not the invariants are enforced by the type system help you answer the question of whether or not it maps to the problem domain? Might you be able to provide another example? Thanks.