1. 14

  2. 2

    This isn’t a very good article for other people to learn from - but I’m sure the author learned from writing it, which is great!

    He says that type safety isn’t something you can can easily pin down but it is easy to pin down. There are two types: A language that is statically or strongly typed and a language which is dynamically typed.

    As for static typing: There are two static properties which define what it means for a language to have type safety: Preservation and Progress.

    • Preservation is the claim that the type of a program doesn’t change during evaluation.
    • Progress is the claim that a well typed program will be able to evaluate completely, rather than get stuck or perform some kind of undefined behavior.

    Languages with dynamic typing don’t have either of these properties but they do perform runtime checks to avoid coercing objects of one type as if they were another.

    1. 1

      I’m not sure I fully understand what progress means. Is something like:

      int f()
         while( 1 ) {}

      type safe?

      1. 2

        I understand your question but let me be careful about terminology first: Type safety is a property of a language not a piece of code, given a type system a piece of code could be determined to be well typed or not.

        Progress says that you will always be able to continue evaluation/execution, it doesn’t require that it should terminate so a language with infinite loops can still have progress. An example of blocking progress would be if a broken type system somehow thought 3 + “foo” was well typed, then it had no rule to execute plus on different types of value.

        1. 2

          Thanks, that definitely clarifies it.