<menace>
but i cannot use functions from the standard library .. (chr and code e.g.)
<Smerdyakov>
They're in modules, not bound at the top level.
bzzbzz has joined #ocaml
<pango_>
what's the benefit of converting a string to a list of char anyway
<menace>
operating on the characters as integers?
<pango_>
characters aren't integers
<menace>
but i can convert them into these
<menace>
and i want to do this
<pango_>
int_of_char and char_of_int, or Char.code and Char.chr
__DL__ has quit [Remote closed the connection]
rq has joined #ocaml
menace has quit [Remote closed the connection]
pango__ has joined #ocaml
pango_ has quit [Read error: 110 (Connection timed out)]
ski__ is now known as ski_
skylan has joined #ocaml
magnus-- has quit [Read error: 110 (Connection timed out)]
exa has quit [Remote closed the connection]
juri has quit [brown.freenode.net irc.freenode.net]
ulfdoz has quit [brown.freenode.net irc.freenode.net]
rq has quit [brown.freenode.net irc.freenode.net]
ski has quit [brown.freenode.net irc.freenode.net]
Bigb[a]ng has quit [brown.freenode.net irc.freenode.net]
Demitar has quit [brown.freenode.net irc.freenode.net]
cmeme has quit [brown.freenode.net irc.freenode.net]
shammah has quit [brown.freenode.net irc.freenode.net]
pnou has quit [brown.freenode.net irc.freenode.net]
TaXules has quit [brown.freenode.net irc.freenode.net]
vincenz has quit [brown.freenode.net irc.freenode.net]
Hadaka has quit [brown.freenode.net irc.freenode.net]
Oatmeat|umn has quit [brown.freenode.net irc.freenode.net]
pango__ has quit [brown.freenode.net irc.freenode.net]
flux__ has quit [brown.freenode.net irc.freenode.net]
noj has quit [brown.freenode.net irc.freenode.net]
skylan has quit [brown.freenode.net irc.freenode.net]
shirogane has quit [brown.freenode.net irc.freenode.net]
Amorphous has quit [brown.freenode.net irc.freenode.net]
CLxyz has quit [brown.freenode.net irc.freenode.net]
knobo has quit [brown.freenode.net irc.freenode.net]
rossberg has quit [brown.freenode.net irc.freenode.net]
haakonn has quit [brown.freenode.net irc.freenode.net]
det has quit [brown.freenode.net irc.freenode.net]
batdog|gone has quit [brown.freenode.net irc.freenode.net]
z|away has quit [brown.freenode.net irc.freenode.net]
justinc has quit [brown.freenode.net irc.freenode.net]
KrispyKringle has quit [brown.freenode.net irc.freenode.net]
pattern has quit [brown.freenode.net irc.freenode.net]
skylan has joined #ocaml
pango__ has joined #ocaml
rq has joined #ocaml
shirogane has joined #ocaml
ski has joined #ocaml
ulfdoz has joined #ocaml
juri has joined #ocaml
Amorphous has joined #ocaml
Demitar has joined #ocaml
cmeme has joined #ocaml
shammah has joined #ocaml
flux__ has joined #ocaml
pnou has joined #ocaml
TaXules has joined #ocaml
CLxyz has joined #ocaml
det has joined #ocaml
pattern has joined #ocaml
haakonn has joined #ocaml
KrispyKringle has joined #ocaml
justinc has joined #ocaml
rossberg has joined #ocaml
z|away has joined #ocaml
batdog|gone has joined #ocaml
knobo has joined #ocaml
vincenz has joined #ocaml
Bigb[a]ng has joined #ocaml
Oatmeat|umn has joined #ocaml
Hadaka has joined #ocaml
noj has joined #ocaml
thedracle has joined #ocaml
<thedracle>
Testing...
thedracle has quit [Remote closed the connection]
_shirogane has joined #ocaml
rossberg has quit [brown.freenode.net irc.freenode.net]
haakonn has quit [brown.freenode.net irc.freenode.net]
shirogane has quit [brown.freenode.net irc.freenode.net]
det has quit [brown.freenode.net irc.freenode.net]
knobo has quit [brown.freenode.net irc.freenode.net]
CLxyz has quit [brown.freenode.net irc.freenode.net]
skylan has quit [brown.freenode.net irc.freenode.net]
Amorphous has quit [brown.freenode.net irc.freenode.net]
justinc has quit [brown.freenode.net irc.freenode.net]
pattern has quit [brown.freenode.net irc.freenode.net]
KrispyKringle has quit [brown.freenode.net irc.freenode.net]
z|away has quit [brown.freenode.net irc.freenode.net]
batdog|gone has quit [brown.freenode.net irc.freenode.net]
batdog|gone has joined #ocaml
justinc has joined #ocaml
KrispyKringle has joined #ocaml
skylan has joined #ocaml
knobo has joined #ocaml
haakonn has joined #ocaml
z|away has joined #ocaml
thedracle has joined #ocaml
pattern has joined #ocaml
det has joined #ocaml
Amorphous has joined #ocaml
rossberg has joined #ocaml
Snark has joined #ocaml
magnus-- has joined #ocaml
shammah has quit [Read error: 104 (Connection reset by peer)]
_shirogane has quit [Remote closed the connection]
magnus-- has quit [Read error: 110 (Connection timed out)]
<flux__>
pango__, uh, obviously for example that you get to use List.filter and List.map for free
<flux__>
anyway, there aren't functions for doing those conversions in the ocaml's standard library
CLxyz has joined #ocaml
<thedracle>
Which conversions?
<flux__>
string -> list and vice versa
schlick has joined #ocaml
thedracle has quit [Read error: 104 (Connection reset by peer)]
<schlick>
I have some questions about typing as handled in ML based languages. First, I'd like to make sure I understand the difference between dynamic and static typing. Is the difference that statically typed languages can check that operations performed on data can occur at compile time, while dynamically typed languages only catch them at run time?
<flux__>
yes
<schlick>
Ok, on type safety.
<schlick>
One thing I've read has me confused. Why is it that you can't convert between types in a type safe language? For instance, what's wrong with converting a string, containing numbers, to integers?
<flux__>
nothing wrong, there are functions to do that
<schlick>
Since it's non-lossy.
<flux__>
but the point in static typing is that the types are known during the compile time
* schlick
nods. "I have a question about that in a bit."
<schlick>
I noticed OCaml doesn't implicitly convert things amongst base types where doing so is safe (the string and integer thing). Is there a reason for that?
<flux__>
the type checker doesn't handle such ambiguities
<flux__>
but languages (I know of) with more sophisticated type checkers (like haskell) don't do it either
<schlick>
But it would still be type safe if it could do so? (just to make sure I have this type safe thing figured out)
<flux__>
it's just that we like to know what kind of data we're handling ;)
<schlick>
I can understand that, my next question will show how I came to the conclusion I need to look at a ML based language.
<flux__>
but it is runtime behavior whether a string contains an integer or not
<schlick>
Hmm. That would not be so if it was a constant though, right?
<flux__>
well, true, but that's hardly a reason to make the type checker support it; after all, if a string is a constant integer used as an integer, why not just use integer
* schlick
laughs. "True, sorry for asking that dumb question. I'm still trying to line this out in my head."
<flux__>
anyway, any integer could still be used as a string. but such implicit conversions are rarely considered a feature among the compiler writing kind of folk, I think ;)
<schlick>
Ok, here's why I decided to look at ML. I'd appreciate some confirmation or correction of my thinking here.
<schlick>
I've been trying to design a programming language. Up to now I'd planned on it being dynamically typed since it seems convenient. It had occured to me that the problems of using a method that a object can't handle ("message not understood" in most OO dynamically typed languages) could be handled by tracing execution paths and making sure no such call could occur.
<schlick>
Here's where the problem creeps in, I think, and where I'd very much like to check my thinking on this...
<flux__>
well, that does sound like an application for static typing
<schlick>
If I'm linking to something I don't have the source code to, only the description of the range of what it considers valid input, and what it's supposed to return as output, I don't think my trick works. This is because I can't trace "into" the library (since I don't have its source), and make sure that any dynamically typed object I hand it will function with whatever the library might hand it off to.
<schlick>
However, statically typed languages just treat everything as "dead data", and thus you can be assured that any data the "outer" function on external code (e.g. the function in the library you call), will have to convert it as appropriate before passing it to anything else. So I don't have to do the tracing thing (if I give up dynamic typing). Is this so?
<flux__>
well, static typing rules serves as a predicate that implements that tracing
<flux__>
in ocaml a function that takes an object as an input parameter will know which methods the object will have, and that's enforced compile time
<schlick>
Dynamic typing would not be able to give that assurance across separatly compiled modules, though, right? The only way to check it is with tracing the whole thing.
<flux__>
I think such tracing is exactly what static typing accomplishes, but with much less work
<flux__>
let's say you have an array of objects
<flux__>
and you have one function to insert objects into it and another that pulls out objects from it
<flux__>
and then you have code that calls the insert with some objects and somewhere else you have code that pulls the objects and calls some method of the pulled object
<flux__>
how would you trace such a program to be executable runtime?
* schlick
takes a while to process your description.
<schlick>
The line I'm having trouble with is "and then you have code that calls the insert..." I'm not sure what you're describing there. I follow up to this point that I have a collection, I have a function to add a object, and one to remove a object.
<flux__>
let's say I have classes A and B, with methods a and b, respectively
<flux__>
and I have code: container.insert(new A); container.insert(new B);
<flux__>
should that work in your language?
<schlick>
Yes.
<flux__>
ok, then you have a = container.pop(); a.methodA();
<flux__>
how will you know if that will work compile time or not?
<flux__>
your best guess is that the container will either contain A's or B's, but you cannot know which one is the first one; obviously the order could be affected by user behavior (keys pressed etc)
<schlick>
Well, doing it my way you'd trace along the execution path till it saw a.methodA being called, then backtrack to be sure that all objects added to the collection have such a method.
<schlick>
This would work, so long as there was no external code.
<schlick>
Oh, execution paths that branch, you'd have to check all branches.
<schlick>
You should still be able to do it.
<flux__>
hmm.. so the later code would fail to compile?
<flux__>
or the first one because later methodA is used which is not in B?
<flux__>
(fixing meal &)
<schlick>
The only part I've noticed a problem is with the situation where I'm calling external code. I can assure my code is ok. I can assure that I have all the methods on the object the external code wants. However, I can't assure that just any object that the external code accepts will succeed, because while the methods on the object I give it may suffice for its interface, they might not suffice for some object the external code hand
<schlick>
It seems like having a limited set of agreed on base types is the only way around it.
<schlick>
Oh, and limiting all interfaces to accepting certain base types (so you can be sure everything is ok as it hops through separatly compiled code).
<flux__>
can't the external intefaces describe which kinds of types they require in great accuracy?
<schlick>
Ok, going back to my original plans.
<schlick>
Let's say I have this application that's linking to a graphics library.
<schlick>
The graphics library has a Window.Paint method that accepts a array (say a bitmap to show, yes I know this is fairly unreasonable but it's at least somewhat realistic).
<schlick>
I can pass it MyCustomArray object, and look at the library's documentation, which says what methods the function calls.
<schlick>
So MyCustomArray will have those.
<schlick>
However, there is no way for me to know that the library won't pass it off to some other object who needs more methods than what I put on.
<flux__>
the library will simply document the external methods it calls as methods it will call, no?
<flux__>
not much unlike java's exception handling
<schlick>
<thinks>
<schlick>
Assuming that the compiler generates a linking spec that is based on the objects other code are allowed to call, and that it overlays these (i.e. object foo calls object bar, bar needs methods a b and c, foo needs methods x y and z, thus the interface for foo requares a, b, c, x, y, z), it should work.
<schlick>
However now I'm wondering if that's static typing or dynamic typing still.
<flux__>
if you know the types compile time, it's static typing.
<schlick>
Would I be knowing the types doing what I described?
<schlick>
For instance, if a Smalltalk like system used the "trace to make sure method calls calls will succeed" within its own code, and did the overlayed limits on linking that I mentioned, would it still be dynamically typed?
__DL__ has joined #ocaml
<ulfdoz>
Gibt's eigentlich irgendwelche Impelementationen, die weitestgehend transparent einen 6to4-Gateway bauen lassen? faith gefällt mir nicht, weil DNS-Gehacke und Servicegebunden. Kann das der 6to4-Router nicht einfach selber passend umbauen?
<ulfdoz>
ECHAN, sorry
<schlick>
Hope I didn't just kill flux__
<flux__>
I would call it statically types, because the types would be known compile time
<flux__>
but I do wonder if it is possible to make smalltalk work that way without breaking the smalltalk language
<ulfdoz>
Isn't small talk one of the main examples for dynamic typing?
<schlick>
Well, actually, the problem I mentioned can't exist in Smalltalk, as such, since there is no such concept as "external code that I don't have the source code for". The Smalltalk "image" is basically one gigantic program.
<schlick>
It's considered dynamically typed yes.
<schlick>
I don't know as anybody here is that interested in my pet language design. The real short version is I'm hoping to have a very /readable/ language (most of the syntax will look like Eiffel, if I can find anything cleaner I'll use it), that does as much static checking as humanly possible. The bits I'd hoped to steal from Smalltalk is avoiding having "int somevariable" everywhere before I could use it (in Smalltalk you just use it
<schlick>
(in Smalltalk you just use it, provided the operation can succeed, you're fine) and everything is represented as a object (the extremely low level objects are usually implemented in assembly or C, but they still /act/ like objects).
<flux__>
you could statically require somevariable to have a value before it is used
<schlick>
I'm considering block based flow control but I'm not sure if it's superior to the usual structured control statements.
<flux__>
(again might not be trivial if the set of features in the languages is something that makes it difficult)
<flux__>
schlick, in any case, I would encourage you to check out ocaml and for example haskell first
<flux__>
they might give you some ideas
<schlick>
On Ocaml, are there any holes in the type system I should know about?
<flux__>
I don't think so
<flux__>
it is possible to subvert ocaml's type system with undocumented magic, though
<flux__>
so in the case you have a 'greater type system' within which you can prove that the types will be correct, it is possible to avoid ocaml's type checker
<schlick>
Would it be possible using the official language constructs? i.e. if my source code only contains stuff from the standard language, can it circumvent the type system?
<flux__>
it still does no runtime checks about the types, so it's very easy to shoot yourself to foot with those features
<flux__>
it has a separate module that has a function that converts any type to any other type
<flux__>
but there's no way you can do that accidently
<flux__>
s/tly/tally/
<schlick>
Hmm. The only thing I can think of from looking at this list of base types (int, float, bool, char, string, and unit) that I can forsee converting between would be strings and the number types, and characters and strings. Do I have to use the dangerous module to do that?
<flux__>
that's different kind of converting
<schlick>
Clarify?
<flux__>
I was referring to converting while keeping the runtime representation the same
<flux__>
like doing casts with (void*) in C
<schlick>
Ack! Why would I want to do that?
<flux__>
if you convert a number to a string, that will change the representation
<flux__>
well, I can only think of one case when I used such magic, which will be btw totally unguaranteed to work with future ocaml versions ;-), I converted Unix.fd to an integer
sese has joined #ocaml
<flux__>
because for some reason there's no function to do that, and the actual filedescriptor is hidden
<flux__>
and I only did it for debugging purposes
<schlick>
So it's only used to interface with external code?
<flux__>
so there very, very rarely is a reason to do that ;)
<flux__>
maybe sometimes when interfacing with C code, maybe
<schlick>
Ok, well, that's comforting.
<schlick>
On things like over/under-flow. Numeric variables and arrays don't do that in Ocaml, right?
<flux__>
they do
<flux__>
and one thing to keep in mind with ocaml is that int is 31 bit signed integer
<flux__>
(there exists Int32 and Int64 modules for those who want bigger numbers)
<flux__>
arrays are my default bounds checked
<flux__>
that can be disabled with a compiler switch, for performance
<schlick>
So I can still run off the end of arrays and add two numbers together and get a negative number in OCaml? <blink>
<flux__>
a) no b) yes
<schlick>
Gee, that's kinda disheartening.
<flux__>
btw, haskell has an interesting solution to the latter, it, by default, has infinite precision integers
<schlick>
There's no built in way to stop that? I'd have to add checking code to all places that modified a variable?
<flux__>
I don't think so. ocaml has some bias to good performance and runtime checking of each math operation doesn't mix well with that goal.
<flux__>
and checking that compile time would be difficult and impossible in many cases
<flux__>
you could define your own integer module and +/-/..-operators for it
<schlick>
I'd read that it does type inference. It seems like you could use that to make sure you had a big enough spot to put the integer for any value it could become.
<flux__>
but it would need to be explicitly converted to the native integer during boundaries to libraries that don't use it (ie. the standard library)
<schlick>
Meaning the C standard library on Unix?
<flux__>
it's impossible, in general, to see the range of values an integer might receive (the halting problem)
<flux__>
no, the standard ocaml runtime library
<schlick>
Well, I have, I think, come up with a possible way to solve the halting problem assuming you don't concern yourself with anything but a serial process (no threads, no other processes), and structured programming. You'd have to make sure input was read inside the loop, and that the input could read in a value that would cause loop termination.
<schlick>
Recursions would have to be treated the same as loops. They are, basically, equivalent.
<flux__>
there are languages that are guaranteed to terminate, and languages that have guaranteed memory requirements, but they aren't turing complete
<flux__>
that might not always matter, though
<schlick>
Yes, they're usually finite state automata, or have a instruction limit (upon reaching the limit they stop).
<schlick>
However, as far as I know the fix I mentioned works.
<schlick>
In traditional languages (with only structured flow control).
<flux__>
let's say you have a program that exits if (is_prime(input) && input % 2 == 0)
<flux__>
how do you check that compile time? prove that primes are not divisible by 2
<Snark>
some do
<Snark>
2, for example *g*
<flux__>
right :-)
<flux__>
% 10 = then
<schlick>
The fix I mentioned is only somewhat practical. The only way to /really/ know if you can read that input is to trace through the standard library, through the kernel, and into whatever input handling driver there is, back to where the hardware is read (where you'd need a description of expected values). If you can't do that (e.g. you're on Windows, which is closed source, or, more generally, the hardware could vary), you're stuck
<schlick>
could vary), you're stuck with the programmer having to provide "assume input can be..."
<flux__>
irc has this annoying 512 character message length limit (including protocol overhead), your first message was cut at "you're stuck"
<flux__>
how would you prove the program terminates, without running it, even if it doesn't interact with the operating system in any way?
<flux__>
let's say the program has its inputs in a list
<schlick>
As for your question, I think most program verifiers have two relevant policies there. First, they run for a finite time, and if they can't prove it safe, they consider it invalid. Further, if they don't know if they're equivalent (there's a famous math theorem people are still whittling at that I can't recall the name of), then they require you to provide the proof, the idea being "if I don't know if it's valid, and you don't kn
<schlick>
don't know if it's valid, it probably isn't, which seems reasonable".
<flux__>
that's one approach, it is difficult to see if reasonable programs would be accepted by it or not
<flux__>
for example would an interpreter be accepted?
<flux__>
because the termination property depends on the script it is given
<schlick>
Termination has to be handled specially.
<schlick>
It's a subject of many papers on how to prove total correctness. Partial correctness and total correctness are the same except with reguard to the "while property is/is-not true" loop. Tracing input back is the only fix I've ever heard of for that.
<schlick>
If it's not possible to read a value from human input, file input, ipc, or the network, that will cause termination, then the program is invalid.
<flux__>
also program isomorphism is a very difficult problem, no? (and subject to halting problem, but as you said it can be 'handled' with limited number of checking steps)
ellisonch has quit ["Leaving"]
<schlick>
Since a interpreter can read the end of file, it would be considered correct, I would think. As for things inside it, theorem provers try to break things down into individual functions (because the state explosion is less than trying to deal with the whole thing at once).
<schlick>
I'm still having to think through my language to see what's wrong with it but basically, Eiffel is a perfect language to run automatic program verifiers on. It's not purely functional, so it's not increadibly easy, however, the language does have all the needed annotations for preconditions/invariants/postconditions. It's one of the reasons for me using it as a model. The other is it gets rid of thatAwfulNotation or xtrml_bbrvtd
<schlick>
thatAwfulNotation or xtrml_bbrvtd_nms ("extremely abbreviated names", as in C, for the leetspeak impaired)
<schlick>
With Eiffel you could concern yourself with proving a method at a time.
<schlick>
After that was done you could prove the execution path.
<flux__>
well, it'll be great if you get it to work for practical programs, good luck :)
<schlick>
If each method's loops are known to terminate within a limited number of steps, or by comparing it to what the programmer claims input can be (the only way to deal with changable hardware and closed source libraries or kernels), /and/ if we handle people feeding us as yet unknown equivalence proofs by requiring them to provide the lemmas, it should work, right? As far as I know all I'm doing is basically gluing Eiffel to ACL2 (a p
<schlick>
As far as I know all I'm doing is basically gluing Eiffel to ACL2 (a program verifier that works more or less like this).
<flux__>
yeah, I imagine the key is programmer provided proofs
<schlick>
I don't think they'd be needed in most cases, do you? Even in 3-D games, which are quite complicated, most of what you'd be concerned with is bounds checking, basic algebra (for verifying that given the preconditions posconditions are true), and making sure loops can terminate (though in practice infinite loops/recursion in serial execution don't seem to happen that much, by accident). I'm wondering if there's some horribly nieve
<schlick>
I'm wondering if there's some horribly nieve assumption I'm making.
<schlick>
I'd think having a prover attached to the compiler would be handy. It'd keep programmers from having to write their own spec for their language to jam it into a generic verifier like ACL2, and then walk it through everything by hand.
revision17_ has joined #ocaml
<schlick>
flux__: Am I off my rocker?
_JusSx_ has joined #ocaml
Revision17 has quit [Read error: 110 (Connection timed out)]
<schlick>
Creepy silence. :P
<flux__>
I think a compiler-integrated proof checker would be nice
<schlick>
After what you said, I was trying to think about how to ease acceptance. Maybe having the option to just ignore verification (like Eiffel with the run time assertions turned off), run time assertions only (the way Eiffel works by default), quick verification and what you can't verify insert run time assertions for, and then full verification (and fail if we can't verify)?
smimou has joined #ocaml
__DL__ has quit [Remote closed the connection]
__DL__ has joined #ocaml
* schlick
waves. "Thanks for talking to me flux__."
<schlick>
I hopefully understand a little better now.
schlick has left #ocaml []
<flux__>
schlick, happy hacking ;)
pango__ is now known as pango
ski_ has quit [Read error: 110 (Connection timed out)]
<sebell>
I'm having difficulties with the lablgtk2 toplevel, `lablgtk2 -thread` complains: 'Cannot find file +threads.' although it was configured and built with system threads. Any insight?
kryptt has joined #ocaml
kryptt has left #ocaml []
<flux__>
my debian's lablgtk2 doesn't work at all, so sorry, no help :)
exa has quit [Remote closed the connection]
gim has joined #ocaml
sebell_ has joined #ocaml
mfurr has joined #ocaml
Skal has quit ["Client exiting"]
magnus-- has quit [Read error: 110 (Connection timed out)]
sebell has quit [Read error: 110 (Connection timed out)]
sebell has joined #ocaml
sebell_ has quit [Read error: 110 (Connection timed out)]
sebell_ has joined #ocaml
smimou has quit [Remote closed the connection]
sebell_ has quit [Read error: 104 (Connection reset by peer)]
sebell_ has joined #ocaml
sebell has quit [Read error: 110 (Connection timed out)]
sebell_ has quit [Read error: 104 (Connection reset by peer)]