What is type safety? • Hacker News Board

Re: What is type safety?

#21

Post by mnarayan01 » Tue, Aug 05, 2014, 4:52 PM UTC

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.

Re: What is type safety?

#22

Post by freyrs3 » Tue, Aug 05, 2014, 4:53 PM UTC

vinceguidry wrote: post #4

freyrs3 wrote: post #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".

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…

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.

Re: What is type safety?

#23

Post by vinceguidry » Tue, Aug 05, 2014, 4:54 PM UTC

tel wrote: post #12

vinceguidry wrote: post #4

Earlier quoted context omitted.

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…

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.

Re: What is type safety?

#24

Post by mnarayan01 » Tue, Aug 05, 2014, 4:57 PM UTC

freyrs3 wrote: post #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".

A substantially better description would be "dynamically type safe".

Re: What is type safety?

#25

Post by vinceguidry » Tue, Aug 05, 2014, 4:59 PM UTC

freyrs3 wrote: post #22

vinceguidry wrote: post #4

Earlier quoted context omitted.

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…

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.

Re: What is type safety?

#26

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

tomp wrote: post #16

nmrm wrote: post #11

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.

Haskell (at least) is actually fine for throwing Segmentation Faults, DivisionByZero, and ArrayOutOfBounds since they can all masquerade as bottom which inhabits every type. Further, this extra inhabitant isn't (too) bad for semantics (it's "morally correct") since you cannot detect it—any attempt to examine bottom results in bottom, it's contagious.

The problem is that you sometimes can distinguish, say, a segfault from an infinite loop. Any code which does that is pretty dangerous.

That's why "pure" exceptions are considered super taboo in Haskell. If you need exception passing then you should do it in something like IO/Either/Cont to contain that effect.

It's also why the couple partial functions in Haskell are all considered warts and never for practical use:

     head :: [a] -> a
     tail :: [a] -> [a]
     (!!) :: [a] -> Int -> a

should all be replaced by

     head :: [a] -> Maybe a
     tail :: [a] -> Maybe [a]
     (!!) :: [a] -> Int -> Maybe a

which now uses exceptions which are marked inside the type system.

Personally, I kind of wish `(/) :: Fractional a => a -> a -> Maybe a` sometimes. It'd get confusing with IEEE floats though since that type already contains values Inf/-Inf/NaN.

[0] http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/fa...

Re: What is type safety?

#27

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

ced wrote: post #19

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…

Common Lisp supports arbitrary type predicates, and I think that SBCL enforces them (not sure) at runtime. For instance, it will call the predicate before setting a struct's field to make sure that it returns true (under high safety compilation, low safety just trusts that it's correct)

That's more of a contract system than a type system, though.

Re: What is type safety?

#28

Post by tel » Tue, Aug 05, 2014, 5:05 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.

As usual, when freyrs3 says "type" he means something simpler and more specific than what you appear to mean. The whole idea is that "type safety" is both specific and not sufficient to mean anything valuable.

Re: What is type safety?

#29

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

mnarayan01 wrote: post #24

freyrs3 wrote: post #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".

A substantially better description would be "dynamically type safe".

In the context of this article that's just confusing the issue. "Type" is both well-defined and not the same as "type" in a Ruby context.

Re: What is type safety?

#30

Post by tel » Tue, Aug 05, 2014, 5:08 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.

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.