Types Are The Truth
michaelrbernste.in
michaelrbernste.in
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 :)
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.
I'm not sure what you're saying here with the "corresponding to" - obviously you can write "unsafe pointers", unions, etc, right in C, and I've not really ever encountered inline assembly for the purposes of subverting the type system. I'll respond to more of your content when I'm confident I've understood you (which I don't mean as a brush off...).
EDIT: I think the difference here is between 'types' and 'tags'. Types are at compile time. Tags are at runtime.
The article talks about translating from a typed lambda calculus to the untyped variant. Real compilers typically translate from the original typed AST gradually through multiple IRs to assembly, which is more complicated since they're changing the form of the program rather than just dropping type annotations, but is generally analogous. What I care about is whether there are programs with "terms" - instruction sequences - which correspond to useful programs which cannot be "typed" in a particular language, i.e. they cannot be produced by a compiler following any kind of straightforward procedure to lower from that language. Of course you can always come up with an equivalent program as long as the language is Turing complete; in particular, just as untyped lambda calculus can also be considered unityped, you can do something like Emscripten where you mechanically translate low level IR into a tiny subset of a higher level language, and maybe the compiler will optimize that subset. But that's not that interesting, because the general case is changing the program to a completely different one, and the special case removes all of the benefits of the type system. Additionally, you can have a language like Rust that lets the programmer poke holes in the type system, which is useful in practice but makes the type system no longer guarantee what it says it guarantees.
So, of course, with these limitations, not only are there correct programs which typical, non-dependent type systems cannot express, but, judging by the high performance of C (which has a type system, but one that provides barely any guarantees and thus has barely any limitations) in practice, these programs are quite common and useful in practice. Dependent type systems, along with their Curry-Howard mirror of theorem provers for low-level languages, can almost always make up for this (though by Gödel's incompleteness theorem there is some correct program somewhere that they can't prove correct), but they're a relative pain to program in and for that reason are uncommon in practice. Or to put it another way, you have a choice between delegating verification of complex properties about programs (the types which are there whether you want them to be or not) to computers, which have rather poor insight, or to humans, which are notoriously unreliable. The ultimate type system is a general AI you can explain the situation to in English.
FWIW, Rust has a pile of behaviours that are undefined behaviour[1]: that is, the compiler will optimise/reason assuming they never happen. These are impossible to hit in safe code, but are possible with `unsafe`, it's up to the programmer to manually maintain them. That is, the type system does guarantee certain things, and it's up to the programmer to not break it inside `unsafe`.
[1]: http://doc.rust-lang.org/master/rust.html#behavior-considere...
I think this is one of the reasons why dynamic languages are popular. It kind of lets you mix different programming styles in a single program, at the cost of laxer type checking (something I hope will get better in the future).
All dynamic typing gets you is that you can ignore this fact, and then hit it head on when you make a mistake.
It is possible to give programs that are truly dynamically typed, but they are not "real" programs. What can you do to a variable with zero information on what it contains ? Not much : return it, pass it around, ... that's about it.
The real complaints are mostly about two things
1) it's hard to know what type an input parameter should be, so I just don't. This is just not a valid complaint. But type inference helps a lot here. Generic programming catches the other usecases.
2) many languages make it really hard to correctly specify types. This is a language flaw. Dynamic typing can be an improvement over C code, but not over Haskell code. Other languages are somewhere in between.
Sometime, it's another flaw that may exist : the standard libraries are not correctly thought out to have a good algebraic structure (e.g. correct IS-A relationships for all number types, and the ability to generalize over them)
These complaints basically boil down to people having constructed wrong type systems. It's a flaw in many, many languages. Python and Haskell are the only ones I know to get it close to right.
3) You want to eval() in your program (or, for example, read in arbitrary json). If you're doing this, you're doing something wrong. Even if you do manage to isolate things correctly (history says you are unlikely to get this right), you're open to trivial DDOSing.
In practice, there are often types that your type system can't express. I didn't start to really grok this till I saw dependent types.
Then again, I am an amateur type theory enthusiast...
My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.
A weaker version of his thesis, which could still support his original phrasing in the GGP, would be "for any correct program, there exists a type system in which it can be typed [though we might not be able to find it]." That doesn't seem to be ruled out, and sounds plausible, though I don't know of any specific results on it.
This article was essentially saying: "You can remove the forms when you are done and your sandcastle will still stand."
Indeed, I think the analogy has pretty good legs. Consider, if you are working with cast iron, molds are the way to go.
Compiled languages are like building a bunch of plaster mold, and then just doing the castle in one step.
Optional typing, or using Any types and casting, is like using molds for a nice foundation, and using your hands to add little bits on top.
Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things.
edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
What you can bet is that absolutely no-one is excited about mission-critical software failing because of a bug that could have been caught by testing... or type checking.
If you scanned through a program looking for syntactic forms that represent types as such, you could find clear examples of such syntax in most programs; some programs would have more and some less, probably determined to a large extent by programming language. It would be things like variable declarations, class declarations, etc. -- essentially declarative scaffolding, which wraps and adds meaning and context to code that does things; the type code itself, though, generates no cpu instructions, because its purpose isn't to represent action, it's orthogonal to action.
You could argue that type code causes actions to be performed, such as when types need to be casted, which may trigger some kind of transformation on the underlying data. But, even though the type helps trigger action (the data transformation), the type is not that action.
I don't know if what I've written will make sense or sound like empty nonsense... but the article itself makes the point that you will generally not find types in machine code; at most you can find indirect evidence that they were there.
You may say, "what difference does that make? Why make the distinction?"
Well, machine instructions are what make the computer do observable things. Any code you have to write that doesn't produce instructions needs to be justified somehow. There are lots of ways of justifying such extra code. But it's orthogonal to actually doing things -- pretty much by definition.
Edit -- to respond more directly: >>What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable).
I think that's a real risk. People tend to get attached to ideas about programming languages in quasi-religious fashion; I think it's healthy to stay in touch with an objective cost/benefit perspective, though. The user doesn't see the code, he/she only sees the results. And the experience of the user is what you should focus on as a programmer -- right?
>>Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things.
I'm not sure I follow the distinction you're making, between the textual representation of the code and -- what? Clearly the text has to be written before the computer will do anything -- so it must be important.
>>edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
I said types don't do anything, and that they don't excite me. I didn't say we should get rid of all types. Tests don't do anything, either (at least, they don't do what the program should do). Tests also don't excite me. That doesn't mean that testing is pointless. Testing can be costly and tedious -- but you have to weigh that against the risk of bugs getting through.
> Well, machine instructions are what make the computer do observable things.
The typechecker is a program, and if the typechecker fails, you will see output.
Typecheckers definitely do things. But are those things interesting?
That seems like asking "seat belts definitely do things, but are those things interesting?"
So, thanks for the well wishes, but in this case I don't think they're needed: any reasonable compiler should be able to do this without great difficulty.
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...
Types in general can be far more expressive than most people know. Very expressive types are not necessarily easy to work with, though.
After psnively's reply, Rich decides to throw a tantrum (read: "bow out").
* open file
* close file
* read form file
with file.open as f do .... alias = f // fail done // autoclose
But then, is it really necessary?
// open : string -> file_mode -> (f : file) | f @ read * f @ close
f = open "input.dat" Read
// close : (f : file) | f @ read * f @ close -> ()
close f
// getline : (f : file) | f @ read -> string | f @ read
s = getline f
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.
Have you also been confused with http://hci.stanford.edu/msb/ or http://michaelbernstein.biz/ and even http://www.mabfan.com/ at SF conventions? ;-)
webmaven was here longer so my money is on his time being up.
(I'd actually put my money on old age and treachery vs. youth and skill if I were you)
That being said, general type erasure can have (massive) problems. Look at Java.
For example, having to use a varargs hack just to make a T[] (that's an array of a a generic type).
Or not being able to call T.class
Or not being able to use instanceof T.
Or having a Object[] that crashes at runtime when you try to put an Object in it.
Or not being able to overload a method based on if it's passed a List<Foo> or List<Bar>. (Also applies to interfaces like Comparable, etc. There's no good way of going "this is a Comparable<Foo> and a Comparable<Bar>, but not a Comparable<Baz>.)
Or for that matter, trying to pass an int[] to something that expects an Integer[], or vice versa.
Or for that matter, someone passing in a List into your parameter expecting List<Foo> and crashing at runtime because it actually was a List<Bar>.
One thing you learn using java is not moving arrays around.
The comparator stuff is true.
Make the compiler to fail if you pass raw classes. A List is not a List<Foo> and in some cases is not a List<?> (where List is a class of <T extends Foo>).
What I miss is some kind of self type, or "return this", I do not know how to tell it. Imagine a imaginary class A:
this aMethod() {
stuff();
return this;
)
B thisIsB = new B();
thisIsB.aMethod().bMethod();And then all of a sudden you have an order of magnitude more memory usage because you have a bunch of Characters as opposed to a bunch of chars.
You end up having to use a collection, which ends up with an order of magnitude more memory usage than an array in the case where you want to store characters. (char is the worst case. But all primitives are pretty bad in that regard.)
Really, a quote I heard once: "Java is like a strawman built specially by people who want to argue against using strong type systems."
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.
That being said, I don't care much for Haskell-based syntax.
The syntax is nice because it enables the programmer to express software in a terse way, generally favoring the types as documentation and a strong mental model to understand the abstraction.
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.
I know that in general the problem is undecidable. But we don't need to solve the entire problem to solve a large chunk of practical cases.
Even a simple runtime cast (with check) / asserting cast (a cast with an assertion that would be triggered at compile time if the compiler can find a valid counterexample, otherwise unchecked) combination would be miles above what we have now in most strongly typed languages.
I'm just guessing, but wouldn't most uses of arrays be in traversing the whole array, ie mapping over the array, folding it etc.? I have seen a ton more
> for i = 0 to a.length -1
then I have seen something like indexing a sorted array like in a binary search. So if these operations are abstracted to functions that don't use array indexing directly, then they could perhaps be proven once in some library. And such a proof seems very straightforward (conceptually, perhaps not realistically) - just prove that your for loop exits when the index i gets incremented to out of bounds of the array.
I think Rust's iterators use no bounds-checked indexing underneath, at least for simple things like mapping over an array. They probably haven't proved that the indexing won't go out of bounds, though, probably just vetted and tested it a lot.
(For those who don't know, an iterator in Rust has a function next() that returns an Option<A>. That allows you to do array bound checking and loop termination checking with a single operation, like when iterating over a linked list.)
Also I've seen a promising paper by Corneliu Popeea: http://gallium.inria.fr/~naxu/research/abce.pdf . It says it works on unmodified C code, doesn't require annotations, and successfully removes all checks in quicksort (!) Kinda sounds too good to be true though, I wonder what's the catch.
That indeed looks promising!
The way I wish things worked:
Programmers code with three types of constraints: soft cast, hard cast, and unsafe cast. Soft cast is a runtime assertion that the constraint isn't violated, hard cast is a "do not compile unless you can prove that this constraint isn't violated" and unsafe cast is a "check at compile time to make sure you cannot provide a counterexample, but do not include a runtime check". Hard cast will be rarely used, for obvious reasons.
Compiler propagates known values / constraints forwards as much as possible, and propagates constraints backwards as much as possible. Note that this generally already happens as part of compiler optimizations. If at any point any value violates a constraint, error out and provide a "constraint trace" of what caused the violation.
After this step, the compiler looks at all unknown-at-compile time variables and randomly (or rather, pseudo-randomly, maybe seeded with the md6 of the file or something to be deterministic) generates and tests values (along with some common values - note that this could be integrated with a test framework built into the language!), ensuring that no constraints are violated. (There are a bunch of optimizations here that I'm not going to mention.) If any constraints are, error out with the variables required to violate the constraint and the values assigned to them.
class IntegerPowerOfTwo {
private int exponent;
public IntegerPowerOfTwo(int exponent) {
this.exponent = exponent;
}
public int toInt() {
return 1 << exponent;
}
}
I'll admit it's not ideal; in fact, it's often downright cumbersome. In some cases, it's not possible to encode desired information into a particular type system.
But in this case, it seems valid to me. There is no way to construct a value of IntegerPowerOfTwo that does not represent a power of two, and therefore it fulfills GP's example requirement.
The whole point of encapsulation is to be able to write data types that have invariants other than those offered by the machine-level types. If you want a type T that satisfies the predicate
∀n∈T: ∃k∈N: n = 2^k
type intPowerOfTwo = unsigned int where ∀intPowerOfTwo n: ∃unsigned int k: n = 2^k
However, I understand this was simply an example and do agree that expressive and powerful type systems are certainly a very useful tool. C++ template metaprogramming (pretty much computing with types as values) is very impressive even if horribly ad hoc and the concepts feature (constrained templates), if ever actually implemented, will make all kinds of things easier.
http://en.wikipedia.org/wiki/Concepts_%28C%2B%2B%29
https://isocpp.org/blog/2013/02/concepts-lite-constraining-t...
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...
I had never seen it written that way. What can full dependent types do that you can't do with refinement types?
However, I can point you to this discussion on Reddit [1]; essentially, one user (kamatsu) is saying that refinement types are not dependent types:
> More or less, if you have sigma and/or pi types, then you have dependent types. If you don't, you don't.
Also, he claims that a crucial difference is that dependent types are proofs, while type-checking refined types requires proof search. Then, another user (neelk) points out an article [2] which claims (I haven't read it) that dependent types can be encoded using singleton types, which can be written using refined types.
[1] http://www.reddit.com/r/programming/comments/26se9k/refined_...
You two could hit it off or something.
Was something new invented in the last 15-20 years that I had missed?
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...