<mr_hugo>
oh yes this genlex looks just what i was looking for :)
<mr_hugo>
i tried ocamllex, but its like lex for C :/
<bluestorm>
with Genlex you have to use streams
<bluestorm>
there are two ways to do it, the low-level one, wich is in the Stream library (Stream.peek and Stream.junk, mostly), and the one using a camlp4 syntax-extension
<bluestorm>
(to be able to compile code using [< >] you have to give "camlp4o.cma" as first parameter of your compilation command : ocaml camlp4o.cma foo.ml, ocamlc camlp4o.cma foo.ml -o foo, etc.)
<flux>
mr_hugo, maybe simply using Scanf.sscanf in aloop will be enough for your purposes
<mr_hugo>
is there any way to create a stream from a string ?
<mr_hugo>
flux, yes, but the characters dont have defined delimiters :/
<mr_hugo>
i can have M 123 321 or M123 321
<mr_hugo>
so lex is probably the right choice
<bluestorm>
mr_hugo: that is in the Stream module documentation
<bluestorm>
the "standard library" part describe all the modules you can use without changing your compilation methods
<bluestorm>
other ones are included but you need to give them to the compiler too
<bluestorm>
(eg. ocamlc str.cma ...)
<mr_hugo>
i installed xml-light for xml parsing
<mr_hugo>
ocaml has a easy syntax for adding extra modules
<mr_hugo>
wich is great
<mr_hugo>
:)
ktne has joined #ocaml
tty56_ has joined #ocaml
pantsd has quit [Read error: 110 (Connection timed out)]
tty56 has quit [Read error: 110 (Connection timed out)]
cpst has joined #ocaml
jlouis has quit [Read error: 110 (Connection timed out)]
ygrek has quit [Remote closed the connection]
Tetsuo has quit ["Leaving"]
dmentre has joined #ocaml
cpst has quit [Read error: 110 (Connection timed out)]
slipstream has joined #ocaml
seafoodX has joined #ocaml
seafoodX has quit [Client Quit]
jlouis_ has joined #ocaml
<ktne>
how do i define mutually recursive functions
<ktne>
?
<bluestorm>
let rec .... and ...
<bluestorm>
"and" replace the second "let"
<bluestorm>
and no need for another "rec"
<ktne>
ah
<ktne>
just like mutually recursive type?
<bluestorm>
yes
<ktne>
ok thanks
<bluestorm>
(and mutually recursive classes ^^)
<danderson>
just like mutually referencing anythings I'd assume
* danderson
guesses that let ... and ... just tweaks the scoping rules to have names defined at the right time
<bluestorm>
what else ?
<fremo>
classes ? :)
<bluestorm>
i mean, what else than tweaking this way ?
<bluestorm>
iirc it's the precise semantic of 'and' : "simultaneous declaration"
<bluestorm>
and the evaluation order is not specified
<danderson>
I don't know. But then again, I've just wasted 2hrs tracking down a bug that turned out to be an obscure technicality of C++ virtual semantics
<danderson>
so my view of what is "sane" is kinda skewed right now
<bluestorm>
( "let x = read_int () and y = read_int () in" are hunting you down ! )
<bluestorm>
hm danderson
<bluestorm>
Is learning OCaml a recovery program ?
<danderson>
it's brain morphine
<danderson>
prevents me going nuts
<bluestorm>
"C++-ill programmer looking for a sweet languagotherapy"
<danderson>
I would be clinically insane right now if I only knew C++ :)
<danderson>
thankfully, I have python and a little ocaml to soothe me.
<danderson>
I know that programming doesn't have to be horrible ;)
<bluestorm>
:p
<ktne>
:)
Demitar has quit [Read error: 113 (No route to host)]
munga has joined #ocaml
<munga>
techinical question: what is the complexity of the type inference algorithm of ocaml ? And ... Is ocaml basically polymorphic lambda-calculus with general recursion ?
<zmdkrbou>
probably exponential
<munga>
you mean exptime-complete ? Do you know of any fringe case that have worst complexity ?
<zmdkrbou>
dunno
* zmdkrbou
not very good at complexity
pattern has quit ["Reconnecting to server - dircproxy 1.1.0"]
<zmdkrbou>
but i guess you could find someone at pps who could answer those questions :)
pattern has joined #ocaml
<munga>
I suppose so :)
<munga>
but not on a friday afternoon in august !
Demitar has joined #ocaml
* zmdkrbou
shakes ppsmimou / smimou
buluca has quit ["Leaving."]
buluca has joined #ocaml
<bluestorm>
hm
<bluestorm>
the type inference complexity was discussed on the mailing-list
<munga>
do you know when (approximately)
<bluestorm>
hm
<bluestorm>
i remember of a quite recent problem with polymorphic variant
<bluestorm>
but polymorphic variant type inference is a special part
<bluestorm>
for your second question, i don't really understand what do you mean by "basically"
<bluestorm>
you can say ML is a typed lambda calculus with parametric polymorphism
<bluestorm>
but there are some more things (let-bindings for example)
<bluestorm>
every language feature add some complexity, so i wouldn't say that's "basically lambda-calculus"
<bluestorm>
(hm and there is some mutability too, wich lambda-calculus does not have (does it ?))
<munga>
ok, so if ocaml is typed lambda calculus with parametric polymorphism what is haskell ? I don't understand why one has explicit type and not the other and what is the complexity of doing type inference for haskell without adding types manually
rwmjones has left #ocaml []
<bluestorm>
haskell does have type inference
<bluestorm>
hm
<bluestorm>
at some point when adding features to the language, you have to make type-inference non-decidable on some part
<bluestorm>
the ocaml choice is to restrict those part as much as possible
<bluestorm>
the haskell one is to use type annotations everywhere
<munga>
ok, then my question is what makes haskell type system not decidable ?
<bluestorm>
hm
<bluestorm>
i'd guess, ad-hoc polymorphism
<bluestorm>
hm
<bluestorm>
GADT require type annotations too (but they are not included in Haskell98 iirc)
<munga>
the magic word ... so ocaml is typed lambda calculus with parametric polymorphism while haskell is typed lambda calculus with ad-hoc polymorphism ?
<bluestorm>
hm
<bluestorm>
haskell has parametric polymorphism too
<bluestorm>
the ad-hoc polymorphism parts are the type classes
<munga>
well yes, but just because ad-hoc polymorphism is a generalization of parametric polymorphism ?
<bluestorm>
hm
<bluestorm>
i don't know these question enough to answer you
<bluestorm>
the haskell.org website has some papers around haskell
<bluestorm>
you should have a look
<munga>
anyway, I've more kewords to google with now :)
<mattam>
TAPL by benjamin pierce is the standard textbook.
<mattam>
higher-order polymorphism makes Haskell type system undecidable, not type classes (although, some typeclasses extensions makes it undecidable too).
Tetsuo has joined #ocaml
<munga>
So ad-hoc polymorphism (even if I don't know what it is ...) is not the problem ...
<bluestorm>
hm
<ktne>
anyone here familiar with f# who can tell me how to access a tuple member?
<bluestorm>
the ocaml way is to do pattern-matching
buluca has quit ["Leaving."]
buluca has joined #ocaml
<bluestorm>
let (_, _, third) = triple in
<ktne>
but i have to access the tuple in a function
<ktne>
no
<ktne>
i need to do something like tuple[0].Read
<ktne>
i need to access the tuple
<ktne>
the tuple is a stream reader
<mattam>
munga: no, at least for H98
<ktne>
bluestorm ok i've done it with match tuple with
<ktne>
i would have hoped there is other way too
<bluestorm>
OCaml have functions for 2-uplets, fst and snd
<bluestorm>
but there is no generic accessor
<ktne>
ok thanks
<ktne>
that's fine
Mr_Awesome has quit ["aunt jemima is the devil!"]
gunark has quit ["Konversation terminated!"]
pango has quit [Remote closed the connection]
buluca has quit [Read error: 113 (No route to host)]
pango has joined #ocaml
<ktne>
hmm
<ktne>
bluestorm still here?
<bluestorm>
:]
<ktne>
:)
<ktne>
i have an issue with a type that describes a function
<ktne>
i want a tuple that stores a function name and a pointer to that function
<ktne>
so i defined a function type
<ktne>
but something is not right
<ktne>
because the function type is like 'a -> 'b
<ktne>
but i want it to accept any function that ends in 'a -> 'b
<ktne>
including 'c -> 'a -> 'b
<bluestorm>
hm
<ktne>
or 'd -> 'c -> 'a -> 'b
<bluestorm>
'c -> 'a -> 'b is 'c -> ('a -> 'b), so is an instance of the " 'a -> 'b " scheme
<bluestorm>
but hm
<bluestorm>
i still don't know how do you want to use it
<bluestorm>
but i'm not sure it's actually possible
<ktne>
well i'
<ktne>
i'm working on a parser
<ktne>
and for each returned tree i want to return the start and end byte positions in source file
<ktne>
the name of the rule
<ktne>
and a pointer to the function that implements the rule
<bluestorm>
hm
<bluestorm>
if you want multi-parameters rules, you may need to abstract over the function type
<bluestorm>
something like
<ktne>
one function for each EBNF rule, the function returns an option, some tree or nothing if the rule hasn't been matched
<bluestorm>
type rule_fun = Immediate of rule | Fun of parameter -> rule_fun
<ktne>
hmm
<ktne>
yes
<ktne>
some rules are immediate
<ktne>
for example rule Identifier
<bluestorm>
but that won't give you 'a -> 'b -> 'c, only 'a -> 'a -> .. -> 'a -> b
<ktne>
but rule Literal requires a parameter
<ktne>
for example Literal "keyword"
<bluestorm>
hm
<bluestorm>
could you not use a sum type ?
<ktne>
a sum type?
<ktne>
hmm
crathman has joined #ocaml
<bluestorm>
type rule_desc = Void of rule | Keyword of string -> rule | ..., for example
<ktne>
hmm
<ktne>
maybe i should explain to you how the parser works
<ktne>
the parser works like this, for each rule there is a function that takes as parameter at least a byte position into input file
<ktne>
it checks if the rule matches there, if not then returns None, otherwise it returns Some {startpos:int, endpos:int, rulename:string, rulepointer:rule_function}
_bt2 has joined #ocaml
<bluestorm>
hm
<ktne>
then to create a compound rule, like for example a sequence of 3 literals i do
<ktne>
where optional checks to see if the previous one failed, if not then it skips the optional part
<ktne>
if the previous one failed then it checks the optional literal
<bluestorm>
should you not do
<bluestorm>
hm
<bluestorm>
i see
<bluestorm>
that really look like a monadic parser
<ktne>
basically optional just skips the optional rule if the previous one has already been found
<bluestorm>
what is the type of :> ?
<ktne>
it's function composition
<ktne>
it should compose the functions such that you get a function that takes as input a stream position (the point from where the matching starts) and returns either None or Some
<bluestorm>
hm
<ktne>
so you compound the smaller rule and create a new function which in turn acts like a bigger rule :)
<ktne>
i'm really not familiar with functional programming :)
<ktne>
i'm not sure how proper my method is :)
<bluestorm>
actually
shrimpx has quit [Read error: 104 (Connection reset by peer)]
<bluestorm>
that looks like a good idea
<ktne>
:))
<bluestorm>
rule would be hm
<bluestorm>
input -> result option
<bluestorm>
and :> would be rule -> rule ?
<ktne>
yes
<bluestorm>
hm
ygrek has joined #ocaml
<bluestorm>
rule -> rule -> rule
<ktne>
there are a few primitive rules like Literal
<ktne>
optional
<ktne>
and many
<ktne>
many checks a rule multiple times
<bluestorm>
hm
<bluestorm>
what i don't understand
<ktne>
(many Statement)
<bluestorm>
is your {startpos:int, endpos:int, rulename:string, rulepointer:rule_function}
<bluestorm>
why rule_function ?
Lectus has left #ocaml []
<ktne>
rule_function is the type of rule functions
<ktne>
the tule type
<bluestorm>
this is the type "result", isn't it ?
<ktne>
each rule is a string and a rule function
<ktne>
the string describes the rule
<ktne>
startpos is the point where matching beings, endpos is the point where matching ends
<ktne>
for example for a literal rule it contains the first byte and last byte positions of the literal
<ktne>
and it returns a tree of that
<bluestorm>
but
<ktne>
the top node would contain the entire source file
<bluestorm>
hm
<ktne>
like (starpos=0, endpos=filesize, rulename="top rule", rulepointer=top_rule_function)
<bluestorm>
if you've got your firstpos and endpos
<bluestorm>
that mean you've already parsed the input
<bluestorm>
doesn't it ?
<ktne>
not really
<ktne>
because i still have to know what rule has been detected there
<bluestorm>
(or does your endpos mean "the last char the parser may read" ?)
<ktne>
the last char in the matched rule
<ktne>
actually the first pos of the following rule
<bluestorm>
hm
<ktne>
even if i have a tree of (startpos,endpos) i still have to know what was actually matched there
<bluestorm>
yes
<bluestorm>
hm
Smerdyakov has joined #ocaml
<ktne>
i guess i could just store the string name with no function pointer
<bluestorm>
the camlp4 way to do that
<ktne>
just the function name
<ktne>
what camlp4 does?
<bluestorm>
is to build an AST with an algebrainc type
<bluestorm>
camlp4 is the ocaml preprocessor
<ktne>
ah
<ktne>
i don't really use ocaml, i use f#
<bluestorm>
and the position information is the first parameter of each constructor
<bluestorm>
something like
<bluestorm>
type AST = Int of 'loc * string | Add of 'loc * AST * AST
<bluestorm>
(for a simple arithmetic language)
<ktne>
i was thinking to pass this (startpos, endpos) to a function that returns AST
<bluestorm>
hm
<bluestorm>
couldn't you build the AST at parsing time ?
<ktne>
so i apply the ebnf parser first, then i validate that and return the AST
<bluestorm>
that looks easier
<bluestorm>
hm
_bt[1] has joined #ocaml
<ktne>
well yes but if you have a programming language i was thinking about forward definitions
<ktne>
like mutually recursive functions, you can't usually validate until you parsed the whole thing
<bluestorm>
hm
dmentre has left #ocaml []
<bluestorm>
mutually recursive functions can be sequentially parsed
<bluestorm>
at the "let" you create a list, then you add an element at each "and"
<ktne>
hmm
<ktne>
i see what you say
<ktne>
i can validate the statement when trying to exit, after i parsed all "and" definitions
<bluestorm>
hm
<bluestorm>
but what exactly do you mean by "validating" ?
<ktne>
i mean, when i try to exit the rule
<bluestorm>
all syntaxic try/error handling could be in your ":>" definition
<ktne>
well i mean making sure that things are defined before used
<bluestorm>
hm, so that's not a syntaxic concern
<ktne>
no
<bluestorm>
wouldn't it be a good move to test such things after the AST building ?
<ktne>
i thought the AST contains only valid stuff
<bluestorm>
syntaxically valid stuff
<ktne>
ah, i was thinking about outputting semantically valid stuff in 2nd phase
<bluestorm>
type-checking for example is obviously performed after the AST building
<bluestorm>
yes, that looks like a good idea
<ktne>
first phase does ebnf parsing, then second phase does semantic validation
<bluestorm>
yes
<bluestorm>
and hm
<ktne>
but i guess i could use that algebraic syntactic type
<ktne>
because now i just use a (rule_result tree)
<ktne>
hmm
<ktne>
anyway i can say that this is going to be the smallest parser i ever written in terms of source line numbers :)
<bluestorm>
:p
<ktne>
it's barelly a page so far :)
<bluestorm>
your :> idea is really clever
<ktne>
:))
<bluestorm>
hm and btw, i have a parser describind monads under the hood
<ktne>
well you know, novice's luck :)
<bluestorm>
if you're interested
<ktne>
i'm not sure what monads are
<bluestorm>
it's interesting, and end with a parser very similar to yours
<ktne>
well, i know that they are the subject of haskell :)
<ktne>
but i haven't succeeded understanding them
<bluestorm>
this paper is great for understanding monads
_bt[1] has quit ["Get out of that boring IRC client! It's no good for you. Bersirc 2.2 is your answer! [ http://www.bersirc.org/ - Open Source"]
EliasAmaral has quit [Remote closed the connection]
<munga>
indeed ... I din't know about dyinn ... nice tody :)
<munga>
do you know of any other video on type theory ? It's a very nice way a getting an overview of the filed ...
<Smerdyakov>
I really have doubts that videos can present such material effectively.
<Smerdyakov>
Maybe you _feel_ like you've engaged in some worthwhile learning, but it's more likely that you're just enjoying sitting back and experiencing something passively, instead of working to read a book.
<munga>
Smerdyakov: a watch a video for what is worth watching in on a friday evening before going home ... I've a stack of book to amuse myself during working hours :)
<Smerdyakov>
I'm just disagreeing that it is "a very nice way of getting an overview of the field."
<bluestorm>
Smerdyakov: after seeing that you can think
<bluestorm>
"i'm totally ignorant of that, but it sounds cool"
<bluestorm>
that's what an "overview" mean :-'
<Smerdyakov>
I'm just going to keep disagreeing. It's sham learning, designed to appease people who feel like they need to put in a certain amount of time per day, not that they need to _learn_ a certain amount per day.
<munga>
ok, point taken... I guess watching a video is good to help you to navigate the amount of information you find in a book... say to focus your attention on what it might be more interesting for you... I don't believe that reading a scientific book back to front is always a good strategy. surely with foundation books, but not with technical books...
<munga>
gotta go. have a nice WE.
munga has quit ["Leaving"]
crabstick has joined #ocaml
tty56_ has quit [Read error: 104 (Connection reset by peer)]
crabstick_ has quit [Read error: 110 (Connection timed out)]
ygrek has quit [Remote closed the connection]
<abez>
Smerdyakov shoots his mouth off again, unable to comphrehend that people don't think the same way he does, as well people learn in different ways! Oh Smerdyakov what fun you'll have teaching undergrads with your total inability to understand that not everyone is you!
<abez>
I guess sitting in classes listening to lectures is sham learning too!
tty56 has joined #ocaml
<abez>
Hell why even have conferences? Why not just publish the proceedings and save everyone the airfare!
<zmdkrbou>
:)
joshcryer has quit [Read error: 104 (Connection reset by peer)]
joshcryer has joined #ocaml
puks has joined #ocaml
ygrek has joined #ocaml
<Smerdyakov>
abez, yes, lectures are crap.
<Smerdyakov>
abez, people who don't learn best through reading are never going to do very well in computer science. I'm not pretending to talk about any other field.
<TFK>
What's the difference between reading a book and listening to a lecture? The bottom line is your own experience with the material. (E.g., homework.)
<Smerdyakov>
A book can communicate technical content more quickly.
<Smerdyakov>
I think a critical difference is that the book proceeds at your pace, while the lecture is on a fixed pace.
<ktne>
i think that using a lecture as starting point in a new field is a good idea
<TFK>
Technical content you'll forget as soon as you shut it.
buluca has joined #ocaml
<ktne>
when i'm looking for something new that i haven't done before i would preffer a good introductory lecture
<ktne>
then i go on with books
<Smerdyakov>
TFK, so? You have to experience some exposition to learn most subjects in computer science. It's worth optimizing that operation.
<ktne>
for example i first watched the intros on f# then i started reading more about f#
<Smerdyakov>
ktne, lectures can work well as advertisements, but I think they are bad for real roll-up-your-sleeves-and-learn.
<ktne>
i think that they are good for fighting the learning curve
<TFK>
Sure. And that exposition can come in many ways.
<Smerdyakov>
What does it mean?
<ktne>
steeper the curve, more useful the lecture
<Smerdyakov>
TFK, yes, and some ways are more efficient than others.
<Smerdyakov>
ktne, do you have any evidence to support that?
<ktne>
Smerdyakov only personal experience
<Smerdyakov>
ktne, or do you just _feel_better_ after goofing off in a lecture than after working hard to read a book? :P
<ktne>
why would they be mutually exclusive?
<Smerdyakov>
What do you mean?
<ktne>
i preffer a lecture to get me started up
<TFK>
Interesting how you associate a lecture with "goofing off" and reading a book as "working hard".
<ktne>
then a book
<TFK>
The reverse can easily apply.
<Smerdyakov>
ktne, have you conducted experiments where you cut out the lecture and measure rate of acquisition?
<ktne>
Smerdyakov no
<Smerdyakov>
ktne, you might find that lectures are just serving to motivate you, not convey information better than a book can.
<ktne>
not to motivate me
<ktne>
they are serving to help me make the first step, to understand the basics so that i can have a better comprehension of the book
<Smerdyakov>
Maybe it was just a bad book!
<ktne>
it works every time, no matter the subject :)
<Smerdyakov>
Well, we need some experimental data.
<ktne>
really, hearing and seeing someone speak on a subject helps much more than reading a book or notes
<abez>
Wait, Smerdyakov pulls the research card, yet totally ignores research on learning styles? Talk about picking and pecking. Even more interesting Smerdyakov has twisted the argument into some weird argument about the optimality of learning methods in CS, which was never the point and yet again ignores learning styles. The lack of distinction between the available, the practical and potential is also muddled where he claims that ...
<abez>
... reading books is the only effective way to learn CS.
<ktne>
althrough i should mention that if i midded a course it was usually very difficult for me to learn that part, because i haven't seen the lecturer speak
<Smerdyakov>
This relates to the popular notion of "learning styles." You're talking about a lecture-aligned learning style, and I'm talking about a book-aligned learning style.
<Smerdyakov>
However, even the people who presented the learning styles workshop here acknowledged that some learning styles are better suited to some subjects.
<ktne>
again, who says that they are mutually exclusive?
<Smerdyakov>
And I think reading and CS go together like that.
<ktne>
i preffer both, the lecture first
<Smerdyakov>
I didn't say you can't do both. I just don't think non-interactive lectures have something to offer beyond what reading does.
<ktne>
who dissagrees with that?
<Smerdyakov>
...for people with a predilection to grok CS.
<ktne>
i just said that a lecture is much better in the first part of the learning curve
<Smerdyakov>
Yes, and I know that's not true for me.
<ktne>
because with a lecture you can aquire a large amount of superficial information in a shorter amount of time than reading it
<Smerdyakov>
It could be true for you, but I would then conclude that your learning style probably promotes learning speed less effectively in CS than mine does.
<ktne>
that superficial information creates a sort of "mesh" where the information you aquire later from the book settles
<Smerdyakov>
Why not read an overview chapter at the start of a book instead?
<ktne>
because i don't see the lecturer speak
<Smerdyakov>
Seeing someone speak doesn't help me.
<ktne>
sure it does help me
<jlouis_>
Smerdyakov: Often, I never open the book when taking courses. I just go to lectures.
<jlouis_>
Sans for exercises, heh
<Smerdyakov>
ktne, right, and I'm saying that your learning style is demonstrably less efficient for learning CS.
<ktne>
Smerdyakov how is that? you still read the book, then where is the issue?
<Smerdyakov>
ktne, you end up needing longer to learn the material.
<ktne>
definitivelly not
<Smerdyakov>
ktne, I believe you will, but we need some data, and I don't have any right now.
<ktne>
learning first from a book is like trying to learn chinese with no dictionary
<Smerdyakov>
It's like that _for_you_.
<Smerdyakov>
Not for everyone.
<ktne>
you need some sort of superficial level of knowledge before reading a book
<Smerdyakov>
Not if the book is written well.
<ktne>
right, but i suppose it's like that for a lot other people
<Smerdyakov>
Fine, fine, but I believe that those other people are not well-equipped to learn CS.
<ktne>
i did learned CS, i'
<ktne>
i'm not well equipped to learn CS?
<ktne>
or maybe yes :)
<Smerdyakov>
It's not a matter of "did you learn it?"; it's a matter of "how quickly did you learn it?".
<ktne>
i'm not really that familiar with the complicated CS parts
<ktne>
it's very important for me to filter large amounts of information
tty56 has quit [Read error: 110 (Connection timed out)]
<ktne>
so it's important to get a first grasp very quickly
<ktne>
so that i can reject the subject
<Smerdyakov>
What you just said is not directly relevant to this discussion.
<Smerdyakov>
Many people best get a first grasp by reading.
<ktne>
the problem is that the first step in the learning curve is also the steepest
<ktne>
you need a minimal fixed set of concepts to work with to even start learning the rest
<Smerdyakov>
Again, this is totally irrelevant.
<bluestorm>
i'm perfectly fine with not using "the fastest way" to do something
<ktne>
i'm confident that a lecturer will provide you with this startup knowledge faster than an introductory chapter
<bluestorm>
what matters to me is having fun
<Smerdyakov>
Many people do best in the first stage of the learning curve by reading.
<bluestorm>
:-'
<ktne>
also in a more resilient way than an introductory chapter
<ktne>
it's easier to remember what a lecturer said than what the first chapter says
<ktne>
since the initial knowledge chunk is mutually dependent, it's therefore important that you remember it all
<Smerdyakov>
No, no, no, it varies by person.
<Smerdyakov>
I remember better what I read in a book than what a lecturer says.
<ktne>
otherwise you return again and again to the first chapter or stay there in an infinite loop until you
<ktne>
"get it"
leo037 has joined #ocaml
<ktne>
well when the lecturer speaks she moves around too, uses plenty of gestures, pauses, etc
<Smerdyakov>
And moving around only helps people with particular learning styles.
<ktne>
i find that easier to remember in large quantities rather large quantities of text
<Smerdyakov>
Are we experiencing a language barrier?
cpst has joined #ocaml
<ktne>
*to remember that
<Smerdyakov>
You keep talking about how you learn, but I thought we could all agree that different people learn best in different ways.
<ktne>
err
<ktne>
but i can only argume from my position
<ktne>
since i have no data :)
<ktne>
&argue
<ktne>
*argue
<Smerdyakov>
The existence of learning styles is pretty universally accepted by now.
<ktne>
yes, but that doesn't make all learning styles equal
<ktne>
some are more common
<Smerdyakov>
And commonality varies among demographics.
<ktne>
and i'm quite sure that a lecturer can give you a large amount of superficial information in a shorter time and more reliable than a book
<Smerdyakov>
Visual learners dominate among people successful in technical fields.
<ktne>
this because it uses spoken and visual cues
<Smerdyakov>
Or maybe I use the wrong word.
<Smerdyakov>
I want the kind that goes with reading books.
<ktne>
no
<ktne>
that's not visual :)
<abez>
You're projecting
<Smerdyakov>
abez, how?
<abez>
You're making assumptions that you situation is the case and your projecting on others.
<Smerdyakov>
abez, I have heard that the book-oriented learning style predominates in technical fields at a presentation by my university's teaching resource center. You think they lied?
<zmdkrbou>
< Smerdyakov> Visual learners dominate among people successful in technical fields. << where are the figures ? how did you get them ? and how do you define "successful" ?
<abez>
Smerdyakov: Kinesthetic learning is pretty popular in CS, programming, etc.
<abez>
Smerdyakov: it explains why so many undergrads avoid formalism and just want to get down to work.
<Smerdyakov>
abez, it may just be that the other main style is very underrepresented.
<ktne>
if there is a market system at work here, then it might be underrepresented with a good reason
<Smerdyakov>
It is my opinion that people who want to avoid formalism should be studying something besides CS.
<Smerdyakov>
Such a field should have a different name.
<ktne>
Smerdyakov it's not like that you necesarly reject formalism because you just want to check a lecture before starting learning the book
<ktne>
otherwise, why have lectures?
<ktne>
you could just pass a bunch of books to the students
ygrek has quit ["Leaving"]
<Smerdyakov>
Indeed, a significant portion of CS students would be better off like that.
<abez>
It is my opinion that much of CS is esoteric wankery that isn't that important, essentially a lot of CS got side tracked by people looking for publishing spaces for their work.
<Smerdyakov>
I don't disagree.
<Smerdyakov>
But what I say is relevant to the truly useful parts.
buluca has quit [No route to host]
<zmdkrbou>
you use a lot of word which you don't define, Smerdyakov. what are the "truly useful parts" ? those *you* define as being useful ?
<zmdkrbou>
mmh, looks like a /ignore :)
<cpst>
the idea that programming should have the support of formal methods doesn't mean that programming should be proving theorems
<zmdkrbou>
?
<cpst>
and "formalism" doesn't even narrow anything down, there are formal methods for analyzing C pointer arithmetic and heap storage
<zmdkrbou>
(programming is somehow proving theorems, anyway)
<cpst>
zmdkrbou: if you fully type everything in a turing-complete type system by hand
<zmdkrbou>
then what ?
<cpst>
zmdkrbou: then programming is actually the same as proving theorems
<cpst>
zmdkrbou: with a type system weak enough to do any real inference, it is very far off
<zmdkrbou>
well writing a program as a typed lambda-term is writing a proof
mr_hugo has left #ocaml []
<cpst>
zmdkrbou: sure, but it is not a proof that the program is correct in the usual sense
<cpst>
zmdkrbou: it's a proof in an extraordinarily weak logic that can not express most things people want to express
<cpst>
zmdkrbou: as soon as you get any measure of expressiveness, you can no longer do inference
<cpst>
zmdkrbou: and you start turning program into computer-aided theorem proving and verification
* zmdkrbou
doesn't really see the point here
<cpst>
zmdkrbou: my point is that even with a language like OCaml, the majority of the process of programming is not formalized
<cpst>
zmdkrbou: so people like Smerdyakov probably need to accept informal methods as well
* TFK
<3 his QA team
<mbishop>
OCaml lacks a denotational semantics
<cpst>
besides, even when you prove things the proof can be incorrect
<cpst>
when they introduced call/cc into SML/NJ, it was unsound
<cpst>
even though a paper proved it was correct
<cpst>
it turns out the section of the paper said the proof followed by analogy and everyone believed it ;-)
<cpst>
so you could crash SML/NJ by using call/cc in a line
<jlouis_>
_that_ is a argument for formalized theorem proving
ktne has quit [Read error: 110 (Connection timed out)]
<tsuyoshi>
or maybe an argument that call/cc isn't worth it...
<cpst>
jlouis_: the problem being that most actual mathematics is much too difficult for machine-verified proofs
<mbishop>
I believe they are still working on a full mechanized proof for SML
<cpst>
mbishop: and that is not even very difficult mathematically, compared to the kinds of things actual mathematicians prove
<cpst>
there aren't very many deep theorems in CS
<jlouis_>
There are parts of mathematics where the proofs are quite far away from a mechanized proof indeed
<cpst>
including most active areas of mathematics
<jlouis_>
still, most humans would agree they are true
<jlouis_>
cpst: indeed
<cpst>
sure, but I find errors in books and theorems all the time
<cpst>
mathematicians rely a lot on the social process as well as their own intuition in addition to published proofs
<cpst>
and it usually gets sorted out well enough in the end
<jlouis_>
mathematicians use each other as one giant human computation grid
<jlouis_>
or verification grid
<cpst>
and mathematicians have different learning styles ;-)
<cpst>
which helps out
<jlouis_>
also true.
<Smerdyakov>
Hi, everyone! Just stepped out to buy something, and am happy to respond to all attacks now. ;)
<Smerdyakov>
cpst, I don't know how you came to think I was somehow deriding anything that doesn't involve hardcore theorem proving.
<cpst>
I am not attacking you
<cpst>
as an actual mathematician, I do find that CS people tend to have bad conceptions about what mathematics and proof is actually about in practice
<cpst>
and that some people in formal methods fail to realize the importance of informal methods in designing real-world systems
<Smerdyakov>
cpst, how do you know that it isn't just that you don't have the write tools to make using formal methods easier?
<cpst>
Smerdyakov: because people have tried and come nowhere near a usable result, and the problem is fundamentally limited by computability theory
<mbishop>
s/write/right/
<Smerdyakov>
cpst, well, think about the amount of time people have been working on formal methods for computers.
<cpst>
Smerdyakov: some proofs are difficult even to write out entirely in informal mathematical notation
<Smerdyakov>
cpst, then look at the amount of time it took people to create formal methods like calculus that could be put to good use in talking about the physical world.
<cpst>
Smerdyakov: but Calculus wasn't formal until the 19th century
<Smerdyakov>
cpst, what is the difference between these cases that leads you to conclude we formal methods people won't come up with a similar innovation?
<cpst>
Smerdyakov: and it was useful for 3 centuries before that
<cpst>
numbers weren't even formal until the 19th century, nevermind calculus ;-)
<Smerdyakov>
I think it's important to note that society is willing to pay for guarantees about its infrastructure, whereas hardly anyone cares about guarantees that research mathematicians' output is sound.
<Smerdyakov>
So, if you think I've ever advocated computer formalizations of any significant fraction of research mathematicians' output, I've not been clear.
<Smerdyakov>
I couldn't really care less about most of that stuff. :()
<cpst>
the most successful systems I have seen have been a comprimise, static analysis tools that are sound for particular kinds of errors on particular kinds of programs
<Smerdyakov>
I work on certification of useful programs, like safety certification of mobile code and correctness of compilers.
<Smerdyakov>
The fact that the proofs, if done up to most mathematicians' standards, are "shallow" doesn't mean that this sort of work isn't _more_ useful to society than classical math.
<TFK>
Hmmm, I understand that OCaml can't do "real" concurrency?
<Smerdyakov>
You mean multi-processing?
<TFK>
I suppose.
<mbishop>
Look at JoCaml?
ocaml has joined #ocaml
<Smerdyakov>
TFK, you can, of course, run multiple processes and make them communicate by IPC.
<TFK>
But there are no plans to make threading actually concurrent?
<TFK>
(Redesign the GC or whatever it takes?)
<Smerdyakov>
I don't know.
<Smerdyakov>
I think you shouldn't bank on it happening soon.
<Smerdyakov>
The incentives for the OCaml team to do it aren't very high.
<TFK>
What are the incentives of the OCaml team in general?
<TFK>
mbishop, when the code is only 99% compatible it might mean that only 1% of libraries can actually be compiled ;-)
<Smerdyakov>
I think their incentives are based on what seems like nifty research.
<TFK>
And concurrency is boring? ;-)
<Smerdyakov>
I think the technical problems here are largely solved in the context of Java... or any unsolved problems would be solved for Java before OCaml people could port the more basic solutions.
<mbishop>
"true" concurrency to me would mean one of the process calculi, like join calculus
<mbishop>
not "threading"
<flux>
concurrent gc suitable for a functional language with high allocation rates might actually be considered to be high-end research..
<flux>
but I suppose that's not the only option; erlang shows that
ocaml is now known as _bt2
<jlouis_>
I think you should forget about concurrent GC due to complexity
<TFK>
flux, why, how does Erlang do concurrency?
<flux>
tfk, even though processes share the same memory space, each process has a separate gc
<jlouis_>
TFK: In Erlang a process is isolated from all others, so each process has a separate gc
<flux>
and then there is an experimental mechanism that still allows sharing between processes, or so I've gathered..
<jlouis_>
binary data buffers are shared
<TFK>
Oh. Sounds wasteful.
<jlouis_>
for instance
<flux>
tfk, wasteful how? there is the "across process boundaries you need to copy messages"-problem, yes..
<flux>
but it looks like message-based concurrency is a good idea anyway
<jlouis_>
message based concurrency seem to be the way to go
<TFK>
I would assume every GC instance takes up some resources.
<flux>
perhaps if you need real sharing of data (rarely) you could have an additional mechanism for that
<jlouis_>
TFK: hardly more resources than a single GC
<flux>
tfk, hm, I don't see that. they can still have a shared list of free pages, for example.
<flux>
tfk, also you can run those gcs in parallel
<TFK>
Hmmm.
<TFK>
So this does mean that Erlang processes can't share data, besides message passing?
<flux>
it's one thing to have a gc that can run in parallel with your actual code and one thing to actually "multi-thread" the process of doing gc also
<flux>
tfk, yes
<flux>
well
<flux>
jlouis apparently knows bette
<flux>
r
<jlouis_>
TFK: almost true
<jlouis_>
TFK: data is passed by copying them
<flux>
I haven't touched erlang, only read about it ;)
<flux>
(a shame erlang is dynamically typed..)
<jlouis_>
flux: indeed!
<jlouis_>
(dynamic typing sucks, IMO)
<TFK>
Smerdyakov said this was solved in Java. How do they do it, then?
<flux>
what I've read it was by luck that erlang was based on dynamic typing ideas
<jlouis_>
TFK: by complex code.
<flux>
tfk, well, I think a typical java application allocates in a lot slower rate than a typical ml program
<flux>
tfk, for example F# can still be 50% slower than ocaml
<jlouis_>
(or erlang program)
<flux>
but I suppose that might not prove anything yet
<flux>
(that is also what I've read: no personal experience)
<jlouis_>
In erlang something of type Binary (Which is a byte array) can be shared between processes. Since Binaries are immutable, and you can slice them, this is simple to do with a ref-count
<jlouis_>
no risk of introducing cycles, since they only contain bytes
<jlouis_>
but binaries below some threshold (64 bytes I believe) are copied anyway
<Smerdyakov>
Singularity uses separate local and shared heaps.
<Smerdyakov>
The shared heap is managed manually by processes, which must be certified to use it properly by static analysis.
<flux>
smerdyakov, what kind of limitations are enforced for its access?
<Smerdyakov>
flux, every allocated object has exactly one owning process at a time.
<Smerdyakov>
flux, ownership is transfered by message passing.
<flux>
so you sort of have handles that point to the actual data, and only one party can own a handle
<flux>
without type system support that would lead to runtime checks
<flux>
hm, linear types?-)
<Smerdyakov>
That's the technique that's used, but all sorts of static analysis schemes are imaginable.
<TFK>
pango, so JoCaml is a "message-passing interface" for OCaml, kinda, and is thus truly concurrent?
<Smerdyakov>
TFK, I don't like this "true concurrency" terminology. Why not say "multi-processing" or "multi-core-capable"?
<TFK>
Alright, I'll say "multi-processing" from now on :-)
<Smerdyakov>
(Maybe enough folks say "true concurrency," but it's not like concurrency on a single core isn't useful, so why should we call it "false"?)
<TFK>
Well, "true" concurrency isn't even theoretically possible on a single core, is it? It's just an illusion created by time-sharing.
<pango>
I don't have much experience in those fields, but as I understand, both OCaml and JoCaml allow concurrent programming, just with different primitives
<flux>
tfk, well, there's hyperthreading..
<flux>
tfk, and for example sun has its niagara processor, or was it called t2
<Smerdyakov>
TFK, don't you need to make a claim about the discrete/continuous nature of the universe to be able to conclude whether your "true concurrency" is possible anywhere?
<flux>
which has 8 cores and each has 8 hardware threads
<flux>
but as smerdyakov says, it doesn't matter
<flux>
I'd take 20GHz machine any day over 20 cores at 1GHz ;)
<Smerdyakov>
Language extensions/libraries like Concurrent ML show how concurrency is useful, even on a single core.
<TFK>
How are they useful, besides in abstraction?
<Smerdyakov>
TFK, your definition of concurrency may say that this isn't "concurrency," but I think you're outvoted there. Concurrency doesn't imply that anything happens simultaneously.
<Smerdyakov>
Heh. That's like asking, "what do you have to eat, besides food?".
<TFK>
You know what I mean, why make this discussion unnecessarily tedious?
<Smerdyakov>
No, I don't know what you mean. Concurrency is useful as an abstraction and modularity mechanism, and I don't have anything else in mind now for the single-core setting. Is that the kind of answer you wanted?
<TFK>
It is also useful for speeding things up in a multi-core environment, which is what I'm interested in ATM.
schme` is now known as schme
<Smerdyakov>
OK, but the context in our last few lines was justifying why concurrency is a useful idiom on single cores.
<TFK>
So I'd like to know, for example, how JoCaml's concurrency model works in multi-core environments. (They don't seem to mention it on their website.)
<TFK>
Or if OCaml can be used like Erlang without having to resort to multiple processes.
<flux>
tfk, I think that by omitting to mention it, it won't support multi-processing ;)
<TFK>
That is my fear :-(
_bt2 has left #ocaml []
<Smerdyakov>
If you want something that complicated that won't generate research prestige for anyone, then you should pay someone to implement it (or do it yourself).
<TFK>
"That complicated"? You mean a multi-threaded GC?
<Smerdyakov>
Yes.
<Smerdyakov>
The TILT Standard ML compiler had a concurrent GC early this century.
<Smerdyakov>
But TILT doesn't have the right social impetus behind it to be developed as a real engineering tool.
<Smerdyakov>
The garbage collector was someone's PhD thesis.
<Smerdyakov>
He later became one of the early members of the group making history with concurrent GC with Java at IBM Research.
<TFK>
Sounds pretty prestigious.
<Smerdyakov>
Yeah, and now he did it, so no one else will get a PhD thesis for it.
<Smerdyakov>
Including no one doing the same things for OCaml
<TFK>
Well, I'm sure there are further problems to be solved. Efficiency, simplicity of implementation, etc.
<TFK>
(Right?)
<Smerdyakov>
All being done in the context of Java at IBM.
<Smerdyakov>
Like I said, porting their infrastructure to OCaml would take long enough that it would probably be outdated before it was debugged.
<TFK>
Hmmm.
<hcarty>
TFK: I have compiled JoCaml on an 8 processor system and run some of the example programs which come with it
<TFK>
And it utilizes those 8 processors?
<hcarty>
Yes, when run with the correct options
<hcarty>
It was a quick experiment on my part, so I don't remember the details. But the raytracing example they have was able to utilize all 8
<TFK>
Nice!
<hcarty>
Can ocamlp3l and Cothreads can do the same? I haven't tested either of those.
<flux>
btw, I recently thought about a problem with the fork-kind of parallelism, which I haven't seen mentioned anywhere..
<flux>
let's say you have 1 megabyte of data you want to share with a subprocess. you fork, and the child process inherits it.
<flux>
after that you drop references to the one megabyte, and it gets released from the parent point of view
<flux>
however, the child can perhaps never do that, because if the code is like: if fork () = 0 then ( .. exit 0 ), the gc doesn't really know you have that exit there, does it?
<flux>
so if the gc has to assume you wont exit (or raise an exception) within the forked block, you will likely have references to that one megabyte of data in upper stack frames
<flux>
is my reasoning correct?
<flux>
hm, one way to solve that would be to replace that with a construct: if fork () = 0 then raise (DoIt (fun () -> ..)) and catch it that at the very topmost level
jedai has joined #ocaml
<flux>
I wonder if that is a real problem or is this only academic pondering :)
Mr_Awesome has joined #ocaml
jlouis has joined #ocaml
jlouis_ has quit [Read error: 110 (Connection timed out)]
piggybox_ has joined #ocaml
pantsd has joined #ocaml
piggybox has quit [Connection timed out]
<fremo>
it seems that fork wins... :)
Tetsuo has quit ["Leaving"]
buluca has joined #ocaml
crathman has quit [Read error: 110 (Connection timed out)]