What is type safety? • Hacker News Board

Re: What is type safety?

#31

Post by freyrs3 » Tue, Aug 05, 2014, 5:11 PM UTC

vinceguidry wrote: post #25

freyrs3 wrote: post #22

Earlier quoted context omitted.

You're putting words in my mouth by implying I denigrated Ruby as unsafe using a much stronger definition of safety. Ruby is type safe under the article's definitions, but I suggest that this claim doesn't carry much information content because a conclusion about the null type system is such a weak claim, like a claim about the null set.

Reducing dynamic typing's safety to a null set claim is exactly the sort of denigration I'm arguing doesn't make sense. Type doesn't disappear just because you aren't encoding it as a first-class PL design concern.

This discussion is just going to reduce down to a runtime tag vs formal type definition. This particular article is using the term type to mean formal type, and my comment is also under this assumption. Under that definition Ruby does have a null type system. That's not a moral judgement of it's design, it's just a fact that follows from the definitions.

Rather than debate this for the gazillionth time, I'll just point you at tel's article which breaks it down very nicely: http://tel.github.io/2014/07/08/all_you_wanted_to_know_about...

Re: What is type safety?

#32

Post by AnimalMuppet » Tue, Aug 05, 2014, 5:12 PM UTC

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

Re: What is type safety?

#33

Post by sparkie » Tue, Aug 05, 2014, 5:15 PM UTC

mnarayan01 wrote: post #21

Ixiaus wrote: post #5

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.

Haskell also allows casting in a way that defeats static type checking - `unsafeCoerce`

Re: What is type safety?

#34

Post by tel » Tue, Aug 05, 2014, 5:21 PM UTC

vinceguidry wrote: post #23

tel wrote: post #12

Earlier quoted context omitted.

freyrs3 didn't say that these languages were unsafe, he said that they were vacuously type safe. The kinds of safety you mentioned do not arise from (static) typing and so, regardless of their validity, it's just not on topic.

How could it not be on topic, when the article clearly said that a type system is that which programs written using it “cannot go wrong”? He then proceeded to use as examples C's lack of memory safety. With a definition that broad, you really need to examine every extant approach to solving the problem, even if you don't want to go in that direction.

He starts with an intuition-bound definition then clarifies as time goes on. Ultimately "go wrong" needs to be embedded in the type system before it applies.

Other things are obviously language safety features, but just are not "types" in the sense of how some languages are "type safe".

Re: What is type safety?

#35

Post by cousin_it » Tue, Aug 05, 2014, 5:21 PM UTC

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.

Re: What is type safety?

#36

Post by AnimalMuppet » Tue, Aug 05, 2014, 5:23 PM UTC

tel wrote: post #14

colanderman wrote: post #6

Earlier quoted context omitted.

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 or fun ping_clients(sm) -> sm' where has_clients(sm) in concert with fun has_clients(sm) -> bool The compiler can then track these, and ensure e.g. th…

You can get this example working with indexed monads in Haskell. You can also do it quite nicely in dependently typed languages like Idris/Agda. However, abitrary predicates is a different matter. Even if you have a language which allows arbitrary computation in types there exist undecidable predicates which may weaken your desire for arbitrary ones.

It seems to me that you probably don't want to do arbitrary computation in types at compile time. Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid. That's not a good position to put your compiler in.

It seems to me to be better to make this a runtime check, which the compiler makes sure to call every time subtraction is applied to a value of that type.

Re: What is type safety?

#37

Post by AnimalMuppet » Tue, Aug 05, 2014, 5:27 PM UTC

cousin_it wrote: post #35

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.

Re: What is type safety?

#38

Post by marcosdumay » Tue, Aug 05, 2014, 5:30 PM UTC

mnarayan01 wrote: post #21

Ixiaus wrote: post #5

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.

Well, "strict" might be a better name for your "strong".

I don't think it's any less precise a concept. Java type system is less strict than Haskell's, has similar "strictiness" to Python or Ruby (while quite different in static typing), and is more strict than C, or Perl.

Re: What is type safety?

#39

Post by dllthomas » Tue, Aug 05, 2014, 5:32 PM UTC

AnimalMuppet wrote: post #36

tel wrote: post #14

Earlier quoted context omitted.

You can get this example working with indexed monads in Haskell. You can also do it quite nicely in dependently typed languages like Idris/Agda. However, abitrary predicates is a different matter. Even if you have a language which allows arbitrary computation in types there exist undecidable predicates which may weaken your desire for arbitrary ones.

It seems to me that you probably don't want to do arbitrary computation in types at compile time. Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid. That's not a good position to put your compiler in. It seems to me to…

I think even better is to have a subtraction that returns a different type, where you can't prove that a > b. Where you can, I don't know that I object to the compiler tracking such things, though I also don't actually use a dependently typed language.

Re: What is type safety?

#40

Post by tel » Tue, Aug 05, 2014, 5:34 PM UTC

AnimalMuppet wrote: post #36

tel wrote: post #14

Earlier quoted context omitted.

You can get this example working with indexed monads in Haskell. You can also do it quite nicely in dependently typed languages like Idris/Agda. However, abitrary predicates is a different matter. Even if you have a language which allows arbitrary computation in types there exist undecidable predicates which may weaken your desire for arbitrary ones.

It seems to me that you probably don't want to do arbitrary computation in types at compile time. Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid. That's not a good position to put your compiler in. It seems to me to…

Well, you'd probably have to introduce a type such that every time you subtracted n from m you must prove that m is at least as big as n. Which would be a pain.

As usual, I really suggest playing with Agda or Idris to get a feel for what sophisticated types actually look and feel like.