Snark has quit [Read error: 110 (Connection timed out)]
Morphous has joined #ocaml
Snark has joined #ocaml
Morphous is now known as Amorhous
Amorhous is now known as Amorphous
Revision17 has joined #ocaml
revision17_ has quit [Read error: 110 (Connection timed out)]
__DL__ has joined #ocaml
smimou has joined #ocaml
Daweos has joined #ocaml
mikeX has quit ["leaving"]
m3ga has joined #ocaml
mikeX has joined #ocaml
bzzbzz has quit [Client Quit]
Tachyon76 has joined #ocaml
Daweos has quit []
m3ga has quit ["disappearing into the sunset"]
Nargg has joined #ocaml
schlick has joined #ocaml
<schlick>
Anyone care to help me think on some source code analysis stuff?
<Smerdyakov>
RULE #1 OF IRC: Just Ask Your Question
<dylan>
hehe, declarative conversation.
<schlick>
I'm currently hung up on how one would check for this error at compile time. In compilation unit A, you allocate some memory, and initialize it as, say, integer 0's. Then you pass it to compilation unit B, which expects it to be initialized as character ".". The same thing could, I think, happen with a compiled garbage collected language by passing a reference to something of the wrong type.
<Smerdyakov>
schlick, isn't that a simple type error, as integer isn't character?
<schlick>
Yes that would be a "simple type error". How one would go about checking for it with the two separate compilation (or more precisely, analysis) units is what I'm hung up on. It seems there'd have to be some way of communicating "the other guy has got integers in this array at the moment".
<Smerdyakov>
In ML, every cross-compilation unit link goes through typed interfaces.
<schlick>
You could catch it by the pointer/reference type passed as a argument, I suppose, but if inside the memory block the initial pointer (passed as the argument) was one type, and (down the line in the data structure) it points at another type, that the two compilation units disagree on, I don't see how you'd check for it statically.
<Smerdyakov>
Type correctness guarantees that types in interfaces are completely accurate.
<Smerdyakov>
There is no possibility for "hidden errors" found by looking deeper into data structures.
<schlick>
I can see how the initial pointer/reference can be checked (since the linking information contains that, no doubt), but not anything else.
<Smerdyakov>
Please give me a complete example in an ML-like setting that you think demonstrates your concern.
<schlick>
It's more a issue for a manually memory managed setting like C where you can't really depend on references and garbage collection (the garbage collector still has to get written somewhere). I think what would happen in a language like ML is each "type" would be handled separatly, you couldn't (implicitly, I guess, since it's garbage collected) allocate a block of mixed types.
<schlick>
It's hard for me to map one to the other mentally.
<Smerdyakov>
So you're talking about an unsafe source-level language?
<Smerdyakov>
Of course there are no guarantees with an unsafe language....
<schlick>
I'm not sure there's anything inherantly "unsafe" about manual memory management and pointers. You have to go through all sorts of contortions to make sure pointers aren't invalid, or don't become invalid, since you don't have references, but I haven't hit any cases where I can't think of a way you just /can't/ do that.
<Smerdyakov>
"Unsafe" means that the compiler doesn't verify that your program won't have a runtime type error.
<schlick>
I haven't, however, reasoned out how you can pass arbitrary data structures around on the heap and make sure no mistakes are made, namely because the only information that is passed, that I know of, is that necessary to make sure the bitwise representation of the two compilation units is agreed on, which revolves around the "first" pointer (the one passed as a argument). The rest is lost as far as I know.
<schlick>
argument). The rest is lost as far as I know, and I don't know how to "pass that along".
<Smerdyakov>
There is a metric tonne of research work on type systems for manual memory management.
<schlick>
And yes, I know about the difference between strong/weak type systems.
<Smerdyakov>
See the calculus of capabilities, alias types, linear types, separation logic, ....
<schlick>
Well, I know of the "try to treat the heap as stack" stuff, which doesn't seem to be a workable general solution. I don't know of anything that handles "how do I glue these two binaries together while making sure the heap they pass around stays sane".
Tachyon76 has joined #ocaml
<schlick>
By "heap as type", I'm referring to things like region inference. Unavoidable leaks are not cool.
<Smerdyakov>
Then follow the references I just gave to be enlightened.
<schlick>
Heap as stack, rather.
<schlick>
Linear types I know a little about. I'm pretty sure that doesn't relate to this problem. The others I'm not sure about.
<schlick>
Looks like calculus of capabilities is tied to region inference too.
<Smerdyakov>
No.
<Smerdyakov>
Calculus of capabilities is expressive enough to encode region-based management, and also much mroe.
<schlick>
Hmm.
<schlick>
Uniqueness types related to any of this?
<Smerdyakov>
Yes
<schlick>
I guess I'll be reading about it for a while. I don't think what I'm baffled by is that you can show that things are handled properly so much as how you would communicate in source code "this is what I'm passing to you" and "this is what I expect" on the two "halves". I guess you could include the full spec of what you expect to be in the unit of heap type-wise, when allocating, and on the "half" you pass it to.
<schlick>
when allocating, and on the "half" you pass it to.
<Smerdyakov>
I must go now.
Snark has quit [Read error: 110 (Connection timed out)]
Snark has joined #ocaml
love-pingoo has quit ["Connection reset by by pear"]
_jol_ has joined #ocaml
adam__ has quit ["BitchX: the headache medicine"]
schlick has left #ocaml []
_jol_ has quit ["leaving"]
magnus-- has quit [Read error: 110 (Connection timed out)]