Types Are The Truth

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 :)

dllthomas3• 12 years ago

"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.

comex3• 12 years ago

For most type systems, they certainly are: most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc. that a compiler for a typical high-level language cannot emit under any circumstances (without being ridiculously intelligent). Languages like ATS and C-plus-formal-verification mostly avoid this problem at the expense of being really hard to write.

ufo5• 12 years ago

My impression is that these type system limitations start showing up once you need to mix and match different type systems. For most terms there is a reasonable type system that will type it but when you scale up to your whole program/system then any single type system might not be able to cover all the terms that you want to write. Some type system features such as parametric polymorphism, subtyping, intersection types, linear types, etc are hard to mix in practice, especially when you worry about decidability and type inference.

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).

steveklabnik5• 12 years ago

I would actually argue the opposite: in theory, there is a type system that describes every system, even 'untyped' ones, which are really uni-typed.

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...

marcosdumay• 12 years ago

Well, in practice we write programs that behave well within the type system we are using. Thus, no, you won't find those very often, but it also does not mean that there is no problem.

dkarapetyan3• 12 years ago

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.

mtdewcmu6• 12 years ago

I wonder if type erasure is profound, or if it only sounds profound after being hypnotized by type theory.

dkarapetyan3• 12 years ago

Don't get me wrong I think type theory is really cool. In fact any kind of theory that makes me a better programmer is cool. That's one of the reasons TypeScript right now is one of my favorite languages. It is the perfect balance between the prototyping power of dynamic languages and the awesome static guarantees of statically typed languages. The best part is that the type system does not get in the way when I'm prototyping and actually starts to help out when I have the design fleshed out. I just wish more languages supported that kind of type system because sometimes I really miss the static checks when writing stuff in Ruby and Python.

dsuth2• 12 years ago

I couldn't decide whether this was an incredibly deep post that I'm missing, or just a very obvious by-product of compilation.

TheLoneWolfling12• 12 years ago

Case in point: try to do the fast inverse square root hack with a (truly) strongly typed language.

phaedrus• 12 years ago

If the language supports union, then simply give your working variable the type of "union { float, long }". This directly expresses the idea that you're working with a piece of memory that is used for two purposes.

gsg2• 12 years ago

What's the difficulty, exactly? You need some mundane float->bits and bits->float operations, which are commonly although not universally provided in strongly typed environments. The rest is integer ops.

takeoutweight• 12 years ago

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:

http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types...

dkarapetyan3• 12 years ago

If you're doing mathematics then multiplication is the thing you care about and not its representation in any given number/notation system but if you're actually implementing multiplication then you definitely care about the actual bits and bytes. What structure you impose on top of the implementation to make it easier is all nice and well but don't fool yourself into thinking that types are the end of it. In fact to truly impose some kind of type structure so you could reason about what was going on at the hardware level you'd need more than just the integer type or the floating point type because those types don't let you reason about overflow/underflow at such a high level. Any correct implementation would need to worry about those restrictions and consequently would have to represent those restrictions in the type system.

kvb• 12 years ago

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).

eudox• 12 years ago

The site is eerily similar to http://www.jonmsterling.com/index.html

You two could hit it off or something.

dicroce• 12 years ago

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."

taeric2• 12 years ago

By that same analogy, building up a sand castle by only using those molds is a ridiculously hard way to build some castles.

Lambdanaut• 12 years ago

Fortunately some languages allow you to construct your own custom molds within the language itself.

TheLoneWolfling12• 12 years ago

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.

I mean, even range types are useful.

Ixiaus• 12 years ago

Dependent Types? Check out Idris.

TheLoneWolfling12• 12 years ago

I shall have to.

That being said, I don't care much for Haskell-based syntax.

cousin_it3• 12 years ago

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:

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.

TheLoneWolfling12• 12 years ago

Well, the thing is, anything would be better than what we have currently.

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.

Dewie4• 12 years ago

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'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.

TheLoneWolfling12• 12 years ago

Elaborating on my previous reply.

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.

lmm2• 12 years ago

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.

ixmatus2• 12 years ago

You can do "kind of" dependent types in Haskell too but it's an ugly mess (like trying to do it in Scala). Idris handles it really well for general programming tasks.

Sharlin2• 12 years ago

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.

groovy2shoes• 12 years ago

I'm not sure why you're being downvoted. This technique is not entirely unlike using a phantom type, which is a common way of encoding such constraints into the type system.

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.

Sharlin2• 12 years ago

I'd like to know why this was downvoted. (Edit: other than the fact that the exponent should be unsigned int :/)

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

then you write a type that only provides operations that maintain the constraint. In this case, for instance, construction from k and multiplication by another T. As I said, some languages like C++ do also allow things such as compile-time conversion of an unconstrained constant integer into a power-of-two integer, with a compile error if the constraint isn't satisfied, but in my opinion that's mostly syntactic sugar. Would be nice if you could simply write, say,

    type intPowerOfTwo = unsigned int where ∀intPowerOfTwo n: ∃unsigned int k: n = 2^k

but what about the unsigned int operations, such as addition, that do not maintain the invariant? Should the type system include a general theorem prover that can deduce which operations are allowed?

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...

tomp3• 12 years ago

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.

[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...

ufo5• 12 years ago

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

I had never seen it written that way. What can full dependent types do that you can't do with refinement types?

TheLoneWolfling12• 12 years ago

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.

lmm2• 12 years ago

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?

TheLoneWolfling12• 12 years ago

Too much wrestling with generics.

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>.

juliangamble• 12 years ago

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...

Dewie4• 12 years ago

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").

gargantuan• 12 years ago

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...?

mcosta3• 12 years ago

I am pretty sure with a elaborate enough system with alias-forbidden types and resource managers you can do it.

with file.open as f do .... alias = f // fail done // autoclose

But then, is it really necessary?

evincarofautumn• 12 years ago

Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode:

    // 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

“open” grants the “read” and “close” permissions to “f”; “close” revokes the “read” permission that “getline” requires, causing “getline” not to typecheck.

salmonellaeater• 12 years ago

You could certainly handle that kind of error using a type system. There could be a scoping rule where certain kinds of operation (i.e. close file) put the reference to the object out of scope. The way Haskell chains I/O operations using monads is another way: the result of the 'close file' operation is basically a world that doesn't contain a reference to the file.

pinealservo3• 12 years ago

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.

CmonDev• 12 years ago

"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?

todd8• 12 years ago

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.

[1] http://stackoverflow.com/questions/3959705/arrays-are-pointe... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/E...

Types Are The Truth

Related Stories