Summary
I am wondering out loud whether a contract can be completely expressed as a type (or type class) in a language with a sufficiently advanced type system.

---

Advertisement

There are clear parallels between types and contracts. For instance, an unsigned integer can be viewed as an integer which maintains the invariant of always being greater than or equal to zero. The only substantial difference I can think of is that types are usually resolved entirely at compile-time while contracts often have assertions that can only be resolved at run-time.

The question that I am pondering is whether I can bridge the two by adding type-safe casting operations to the definitions of types. Perhaps by using some form of type-class, or concept.

Consider the following function grow_list which takes a list and appends an element to it a specified number of times:

define grow_list : (a:list x:value n:uint) -> (b:list)
{
  [[dup [append] dip] dip dec] [dup neqz] while pop pop
}

(note: this is not yet implemented on the Cat compiler!)

If the implementation is meaningless to you, it isn't very important, but it is pretty much the same as Joy.

The question is, should I express the postcondition as part of the type expression? The postcondition can be expressed in pseudo-code:

[{ b size } { a size n + } eq]

Note that you can name arguments for the purpose of type expressions, but not as part of the implementation. The curly braces have actually no meaning, and are simply there to help clarify the structure of the program. So there are two questions here:

1. should the type system capture postconditions and other constraints
2. if so then what should the mechanism be for expressing constraints?

I am currently of the feeling that behavioral constraints should be expressed in the type system. I am playing with the current ad-hoc notation:

define grow_list : (a:list x:any n:int)->(b:list) 
  <: [{ b size } { a size n + } eq]
{
   ...
}

Anyway, this is as far as I've managed to get so far today. I'd appreciate any opinions shared on the issues presented.

Talk Back!

Have an opinion? Readers have already posted 38 comments about this weblog entry. Why not add yours?

RSS Feed

If you'd like to be notified whenever Christopher Diggins adds a new entry to his weblog, subscribe to his RSS feed.

Digg | del.icio.us | Reddit

About the Blogger

Christopher Diggins is a software developer and freelance writer. Christopher loves programming, but is eternally frustrated by the shortcomings of modern programming languages. As would any reasonable person in his shoes, he decided to quit his day job to write his own ( www.heron-language.com ). Christopher is the co-author of the C++ Cookbook from O'Reilly. Christopher can be reached through his home page at www.cdiggins.com.