What is type safety?
pl-enthusiast.net
What is type safety?
1–10 of 71 posts
Re: What is type safety?
#2> As such, we can think of these languages as type safe according to the null type system
I think a term like vacuously type safe is a good description of what Python/Ruby are under this set of definitions. So as to distinguish from languages where type safety actually means something slightly stronger than "all syntactically valid programs are accepted by the null type system".
Re: What is type safety?
#3I think it's worth talking about the ability to propagate user-defined invariants. To me the most useful aspect of a type system is that it enables you to declare that all Xs have some property, and then the language guarantees that this holds. "Has a method named .foo(...)", while useful, shouldn't be the end of what we try to encode, but there's a big gap between allowing things like "an X is either a Y or a Z" and allowing arbitrary type-properties, liquidhaskell style, which the article just glosses over.
Which is a shame, because it's precisely this range - the gap between non-liquid Haskell or Ocaml and Java - which is most relevant to today's programmers making choices of programming language.
Re: What is type safety?
#4> As such, we can think of these languages as type safe according to the null type system I think a term like vacuously type safe is a good description of what Python/Ruby are under this set of definitions. So as to distinguish from languages where type safety actually means something slightly stronger than "all syntactically valid programs are accepted by the null type system".
I don't think it's quite right to denigrate the actual safety you get in dynamic languages by referring to their type systems as such.
They are indeed safe, you won't get undefined behavior in the vein of C/C++. In fact, if they weren't such, there wouldn't any point to using them over more performant architectures.
The only time as a Ruby developer I've ever encountered a segfault is when a library calls out to a C extension, the problem is fixed by switching to a different gem. I'm safe in that whenever my program fails, the bug is in something I've written. I've never found an actual bug in Ruby.
Sure, I'm giving up a hell of a lot of performance for this safety, but it's more than worth it for my company's use case.
In fact, I can't even imagine a form of safety you could add to Ruby that isn't a Very Hard Problem, e.g. safety from race conditions. TDD in Ruby gives you a kind of certainty about the correctness your code that is hard to get in other languages. If something breaks, just add another test.
Re: What is type safety?
#5To 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?
Re: What is type safety?
#6I think it's worth talking about the ability to propagate user-defined invariants. To me the most useful aspect of a type system is that it enables you to declare that all Xs have some property, and then the language guarantees that this holds. "Has a method named .foo(...)", while useful, shouldn't be the end of what we try to encode, but there's a big gap between allowing things like "an X is either a Y or a Z" and…
Yes, I've long wanted to be able to attach arbitrary predicates to types. This is great for functional state machines; say the state machine type is sm, you can specify functions like
fun initialize(sm) -> sm'
where sm.state == uninitialized, sm'.state != uninitialized
fun ping_clients(sm) -> sm' where has_clients(sm)
fun has_clients(sm) -> bool
An even smarter compiler can, if it knows the definitions of these functions, determine statically whether a given predicate is guaranteed to produce the same result on a modified object. (e.g. simply by inspecting which fields are inspected and modified)
Re: What is type safety?
#7It is also interesting to consider the PL definition of type safety: the progress and preservation theorems.
Progress: if an expression is well typed then either it is a value, or it can be further evaluated (in the sense that "an appropriate evaluation rule exists").
Preservation: if an expression e has type t, and is evaluated to e', then e' has type t.
That's it, really (well, you can do a few extensions to allow errors such as division by zero, or take memory into account).
If your language has both of these properties, they tell you that typed expressions will behave nicely at run time.
Re: What is type safety?
#8> A classic English example is Chomsky’s “Colorless green ideals sleep furiously”—perfectly syntactically correct, but meaningless.
Interesting. But is it meaningless? Isn't its very meaninglessness its meaning because it has come do be known due to it being bandied about far and wide as an example of meaninglessness.
Maybe it's something more. Clearly, for all X, X cannot be at one and the same time both green and colorless. Similarly ideals do not _literally_ belong to the class of things which can sleep. Finally, sleeping as an activity is never done furiously as fury signifies intent and whatever else may be true when one is asleep it is certainly true that one lacks intent when asleep.
Thus packed into that sentence are three ways in which it _cannot_ be the case or refer to something _actual_ in the world. Is it in this way that it fails to have meaning and so will always continue to fail to have meaning?
postscript:
> Let’s deconstruct this phrase and define its parts, considering the second part first.
Let's use the word analyse rather than deconstruct when that is the word needed.
Re: What is type safety?
#9To 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?
"Type-safe" as used in the FP community tends to be a much stronger claim than what's described in this post. At the very least, throwing a runtime exception is considered "going wrong" in the Haskell community, and this post keeps throwing out examples of runtime exceptions as avoiding "going wrong".
Re: What is type safety?
#10> As such, we can think of these languages as type safe according to the null type system I think a term like vacuously type safe is a good description of what Python/Ruby are under this set of definitions. So as to distinguish from languages where type safety actually means something slightly stronger than "all syntactically valid programs are accepted by the null type system".
I don't think it's quite right to denigrate the actual safety you get in dynamic languages by referring to their type systems as such. They are indeed safe, you won't get undefined behavior in the vein of C/C++. In fact, if they weren't such, there wouldn't any point to using them over more performant architectures. The only time as a Ruby developer I've ever encountered a segfault is when a library calls out to a C…
> TDD in Ruby gives you a kind of certainty about the correctness your code that is hard to get in other languages.
? TDD is pretty easy in many other languages, both dynamic and static. In some ways, static type systems can enhance TDD by making testing to validate invariants that are beyond what the type system can statically verify easier, because static types can be used to generate test data automatically, so instead of specify specific tests, you specify the universally quantified invariant that must hold and the testing framework generates numerous tests. Both Haskell and Scala (and no doubt other languages) have testing frameworks that leverage the type system to allow this.