## Microsoft PDC "Language" Talks

Surprised to see there hasn't been a mention of Microsoft's recent PDC. They have some interesting talks available on the web.

There are a couple of videos on "Oslo," their DSL framework. Discussion of finding bugs in concurrent programs. An introduction to F#. For me, the most interesting, and the most unexpected talk was on contracts being integrated into .NET as a library. These pre/post conditions and invariants can be checked at compile time and another project "Pex" can use them to generate unit tests.

## Comment viewing options

### I agree. We need more

I agree. We need more coverage of this.

There are several good blog posts about M but I haven't managed to collect them for a story here yet. Any help is appreciated.

### M Intro

There's a good M intro (conversational piece with whiteboarding and even the creation of Channel 9 DSL using M) on C9 with Don Box, Chris Anderson and new M team member and languages veteran Paul Vick (of VB fame) on Channel 9. Here's the link For alternate versions please just hover over the Downloads link below the video. We offer multiple versions of media files which should work on several platforms. This is by design :) And here is a direct link to PDC2008 language sessions on Channel 9. Enjoy! One of my favorites is the Future of Programming Languages panel. C

### Here's a short screencast

Here's a short screencast that I found useful.

### Does the videos skip for

Does the videos skip for somebody else ? I'm running Silverlight 2.0 on OS X 10.5.5

### MP4, WMV

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.

### contracts vs types

Variables can be given a type as follows:

int x;

Contracts also limit the values x can take on:

Contract.(x > 10);//whatever the right syntax is
//gt, lt are greater than, less than, respectively...html eats actual symbols

Aren't contracts just a generalization of types?

In other words, if a language was being designed from scratch, could
types be defined as follows:

type int = Contract.(x > 2147483647 && x < -2147483647);
int x;

How about function types? Generics (list of integers or list of lists of string)?

edit: Thanks matthias, changed lt/gt signs

### Off-topic:Put an & in front

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 types

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

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.

### Dependent Types

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

### Contracts & Distributed Systems

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.

### Nope

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?

### Tangential

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.

### Misunderstanding

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?

### How contracts are "more applicable"

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!

### Precisely

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.

### Actually

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.

### I have served the devil too well...

"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

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

### Such A System Is Not Available For My Toaster

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