sponge45 changed the topic of #ocaml to: Discussions about the OCaml programming language | http://caml.inria.fr/
mbishop has quit [Remote closed the connection]
mbishop has joined #ocaml
smimou has quit ["bli"]
<twobitsprite> so... I can't find a good example of this in the docs, but if you define a type fully in the signature of a module, do you need to repeat that definition in the module itself?
<Smerdyakov> Yes.
<twobitsprite> k, thanks
<Smerdyakov> If you want that equation to be visible to clients
<twobitsprite> right... and I need to do that if it's a variant type of which I want the clients to be able to use the constructors, right?
<Smerdyakov> You can define work-alike wrapper functions for them if that suits your purposes.
<twobitsprite> so that's a yes? :P
<Smerdyakov> No. You haven't sufficiently defined "use the constructors."
<twobitsprite> module Foo : sig type my_type = Bar of int | Baz of float end = type my_type = Bar of int | Baz of float end ;; let _ = Bar 4
<Smerdyakov> See, you could include a bar function that calls Bar, and clients could use that.
<twobitsprite> er... let _ = Foo.Bar 4
<twobitsprite> right, but what I've just defined is correct?
<Smerdyakov> No. You missed 'struct'.
<twobitsprite> nit-picker :P
jlouis has joined #ocaml
* Smerdyakov is so excited to see jlouis that he almost soils himself.
<jlouis> oh, stop it!
<jlouis> hehe
pango_ has joined #ocaml
nonpop has quit ["Leaving."]
<Smerdyakov> jlouis, you might like to read this page I have made and tell me what you think: http://www.cs.berkeley.edu/~adamc/mlcomp/ (comparison of OCaml and SML)
<jlouis> Reading after I get some coffee inboards the system
nonpop has joined #ocaml
<twobitsprite> Smerdyakov: you're peoples have no arms... how sad...
<Smerdyakov> It is their way.
* twobitsprite wonders how they interact with thier text editors...
<jlouis> Now the coffee is steaming hot. Then I can read
pango has quit [Remote closed the connection]
<twobitsprite> yeah... I still think I like OCaml better, however I wish it had some of the features of SML
<twobitsprite> but then again, I have no problem with "imperative" programming style...
<twobitsprite> (which seems to be more widely supported by OCaml...)
<jlouis> Smerdyakov, pretty good and comprehensive comparison. I wasn't aware of many of them. I have always tended to use SML-style stuff in OCaml
<jlouis> OTOH, my OCaml coding is very limited
<Smerdyakov> jlouis, BTW, what is your student/professional status now?
<jlouis> haha
<jlouis> I am nowhere
<jlouis> Still undergrad
<jlouis> Working half-time
<jlouis> (In Java, of all abominations)
<Smerdyakov> How long have you been an undergrad?
<jlouis> 6 years I think
<Smerdyakov> Ew.
<jlouis> Which is far too long
<Smerdyakov> I'm hoping to finish undergrad + masters + PhD in not much longer. :)
<jlouis> I Can't focus on a single subject.
<jlouis> its not impossible to undergrad + masters + PhD in that time
<jlouis> still hacking certifying comp?
<Smerdyakov> I'm not sure what that is supposed to expand to.
nonpop has left #ocaml []
<jlouis> certifying compilation
<Smerdyakov> No, I'm doing certified compilation now.
<jlouis> what is the difference?
<Smerdyakov> Prove the compiler works instead of proving that individual outputs work.
<jlouis> (or is my grammar miserable)
<jlouis> aha!
<jlouis> Does this include great familiarization with Coq and Twelf?
<jlouis> anyhow, the comparison is good! It must have taken some hours to punch together
<Smerdyakov> I have moderate familiarity with Twelf, and I think it's fair to say that I am a genuine Coq wizard by this point.
<jlouis> thought as much
<Smerdyakov> I don't think Twelf has much mileage left in it. ;(
<Smerdyakov> Er, ;)
<jlouis> I ponder how far down you are proving stuff. Does it include the runtime and GC? I remember Doliguez did that for OCamls GC
<Smerdyakov> He proved a correctness theorem for OCaml's garbage collector in Coq? O_O
<jlouis> It was not in Coq, but rather "on paper" IIRC
<Smerdyakov> Oh. A "folk proof." ;D
<jlouis> haha
<Smerdyakov> The initial project I cut off as a "publishable unit" is parametric in arbitrary runtime systems satisfying particular criteria. I didn't actually build or certify such a system.
<jlouis> ok, It is also a daunting task to do
<jlouis> on the other hand, when you do have a certified compiler, it is going to be extremely valuable
<jlouis> I have been looking a bit into program inversion lately. Its a quite interesting subject
<twobitsprite> inversion?
<jlouis> ie, given a program p : X -> Y such that p(x) = y, does p^-1 exist with p^-1 : Y -> X such that p^-1(y) = x
<Smerdyakov> I _do_ have a certified compiler.
<jlouis> A program inverter is a program that can invert other programs
<twobitsprite> jlouis: ahh...
<Smerdyakov> Writing certified compilers is easy. You have to specify what's being compiled to what and what's being certified to make it hard.
<jlouis> Smerdyakov, for ML? There are certain "practicality" criteria that has to be fulfilled I might add ;)
<jlouis> Smerdyakov, indeed
<Smerdyakov> jlouis, I'm hoping to do a certified compiler for a larger subset of ML eventually. Right now I have one for STLC.
<jlouis> ST-Lambda-Calc?
<jlouis> I don't know the language
<Smerdyakov> Yes.
<Smerdyakov> Simply-typed lambda calculus
<jlouis> ah, then I _do_ know the language, but not the abbreviation ;)
<jlouis> twobitsprite, The "vision" is to define an encoder for eg a compression routine and then have it derive the decoder
<Smerdyakov> jlouis, is that really a useful project?
<jlouis> It will take some time before we are there, though
<jlouis> Smerdyakov, I think it is more about the low-hanging fruit that might fall out
<jlouis> The problem is that these guys are bored because they have been working on partial evaluation for 25 years
<jlouis> So they are looking for greener grass
<Smerdyakov> Certified software is where the future is.
<twobitsprite> Smerdyakov: I didn't think "usefullness" was a criteria for academic projects...
<Smerdyakov> The area is getting to the point of escaping the aspersions cast on it on the 80's and holding down a respectable dedicated session of POPL each year. :)
<jlouis> twobitsprite, the pessimistic would say that "publishable material" is..
<twobitsprite> jlouis: and the optimist?
* twobitsprite is alien to the academic world...
<jlouis> He would quote Feynman.
<twobitsprite> (at least, the academic "computer science" world...)
<jlouis> (ie, work on something you think is fun. It may have something interesting in it)
<twobitsprite> jlouis: ahh
<twobitsprite> jlouis: I guess that's what I'm kinda doing with my project
<jlouis> Well, there is the little caveat that you probably _should_ find something which can be picked up by a respectable journal.
<Smerdyakov> There's the small matter of _surviving_ whilst working on your little toy. ;)
<twobitsprite> well... I'm not really concerned with either "respecable" nor journals
<jlouis> In due time. Hence it is too risky to spend 5 years searching in vain for something. And it might have been better to take that as 6 1-year steps instead
<twobitsprite> s/either/neither
<jlouis> I think the era of the "lone researcher" is well over
* twobitsprite isn't "researching"
<jlouis> what are you doing?
<twobitsprite> programming :P
<twobitsprite> just for shits and grins
<jlouis> yes, but _what_?
<twobitsprite> an AI to play Go
<twobitsprite> (the board game)
<jlouis> That is interesting
<twobitsprite> namely, and genetic programming experiement in search for a strong board position analyser, using massively distributed (a la SETI@Home) populations
<Smerdyakov> twobitsp1ite, not exactly an original project idea, eh?
<twobitsprite> no?
<Smerdyakov> No.
* twobitsprite has looked far and wide for distributed genetic programming
<Smerdyakov> Game playing is tres cliche, as are genetic algorithms, especially among laypeople.
<mbishop> There is a show on the history channel right now that just mentioned AI and robots taking over the world :P
<mbishop> It's a show about possible ends to the world
<twobitsprite> Smerdyakov: ohh... I thought you were saying that someone else has started my project...
<twobitsprite> mbishop: speaking of unoriginal ideas... haven't they seen War Games?
<jlouis> twobitsprite, Is OCaml your delivery vehicle?
<twobitsprite> jlouis: it is what I'm writing my program in, if that's what you mean
<twobitsprite> jlouis: unless you mean the language that the agents are writen in, in which case its a small postscript-like subset
<jlouis> Yes, it was what I meant
<twobitsprite> Smerdyakov: so you dislike my project idea because GA is cliche?
<Smerdyakov> twobitsp1ite, yes, that's why I have a negative initial reaction to it.
<twobitsprite> interesting... why so?
<twobitsprite> do you have any pragmatic arguments against it, or is it just a matter of "GA is like sooo last season"?
<Smerdyakov> I think it's likely that you have no special insight and are just going after ideas portrayed glamorously in popular media.
<twobitsprite> Smerdyakov: so, the latter
<twobitsprite> besides, I haven't seen GA portrayed much in popular media...
<jlouis> GA is definitely one of the more portrayed parts
* twobitsprite doesn't read much popular media
<twobitsprite> Smerdyakov: do you have alternative recommendations in the vein of search algorithms?
<jlouis> Is there BTW a good OCaml syntax introduction for an SML bastard like me?
buluca has quit [Remote closed the connection]
<Smerdyakov> jlouis, see the link on the page I linked.
<jlouis> (Who also looked into Scheme, Haskell, Erlang, Python)
<Smerdyakov> twobitsprite, nah. The only search that interests me is proof search/logic programming.
<twobitsprite> Smerdyakov: so you're just biased against automated algorithm search...
<twobitsprite> ?
<twobitsprite> (I'm not sure if I worded that well)
<jlouis> Smerdyakov, Do you mean Rossberg's syntax comparison?
<Smerdyakov> jlouis, yes.
<jlouis> ok, It will come handy
<Smerdyakov> twobitsprite, it doesn't interest me, so I don't know much about the literature.
<twobitsprite> Smerdyakov: yet, you assert that my choice is a poor one?
<Smerdyakov> twobitsprite, let me rephrase that: "automatic algorithm search" based on theorem-proving techniques do interest me; I just find genetic programming uninspiring.
<twobitsprite> Smerdyakov: hmm... I'm not well read in theorem-proving... would there be applications in game programming?
<Smerdyakov> Have you seen any evidence that algorithm search is effective in game programming?
<twobitsprite> I haven't seen any application of it to game programming, so no.
<Smerdyakov> I'm not aware of any threads in the research world where this line of inquiry is considered fruitful.
<twobitsprite> most papers seem to be searching for i.e. compression algorithms, or chip layout kind of stuff... occasionally applied to industrial systems...
<twobitsprite> however, I have seen one program which applies a _very_ simple search for a Go playing algorithm which over small time scales yield interesting results... but that mostly seemed like a little toy project
<twobitsprite> my understanding of GA/GP is that it mostly boils down to a compromise between quick convergance, which might converge to something too simplistic, or broad convergange which might yield more complex systems, but take much longer time
<twobitsprite> hence my idea that massively distributed search might be interesting
buluca has joined #ocaml
triple__ has quit [Remote closed the connection]
<jlouis> twobitsprite, Genetic algorithms for search will always be a heuristic. There might be other ways to go which are better
<jlouis> In chess for instance, that seems to be the case
<twobitsprite> jlouis: I'm not sure I understand
<jlouis> twobitsprite, I am just saying that GP might not be the best solution to your problem
<twobitsprite> jlouis: any suggestions?
<twobitsprite> and I'm not sure what you mean by "will always be a heuristic"...
<jlouis> A pruning search of the tree is what works with chess. I do not know if that works well with Go though. I don't think so
<twobitsprite> very much not so
<twobitsprite> the branching factor in Go is _much_ steeper
<jlouis> Indeed
triple__ has joined #ocaml
<Smerdyakov> twobitsprite, what makes you believe that there exists a compact enough algorithm to find?
<twobitsprite> Smerdyakov: compact enough?
<Smerdyakov> Yeah. Small enough that GP has any hope of finding it.
<twobitsprite> I realise what you mean: that GA loses efficiency when the algorithms become more complex... but again, hence the distribution
<Smerdyakov> Or small enough that it's even of any _use_ to you if an oracle hands it to you.
<twobitsprite> I guess I'm hoping for the brute-force power of a large-scale computing system
<jlouis> exhaustive search of a steep tree... ;)
<jlouis> You have the O-notation against you, my friend ;)
<twobitsprite> jlouis: well, the problem with that, is that must be done at real-time by the system as a whole during the course of a single game...
<jlouis> If you believe in it, I think you should build it. But if it fails, be sure to document as to why
<twobitsprite> with the GA, each node in the system might have its own population, which occasionally spills over onto the other nodes, eventually yeilding a single algorithm (amongst others) which is efficient enough to be run on a smaller system
<jlouis> Negative research is not valued much, but it is important
<twobitsprite> I think my first concern with it not being successful is not attracting enough nodes...
<jlouis> heh
<twobitsprite> i.e. I plan to write a nice colorful interesting screensaver that people will want to run :)
<jlouis> haha
<twobitsprite> (but that's much further down the line, I haven't given it much thought than that)
<jlouis> I've always said they should entertain at universities in Social Engineering, hehe
triple__ has quit [Remote closed the connection]
<twobitsprite> :)
<twobitsprite> anyways... thanks for the feedback y'all... I'll be sure to keep you all posted :)
* twobitsprite must go entertain the wife
<jlouis> That sounds far too perverted for a programming channel. I'll look more at Erlang then ;)
FZ has joined #ocaml
triple__ has joined #ocaml
bluestorm_aw has quit ["Konversation terminated!"]
swater has quit [Remote closed the connection]
mbishop has quit [Remote closed the connection]
malc_ has joined #ocaml
descender has quit [Read error: 110 (Connection timed out)]
malc_ has quit ["leaving"]
descender has joined #ocaml
mbishop has joined #ocaml
joshcryer has quit [Client Quit]
pantsd has joined #ocaml
pantsd has quit [Client Quit]
pstickne has quit [Remote closed the connection]
pantsd has joined #ocaml
levi_home has quit [Read error: 104 (Connection reset by peer)]
levi_home has joined #ocaml
Smerdyakov has quit ["Leaving"]
_velco has joined #ocaml
smimou has joined #ocaml
bluestorm has joined #ocaml
FZ has quit ["ERC Version 5.0.4 $Revision: 1.726.2.20 $ (IRC client for Emacs)"]
asm has joined #ocaml
pango_ has quit [Remote closed the connection]
velco has joined #ocaml
pango has joined #ocaml
bluestorm is now known as bluestorm_aw
swater has joined #ocaml
buluca has quit [Read error: 110 (Connection timed out)]
buluca has joined #ocaml
buluca has quit [Read error: 110 (Connection timed out)]
pstickne has joined #ocaml
batdog is now known as batdog|gone
bluestorm_aw is now known as bluestorm
bluestorm is now known as bluestorm_aw
asm has quit [Read error: 60 (Operation timed out)]
slipstream has quit [Remote closed the connection]
bluestorm_aw has quit [Remote closed the connection]
slipstream has joined #ocaml
bluestorm has joined #ocaml
nonpop has joined #ocaml
Demitar has joined #ocaml
slipstream-- has joined #ocaml
ikaros has quit [Read error: 110 (Connection timed out)]
ikaros has joined #ocaml
klapmuetz has joined #ocaml
slipstream has quit [Read error: 110 (Connection timed out)]
piggybox has quit []
klapmuet1 has quit [Read error: 60 (Operation timed out)]
joshcryer has joined #ocaml
MrCraps has joined #ocaml
Smerdyakov has joined #ocaml
asmanian__ has joined #ocaml
MrCraps has quit [Read error: 104 (Connection reset by peer)]
asmanian__ has quit ["Verlassend"]
Demitar has quit [Read error: 110 (Connection timed out)]
velco has quit ["Ex-Chat"]
MrCraps has joined #ocaml
AWizzArd has joined #ocaml
MrCraps has quit [Remote closed the connection]
_velco is now known as velco
malc_ has joined #ocaml
_JusSx_ has joined #ocaml
AWizzArd has left #ocaml []
Demitar has joined #ocaml
bluestorm is now known as bluestorm_aw
pantsd has quit [Remote closed the connection]
dark_light has joined #ocaml
<dark_light> format_of_string was meant for what? it don't accept any strings i am testing (maybe it accepts only static strings - but static strings already can be read was formatters!)
malc__ has joined #ocaml
malc_ has quit [Read error: 110 (Connection timed out)]
postalchris has joined #ocaml
<pango> dark_light: let a = format_of_string "%s out of %s" in Printf.printf a "one" "two"
<dark_light> only this? i am trying to print a string with spaces with the Format.printf (translating all spaces to "@ "), so the formatter may break at each space
<Smerdyakov> dark_light, that's not possible.
<dark_light> so i think i must scan the strings and call the Format.print_* functions
<Smerdyakov> The only programmatic way for building format strings that I'm aware of is to start with string constants and concatenate with ^^.
<Smerdyakov> And that is still very limited, since the OCaml type system isn't expressive enough to describe types of intermediate format strings in loops.
<dark_light> the problem is that i will receive the string from a file
<Smerdyakov> You will receive the format string from a file?
* dark_light thinks Format module is too restricted
<dark_light> Smerdyakov, no, the text itself
<dark_light> and i will attempt to pretty-print it
<dark_light> hint-breaking in each space
<Smerdyakov> dark_light, the whole format string business is already a horrible hack without principled type system support.
<Smerdyakov> That reminds me to add this to my comparison page. :D
<dark_light> but the other technique (parsing the string, and calling appropriate functions) don't seems very nice
<Smerdyakov> I don't understand.
<dark_light> hmmmn, just ugly:)
FZ has joined #ocaml
dark_light has quit [Read error: 104 (Connection reset by peer)]
FZ has quit ["nite nite..."]
stevan has quit ["Leaving"]
_JusSx_ has quit [Client Quit]
stevan has joined #ocaml
swater has quit ["Quat"]
smimou has quit ["bli"]
stevan_ has joined #ocaml
stevan has quit [Read error: 110 (Connection timed out)]
velco has quit ["I'm outta here ..."]