Or provide guarantees at the type-level, such that when a particular value is constructed, it is checked that certain properties hold thereafter, e.g. int -> nat. Why should you have to duplicate assumptions about a type when it can be encoded in the type itself.
type nat = int x where x >= 0;
type defined<t> = t x where x != null; // of course here we'd prefer that defined<t> was the default for all t
This would enable invariants by construction. And some more ideas -
type const<t> = const<t>; //compiler magic, ensures constness (or define at member level via some syntax)
type clean<t> = clean<t>; //compiler magic, ensures purity (no exceptions, etc.)
type pure<t> = transitively<clean<t>>; // transitive compiler magic
I can see this syntax and semantics compile at least partially down to library annotations using System.Diagnostics.Contracts. And it appears somewhat more useful that just pre- and postconditions.
Also
public t pct<t>(t x) where x >= 0 and x <= 100
...
In this case we define t in the function definition itself and expect the compiler (compile-time or run-time) to check that x >= 0 && x <= 100 holds for all x of t. This function will also return values of an "anonymous" type t which will have the desirable properties or fail predictably when they break.
And finally
type purecsharp = transitively<clean<csharp>>; // compiler magic that transforms a C# compiler value into a transitively clean C# compiler value; all you do then is write to disk and start using!
ASP.NET: Presenting in Europe Next Week
WindowsClient: You know your post rate has gone down...
Silverlight: Geek Profiles – Scott Guthrie
