exa has quit [Read error: 110 (Connection timed out)]
flux__ has joined #ocaml
zigong has joined #ocaml
_fab has quit [Remote closed the connection]
Mathman has joined #ocaml
<Mathman>
how do I determine how many elements a list has? the documentation is saying length, but then ocaml complains on me. I'm doing something like this: let line_length = line.length in
<Mathman>
it tells me "Unbound record field label length"
<pango>
List.length line
<Mathman>
ah, gotcha. thanks.
<Mathman>
hmm. I coulda sworn that the documentation said input_line returned a list of characters, but now it's telling me my line is a string, not a list.
<pango>
# input_line ;;
<pango>
- : in_channel -> string = <fun>
<Mathman>
don't suppose you'd mind looking at what I have so far, just so I know I'm not going about this the wrong way totally? http://rafb.net/paste/results/kHlOj532.html
<pango>
well, the style is very imperative, but I suppose it does the work
<pango>
you could have used output_string to save you the trouble of getting string length...
<pango>
you haven't closed the files too. They'll be closed upon program termination however
Raziel has quit [Read error: 104 (Connection reset by peer)]
Raziel has joined #ocaml
<pango>
Mathman: oh uh input_line does not keep the newline in returned string
pango is now known as pangoaway
<Mathman>
well I threw this in there: output_string output_file "\n";
<Mathman>
now comes the fun part. I need to figure out how to do regular expressions.
pangoaway is now known as pango
<pango>
ocaml native regexps are in Str module
<pango>
they're also bindings for Pcre, iirc
pango_ has joined #ocaml
pango has quit [Read error: 110 (Connection timed out)]
rq has quit ["Leaving"]
Raziel has quit ["Yo soy goma. Tú eres cola."]
shirogane has quit [Read error: 104 (Connection reset by peer)]
rq has joined #ocaml
<lispy>
and there is a syntax extension that allows pattern matching to use regexp
descender has joined #ocaml
lispy has quit [Remote closed the connection]
lispy has joined #ocaml
skylan has quit [Remote closed the connection]
skylan has joined #ocaml
mlin has joined #ocaml
_exa has quit [Remote closed the connection]
Snark has joined #ocaml
Revision17 has quit [Read error: 110 (Connection timed out)]
Revision17 has joined #ocaml
vodka-goo has joined #ocaml
joshcryer has quit [Connection timed out]
mlin has quit []
demitar_ has joined #ocaml
demitar__ has quit [Read error: 110 (Connection timed out)]
pango_ has quit [Remote closed the connection]
pango has joined #ocaml
vincenz has joined #ocaml
lightstep has joined #ocaml
<lightstep>
are there any OrderedType modules in the standard library?
m3ga has joined #ocaml
<flux__>
?
<flux__>
you usually provide your own compare function for your datatype which is then passed to modules that may make use of it..
<lightstep>
yes, but i want a simple string map
<lightstep>
i figured how to define my module for it in two lines, but i want to check wether it's already included
<lightstep>
*whether
<vodka-goo>
I don't think it is, people keep writing the same struct type t = string let compare = compare end many times
<vodka-goo>
but it's not so bad
<pango>
module StringSet = Set(String) ?
<vodka-goo>
hehe, so simple :)
<vodka-goo>
I had never noticed that the signature was fine
<lightstep>
whoa
<pango>
and module StringMap = Map(String)
<lightstep>
thanks
<pango>
learned the tip from some website not so long ago
<vincenz>
there's a String?
<vincenz>
shit, and here I'm making HashString
<vincenz>
wait... String doesn't have an equal or a compare
<vincenz>
I mean equal or hash
<vincenz>
so I can't do
<vincenz>
StringHash = Hashtbl.Make(String)
<vincenz>
pango: and it's Map.Make
<pango>
correct
<lightstep>
what's wrong with using ('a,'b) Hashtbl.t? why do you want 'b Hashtbl.Make(HashedA).t?
<vincenz>
module T = Environment.Functional.Make(Map.Make(HashString))
<vincenz>
but for that I can use string :)
<vincenz>
and the problem with Hashtbl is that it does not define a key type
m3ga has quit [Read error: 104 (Connection reset by peer)]
MisterC has joined #ocaml
Raziel has joined #ocaml
Revision17 has quit [Read error: 110 (Connection timed out)]
<vincenz>
damn sourceforge mailinglist is slow
<vincenz>
I sent a mail to it about an extension to extlib
<vincenz>
and it's still not there
gim has joined #ocaml
Schmurtz has quit ["Plouf !"]
ppsmimou has joined #ocaml
Skal has quit [Read error: 110 (Connection timed out)]
<lightstep>
are there non-string buffers in ocaml?
ppsmimou has quit ["Leaving"]
_fab has joined #ocaml
gim has quit []
<lightstep>
can i create a value of type 'a?
schlick has joined #ocaml
<lightstep>
i mean, an error value, that i can store in an uninitialized array?
<schlick>
I had a idea to deal with the people complaining memory allocation/deallocation is slow. I'm not convinced it's a good idea but I thought I'd ask. Would a non-blocking version of malloc and free make sense? Assuming the programmer was expecting it to not be immediate it would let them do further processing while waiting.
<dylan>
lightstep: not without using magical things... Why do you want to do this?
<lightstep>
to define a 'a buffer type
<lightstep>
and the efficient implementation uses uninitialized arrays
<pango>
lightstep: you can use option types... I think extlib provides uninitialized values in arrays, but it's not in standard "ocaml spirit"
<lightstep>
that's a good idea
<dylan>
pango: it's possible with the evils of module Obj, too.
Schmurtz has joined #ocaml
<pango>
dylan: sure, but I think extlib does something almost sane (raise an exception if an uninitialized is read)
<pango>
I'm not sure if it's extlib however, I'm still looking for an authoritative answer ;)
ppsmimou has joined #ocaml
<dylan>
pango: interesting!
<pango>
lightstep: or maybe extlib's DynArray is what you were looking for ?
gim has joined #ocaml
SnarkBoojum has joined #ocaml
Snark has quit [Nick collision from services.]
SnarkBoojum is now known as Snark
Raziel has quit [Read error: 104 (Connection reset by peer)]
Raziel has joined #ocaml
<pango>
lightstep: anyway, any implementation of arrays in ocaml will have a creation complexity of O(n)
<pango>
some libs don't require you to provide the value used to initialize new elements, using some magic value
<pango>
but all need to initialize elements somehow, to make the GC happy
Tachyon76 has joined #ocaml
* schlick
wanders off.
schlick has left #ocaml []
ppsmimou has quit ["Leaving"]
Schmurtz has quit [Remote closed the connection]
joshcryer has joined #ocaml
Tachyon76 has quit ["Leaving"]
<vincenz>
schlick: n
<vincenz>
schlick: no eve
Schmurtz has joined #ocaml
lightstep has quit ["leaving"]
Schmurtz has quit [Read error: 104 (Connection reset by peer)]
<vincenz>
Anyone here work on extlib?
* vincenz
just send an update to his patch for extList.ml
Schmurtz has joined #ocaml
Schmurtz has quit [Read error: 104 (Connection reset by peer)]
Schmurtz has joined #ocaml
batdog is now known as batdog|gone
zigong has quit [Remote closed the connection]
Bigb[a]ng is now known as Bigbang
exa has joined #ocaml
__DL__ has joined #ocaml
schlick has joined #ocaml
<schlick>
Anyone want to share references for program analysis (e.g. static checking, optimizing) references (books, websites, etc) or open source code I could look at? BANSHEE (latest incarnation of BANE) is all that I've found.
<vincenz>
how about the bible?/
<vincenz>
muchnick
<schlick>
Not familiar?
<schlick>
I was about to ask what Jesus had to say about optimization. :P
<schlick>
Thou shalt not include dead code in thine binaries...
<Smerdyakov>
I like Appel's compilers textbook.
<Smerdyakov>
That will explain the basic stuff.
* schlick
tries to searcn on Amazon to find these.
<vincenz>
muchnick is the most famous book on optimizations
<schlick>
I've heard of Appel's. He has several versions. I think one is for ML. Does it matter which I use?
<vincenz>
no
<vincenz>
iti's just implementation
<schlick>
vincenz: have any recommendation for what's the easiest to make out? ML code doesn't look too bad to my eyes. C has a awful lot of excessive abbrevation.
<Smerdyakov>
I'd go for ML, since none of the other languages allow code that is as readable.
* vincenz
grins at Smerdyakov
<vincenz>
I actually had the C first for a course and then bought the ML one just for the implementation
<vincenz>
anyways
<vincenz>
appel is about compilation in general, not optimization
<schlick>
Really I'd be really happy with ML if it didn't have the possibility of having a integer overflow. Kinda surprised nobody seems to talk about it. I only recently found out about it.
<vincenz>
muchnick is much better for optimizations
<Smerdyakov>
schlick, Standard ML (the one used in the book) doesn't.
<schlick>
I am interested in optimization, but to be honest the main thing I'm interested in is static analysis (to find bugs). I'd like texts on that the most.
<Smerdyakov>
schlick, 'int' operations raise Overflow on overflow.
<Smerdyakov>
schlick, and both SML and OCaml have "bignum" modules in their standard libraries.
<schlick>
Oh so you can check it?
<schlick>
Is there any way to handle it, other than crashing at runtime, or inserting checks manually?
<Smerdyakov>
Yes. There are no special "uncheckable" exceptions in SML.
<schlick>
Oh, well that's encouraging. :)
<schlick>
Ok, so on the static analysis stuff? Any recommendations? I have CQual (type checker), several model checkers, two theorem provers (one of them uses ML, MetaPRL), and several Lint-Like tools to look at source code wise. Something book or website wise would help, but I haven't turned up much good by googling yet.
<flux__>
I wouldn't btw personally mind if ocaml had runtime checks for integer overflows, because it is not difficult to forget that ints are always 31 bit (including sign) :)
<flux__>
I do wonder how often the checks could in practice be optimized out, though
<schlick>
I'm just happy to find there's some way to handle it other than having to write checks around every integer operation.
<flux__>
schlick, you're referring to coq with the theorem prover written in ml?
<schlick>
I'll need to use OCaml since some of the packages I'm working with require it.
<flux__>
you could write a module that redefines operators on integers to do checks
<Smerdyakov>
schlick, I don't think it's a good idea to try to learn by reading source code.
<flux__>
smerdyakov, easy to learn bad habits or why?
<Smerdyakov>
schlick, you are unlikely to find a unified text on the four categories of tools that you listed. Each belongs to a separate research/development community.
<Smerdyakov>
flux__, too hard to see the big picture.
<schlick>
flux__: referring to MetaPRL. I have a interest in automatically verifying programming languages. ACL2 and MetaPRL are the only two examples I can find. They aren't entirely automatic (at least in ACL2's case), but at least you can write a program, and say "show me that this is or isn't true" and they can do it (or tell you you need to give more information...).
<flux__>
I've found it often a good idea to get some picute of a language by reading source of programs written in it
<Smerdyakov>
schlick, come on, forget the rest and stick with the best: Coq! :D
<flux__>
they atleast have a goal of doing something and might reveal some general idioms
<Smerdyakov>
flux__, we're talking about static analysis techniques, not languages.
<flux__>
oh
<schlick>
Smerdyakov: It doesn't let you "program in it" as far as I know.
<Smerdyakov>
schlick, sure it does.
<Smerdyakov>
schlick, I program in Coq all day long!
<schlick>
But yes I am interested in how to perform the techniques. I can dig through the source better after I have the basic idea.
<schlick>
Smerdyakov: You're not taking advantage of a poor newbie are you? I haven't seen any theorem provers you could feed programs to other than ACL2 and MetaPRL, and I looked.
<schlick>
Talking about realistic programs now, not just math formulas.
<schlick>
There's quite a few model checkers.
<schlick>
For that, that is.
<Smerdyakov>
schlick, this is my research area. I'm not taking advantage of a poor newbie. :)
<Smerdyakov>
I write model checkers in Coq.
<schlick>
Smerdyakov: Can you tell me everything you know? :P
<Smerdyakov>
Dependently typed implementations where type-checking implies correctnessd
<schlick>
For some reason I can't seem to find people interested in this stuff. :(
<Smerdyakov>
schlick, in what environment?
<flux__>
interesting that google finds two distinct sets of results when one searches for writing programs with coq and for writing programs in coq - one would've imagined 'in' and 'with' to be stop-words
<flux__>
I'm actually interested in coq too, infact so much that I bought a book on it
<flux__>
I'm yet to read it, though ;)
<schlick>
Smerdyakov: Basically I have a issue with unstable software. <eye twitches> I really don't like it. I'd like to write a programming language that bears some resemblance to Eiffel, but has a integrated automatic program verifier. That's basically my idea in a nutshell. It'd be sorta like ACL2 or MetaPRL, only with the preconditions/postconditions/invariants/assumptions embedded in the code (like Eiffel), and noninteractive.
<schlick>
preconditions/postconditions/invariants/assumptions embedded in the code (like Eiffel), and noninteractive.
<schlick>
I can't be too loony tunes, right? I mean, someone already almost did it with ACL2 and MetaPRL...
<Smerdyakov>
schlick, I suggest looking at using dependent type systems instead.
<Smerdyakov>
schlick, and my question was about your physical/professional/academic environment. Who is around you such that you can't find anyone interested?
<schlick>
Oh, heh! I'm just some loser who's technically labled as a hardware technician, that's a hardware and software technician that also does some sysadminning, at probably what's a dead end job. But hey, everybody has to have a hobby, right? Mine's just a little ... strange.
<Smerdyakov>
That would explain why no one around you is interested. You shouldn't be surprised.
<schlick>
Well, you can poke around IRC and finding anybody interested there is hard too.
<schlick>
In the programming channels, of course.
<Smerdyakov>
You will not have trouble finding people interested in static analysis in ML channels. :)
<schlick>
Sounds like I should hang out here more then. People get REALLY hostile when you talk about static analysis on some channels. Yee.
<schlick>
Especially if you do it in reference to C or C++'s problems.
<Smerdyakov>
I don't know your background, but you might find it helpful to read first Benjamin Pierce's "Typed and Programming Languages" and then Bertot & Casteran's "Coq'Art."
<Smerdyakov>
This is a path that should work for someone with a basic college education to learn how dependent types solve all your problems. :)
<schlick>
I've heard of Lambda the Ultimate. I thought it was just some news site, sorta like Slashdot? It's cropped up on some websearches I did.
<Smerdyakov>
s/Typed and/Types and
<flux__>
schlick, same idea, but interesting articles ;)
<flux__>
schlick, btw, in addition to ml-people, also haskell-people are interested in static properties of the programs
<flux__>
also, #haskell is huge on freenode :-o (plus it has a few associated overflow channels)
<schlick>
Yes, I'm a graduate, with honors. :P Two social science degrees (don't kill me! I started out in CS, there were just people problems!). My math is a little weak but I seem to do ok so long as I'm interested.
<schlick>
Smerdyakov: these are books?
<flux__>
you started out in cs yet you have two social degrees, how does that work out?-o (or did I misunderstand)
<Smerdyakov>
schlick, yes.
<schlick>
Ok, here's the short version.
<schlick>
I live out in boonieville. Amazingly, when I was 7 or 8, I got ahold of a Commadore 64.
<schlick>
I'm a single child and wasn't allowed to have people over. Me and the computer made great friends.
<schlick>
I went through the usual "I want to be a hacker and I want to be a game programmer" phase.
<schlick>
Got into college, went into CS.
<schlick>
Now... the local college is a bit weird.
<schlick>
Grad students didn't know how to use a debugger.
<schlick>
They had you take CRAPLOADS of math, but not one class in discrete mathematics. All calculus of continuous functions.
<flux__>
:-o
<schlick>
Anyways, about the time I quit being a CS major I was getting fed up with the irrelivent math (our teacher spent something like 4 months dealing with imaginary numbers, which were just a little too imaginary for my tastes). I was getting a F in calculus and I was in this C++ class...
<schlick>
The teacher had this odd habit of grading things on things other than programming. Especially spelling and grammar.
<schlick>
If you had a function to count Fords and Fhevrolets, and it had a integer for the number of Fords and and aother for number of Chevrolets, he would require you to name them "the_number_of_fords_seen" rather than "fords"...
<Smerdyakov>
I think I can summarize this with a usual scenario title: "Someone with the actual ability and desire to learn makes the mistake of attending a 'local college.'"
<schlick>
Every so often you'd be docked for some new rule. He'd always dock you first, and then tell you what rule you violated. Almost all of them were nonsensical. The worst part is he violated them in his own handouts which were riddled with spelling and grammar mistakes.
<schlick>
Well, one day he dropped one guy /a full lettergrade/ for the brand of diskette he turned in his work on (I kid you not).
<schlick>
This pissed me off so much that I took a witness to the head of the department, spread out all his handouts so far, and graded them by his own rules (up to this point). He was making D's and F's because he docked you by 10 points (out of 100) for each error. Oddly, a program that didn't run could get a A, and one that ran and produced correct output could get a F.
<schlick>
They told me "he can run the class the way he wants".
<schlick>
I switched majors.
<schlick>
I got the sociology major "for free" since I had enough spare hours for it.
<schlick>
So the short version is I have a lot of interest, and a good bit of practical experience dealing with computers, but next to jack for formal training.
<Smerdyakov>
schlick, was there a reason that you couldn't go to a real university?
<schlick>
Lots of trouble finding sources since I don't know the proper terminology, only the idea I'm trying to communicate.
<schlick>
Smerdyakov: My parents were paying, and people where I live aren't made of money.
<Smerdyakov>
schlick, you didn't have the kind of credentials to get a full scholarship to a good state university?
<schlick>
Don't know what credentials those would be. I'm just some hick from boonieville that likes to play with computers. I visit some of my professors (the psychology and sociology ones) now and then. They tell me I could go to grad school in those fields or maybe CS, but I can't do that and hold a job, there's not enough time to do both and the work schedule is very erratic and very demanding at times.
<Smerdyakov>
If you get a 1600 SAT score, most universities in the USA will give you a full scholarship.
<schlick>
Hmm, maybe I didn't score high enough. Or maybe my parents didn't check.
<schlick>
Anyways I've graduated now.
<schlick>
Sort of water under the bridge.
<Smerdyakov>
Maybe yes, maybe no. You can always go back to school for a real CS degree and escape from your dead end.
* dylan
scratches his head.
<schlick>
I thought about that. Same thing about the psychology thing too. Sociology is too depressing for me to consider working in. I could probably function psychology wise. There is a demand for human interface design, blending psychology and computer science (with emphasis on the psychology part). I could stand doing that, but it's not really where my interests lie. The main thing is...
<schlick>
What if I did get my masters or PhD? What would I do with it then?
<schlick>
I don't want to be a professional programmer. I know how those get treated, what few haven't been outsourced.
<Smerdyakov>
schlick, do you know how they get treated at Microsoft?
<schlick>
I know they have to get out of bed and come in to fix it /immediatly/ if they break the build. I haven't looked into the rest. Have issues with MS's business practices. But yes I know they aren't going away any time soon.
zigong has joined #ocaml
<Smerdyakov>
The general rule for getting a PhD is that you wouldn't mind being a professor or research scientist in your chosen field for a good chunk of your life.
<schlick>
Referring to the nightly build.
<Smerdyakov>
It's unlikely that you'd be admitted to a reputable CS graduate program without a degree in a related field.
<schlick>
I wouldn't want to be a professor. My mom was a teacher. College isn't as bad as elementry school but it's still the job that never ends. Wouldn't leave enough time for me to play with the fun stuff, what with all the homework grading and lesson plans and all.
<schlick>
Researcher, maybe...
<schlick>
It'd be ok if it was something I was interested in.
<schlick>
Mostly I just want to write a language that does as much static checking as possible, and then write a OS in it, with just a few unique ideas (the only one never done before is my window manager). To be honest I don't really know why, it's just what I'm interested in. Guess if I managed to do that and wasn't dead yet or so old I couldn't do more, I'd like to work on preserving interesting old game designs like Widget Workshop.
<schlick>
old I couldn't do more, I'd like to work on preserving interesting old game designs like Widget Workshop.
<schlick>
Admittedly not terribly practical.
<dylan>
writing a memory manager is tedious but interesting.
<schlick>
By preserving I mean writing a copy that will run on modern OS's/hardware.
<schlick>
I think OS's and languages in general are interesting. The actual writing it can be grueling, but reading about it or working out solutions is neat.
<dylan>
Ja
<dylan>
And freaking out your "introduction to operating systems" teacher by presenting a bootable text editor on a floppy, in protected mode. :-)
<schlick>
Smerdyakov: That may be so (on not having a CS degree). I figure that part of my life is just sort of over. What's left of it maybe I can do some good with my hobbies.
Raziel has quit ["Yo soy goma. Tú eres cola."]
<vincenz>
anyone know a func that does
<vincenz>
(a' -> 'b ) -> ('b -> 'c) -> ('a -> 'c)
<vincenz>
or possibly
<vincenz>
('b -> 'c) -> ('a -> 'b ) -> ('a -> 'c)
Raziel has joined #ocaml
<flux__>
I don't think those come with ocaml, buy you can write them :)
Raziel has quit [Read error: 104 (Connection reset by peer)]
<schlick>
I sorta need to do this to keep me sane. My job drives me crazy. All the worst problems with Windows bite me constantly, namely, "mass deployment of software" is a unknown concept in the Windows world. It only works without great pains if the company thought of it, and they never do. So some distraction helps. Also keeps me from getting too depressive or worried if I keep my mind busy.
<flux__>
let (@.) a b = fun c -> a (b c) is something I've used
<schlick>
keeps me from getting too depressive or worried if I keep my mind busy.
<flux__>
(maybe)
Raziel has joined #ocaml
<vincenz>
flux__: that have right associativity?
Revision17 has joined #ocaml
<flux__>
vincenz, that's why I picked operator @. ?
<dylan>
All operators that start with @ have the same associativity of @?
<flux__>
yes
<dylan>
sweet zombie jesus, now the >:: operators of oUnit make sense.
* schlick
pokes Smerdyakov now that they've been put to sleep by the long story. :P
<flux__>
dylan, :)
<schlick>
So what were those recommendations for reading for static analysis to find bugs?
<schlick>
I'm also interested in any program-oriented theorem provers or model checkers you know of. I know you can jam a program into a generic math theorem prover but I'm afraid I'm just not at that level of sophistication. I need something easier to start with to get a idea of what I'm doing.
<vodka-goo>
if you wanna go for theorem provers and already know ocaml, coq is a nice one, and the coqart is a good reference, as Smerdyakov said
<vodka-goo>
but it's not a tool for static analysis of existing programs, rather a language in which you strongly specify programs you write
<schlick>
I'm mostly interested in the basic concepts, and in implementations of annotation-based checkers. It's not that I wouldn't look at anything else, all the ideas are worth considering, I just think it would have higher utility to have the language and the checker be integrated.
<schlick>
Such could probably be implemented on top of Coq I suppose.
<dylan>
perhaps translate an ocaml program to a coq proof? I wonder if that would be feasible?
* Smerdyakov
returns for a brief moment from practicing a talk on Coq. :)
<Smerdyakov>
I repeat what I said before:
<Smerdyakov>
Smerdyakov I don't know your background, but you might find it helpful to read first Benjamin Pierce's "Typed and Programming Languages" and then Bertot & Casteran's "Coq'Art."
<Smerdyakov>
dylan, that's what my talk is on!
<KrispyKringle>
Hmm. Is there an easy way to create an output_channel that wraps a string buffer or something?
<KrispyKringle>
Like StringBuffer in Python?
<KrispyKringle>
I have a function that prints to an output_channel and my preference for design reasons would be to not rewrite it but rather to have it write to something that becomes a string.
<dylan>
if the function takes an output_channel, you'd have to give it one.
<KrispyKringle>
I'm aware of that.
<KrispyKringle>
I didn't ask if I couldd pass it a string.
<KrispyKringle>
So for example, an ugly way to do what I want to do would be this:
<vincenz>
schlick: what's your background?
<KrispyKringle>
Create a pipe, pass the write end of the pipe to the function, read from the read end of the pipe into a string.
<KrispyKringle>
But like I said, this is really ugly.
<vincenz>
it's a pity that we don't have typeclasses
<KrispyKringle>
I was wondering if there's a good way to do this.
<vincenz>
or you could make your own OutputChannel that just pipes
<KrispyKringle>
Right, ok.
<dylan>
or if output_channel was a class
<KrispyKringle>
Sorry, out_channel. I typoed.
<flux__>
smerdyakov, how far can that conversion be automated?-o
<KrispyKringle>
I'm not familiar with how out_channels work. Their usage implies they can wrap different sorts of IO.
<KrispyKringle>
Or maybe not. Being used for both sockets and files doesn't mean a lot, since those are essentially the same on Unix anyway.
<dylan>
then you could have functions like val write_thesis : < out_string : string -> unit; .. > -> unit
<KrispyKringle>
What Cash does is emulate string channels with temp files.
<KrispyKringle>
God. If that's the best they can do, I think I ought to just rewrite this function.
<vincenz>
ARGHGHHHH
<vincenz>
why the F*CK do Map and Hashtbl not use a similar interface
<vincenz>
Hasthbl: 'a t -> key -> value -> unit
<vincenz>
Map: key -> value -> 'a t -> 'a t
<vincenz>
make em both either take key value first or the table first
* vincenz
grrs
<dylan>
vincenz: Because functional modules tend to have the structure data last,
<dylan>
so you can do neat things with fold_left and lists.
<vincenz>
dylan: yeah but why not do the same with imperateive modules
<vincenz>
at least it's consequent
* vincenz
mutters
<dylan>
True
<dylan>
Both Queue and Stack are like that
<vincenz>
I have a Functional Environment impl
<vincenz>
and a SharedFucntional impl
<vincenz>
one is a stack of Maps the other a stack of hashtbls
* vincenz
grrs
<vincenz>
blegh
<schlick>
vincenz: As for my background, assume I'm a idiot, it's easier, and avoids ego battles. :P I give up before they start, and at least you won't be talking over my head.
<schlick>
I'm sorry for being slow, I was talking elsewhere.
pango has quit ["Leaving"]
<vincenz>
blegh
pango has joined #ocaml
<vincenz>
schlick: it's got nothing to do with ego battles, just curious why you need this
<dylan>
mmm, waffles.
<vincenz>
how come there's no map for Hashtbl?
<dylan>
There's a fold.
<vincenz>
no map tho
<vincenz>
extlib has it apparently, but not for the functorized version
<vincenz>
what crap
<schlick>
vincenz: The reason I need this is I'm obcessive and I hate bugs. My entire village was wiped out by a marauding group of bugs, lead by the evil empire which shall not be named. My father gasped out his last wish that I learn how to eradicate them from the face of the earth, and so here I am.
<vincenz>
...
<schlick>
vincenz: Well, the first part is true at least. ;)
* dylan
snickers.
<vincenz>
...
<dylan>
Sorry, um... American joke?
<dylan>
Hmm, it seems like lablgtk programs don't use the same gtk theme as other gtk apps.
<KrispyKringle>
Could it be that it's using GTK1 while other apps are using 2? Or the other way around?
<KrispyKringle>
The two engines have different theme configs, if I remember right.
<schlick>
Thanks for the pointers to references vincenz, Smerdyakov, and dylan.
<schlick>
And thanks for not beating me over the head for asking.
<schlick>
Random ML question...
demitar_ has quit ["Bubbles..."]
<schlick>
Why is it more languages don't allow nested block comments?
mrpingoo has joined #ocaml
<schlick>
Is there some problem with them I haven't noticed?
mrpingoo is now known as edesarna
<schlick>
They seem like the obvious 'right thing to do' comment wise.
vodka-goo has quit [Read error: 110 (Connection timed out)]
<schlick>
Smerdyakov: Anywhere the information in your talk would be made available online?
<schlick>
Everybody's gone quiet. I must have said something stupid again.
m3ga has joined #ocaml
raziel_ has joined #ocaml
raziel_ has quit [Client Quit]
<Schmurtz>
schlick, for nested comments, I think it's a problem of parsing
<Schmurtz>
it's far from easier to parse a non-nested comments with a home made parser
<schlick>
Suppose so. Seems like widespread things like C and C++ would have added them by now.
<Schmurtz>
an other idea : I don't think one can extract nested comments with a lexer
<schlick>
Hmm. Why would that be?
lightstep has joined #ocaml
m3ga has quit ["disappearing into the sunset"]
<Schmurtz>
a lexer is just a program that cut the entry in tokens
<Schmurtz>
with lex, you define each token with a regular expression
<Schmurtz>
nested comments cannot be extracted with regular expressions
<flux__>
but the tokenizer could just (almost) as easily handle recursive comments as it can now non-recursive
<Schmurtz>
if the tokenizer know how many comments are currently opened
<flux__>
and it can know
<flux__>
we're talking about few additional lines of code at worst, aren't we? btw, sometimes it can be useful to have non-recursive comments
<Schmurtz>
yes, but if you use a standard lexer like lex, you can't
<Schmurtz>
(-standard + generic)
<flux__>
for example I think in pascal I might have written code (while debugging, developing) like a := b + c (* + 42*); and changed that to a := b (* + c (* + 42*);
<flux__>
so a larger commented region without the need to match the end marker ;)
kmagdsick has joined #ocaml
<schlick>
I see, so it makes parsing slightly harder.
<flux__>
I think this is a minor issue though. one POV might be that not allowing recursive comments discourages leaving large blobs of dead code inside comments into the code
<schlick>
On Coq'Art I can't seem to find that book on Amazon.com
<flux__>
"Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions"
<schlick>
flux__: it seems like it should be minor given the other problems a compiler would have to deal with. It just looks like it'd make it really easy to comment chunks out without much effort, or risk of screwing up (as the famous non-nested C/C++ comments cause).
<lightstep>
i'm having problems with lists and maps. i'm trying to create a map of values to their indices in a string, and i can't find a functional way to do this: http://rafb.net/paste/results/yZmYfI51.html
<lightstep>
s/in a string/in a list/
<schlick>
I see. I used the advanced search for the author's name and that came up, after the title by itself didn't. I didn't know it was the same book. I just saw the part before the Coq'Art.
<flux__>
lightstep, fold
<flux__>
lightstep, original parameter for fold would be (map, 0)
<lightstep>
oh, thanks. i got it.
<Schmurtz>
fold, may be viewed as a iter function with a global variable
<lightstep>
yes, i forgot the ability to pass a state in the side (thought of it a map)
<schlick>
flux__: Thank you.
<schlick>
I suppose it would be worthwhile to look at "Advanced Topics in Types and Programming Languages" as well?
lightstep has quit [Remote closed the connection]
edesarna is now known as vodka-goo
<vincenz>
re
<vincenz>
schlick: I doubt ATTAPL is useful
<schlick>
vincenz: Why is that?
<vincenz>
it's rather advanced
<vincenz>
with very specific topics
<schlick>
Would it make sense after the first book?
<vincenz>
I haven't looked at it
<vincenz>
but I looked at the amazon description
<vincenz>
and it seemed too specific for my use
<schlick>
On theorem provers... It's my understanding you can't generate counter-examples with them. Is there some particular reason for this? Sorry if it should seem obvious. It's obvious why model checkers can to me. But it seems like it should be possible.
<vincenz>
not sure what you mean
<schlick>
If your program violates some rule for the language (e.g. writing past the end of a array), or one of your preconditions/postconditions/invariants, it's handy to know why. A counter example is a example of input that would cause a violation of one of the rules.
<schlick>
Model checkers try all the possible states the program can get into, so obviously they can just show you one that would trigger it, since they already know of it.
<vincenz>
I think it's cause theorems form an infinite set
<vincenz>
while states do not
<schlick>
Hmm.
<schlick>
To make useful statements about a program, wouldn't you have to specify the set that's valid for input, and the set that's valid for output, for a function, at the very least?
<schlick>
I can see how that would be vast, but it seems like it would be finite.
<vincenz>
yes but you specify them with types
<schlick>
I suppose that's true. From most languages use of the term it isn't terribly clear to me what is ment by types. I've read the definition but it doesn't help much. In any case I'm just not sure why since you know the set that you allowed, and the set that's invalid, why you can't at least theoretically solve for the set that overlaps (if any).
<vincenz>
read tapl
<schlick>
I plan to. I don't have a copy yet though.
<vincenz>
you can see types as assertions on values
<schlick>
Types according to most programming languages seem to mean limits on what you can do with a variable (e.g. if it's "const" you can't write to it) and how much space is allocated to it.
<vincenz>
(I'm not a formal Cser so just trying to explain how I see it)
<vincenz>
yes
<vincenz>
but they're assertions to open ended sets
<schlick>
But then there's very peculiar types like those used in CQual.
<vincenz>
no idea
<schlick>
And apparently there are ways of inferring them, and so on.
<schlick>
I'm going back through these theorem provers that are software oriented to see if I missed any and apparently I did. My list now says ACL2, MetaPRL, Coq, Isabelle, and Larch. Are there any others?
<vincenz>
no idea
<vincenz>
not my field
<schlick>
Smerdyakov: Any input?
__DL__ has quit ["Bye Bye"]
zigong has quit [Remote closed the connection]
Snark has quit ["Leaving"]
Bigbang is now known as Bigb[a]ng
joshcryer has quit []
_fab has quit [Remote closed the connection]
<vodka-goo>
schlick: there are really a lot of them.. I think of mizar and twelf right now.