The Artima Developer Community
Sponsored Link

Weblogs Forum
Can Contracts be Equated with Types?

38 replies on 3 pages. Most recent reply: Aug 18, 2006 6:45 AM by Achilleas Margaritis

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 38 replies on 3 pages [ 1 2 3 | » ]
Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Can Contracts be Equated with Types? (View in Weblogs)
Posted: Aug 5, 2006 4:11 PM
Reply to this message Reply
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.


Adi Shavit

Posts: 6
Nickname: adish
Registered: Apr, 2005

Re: Can Contracts be Equated with Types? Posted: Aug 6, 2006 3:51 AM
Reply to this message Reply
Amazing! I was thinking about the same thing in my car this morning!

Jules Jacobs

Posts: 119
Nickname: jules2
Registered: Mar, 2006

Re: Can Contracts be Equated with Types? Posted: Aug 6, 2006 6:15 AM
Reply to this message Reply
If you expand the type system more you'll see that you're writing the implementation twice: (a) in the type signature (b) in the body of the procedure. What if you want to express (in the type system) that the appended items are in fact x? You're writing the same thing twice (only in another language).

Therefore I think this isn't good. A type system is good if it adds functionality like polymorphism.

Type-safe casting:

str->int :: (str) -> (int)
int->str :: (int) -> (str)


or:

to-str :: (any) -> (str)

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Can Contracts be Equated with Types? Posted: Aug 6, 2006 12:38 PM
Reply to this message Reply
> If you expand the type system more you'll see that you're
> writing the implementation twice: (a) in the type
> signature (b) in the body of the procedure. What if you
> want to express (in the type system) that the appended
> items are in fact x? You're writing the same thing twice
> (only in another language).

Do you mean that the constraints can be used to completely express the solution to problem, ala constraint based programming?

This would definitely be interesting. For trivial programs I agree, but for non-trivial programs I am not sure that the preconditions and postconditions can completely express the implementation. I am not saying that you aren't right though.

Howard Lovatt

Posts: 321
Nickname: hlovatt
Registered: Mar, 2003

Re: Can Contracts be Equated with Types? Posted: Aug 6, 2006 10:10 PM
Reply to this message Reply
There is a whole field of study 'dependent types':

http://en.wikipedia.org/wiki/Dependent_types
http://www.e-pig.org/downloads/ydtm.pdf

special languages, e.g.:

http://en.wikipedia.org/wiki/Epigram_programming_language

and associated conferences, e.g.:

http://www.cs.nott.ac.uk/types06/

That attempt to do exactly this; express all the constraints of a program in the type system.

Vincent O'Sullivan

Posts: 724
Nickname: vincent
Registered: Nov, 2002

Re: Can Contracts be Equated with Types? Posted: Aug 7, 2006 3:57 AM
Reply to this message Reply
> ...an unsigned integer can be viewed as an integer
> which maintains the invariant of always being greater than zero.

Perhaps you'd better update Wikipedia (et al.). They seem to think unsigned integers can include the value zero
(http://en.wikipedia.org/wiki/Integer_%28computer_science%29).

Alex Stojan

Posts: 95
Nickname: alexstojan
Registered: Jun, 2005

Re: Can Contracts be Equated with Types? Posted: Aug 7, 2006 8:18 PM
Reply to this message Reply
> Perhaps you'd better update Wikipedia (et al.). They seem
> to think unsigned integers can include the value zero
> (http://en.wikipedia.org/wiki/Integer_%28computer_science%2
> 9).

The text says "... greater than or equal to zero".

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Can Contracts be Equated with Types? Posted: Aug 7, 2006 10:01 PM
Reply to this message Reply
> > Perhaps you'd better update Wikipedia (et al.). They
> seem
> > to think unsigned integers can include the value zero
> >
> (http://en.wikipedia.org/wiki/Integer_%28computer_science%2
>
> > 9).
>
> The text says "... greater than or equal to zero".

I changed it after Vincent pointed out the mistake/

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Can Contracts be Equated with Types? Posted: Aug 8, 2006 8:06 AM
Reply to this message Reply
Chris,

the provability of a type system is limited by the nature of the Turing machine. The halting problem proves that any algorithmic system can not be proven to terminate, and therefore a depentent type system is undecidable for all cases.

A contracts system equals a type system where types are values, i.e. a depentent type system.

A dependent type system is the only kind of type system that can catch logical errors in the code. It is precisely the lack of this that makes our programs have logical bugs.

Of course, there is room for improvement. If you remember, I have sent you an e-mail about how to make contracts statically proven in most cases (you did not reply to me; didn't you get the e-mail?). I would be more than happy to send you again the e-mail, if you wish.

Jules Jacobs

Posts: 119
Nickname: jules2
Registered: Mar, 2006

Re: Can Contracts be Equated with Types? Posted: Aug 8, 2006 5:12 PM
Reply to this message Reply
Could you post the email here? I'm sure I'd find it very interesting!

Eelis van der Weegen

Posts: 2
Nickname: eelis
Registered: Aug, 2006

Re: Can Contracts be Equated with Types? Posted: Aug 8, 2006 7:53 PM
Reply to this message Reply
> Chris,
>
> the provability of a type system is limited by the nature
> of the Turing machine. The halting problem proves that any
> algorithmic system can not be proven to terminate, and
> therefore a depentent type system is undecidable for all
> cases.

"Any algorithmic system" is a LOT broader than just Turing machines. There are various interesting (and useful!) algorithmic systems that are not Turing complete.

For the issue at hand, I present Coq's [1] Calculus Of Inductive Constructions (CIC) as a counterexample to your claim that dependent type systems are inherently undecideable. The CIC includes a type system that supports dependent types, and yet type checking in the CIC is decideable.

It is true that type-checking in a type system with dependent types may involve execution of arbitrary algorithms in that system. And if that system is Turing Complete, then yes, it becomes undecideable. However, the CIC is not Turing complete.

In the CIC, one can only write algorithms that terminate. For example, when one wants to do recursion (which is the only way to "loop" in the CIC), one is obligated to formally prove (in the same logical system) that the recursion will eventually terminate.

Fortunately, the vast majority of interesting algorithms can be proven to eventually terminate, so a lot of interesting algorithms (and other math) can be formalized in Coq, despite the lack of Turing-completeness.

Turing-completeness is overrated. ;-)

[1] Coq - http://coq.inria.fr/

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Can Contracts be Equated with Types? Posted: Aug 9, 2006 1:53 AM
Reply to this message Reply
> Of course, there is room for improvement. If you remember,
> I have sent you an e-mail about how to make contracts
> statically proven in most cases (you did not reply to me;
> didn't you get the e-mail?).

I did reply on March 21st:

Hi Achilleas,

I'm sorry it took me so long to get back to you. This new job has me swamped. I've looked at your idea, and it does seem solid for languages without side-effects (for example Unimperative, or Joy or Haskell). For languages with side-effects, then I don't see how we can practically measure the output of a function (since it can affect any part of the state). I hope this makes some sense. I think your idea merits further exploration in the context of smaller, easier to study languages. I do think that LtU would have some good feedback. If you are nervous about sharing your ideas, I suggest to start by asking questions to find out about related work. There is a possibility this idea is currently being researched. However, it definitely makes me think about what could be done applying your idea to Unimperative. Keep coming up with good ideas!

Christopher

> I would be more than happy to
> send you again the e-mail, if you wish.

I encourage you to post it here!

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Can Contracts be Equated with Types? Posted: Aug 9, 2006 1:56 AM
Reply to this message Reply
> Turing-completeness is overrated. ;-)

Good point. Thanks for sharing that post!

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Can Contracts be Equated with Types? Posted: Aug 9, 2006 4:32 AM
Reply to this message Reply
> I did reply on March 21st:
>
> Hi Achilleas,
>
> I'm sorry it took me so long to get back to you. This new
> job has me swamped. I've looked at your idea, and it does
> seem solid for languages without side-effects (for example
> Unimperative, or Joy or Haskell). For languages with
> side-effects, then I don't see how we can practically
> measure the output of a function (since it can affect any
> part of the state). I hope this makes some sense. I think
> your idea merits further exploration in the context of
> smaller, easier to study languages. I do think that LtU
> would have some good feedback. If you are nervous about
> sharing your ideas, I suggest to start by asking questions
> to find out about related work. There is a possibility
> this idea is currently being researched. However, it
> definitely makes me think about what could be done
> applying your idea to Unimperative. Keep coming up with
> good ideas!
>
> Christopher
>
> > I would be more than happy to
> > send you again the e-mail, if you wish.
>
> I encourage you to post it here!

Ah, ok. Somehow I did not get hold of it.

I disagree that it can not be applied to languages without referential transparency.

I won't be posting these ideas to LtU, because I am too lazy to formalize them. If anyone is interested, feel free to pick up the idea and make a formal paper out of it.

Anyway, for anyone interested, the idea is:

A block of code has a set of inputs (allowed values) and outputs (possible outcomes). When two blocks of code are paired up in a sequence, the outputs of the 1st block must be a subset of the inputs of the 2nd block. A compiler rejects a block of code that does not conform to this simple rule. This technique could enable static contract evaluation.

The set of inputs can be precisely defined by declaring contracts.

In order to implement this, sets should be smartly represented, either as sets of discrete values, or ranges, or intersections/unions. You do not have to perform big computations, because the I/O sets are small usually.

The real interesting trick in this technique is that when two blocks of code are combined, new sets of inputs and outputs are created for the combined block, which does not necessarily include the values of the two blocks that where combined.

The above does not relate to the halting problem in anyway. It does not tell you if an algorithm terminates or not; it is a mechanism for checking contracts at compile-time, instead of run-time.

I am optimistic about this technique that it can even tell you if some algorithms loop forever, by treating the Program Counter as an input/output value.

The input/output information can be kept around in libraries, so as that when one uses the library, the contracts are part of the system.

Jules Jacobs

Posts: 119
Nickname: jules2
Registered: Mar, 2006

Re: Can Contracts be Equated with Types? Posted: Aug 9, 2006 3:04 PM
Reply to this message Reply
This sounds interesting. Do you have any ideas about recursion?

For example:

f = a b [f] if

How do you make sure that the output of f is correct if it depends on f itself (and maybe on the correctness of f)?

Flat View: This topic has 38 replies on 3 pages [ 1  2  3 | » ]
Topic: Can Contracts be Equated with Types? Previous Topic   Next Topic Topic: Are Web Services Real? Part II


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2014 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us