Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: 2003-11-19 (02:26)
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

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

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! *)
     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 

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: