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
Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Johan Baltié <johan.baltie@w...>
Subject: Re: [Caml-list] Sub{range,type} (was: Statically detecting arrays bound exceptions ??)
> From: "Johan Baltié" <>
> > > 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 ?).


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