3 ms·

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 peopl

by nmrm 12y ago

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.

tomp 12y ago
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.
- tel 12y ago
  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/fast+loose.pdf http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/fa...
- Nav_Panel 12y ago
  To add on to tel's response, another method of supporting exceptions is to rewrite progress as "if x : t then either x |-> x', x is a value, or x is an error". To do this, you need to define another decently large set of judgments for error propagation (such as "if x is an error and y : t then (x,y) is an error" and vice versa), but ultimately you can maintain type safety via progress and preservation while still accounting for exceptions as we know them. On the topic of whether it would make ASM well-typed, I figure that the lack of array bounds checking would be one reason why ASM would have problems, but I haven't thought it through fully. However, I found a neat paper that tries to create a type-safe assembly language pretty similar to x86: http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf
  - nmrm2 12y ago
    wrt ASM, I think tomp meant something like what Robert Harper is getting at in his post on the linked article. edit: got grandparent's username wrong.
- nmrm2 12y ago
  Yes. A convenient way to do the former is to add another judgement err, so that you can prove theorems about things which go err, and know that there's nothing which isn't safe and also isn't subject to your theorems about going err. (edit: tel provides perhaps a better "irl" example) But... that's why I added the "In the simplest case". If you're not familiar with the "progress + preservation" definition, then it's going to be rough going understanding anything else without lots of background in logic or proof theory, especially in the case of programming languages as they relate to software engineering. As a prime example, your comment ("include exceptions in the set of values") really very often means something quite different to someone who has an intuitive grasp on the "progress + preservation" definition, and someone who does not. See also Robert Harper's post and Michael Hicks's response on the article in question.
scott_s 12y ago
Jeremy Siek has an excellent blog post explaining this called "Crash Course on Notation in Programming Languages": http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.com/2012/07/crash-course-on-notation-in...
- nmrm2 12y ago
  Thanks for sharing, that's very well written! I'm not surprised, either. Siek's papers are always as accessible as they are insightful.

by nmrm 12y ago

tomp 12y ago

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.

tel 12y ago
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/fast+loose.pdf http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/fa...
Nav_Panel 12y ago
To add on to tel's response, another method of supporting exceptions is to rewrite progress as "if x : t then either x |-> x', x is a value, or x is an error". To do this, you need to define another decently large set of judgments for error propagation (such as "if x is an error and y : t then (x,y) is an error" and vice versa), but ultimately you can maintain type safety via progress and preservation while still accounting for exceptions as we know them. On the topic of whether it would make ASM well-typed, I figure that the lack of array bounds checking would be one reason why ASM would have problems, but I haven't thought it through fully. However, I found a neat paper that tries to create a type-safe assembly language pretty similar to x86: http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf
- nmrm2 12y ago
  wrt ASM, I think tomp meant something like what Robert Harper is getting at in his post on the linked article. edit: got grandparent's username wrong.
nmrm2 12y ago
Yes. A convenient way to do the former is to add another judgement err, so that you can prove theorems about things which go err, and know that there's nothing which isn't safe and also isn't subject to your theorems about going err. (edit: tel provides perhaps a better "irl" example) But... that's why I added the "In the simplest case". If you're not familiar with the "progress + preservation" definition, then it's going to be rough going understanding anything else without lots of background in logic or proof theory, especially in the case of programming languages as they relate to software engineering. As a prime example, your comment ("include exceptions in the set of values") really very often means something quite different to someone who has an intuitive grasp on the "progress + preservation" definition, and someone who does not. See also Robert Harper's post and Michael Hicks's response on the article in question.

scott_s 12y ago

Jeremy Siek has an excellent blog post explaining this called "Crash Course on Notation in Programming Languages": http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.com/2012/07/crash-course-on-notation-in...

nmrm2 12y ago
Thanks for sharing, that's very well written! I'm not surprised, either. Siek's papers are always as accessible as they are insightful.