Version française
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] GC and file descriptors
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Brian Hurt <bhurt@s...>
Subject: Design by Contract, was Re: [Caml-list] GC and file descriptors
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