<story><title>What is type safety?</title><url>http://www.pl-enthusiast.net/2014/08/05/type-safety/</url></story><parent_chain></parent_chain><comment><author>nmrm</author><text>I think &amp;quot;type safety&amp;quot; is one of those things that&amp;#x27;s so well-defined in theory that there&amp;#x27;s always a huge disconnect between people who know the theory and people who don&amp;#x27;t. Therefore, I always like to explain the &amp;quot;progress + preservation&amp;quot; view whenever describing type safety, because it illustrates the term really has a pretty precise meaning at least in the simple cases.&lt;p&gt;In the simplest case, think of your &amp;#x27;interpreter&amp;#x27; 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).&lt;p&gt;Let&amp;#x27;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) |--&amp;gt; (x + 2)(1) |--&amp;gt; (1+2) |--&amp;gt; 3.&lt;p&gt;Type safety goes like this: If x has type T then either x |--&amp;gt; x&amp;#x27; or x is a value. Also, if x has type T and x |--&amp;gt; x&amp;#x27; then x&amp;#x27; also has type T.&lt;p&gt;The first property is &amp;quot;well-typed programs don&amp;#x27;t go wrong&amp;quot; and the second property closes a loophole (&amp;quot;if you&amp;#x27;re a well-typed program, then you&amp;#x27;re never going to evaluate to anything that isn&amp;#x27;t also well-typed&amp;quot;, so we never escape from the first property by evaluating)&lt;p&gt;* using the product syntax because some people will get confused by f 1 2, but that&amp;#x27;s in fact what I mean.</text></comment>
<story><title>What is type safety?</title><url>http://www.pl-enthusiast.net/2014/08/05/type-safety/</url></story><parent_chain></parent_chain><comment><author>lmm</author><text>I think it&amp;#x27;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. &amp;quot;Has a method named .foo(...)&amp;quot;, while useful, shouldn&amp;#x27;t be the end of what we try to encode, but there&amp;#x27;s a big gap between allowing things like &amp;quot;an X is either a Y or a Z&amp;quot; and allowing arbitrary type-properties, liquidhaskell style, which the article just glosses over.&lt;p&gt;Which is a shame, because it&amp;#x27;s precisely this range - the gap between non-liquid Haskell or Ocaml and Java - which is most relevant to today&amp;#x27;s programmers making choices of programming language.</text></comment>