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

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

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