Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Johan Baltié]

Ok as there were the two same comments on my post I do a single answer.

Here my first post:

>> What about defining type that are subranges of int ?
>> à la ADA...


Here the comments:
-----
>Then how do you make sure that the result of an arithmetic expression is
>still within that sub-range? For example, m.( i + j ) ?
>
>Cheers,
>Hao-yang Wang

-----

>as i said to john skaller, won't you then get index incrementation exceptions ?
>anyway, it's a trade-off.
>
>-- 
>Berke
>mayur_naik@my-deja.com writes:

-----

Now, as I am not an ADA guru I just show you my source:

http://groups.google.com/groups?hl=fr&lr=&ie=UTF-8&oe=UTF-8&frame=right&th=5c68b368acf1e99&seekm=00-04-194%40comp.compilers#link5

------------- BEGIN OF FOLLOWUP -------------

> Does any language or any machine provide some mechanism to:
>
> 1. index an array without checking its bounds
> 2. throw an exception if the index was actually out of range
> 3. allow the programmer to catch and handle the exception rather than
>    terminate the program

Well, Ada does. The strong typing gives information to the compiler for it to
deduce when range checking is not needed:

declare
  subtype Index is Integer range 1..10;
  type Arr is array (Index) of Integer;
  a : Arr;
  element : Integer;
  j : Index := 1;
  k : Integer := 11;
begin
  for i in a'Range loop
    element := a(i); -- no range checking needed, i is in range by definition
  end loop;
  a(j); -- range checking not needed, j is within Index by definition
  a(k); -- range checking needed due possibility of k being outside of Index
exception
  when Constraint_Error =>
     -- process the out-of-range error from a(k)
end;

--
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,
blaak@infomatch.com                            The Rhythm has my soul.

------------- END OF FOLLOWUP -------------

IMHO, the use of subtypes help to avoid a lot of bound check, maybe not all of
them, but I do not think that eliminating *all* the bounds check is useful.

Another point is that using subranges you're not allowed to do many errors as
when you are using bare int.

Ciao

Jo
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Jacques Garrigue]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: Text/Plain; charset=us-ascii, Size: 2454 bytes --]

From: "Johan Baltié" <johan.baltie@wanadoo.fr>

> Well, Ada does. The strong typing gives information to the compiler for it to
> deduce when range checking is not needed:
> 
> declare
>   subtype Index is Integer range 1..10;
>   type Arr is array (Index) of Integer;
>   a : Arr;
>   element : Integer;
>   j : Index := 1;
>   k : Integer := 11;
> begin
>   for i in a'Range loop
>     element := a(i); -- no range checking needed, i is in range by definition
>   end loop;
>   a(j); -- range checking not needed, j is within Index by definition
>   a(k); -- range checking needed due possibility of k being outside of Index
> exception
>   when Constraint_Error =>
>      -- process the out-of-range error from a(k)
> end;

This is similar to Pascal ranges.
The trouble is that typical code doesn't look like that, but rather

    let bubble_once arr =
      for i = 0 to Array.length arr - 2 do
        if arr.(i) > arr.(i+1) then begin
          let tmp = arr.(i) in
          arr.(i) <- arr.(i+1);
          arr.(i+1) <- tmp
        end
      done

or worse

    let bubble_one arr last =
      assert (last < Array.length arr);
      let swap i =
        let tmp = arr.(i) in
        arr.(i) <- arr.(i+1);
        arr.(i+1) <- tmp
      in
      for i = 0 to last - 1 do
        if arr.(i) < arr.(i+1) then swap i
      done

In the first case, that's not too difficult: you just have to know
that Array.length returns the length of an array, and do a bit of
arithmetic.

In the second case, you should propagate the information from the
assertion to the loop bound, and additionally treat swap as if it were
inlined (we know it is its only call context).  And it's fragile:
if you move "swap" out of the function, then it might be used on any
array, and you have to do the bound check.
By the way: if you forgot the assertion, would it be ok to have the
compiler insert it automagically and fail early?  As I see an
out-of-bound error as fatal, this would seem reasonnable to me, but
this should be somewhere in the semantics of the language.

There are lots of things you can do without real type inference, but
the real trouble is that what is a reasonable target is not clear...

    Jacques Garrigue
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Johan Baltié]

> From: "Johan Baltié" <johan.baltie@wanadoo.fr>
> 
> > Well, Ada does. The strong typing gives information to the compiler for it to
> > deduce when range checking is not needed:
> > 
> > declare
> >   subtype Index is Integer range 1..10;
> >   type Arr is array (Index) of Integer;
> >   a : Arr;
> >   element : Integer;
> >   j : Index := 1;
> >   k : Integer := 11;
> > begin
> >   for i in a'Range loop
> >     element := a(i); -- no range checking needed, i is in range by definition
> >   end loop;
> >   a(j); -- range checking not needed, j is within Index by definition
> >   a(k); -- range checking needed due possibility of k being outside of Index
> > exception
> >   when Constraint_Error =>
> >      -- process the out-of-range error from a(k)
> > end;
> 
> This is similar to Pascal ranges.
> The trouble is that typical code doesn't look like that, but rather
> 
>     let bubble_once arr =
>       for i = 0 to Array.length arr - 2 do
>         if arr.(i) > arr.(i+1) then begin
>           let tmp = arr.(i) in
>           arr.(i) <- arr.(i+1);
>           arr.(i+1) <- tmp
>         end
>       done
> 
> or worse
> 
>     let bubble_one arr last =
>       assert (last < Array.length arr);
>       let swap i =
>         let tmp = arr.(i) in
>         arr.(i) <- arr.(i+1);
>         arr.(i+1) <- tmp
>       in
>       for i = 0 to last - 1 do
>         if arr.(i) < arr.(i+1) then swap i
>       done
> 
> In the first case, that's not too difficult: you just have to know
> that Array.length returns the length of an array, and do a bit of
> arithmetic.
> 
> In the second case, you should propagate the information from the
> assertion to the loop bound, and additionally treat swap as if it were
> inlined (we know it is its only call context).  

No it's not such a mess.
A subrange is  a type. As ocaml is a bit strong on is types it solves itself the
problem

     let bubble_one arr last =
       assert (last < Array.length arr);
       let swap i =
         let tmp = arr.(i) in
         arr.(i) <- arr.(i+1);
         arr.(i+1) <- tmp
       in
       for i = 0 to last - 1 do
         if arr.(i) < arr.(i+1) then swap i
       done

the {..} are my subranges types

bubble_one: a' {0..b'} array -> int -> unit
swap: {0..b'} -> unit

the "for" should be like in Ada, working with range types and no problem will
ever occur.

> And it's fragile:
> if you move "swap" out of the function, then it might be used on any
> array, and you have to do the bound check.

If you move swap out of the function, in another one using another array, the
type will change and a warning/error/check will occur if the types are incompatible.


> [snipped]
>     Jacques Garrigue


Ciao

Jo
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Jacques Garrigue]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: Text/Plain; charset=us-ascii, Size: 1914 bytes --]

From: "Johan Baltié" <johan.baltie@wanadoo.fr>

> > In the second case, you should propagate the information from the
> > assertion to the loop bound, and additionally treat swap as if it were
> > inlined (we know it is its only call context).  
> 
> No it's not such a mess.  A subrange is a type. As ocaml is a bit
> strong on is types it solves itself the problem

OK, I should have been clearer about my basic assumption: I was
talking about what you can do _without_ modifying the typing.
Modifying the typing is a mess: if your bounds are no longer integers,
then how can you convert between them and integers, back and forth.
You could use subtyping in one direction, but there is no implicit
subtyping in ocaml, as this would badly break type inference.

> > And it's fragile:
> > if you move "swap" out of the function, then it might be used on any
> > array, and you have to do the bound check.
> 
> If you move swap out of the function, in another one using another array, the
> type will change and a warning/error/check will occur if the types
> are incompatible.

No, I was just saying moving swap to the toplevel:
  let swap arr i = ....

Supposing you use the original plain type, you are in trouble.

But it looks like you're just asking for dependent types, no less...

I think this discussion started on efficiency considerations;
my belief is that you can already already optimize a lot, without
using fancy type systems. Such type systems are not only hard to
implement (and mix with an existing type system);  while they
certainly take bugs, they also get in your way when you get out of
their small understanding.

Cheers,

        Jacques Garrigue
-------------------
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

Re: [Caml-list] Sub{range,type} (was: Statically detecting arrays bound exceptions ??)

[Johan Baltié]

> From: "Johan Baltié" <johan.baltie@wanadoo.fr>
> 
> > > In the second case, you should propagate the information from the
> > > assertion to the loop bound, and additionally treat swap as if it were
> > > inlined (we know it is its only call context).  
> > 
> > No it's not such a mess.  A subrange is a type. As ocaml is a bit
> > strong on is types it solves itself the problem
> 
> OK, I should have been clearer about my basic assumption: I was
> talking about what you can do _without_ modifying the typing.
> Modifying the typing is a mess: if your bounds are no longer integers,
> then how can you convert between them and integers, back and forth.
> You could use subtyping in one direction, but there is no implicit
> subtyping in ocaml, as this would badly break type inference.

*sigh* :,(
I was dreaming of that kind of stuff.

But I do not see why type inference reach an end with subtyping.
Can you elaborate on this ?
 
> > > And it's fragile:
> > > if you move "swap" out of the function, then it might be used on any
> > > array, and you have to do the bound check.
> > 
> > If you move swap out of the function, in another one using another array, the
> > type will change and a warning/error/check will occur if the types
> > are incompatible.
> 
> No, I was just saying moving swap to the toplevel:
>   let swap arr i = ....
> 
> Supposing you use the original plain type, you are in trouble.
> 
> But it looks like you're just asking for dependent types, no less...

I did not know this name, and after a quick browse I can answer: "Yes" :)

 
> I think this discussion started on efficiency considerations;
> my belief is that you can already already optimize a lot, without
> using fancy type systems. 
Ok, I left the previous thread, cause I'm getting totally of topic.

> Such type systems are not only hard to
> implement (and mix with an existing type system);  while they
> certainly take bugs, they also get in your way when you get out of
> their small understanding.
With my new and small understanding of dependent type, it seems to me that Ada
types look a lot like this. It seems to add power to the type checker, so why
would this be a bad thing ? Did I miss something ?


The only problem that I see is that if you consider list type dependent of size,
this kind of type cannot staticaly determined (is it the point that break type
inference ?).

Ciao

Jo
-------------------
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

[Caml-list] productivity improvement

[Oleg]

Hi

As part of learning O'Caml I was rewriting small personal utility programs 
from C++ to O'Caml and I have not seen any productivity improvement so far. 
Possibly, this is because I essentially use the same imperative style or 
because my knowledge of O'Caml is rudimental or because there is no 
productivity enhancement, at least for the programs I was translating or for 
small programs in general.

What are the _simplest_ examples that demonstrate considerable (> 2:1) O'Caml 
vs C++ productivity improvement (in terms of program size) and where can I 
find them?

Thanks
Oleg

P.S. Just trying to stay motivated.
-------------------
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

[Caml-list] Universal Serializer (was: productivity improvement)

[Oleg]

On Monday 08 July 2002 04:05 pm, John Malecki wrote in personal email:

> This is no an ocaml specific productivity improvement but the ability
> to marshal a data structure without having to write any data structure
> specific code is very productive.  

Speaking of complex data  structures with no code: Oftentimes, I need to 
create data structures, then write code that saves the structure to a file 
and code that reincarnates it. 

AFAICT if a data structure is created using combinations of unions, lists, 
arrays, etc. of built-in types or objects that, e.g. already have "write" and 
"read" methods defined,  then in theory, a hypothetical compiler ought to be 
able to generate such serialization functions automatically (IIRC Lisp and 
Scheme do this because of the simplicity of their type systems, but I may be 
wrong here).

Does O'Caml allow any type of short-cuts to avoid coding serialization 
manually?

Thanks
Oleg
-------------------
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

Re: [Caml-list] Universal Serializer (was: productivity improvement)

[Nicolas Cannasse]

> > This is no an ocaml specific productivity improvement but the ability
> > to marshal a data structure without having to write any data structure
> > specific code is very productive.

BTW OCaml functional programming and memory management are two ways of
increasing productivity. Pattern matching on structures is also wonderful.
For most of the programs, I will say that the productivity rate against C is
around 1:3.

Nicolas Cannasse

-------------------
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

Re: [Caml-list] Universal Serializer (was: productivity improvement)

[John Max Skaller]

>
>
>
>BTW OCaml functional programming and memory management are two ways of
>increasing productivity. Pattern matching on structures is also wonderful.
>For most of the programs, I will say that the productivity rate against C is
>around 1:3.
>
>Nicolas Cannasse
>
You must be an academic.:-) Try between 10:1 and 100:1,
*assuming* that any libraries you need are available,
and a reasonably complex piece of software.

You just can't underestimate how difficult it is to find
bugs in C codes of reasonable size. Such bugs almost never
happen in Ocaml. The biggest problem in Ocaml is type inference,
and the resulting loss of localisation of error diagnostics, but
such compile time errors can be resolved *definitely*;
that is, you know for sure when you've fixed them
(because the compiler stops hassling you).

Ohhhh.. just imagine if GTK/Gnome/Gui stuff on RH linux
were written in Ocaml .. it might actually work!

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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

Re: [Caml-list] Universal Serializer (was: productivity improvement)

[Michael Vanier]

> Date: Thu, 11 Jul 2002 02:06:15 +1000
> From: John Max Skaller <skaller@ozemail.com.au>
> 
> >
> >BTW OCaml functional programming and memory management are two ways of
> >increasing productivity. Pattern matching on structures is also wonderful.
> >For most of the programs, I will say that the productivity rate against C is
> >around 1:3.
> >
> >Nicolas Cannasse
> >
> You must be an academic.:-) Try between 10:1 and 100:1,
> *assuming* that any libraries you need are available,
> and a reasonably complex piece of software.
> 

I agree, but the productivity increase is going to depend a lot on the
experience and skill of the ocaml programmer.  As a newbie, I find myself
using a lot of lame imperative idioms before discovering more elegant (and
concise) functional ones.

> You just can't underestimate how difficult it is to find
> bugs in C codes of reasonable size. Such bugs almost never
> happen in Ocaml. 

Definitely, although the same could be said for java or C#, if by "such
bugs" you mean memory leaks and memory corruption.  For a more
ocaml-specific example, I find that algebraic data types with
pattern-matching (and the compiler warnings that occur if you fail to match
all patterns) is something that ocaml has that java/C# don't and which
can massively improve the quality of code (as well as making it much more
comprehensible).

> The biggest problem in Ocaml is type inference,
> and the resulting loss of localisation of error diagnostics, but
> such compile time errors can be resolved *definitely*;
> that is, you know for sure when you've fixed them
> (because the compiler stops hassling you).

What do you mean by "loss of localisation of error diagnostics"?  Do you
mean that a type error in one location giving an expression which can still
compile (but to the wrong type) results in an obscure error message
elsewhere?  I agree that that's occasionally a minor pain, but it's hardly
in the same league with memory leaks etc.  If that's ocaml's biggest
problem, then ocaml is the best computer language I've ever seen.

> 
> Ohhhh.. just imagine if GTK/Gnome/Gui stuff on RH linux
> were written in Ocaml .. it might actually work!
> 

*drool*  I would totally *love* to have this.

Mike
-------------------
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

Re: [Caml-list] Universal Serializer (was: productivity improvement)

[John Max Skaller]

Michael Vanier wrote:

>>You must be an academic.:-) Try between 10:1 and 100:1,
>>*assuming* that any libraries you need are available,
>>and a reasonably complex piece of software.
>>
>
>I agree, but the productivity increase is going to depend a lot on the
>experience and skill of the ocaml programmer.  As a newbie, I find myself
>using a lot of lame imperative idioms before discovering more elegant (and
>concise) functional ones.
>
Ocaml does imperative programming better than C and C++ too.
So even your 'lame' imperative code can be produced faster and more
reliably in Ocaml.

Example: values (declared in let bindings) scope better.
Variables (references) must be initialised -- sometimes this
is a pain, but usually it is a bonus.

>You just can't underestimate how difficult it is to find
>bugs in C codes of reasonable size. Such bugs almost never
>happen in Ocaml. 
>
>
>Definitely, although the same could be said for java or C#, if by "such
>bugs" you mean memory leaks and memory corruption. 
>
 Well, if you run java or C#, you still have to cast 'object' down, and 
so you can get run-time
errors -- where using Ocaml this class of error cannot happen.

Ocaml run time errors include array (and string) bounds exceptions and 
infinite recursions:
static type checking could detect the first, but not the second.


>>The biggest problem in Ocaml is type inference,
>>and the resulting loss of localisation of error diagnostics, but
>>such compile time errors can be resolved *definitely*;
>>that is, you know for sure when you've fixed them
>>(because the compiler stops hassling you).
>>
>
>What do you mean by "loss of localisation of error diagnostics"?  Do you
>mean that a type error in one location giving an expression which can still
>compile (but to the wrong type) results in an obscure error message
>elsewhere?  
>
Yes.

>I agree that that's occasionally a minor pain, but it's hardly
>in the same league with memory leaks etc.  
>
Agree.

>If that's ocaml's biggest problem,
>
It's one of them (IMHO)

>then ocaml is the best computer language I've ever seen.
>
I agree :-)

>Ohhhh.. just imagine if GTK/Gnome/Gui stuff on RH linux
>were written in Ocaml .. it might actually work!
>
>*drool*  I would totally *love* to have this.
>
heh :-)

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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

[Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Berke Durak]

On Fri, Jul 12, 2002 at 10:41:35PM +1000, John Max Skaller wrote:
[...]
> Ocaml run time errors include array (and string) bounds exceptions and 
> infinite recursions:
> static type checking could detect the first, but not the second.

Hey, wait a minute, how do you plan to statically detect bounds exceptions ?
It's as undecidable as detecting infinite recursions.

	let rec f () =
	   let a = [|1;2|] in
       if compiler_is_gonna_say_that_there_is_gonna_be_a_bounds_error f then
          a.(0)
       else
          a.(3)
-- 
Berke Durak
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Alessandro Baretta]

Berke Durak wrote:
> On Fri, Jul 12, 2002 at 10:41:35PM +1000, John Max Skaller wrote:
> [...]
> 
> Hey, wait a minute, how do you plan to statically detect bounds exceptions ?
> It's as undecidable as detecting infinite recursions.
> 
> 	let rec f () =
> 	   let a = [|1;2|] in
>        if compiler_is_gonna_say_that_there_is_gonna_be_a_bounds_error f then
>           a.(0)
>        else
>           a.(3)

If the compiler attempted to catch at least the most evident 
  bounds errors, it would very simply detect that your code 
contains an expression which, if evaluated, would raise a 
runtime bounds error. Hence, the compiler should simply 
reject the code. Of course, in the absence of some unusual 
limitation on the expressive power of array creation and 
indexing expression, the general problem of static detection 
of array indexing errors is undecidable.

I wonder if the compiler gurus at the INRIA know what kinds 
of constraints imposed on the language would allow the 
compiler to statically check array indexing. I can imagine a 
few applications, such as signal analysis, where the program 
logic is simple enough that such a restricted language might 
suffice, and come to the aid of the developer who presently 
uses unsafe arrays for the sake of speed, but with no help 
from the compiler at prooving that the program is correct 
with respect to array indexing.

I have a feeling that most applications which would benefit 
from static checking of array indexing boil down to finite 
state automata. I'm pretty sure that a language based of 
FSAs could do static bounds checking.

Alex

-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Xavier Leroy]

> Of course, in the absence of some unusual 
> limitation on the expressive power of array creation and 
> indexing expression, the general problem of static detection 
> of array indexing errors is undecidable.

Indeed.

> I wonder if the compiler gurus at the INRIA know what kinds 
> of constraints imposed on the language would allow the 
> compiler to statically check array indexing.

Well, for this purpose, array index expressions must be restricted to
a sub-language where inequations between index expressions are
decidable.  A well-known such sub-language is Presburger arithmetic:
index expressions are variables, constants, and sums and products of
expressions.  I don't know of any significantly more expressive
sub-language that has the required decidability properties.

> I can imagine a few applications, such as signal analysis, where the
> program logic is simple enough that such a restricted language might
> suffice, and come to the aid of the developer who presently uses
> unsafe arrays for the sake of speed, but with no help from the
> compiler at prooving that the program is correct with respect to
> array indexing.

Obligatory preliminary remark: the cost of run-time array bound checks
is not that high, since on modern processors it is performed
largely in parallel with the actual array access.  On my tests,
ocamlopt -unsafe is at best 25% faster than ocamlopt on array
intensive programs.

This said, the approach you outline was investigated in depth by
Hongwei Xi in his work on Dependent ML:

        http://www.ececs.uc.edu/~hwxi/DML/DML.html

It's an interesting reading.

- Xavier Leroy
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Noel Welsh]

--- Alessandro Baretta <alex@baretta.com> wrote:
> I wonder if the compiler gurus at the INRIA know
> what kinds 
> of constraints imposed on the language would allow
> the 
> compiler to statically check array indexing. 

I'm not a compiler guru from INRIA but I can point out
the languages SAC (Single Assignment C) and FiSH (ask
Google; I'm feeling lazy) that do array shape
inference.  Basically the type system for arrays in
augmented by their shape and shapes are inferred in a
similar way to types.  In addition to eliminating
bounds checks the compiler can do funky reordering
optimisations (because these are functional languages,
so evaluation order is not important) and produce code
faster than Fortran. Exciting stuff if you're into
numerical code.

Noel

__________________________________________________
Do You Yahoo!?
Yahoo! Autos - Get free new car price quotes
http://autos.yahoo.com
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Oleg]

On Monday 15 July 2002 04:39 am, Noel Welsh wrote:
> FiSH (ask
> Google; I'm feeling lazy)

Even Altavista doesn't support case-sensitive searches anymore.

Oleg
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Michael Vanier]

http://www-staff.mcs.uts.edu.au/~cbj/FISh/

Mike

> From: Oleg <oleg_inconnu@myrealbox.com>
> Date: Mon, 15 Jul 2002 17:22:35 -0400
> 
> On Monday 15 July 2002 04:39 am, Noel Welsh wrote:
> > FiSH (ask
> > Google; I'm feeling lazy)
> 
> Even Altavista doesn't support case-sensitive searches anymore.
> 
> Oleg
-------------------
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

Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Florian Hars]

Oleg wrote:
> On Monday 15 July 2002 04:39 am, Noel Welsh wrote:
> 
>>FiSH (ask Google; I'm feeling lazy)
> 
> Even Altavista doesn't support case-sensitive searches anymore.

Learn to use search engines intelligently: You know that *FiSH* (correct 
capitalization is FISh, so a case sensitive search wouldn't have bought 
you anything, anyway :-)) is a *language* with good *array* processing 
capabilities. So here we go:

http://www.google.com/search?q=fish+language+array

The first four results are relevant.

Yours, Florian Hars

-------------------
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