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