> Types are there whether you want them to be or not
But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system.
There is also a minor thing that came to my mind. Types are most often associated with intuitionist logics, which are about constructive provability, as opposed to classical logics, which are about "truthyness" so the title of the post is a bit misleading :)
"But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system."
In theory, yes - I came here to make that same objection.
In practice, there arises the question of whether such terms are actually ever encountered for a given type system when solving realistic problems.
If you were building a sandcastle, a type system is like plastic forms in the shape of castle components (walls, towers, etc)... They help you create a better sandcastle...
This article was essentially saying: "You can remove the forms when you are done and your sandcastle will still stand."
Yes, type erasure is neat and a bit of thinking will make it obvious why proving static properties does not require run time checks if the transformations you perform on your program preserve those static properties. I disagree with the author's claim though that types are everywhere. Types in fact are extra structure that is hoisted onto programs. At the end of the day the machine knows nothing about the types and will shuttle bytes back and forth all day long. Furthermore, types restrict the universe of computation and there are examples of programs that are not well-typed but don't go wrong when evaluated.
Types give you the power of abstraction -- they allow you to define new concepts that "don't to go wrong" and allow you to speak of things other than just bytes-shuttled-on-a-turing-tape. Rigorously justifying the ignorance of the underlying bytes (i.e. being parametric over representation) is an advantage, not a downside.
But maybe I am misunderstanding your comment? Perhaps you were just equivocating over what "really there" means? If that's the case, is multiplication not "really there" because it can be implemented in terms of bit shifting and addition? We don't imagine multiplication as somehow putting these restrictions on what we can do with our bit shift operators -- the multiplication is the "real" thing we care about and the binary operations are incidental.
In any case, see the famous parable that opens Reynolds' "Types, Abstraction, and Parametric Polymorphism" for a colourful example of ignoring the underlying data representation:
This is an execution-centric view; I think that types really are everywhere when it comes to how typical programmers think about their code (even in dynamically typed languages).
Some food for thought from Rich Hickey:
"Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system."
http://www.reddit.com/r/programming/comments/lirke/simple_ma...
He seems to be saying "types are just a formal system; they are meaningless until given meaning by an interpretation". Which is, of course, true. But the same can be said of programming languages. They're just meaningless squiggles until interpreted by human or machine.
Assuming you have some sort of specification for your program, you can use a formal system (such as a static type system) to describe aspects of the specification. It's up to you to correctly model the requirements in the system, but it's similarly up to you to model the requirements of the system in your (far larger and more complex) program. The types ensure that the program fits the aspects of the specification you were able to describe with them.
Also what about protocols? Can type systems handle that. Things like:
* open file
* close file
* read form file
That can be type checked up and down it will still be broken. Is that Rich Hickey meant? Here we are dealing with a real world -- a file. And it has a protocol to access it. So in a sense we want a protocol checker not a type checker in that case...?
I was more convinced by someone who replied to that post (psnively). He seems to be saying that type systems can't model the world as we know it perfectly, in which case it sounds like a Nirvana fallacy - we can model a lot of things that we care about as programmers, so even though we can't model all of it, it still has merit. If what he is referring to is that type systems are somehow "separate" from the outside world, then it seems somewhat like saying that mathematics is a wholly abstract field. Still, though, applied mathematics has been incredibly successful.
After psnively's reply, Rich decides to throw a tantrum (read: "bow out").
Isn't type erasure just a rather limited subclass of compiler optimization, and as such comes "for free" without having to explicitly code for it? The compiler frontend can leave in all type checks, having most of them can be removed by the optimizer, the same way you can remove any sort of redundant check (a default case in a switch statement over an enumeration, etc, etc)
That being said, general type erasure can have (massive) problems. Look at Java.
I'd say Java's type erasure has on the whole been massively successful (and it's allowed integration with e.g. Scala that a more reified type system might make difficult). What do you see as wrong with it?
Personally, I wish that type systems allowed for arbitrary pure (as in "same input -> same output") code to define what is and isn't a valid instance of a type at compile time.
Being able to declare a function that is only valid for, say, power of two inputs (say: a hashmap's initial size, when the hashmap is using a bitwise and for wrapping) and having it actually enforced at compile time would be very useful.
Any such system would need a theorem prover that's powerful and easy to use, and such a prover doesn't exist. For example, to implement an algorithm that involves arrays and indices, you'd need to supply machine-checkable proofs that all indices involved in the algorithm are valid for their respective arrays. That's really difficult, e.g. you can try to come up with some static reasoning scheme that would work on this algorithm:
The original paper on this topic is Hongwei Xi's "Eliminating array bound checking through dependent types", http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf . You will note that he failed to remove all bound checks in the algorithm, even though he started out with a good language (ML), added many manual annotations, and used a sophisticated method of automatically proving theorems. Also, his method and most subsequent methods will fail on any problem that involves multiplication of integers to get array indices, e.g. addressing a rectangular array as a[i*n+j], because integer arithmetic with multiplication is undecidable and even simple instances make the computer cry.
This is a hard research problem. If you come up with a language design that is guaranteed to be memory-safe, eliminates array bound checks in most realistic use cases, and can be used by regular programmers, you will be hailed as a hero. I'm not exaggerating at all.
In general, what you want to be able to mix types and values are dependent types (see languages such as Coq, Agda, Idris). However, dependent types are way too powerful, and as such extremely difficult to use.
A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return types. As refined types are way more limited than full dependent types (essentially, linear arithmetics, logic, and simple stuff like this), you don't always need to write the proofs manually but can use an automated theorem prover such as Z3.
This is a hot research topic. There are attempts to do type inference for refined types - see [1] and [2]. The Liquid Haskell team is also exploring the issue of dependent types and laziness [3]. Below you mentioned that you want "soft casts" as well - check out [4], which attempts to do just that (implemented in language Sage [5]).
I'm very interested in this topic as well, and have experimented a bit [6]; as it turns out, it's not that hard to implement a basic type-checker for simple refined types. It's also quite powerful - using Z3, even non-linear problems such as rectangular array access (mentioned by a poster below) are solvable, since you can trivially prove its safety using real arithmetics (which is decidable).
The only big disadvantage that I see is the difficulty with dealing with state, but then again, even programmers can't reason about it properly; I mean, if `x` is a mutable object, can you really say `if x.a != 0 then 1 / 0` and be sure that no-one will modify `x.a` in the meantime from another thread? I hope that linear types could help.
Your example is perfectly possible to implement in most languages; you just can't expect to give a function an arbitrary run-time integer value and have its validity checked at compile time :) So, the type would have to look something like this:
class IntegerPowerOfTwo {
private int exponent;
public IntegerPowerOfTwo(int exponent) {
this.exponent = exponent;
}
public int toInt() {
return 1 << exponent;
}
}
If you want a compile-time conversion from a constant integer to an IntegerPowerOfTwo, it is possible with C++, for instance, although you need a bit of template metaprogramming.
You can do that in Scala (though it won't necessarily be easy). Just require an implicit parameter that witnesses whatever constraint you want, and define basically functions at the type level that supply it.
"Whether your programming language "embraces" types or has a modern type system or not, these concepts are central to how programs execute, because they are a fundamental part of how computation works." - what are "modern" type systems?
Was something new invented in the last 15-20 years that I had missed?
The discussion of types here is all over the place. This is because they are handled so differently in various programming languages. Pascal included array bounds in the type annotation for arrays and subscripting was enforced (at runtime) to be withing bounds. In C (and C++) arrays are almost equivalent to pointers (the full answer is complicated see [1]) and there is a real danger of buffer overflows. Python doesn't include type annotations, but the run-time enforces strong typing, lists carry their type information and will throw an exception if subjected to a non-list operation. The type system in Haskell is perhaps the best example of a really expressive and really effective system for ensuring that the compiler can catch as many error as possible at compile time.
Haskell programmers sometimes say that if a program compiles it almost always works. This is interesting, but unfortunately, types and type annotations in use today don't fully capture the formal specification needed to guarantee program correctness.
Just writing down specification in preparation for a proof of correctness can be difficult. The specifications have to be expressed in a formal system, for example some form of mathematical logic like predicate calculus. Working with anything less than a formal specification is like trying to solve a mathematical set of equations without using math symbols. Natural language is just inadequate to the task. See [2].
Getting the specifications right isn't easy. I remember my first attempt at proving the correctness of a sorting program. I understood that I needed to insure that A[i] <= A[i+1] for all elements in the array, but I forgot that the final result had to include all and only the original elements (i.e. that it had to be a strict permutation of the input elements). I don't believe that type systems are currently useful for these kind of specifications and verifications of program correctness.
Real programs interact with the outside world (e.g. GUI's are hard to describe mathematically). Real programs often have distributed or concurrent execution for which new logics (like Temporal Logic) may have to be employed. Proving that a program will terminate or make progress or not deadlock or not livelock or will meet some real-time constraints are all exceptionally hard.
Many years ago (in the 1980's) I worked on this research area at University. I had the hope that eventually, programming would be more like an interactive exploration with a sophisticated program prover. I thought that the programmer and software-prover would work together to produce a correct program. Today, we are still programming in pretty much the same old ways as back then. The languages are much better, but it's a harder problem than I thought it was going to be.
[+] [-] ufo|11 years ago|reply
But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system.
There is also a minor thing that came to my mind. Types are most often associated with intuitionist logics, which are about constructive provability, as opposed to classical logics, which are about "truthyness" so the title of the post is a bit misleading :)
[+] [-] dllthomas|11 years ago|reply
In theory, yes - I came here to make that same objection.
In practice, there arises the question of whether such terms are actually ever encountered for a given type system when solving realistic problems.
[+] [-] dicroce|11 years ago|reply
This article was essentially saying: "You can remove the forms when you are done and your sandcastle will still stand."
[+] [-] taeric|11 years ago|reply
[+] [-] dkarapetyan|11 years ago|reply
[+] [-] takeoutweight|11 years ago|reply
But maybe I am misunderstanding your comment? Perhaps you were just equivocating over what "really there" means? If that's the case, is multiplication not "really there" because it can be implemented in terms of bit shifting and addition? We don't imagine multiplication as somehow putting these restrictions on what we can do with our bit shift operators -- the multiplication is the "real" thing we care about and the binary operations are incidental.
In any case, see the famous parable that opens Reynolds' "Types, Abstraction, and Parametric Polymorphism" for a colourful example of ignoring the underlying data representation:
http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types...
[+] [-] mtdewcmu|11 years ago|reply
[+] [-] kvb|11 years ago|reply
[+] [-] TheLoneWolfling|11 years ago|reply
[+] [-] juliangamble|11 years ago|reply
[+] [-] pinealservo|11 years ago|reply
Assuming you have some sort of specification for your program, you can use a formal system (such as a static type system) to describe aspects of the specification. It's up to you to correctly model the requirements in the system, but it's similarly up to you to model the requirements of the system in your (far larger and more complex) program. The types ensure that the program fits the aspects of the specification you were able to describe with them.
[+] [-] gargantuan|11 years ago|reply
[+] [-] Dewie|11 years ago|reply
After psnively's reply, Rich decides to throw a tantrum (read: "bow out").
[+] [-] webmaven|11 years ago|reply
[+] [-] mrbbk|11 years ago|reply
[+] [-] ludicast|11 years ago|reply
webmaven was here longer so my money is on his time being up.
[+] [-] TheLoneWolfling|11 years ago|reply
That being said, general type erasure can have (massive) problems. Look at Java.
[+] [-] lmm|11 years ago|reply
[+] [-] TheLoneWolfling|11 years ago|reply
Being able to declare a function that is only valid for, say, power of two inputs (say: a hashmap's initial size, when the hashmap is using a bitwise and for wrapping) and having it actually enforced at compile time would be very useful.
I mean, even range types are useful.
[+] [-] cousin_it|11 years ago|reply
http://en.wikipedia.org/wiki/Knuth%E2%80%93Morris%E2%80%93Pr...
The original paper on this topic is Hongwei Xi's "Eliminating array bound checking through dependent types", http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf . You will note that he failed to remove all bound checks in the algorithm, even though he started out with a good language (ML), added many manual annotations, and used a sophisticated method of automatically proving theorems. Also, his method and most subsequent methods will fail on any problem that involves multiplication of integers to get array indices, e.g. addressing a rectangular array as a[i*n+j], because integer arithmetic with multiplication is undecidable and even simple instances make the computer cry.
This is a hard research problem. If you come up with a language design that is guaranteed to be memory-safe, eliminates array bound checks in most realistic use cases, and can be used by regular programmers, you will be hailed as a hero. I'm not exaggerating at all.
[+] [-] tomp|11 years ago|reply
A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return types. As refined types are way more limited than full dependent types (essentially, linear arithmetics, logic, and simple stuff like this), you don't always need to write the proofs manually but can use an automated theorem prover such as Z3.
This is a hot research topic. There are attempts to do type inference for refined types - see [1] and [2]. The Liquid Haskell team is also exploring the issue of dependent types and laziness [3]. Below you mentioned that you want "soft casts" as well - check out [4], which attempts to do just that (implemented in language Sage [5]).
I'm very interested in this topic as well, and have experimented a bit [6]; as it turns out, it's not that hard to implement a basic type-checker for simple refined types. It's also quite powerful - using Z3, even non-linear problems such as rectangular array access (mentioned by a poster below) are solvable, since you can trivially prove its safety using real arithmetics (which is decidable).
The only big disadvantage that I see is the difficulty with dealing with state, but then again, even programmers can't reason about it properly; I mean, if `x` is a mutable object, can you really say `if x.a != 0 then 1 / 0` and be sure that no-one will modify `x.a` in the meantime from another thread? I hope that linear types could help.
[1] http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf
[2] https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf
[3] http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pd...
[4] http://www.kennknowles.com/research/knowles-flanagan.toplas....
[5] http://sage.soe.ucsc.edu/sage-tr.pdf
[6] https://github.com/tomprimozic/type-systems/tree/master/refi...
[+] [-] Sharlin|11 years ago|reply
[+] [-] Ixiaus|11 years ago|reply
[+] [-] lmm|11 years ago|reply
[+] [-] eudox|11 years ago|reply
You two could hit it off or something.
[+] [-] CmonDev|11 years ago|reply
Was something new invented in the last 15-20 years that I had missed?
[+] [-] todd8|11 years ago|reply
Haskell programmers sometimes say that if a program compiles it almost always works. This is interesting, but unfortunately, types and type annotations in use today don't fully capture the formal specification needed to guarantee program correctness.
Just writing down specification in preparation for a proof of correctness can be difficult. The specifications have to be expressed in a formal system, for example some form of mathematical logic like predicate calculus. Working with anything less than a formal specification is like trying to solve a mathematical set of equations without using math symbols. Natural language is just inadequate to the task. See [2].
Getting the specifications right isn't easy. I remember my first attempt at proving the correctness of a sorting program. I understood that I needed to insure that A[i] <= A[i+1] for all elements in the array, but I forgot that the final result had to include all and only the original elements (i.e. that it had to be a strict permutation of the input elements). I don't believe that type systems are currently useful for these kind of specifications and verifications of program correctness.
Real programs interact with the outside world (e.g. GUI's are hard to describe mathematically). Real programs often have distributed or concurrent execution for which new logics (like Temporal Logic) may have to be employed. Proving that a program will terminate or make progress or not deadlock or not livelock or will meet some real-time constraints are all exceptionally hard.
Many years ago (in the 1980's) I worked on this research area at University. I had the hope that eventually, programming would be more like an interactive exploration with a sophisticated program prover. I thought that the programmer and software-prover would work together to produce a correct program. Today, we are still programming in pretty much the same old ways as back then. The languages are much better, but it's a harder problem than I thought it was going to be.
[1] http://stackoverflow.com/questions/3959705/arrays-are-pointe... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/E...
[+] [-] pfh|11 years ago|reply
[deleted]