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

["Johan Baltié" <johan.baltie@wanadoo.fr>]

> 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