The way that Harper talks about types, such as, "It is not a matter of opinion whether an untyped language is unityped, it is a matter of fact." gives me a different perspective when I program in a language that is effectively unityped.
"These rules are together called “preservation” and “progress”. Notably, they leave a lot of room for the language to define what it means to justify a change in types (automatic upcasting, for instance, is interesting) or well-define program dynamics."
Safety and progress is a weird distinction in the types of properties you can express. It seems to be context dependent. (I'm using what I consider the "standard", loose definitions of safety and progress: safety means the program will not go wrong, bad things won't happen; progress means the program will perform correctly, good things will (eventually?) happen.
For example, consider a program involving binary search on an array. Clearly, "does not access elements outside the bounds of the array" is a good safety property, but what is the status of "if the array is sorted, the search will correctly find a matching element or report that none exists"? It looks like a progress property, but depending on how the results are used I can see how it would become a safety problem. (I think; I'm still undecided on that point.)
Formally, "safety" = "preservation" + "progress". So, using those loose definitions together doesn't fit what I'm referring to.
In particular, "does not access elements outside of the bounds of the array" is not directly a safety property, though it could be interpreted within the dynamics in order to ensure progress. For instance, if you outlaw exception throwing then the types must ensure that exceptional states cannot arise. Else the program can "get stuck" and progress is refuted.
The final point about sorted arrays again mistakes putting "safety" and "progress" on the same epistemological ground.
Hm. I had never heard of "preservation" as a category in itself, other than as a synonym for safety. But I come from a distributed systems/network protocol background, many years ago, so all of the landmarks have moved. Not sure what the distinction buys you, though.
It gives you the proof that's loosely stated as "well-types programs do not go wrong". The sketch is that if some thing is well-typed then progress means it won't "go wrong" and preservation means it'll stay well-typed. Thus: well-typed programs progress all the way to stable values.
7 comments
[ 2.6 ms ] story [ 26.8 ms ] threadI was delightfully surprised running into this comment in a footnote :)
Here's the direct link to Harper's comment: http://www.pl-enthusiast.net/2014/08/05/type-safety/#comment...
The way that Harper talks about types, such as, "It is not a matter of opinion whether an untyped language is unityped, it is a matter of fact." gives me a different perspective when I program in a language that is effectively unityped.
Safety and progress is a weird distinction in the types of properties you can express. It seems to be context dependent. (I'm using what I consider the "standard", loose definitions of safety and progress: safety means the program will not go wrong, bad things won't happen; progress means the program will perform correctly, good things will (eventually?) happen.
For example, consider a program involving binary search on an array. Clearly, "does not access elements outside the bounds of the array" is a good safety property, but what is the status of "if the array is sorted, the search will correctly find a matching element or report that none exists"? It looks like a progress property, but depending on how the results are used I can see how it would become a safety problem. (I think; I'm still undecided on that point.)
In particular, "does not access elements outside of the bounds of the array" is not directly a safety property, though it could be interpreted within the dynamics in order to ensure progress. For instance, if you outlaw exception throwing then the types must ensure that exceptional states cannot arise. Else the program can "get stuck" and progress is refuted.
The final point about sorted arrays again mistakes putting "safety" and "progress" on the same epistemological ground.