Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What is type safety?

pl-enthusiast.net

Post reply on HN
Print view View original

11–20 of 71 posts

Re: What is type safety?

#11

Post by nmrm »

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 'interpreter' as a program that translates programs into values. For example, 1 is a value and \x.x+1 (the lambda expression) is a value, but (\x.x+1)1 is not a value because it evaluates to 2 (or, at least, to 1+1).

Let's say that your interpreter does this a single small step at a time; so for instance, if you have* f(x,y) = x+y, then f(1,2) |--> (x + 2)(1) |--> (1+2) |--> 3.

Type safety goes like this: If x has type T then either x |--> x' or x is a value. Also, if x has type T and x |--> x' then x' also has type T.

The first property is "well-typed programs don't go wrong" and the second property closes a loophole ("if you're a well-typed program, then you're never going to evaluate to anything that isn't also well-typed", so we never escape from the first property by evaluating)

* using the product syntax because some people will get confused by f 1 2, but that's in fact what I mean.

Re: What is type safety?

#12

Post by tel »

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…

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.

Re: What is type safety?

#14

Post by tel »

colanderman wrote: post #6
lmm wrote: post #3

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

Re: What is type safety?

#15

Post by tel »

emillon wrote: post #7

It 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…

That's it for the definition, but it's far from it for the meaning. Python/Ruby make a great example when they're interpreted as vacuously type safe—clearly this definition needs other components in order to be meaningful.

And that's really the rub. You want a language which is type safe and possessing expressive types. Getting both is challenging.

Re: What is type safety?

#16

Post by tomp »

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.

Re: What is type safety?

#17

Post by tel »

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?

"Type safe" is both a marketing line and a technical definition. As a technical definition, many languages are type safe (including, say, Ruby) but they achieve this by having very low meaning to their (static) types.

Typically, the marketing definition means "type safe and expressively typed" which outlaws trivial type systems and their trivial type safety.

Re: What is type safety?

#18

Post by emillon »

tel wrote: post #15
emillon wrote: post #7

It 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…

That's it for the definition, but it's far from it for the meaning. Python/Ruby make a great example when they're interpreted as vacuously type safe—clearly this definition needs other components in order to be meaningful. And that's really the rub. You want a language which is type safe and possessing expressive types. Getting both is challenging.

Indeed. In dynamically typed, every expression is well typed and there is always an evaluation rule that works, so this trivially holds but means nothing.

Re: What is type safety?

#19

Post by ced »

colanderman wrote: post #6
lmm wrote: post #3

I 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 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)

Re: What is type safety?

#20

Post by pmahoney »

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…

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

Surely you're not trading performance for safety, as dozens of languages are "safe" while having much higher performance over Ruby including similarly dynamic languages JavaScript and Lua, or others such as Java, Scala, Clojure, Haskell, OCaml, and so on.

There are, of course, other reasons to choose Ruby, perhaps because of Rails, large talent pool, code conciseness, etc.

Post reply on HN