41–50 of 71 posts
So type safety is just a synonym for "no undefined behavior"? What about code like "i=i++", which leads to undefined behavior but doesn't seem to have any type errors? I thought type safety referred to only a subset of undefined behaviors, namely using a value of type A as though it had type B.
To those that know more than I: my understanding before this article was that the only "type-safe" languages were or like Haskell, OCaml, Idris, Agda, etc... If that's not the case is "type-safe, pure, and functional" a good epithet to extend, say, Haskell's "type-safe" tag with many of its other features that weave with the type system well?
I believe Haskell would be considered have "strong static typing". Unfortunately, "strong" in this context is less precise than one might like: both Haskell and Java are generally considered "strongly typed", but Java allows e.g. type casting in a way that will not be statically type checked. Haskell also uses type inference rather than requiring type declarations, but that is not _directly_ related.
That's not totally static, but within the definitions of the article, it might be good enough to count as "type safety" without falling into the "null type safety" category.
So type safety is just a synonym for "no undefined behavior"? What about code like "i=i++", which leads to undefined behavior but doesn't seem to have any type errors? I thought type safety referred to only a subset of undefined behaviors, namely using a value of type A as though it had type B.
This seems to be C/C++ code. The article said that C and C++ were not type safe, so "doesn't seem to have any type errors" within C/C++ doesn't mean that it's type safe. That said, the article did say that Java was type safe, and you can write that same expression in Java. I don't recall whether the result is undefined in Java.
Earlier quoted context omitted.
I believe Haskell would be considered have "strong static typing". Unfortunately, "strong" in this context is less precise than one might like: both Haskell and Java are generally considered "strongly typed", but Java allows e.g. type casting in a way that will not be statically type checked. Haskell also uses type inference rather than requiring type declarations, but that is not _directly_ related.
Type casting has to be modeled (more or less) as (a) upcasting only (b) a failure of type safety, or (b) an admission that the type system is entirely vacuous.
I think "type safety" is one of those things that's so well-defined in theory that there's always a huge disconnect between people who know the theory and people who don't. Therefore, I always like to explain the "progress + preservation" view whenever describing type safety, because it illustrates the term really has a pretty precise meaning at least in the simple cases. In the simplest case, think of your 'interpre…
But this type theoretical definition is not really well-suited for the real world; either you have to include exceptions in the set of values, which could include even things like Segmentation Fault, making ASM well-typed, or you don't allow exceptions as values, which means that not even OCaml and Haskell are well-typed with their DivisionByZero and ArrayOutOfBounds exceptions.
To do this, you need to define another decently large set of judgments for error propagation (such as "if x is an error and y : t then (x,y) is an error" and vice versa), but ultimately you can maintain type safety via progress and preservation while still accounting for exceptions as we know them.
On the topic of whether it would make ASM well-typed, I figure that the lack of array bounds checking would be one reason why ASM would have problems, but I haven't thought it through fully. However, I found a neat paper that tries to create a type-safe assembly language pretty similar to x86: http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf
"Well typed programs don't go wrong" only for sufficiently narrow definitions of "go wrong". They don't go wrong by doing undefined behavior. They can still go horribly wrong by doing unintended behavior, though. Type safety doesn't eliminate all bugs, just a subset of them.
I think "type safety" is one of those things that's so well-defined in theory that there's always a huge disconnect between people who know the theory and people who don't. Therefore, I always like to explain the "progress + preservation" view whenever describing type safety, because it illustrates the term really has a pretty precise meaning at least in the simple cases. In the simplest case, think of your 'interpre…
"Well typed programs don't go wrong" only for sufficiently narrow definitions of "go wrong". They don't go wrong by doing undefined behavior. They can still go horribly wrong by doing unintended behavior, though. Type safety doesn't eliminate all bugs, just a subset of them.
I think "type safety" is one of those things that's so well-defined in theory that there's always a huge disconnect between people who know the theory and people who don't. Therefore, I always like to explain the "progress + preservation" view whenever describing type safety, because it illustrates the term really has a pretty precise meaning at least in the simple cases. In the simplest case, think of your 'interpre…
But this type theoretical definition is not really well-suited for the real world; either you have to include exceptions in the set of values, which could include even things like Segmentation Fault, making ASM well-typed, or you don't allow exceptions as values, which means that not even OCaml and Haskell are well-typed with their DivisionByZero and ArrayOutOfBounds exceptions.
But... that's why I added the "In the simplest case".
If you're not familiar with the "progress + preservation" definition, then it's going to be rough going understanding anything else without lots of background in logic or proof theory, especially in the case of programming languages as they relate to software engineering. As a prime example, your comment ("include exceptions in the set of values") really very often means something quite different to someone who has an intuitive grasp on the "progress + preservation" definition, and someone who does not.
See also Robert Harper's post and Michael Hicks's response on the article in question.
I think "type safety" is one of those things that's so well-defined in theory that there's always a huge disconnect between people who know the theory and people who don't. Therefore, I always like to explain the "progress + preservation" view whenever describing type safety, because it illustrates the term really has a pretty precise meaning at least in the simple cases. In the simplest case, think of your 'interpre…
Jeremy Siek has an excellent blog post explaining this called "Crash Course on Notation in Programming Languages": http://siek.blogspot.com/2012/07/crash-course-on-notation-in...
I'm not surprised, either. Siek's papers are always as accessible as they are insightful.