Lambda the Ultimate

At the bottom of channel 9 articles, just above the beginning of the comments you'll see some icons for MP4 and WMV files. The WMV(high) works for me on Ubuntu.

Off-topic:

Put an & in front of your lt or gt and a ; behind it. &gt; becomes > and &lt; becomses < (i.e. just use the normal HTML entities).

On-topic:

I heard there is a language called TLA that does something similar, but I have't looked at it, so I may be wrong

Pascal (and I think Ada) had an explicit notation to define the range for types:

type MYVAR is range 0 .. 100;

One could consider any finite number to be a type of set which could be typed as an enumeration. Of course, if the range is fairly large, the definition could get rather longish and be effectively unattainable. Also, the optimization techniques wouldn't be near as effective. One could try to make the argument that these things are not statically checkable. But then divide-by-zero and underflow/overflow are not usually circumvented (short of developing a full blown dependent type system).

Anyhow, the difference between types defined through explicit type annotation and types defined through contracts is that one is statically verifiable, whilst the other can only be checked while in the midst of running the code.

I guess I should note that types can be much more complicated than simply clamping the range. For example, the classic case is the set of prime numbers.

Yes, Ada allows a variety of constraints to be included in type declarations. However, note that things like range are not always statically verifiable (for obvious reasons). This is why formally the type declaration creates a type (which is checked statically) and a constrained first subtype of the type which is constrained to the right range. Subtype checks are not always static.

That is what dependent types do. Basically, contracts are a workaround for the lack of dependent types. Instead of static verification, they (usually) check the properties in question at runtime (with the respective limitations).

I think the big difference with contracts that are dynamically checked is that they give you confidence when working with untrusted and remote resources.

I fear that one of the unfortunate beliefs in the statically typed, type inferring functional language crowd is that we will some day get over bytes and be able to construct statically checked network programs that work with typed values instead. Essentially, we end up with all network programs being partial functions on strings with relatively narrow domains. Hello, exceptions!

A simple example of this kind of over-simplification is Haskell's read, which accepts a String and produces a value or a crash depending on the String. From a reliability standpoint, it is much nicer to work with variants of read that are total but require the programmer to handle a compound error/result type.

I don't mean to argue that all functions should be total or that type-checking does not buy us anything -- indeed, it buys nearly everything you can get on a single computer. Runtime checks buy us something dependent types can't -- safety from adversaries.

It is perfectly possible to handle exceptional cases and still give statically checked guarantees. Just work in an exception monad: the dynamic check either produces a proof of the static property or an exceptional case. The rest of the program can the assume the property to hold. Is that not good enough?

Really, you do not give me enough credit. In my post, I give an example of statically checking that one handles exceptional cases.

My point was that the dynamic checks that fall out of contracts can not be done away with through a stronger type system like dependent types. Some of those dynamic checks are there for reasons of distrust as well as program correctness.

Sorry, I misinterpreted your comment as saying contracts were in some way "more applicable" than dependent types, my apologies. What are these dynamic checks that fall out of contracts precisely, could you give some examples?

For example, if your contract is checking a genuinely dynamic property, then obviously it can't be turned into static verification. For example, we could write a contract to ensure that a piece of code is only run on Tuesdays -- this is obviously something we can't check via dependent typechecking, because typechecking can only depend on the program itself, and not on external facts like the day of the week.

Of course, we could write a dependent type which requires all of its inhabitants to check dynamically whether it is Tuesday!

I just meant that a dynamic check can be embedded into a dependent type, so it is equally applicable. I made the assumption that properties are always "static", modulo monadic plumbing needed to express properties dependent on the Real World, the execution of the program etc.., maybe that's wrong.

For example, we could write a contract to ensure that a piece of code is only run on Tuesdays -- this is obviously something we can't check via dependent typechecking, because typechecking can only depend on the program itself, and not on external facts like the day of the week.

Actually, I wouldn't be surprised if it was possible to come up with some fancy modal type or effect system that can check something like that.

Runtime checks buy us something dependent types can't -- safety from adversaries.

Proper runtime checks aren't guaranteed to be run. Dependent types can ensure that the appropriate runtime checks are indeed run. "Runtime checks or typing" is a false dichotomy. If anything, typing can make runtime checking even safer.

"Runtime checks or typing" is a false dichotomy.

Yes, I did not meant to suggest otherwise. I have been on #haskell at times when people have floated the notion that more elaborate type-checking, coupled with certification, could save us from the FFI and the vagaries of file I/O. The idea that contracts could be done away with via dependent types seemed to be in the same vein -- hence my one-sided remark.

Proper runtime checks aren't guaranteed to be run. Dependent types can ensure that the appropriate runtime checks are indeed run.

That is the perspective I meant to promote.

Contracts can indeed be done away with where a sufficiently rich dependent type system is available. At least in principle. I/O and FFIs are no counterexamples to this claim - they are simply examples of places where such a type system is not available (until OSes and their APIs and file systems are put under the discipline of such types, too, which, of course, is largely hypothetical...).

At least in principle, I/O and FFIs are no counterexamples to this claim - they are simply examples of places where such a type system is not available (until OSes and their APIs and file systems are put under the discipline of such types, too, which, of course, is largely hypothetical...).

I'm not sure how much an OS can guarantee. I guess it can promise not to send us garbage; but in the event of a hardware fault it would have to send us an error. An on-disk list and a plain old list must retain distinct semantics.

With network services, we deal with components that advertize a certain discipline but can not be known to actually follow it. It is most desirable to be able to demonstrate, beyond a shadow of a doubt, that we have written or employed checks for every failure case that results from the mismatch between our expectation that data should be whole and on-time and the network's lame (but super cheap and generally good enough) promise to send us garbage at its leisure.

Though I would rather demonstrate that sort of thing with the richest type system I can get my hands on :)