From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id DAA23362; Wed, 19 Nov 2003 03:26:03 +0100 (MET)
X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id DAA23683 for <caml-list@pauillac.inria.fr>; Wed, 19 Nov 2003 03:26:02 +0100 (MET)
Received: from herd.plethora.net (herd.plethora.net [205.166.146.1])
	by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id hAJ2Q1120128
	for <caml-list@inria.fr>; Wed, 19 Nov 2003 03:26:01 +0100 (MET)
Received: from bhurt.plethora.net (bhurt.plethora.net [205.166.146.49])
	by herd.plethora.net (8.11.6/8.10.1) with ESMTP id hAJ2KTC28802;
	Tue, 18 Nov 2003 20:20:35 -0600 (CST)
Date: Tue, 18 Nov 2003 21:19:58 -0600 (CST)
From: Brian Hurt <bhurt@spnz.org>
X-X-Sender: bhurt@localhost.localdomain
To: Martin Berger <martinb@dcs.qmul.ac.uk>
cc: skaller@ozemail.com.au, Caml Mailing List <caml-list@inria.fr>
Subject: Design by Contract, was Re: [Caml-list] GC and file descriptors
In-Reply-To: <3FBAC862.7010603@dcs.qmul.ac.uk>
Message-ID: <Pine.LNX.4.44.0311182109210.5009-100000@localhost.localdomain>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Loop: caml-list@inria.fr
X-Spam: no; 0.00; caml-list:01 dependencies:01 decidable:01 inference:01 non-trivial:01 arrays:01 compiler:01 ocaml:01 contracts:98 descriptors:01 nov:01 float:02 float:02 wrote:03 classic:03 
Sender: owner-caml-list@pauillac.inria.fr
Precedence: bulk

On Wed, 19 Nov 2003, Martin Berger wrote:

> > Well, exceptions are 'really' wrong: they're 'really' a constraint
> > on the type of the argument, for example 
> > 
> > 	divide: float -> float not zero -> float
> > 
> > but expressed negatively (throws divide by zero).
> 
> that's one way of looking at it. another would be to say
> we have dependent types ... unfortunatly neither rich
> specifications nor type dependencies lead to decidable
> type inference so we need to be less precise.
> 
> martin
> 

This actually brings to mind another way to improve Ocaml: Contracts, ala 
eiffle.  The problem in the above example is that the constraint that the 
second argument not be zero is a contract.

A classic example of a contract is Array.get, which requires the index to 
be >= 0 and < the length of the array.  Being able to hoist this check out 
of Array.get can lead to non-trivial optimization opportunities.  For 
example, consider the following code:

    for i = 0 to n do
        a.(i) <- 0
    done

This gets compiled like:
    for i = 0 to n do
        if i < Array.length a then
            a.(i) <- 0
        else
            raise Invalid_argument "Array.get"
    done

Strength reduction can then be applied to eliminate the redundant checks:

     let limit = min n ((Array.length a) - 1) in
     for i = 0 to limit do
         a.(i) <- 0 (* no check needed! *)
     done;
     if n >= (Array.length a) then
         raise Invalid_argument "Array.get"
     else ()

With arrays, you could simply declare them part of the language that the 
compiler knows about.  But I'd like a more general approach.

-- 
"Usenet is like a herd of performing elephants with diarrhea -- massive,
difficult to redirect, awe-inspiring, entertaining, and a source of
mind-boggling amounts of excrement when you least expect it."
                                - Gene Spafford 
Brian

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners