flux changed the topic of #ocaml to: Discussions about the OCaml programming language | http://caml.inria.fr/ | OCaml 4.00.1 http://bit.ly/UHeZyT | http://www.ocaml.org | Public logs at http://tunes.org/~nef/logs/ocaml/
zpe has joined #ocaml
zpe has quit [Ping timeout: 260 seconds]
darkf has joined #ocaml
jsvgoncalves has joined #ocaml
jsvgoncalves has quit [Remote host closed the connection]
ulfdoz has quit [Ping timeout: 245 seconds]
jsvgoncalves has joined #ocaml
smerz_ has quit [Ping timeout: 245 seconds]
zpe has joined #ocaml
jsvgoncalves has quit [Remote host closed the connection]
RagingDave has quit [Quit: Ex-Chat]
jsvgoncalves has joined #ocaml
zpe has quit [Ping timeout: 264 seconds]
madroach has quit [Ping timeout: 258 seconds]
madroach has joined #ocaml
Neros has quit [Ping timeout: 272 seconds]
tani has quit [Quit: Verlassend]
emmanuelux has quit [Ping timeout: 246 seconds]
fraggle_ has joined #ocaml
zpe has joined #ocaml
zpe has quit [Ping timeout: 260 seconds]
emmanuelux has joined #ocaml
middayc has quit [Quit: Lost terminal]
q66 has quit [Remote host closed the connection]
derek_c has joined #ocaml
<derek_c> Hello! I've defined a module called "TitleOrder" where "type t = int * int". Later, when I try to match (x, y) against a value of TileOrder.t, the compiler compains that "This expression has type TileOrder.t but an expression was expected of type int * int". Can anyone tell me what's the problem?
zpe has joined #ocaml
emmanuelux has quit [Quit: emmanuelux]
zpe has quit [Ping timeout: 272 seconds]
derek_c has quit [Ping timeout: 260 seconds]
areece has left #ocaml []
zpe has joined #ocaml
yacks has quit [Read error: Connection reset by peer]
zpe has quit [Ping timeout: 245 seconds]
yacks has joined #ocaml
yacks has quit [Quit: Leaving]
thieusoai has joined #ocaml
thieusoai has quit [Remote host closed the connection]
yacks has joined #ocaml
zpe has joined #ocaml
paolooo has joined #ocaml
zpe has quit [Ping timeout: 256 seconds]
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
groovy2shoes has quit [Quit: groovy2shoes]
zpe has joined #ocaml
zpe has quit [Ping timeout: 245 seconds]
leoncamel2 has quit [Quit: WeeChat 0.3.9.2]
leoncamel has joined #ocaml
leoncamel has quit [Quit: WeeChat 0.3.9.2]
cdidd has joined #ocaml
zpe has joined #ocaml
zpe has quit [Ping timeout: 256 seconds]
eni has joined #ocaml
asmanur has quit [Ping timeout: 252 seconds]
asmanur has joined #ocaml
derek_c has joined #ocaml
lusory has quit [Quit: leaving]
zpe has joined #ocaml
lusory has joined #ocaml
paolooo has quit [Ping timeout: 245 seconds]
eni has quit [Ping timeout: 252 seconds]
eni has joined #ocaml
ttamttam has joined #ocaml
derek_c has quit [Quit: leaving]
ulfdoz has joined #ocaml
ttamttam has quit [Remote host closed the connection]
weie_ has joined #ocaml
eni has quit [Ping timeout: 252 seconds]
weie has quit [Ping timeout: 256 seconds]
ttamttam has joined #ocaml
ttamttam has quit [Remote host closed the connection]
ttamttam has joined #ocaml
Watcher7 is now known as Watcher7|off
ttamttam has quit [Remote host closed the connection]
ttamttam has joined #ocaml
eikke has joined #ocaml
ttamttam has quit [Quit: ttamttam]
paolooo has joined #ocaml
eikke has quit [Ping timeout: 240 seconds]
Arsenik has joined #ocaml
leoncamel has joined #ocaml
q66 has joined #ocaml
Anarchos has joined #ocaml
astertronistic has quit [Quit: Leaving]
nalaginrut has quit [Ping timeout: 264 seconds]
paolooo has quit [Ping timeout: 245 seconds]
ulfdoz has quit [Read error: Operation timed out]
Neros has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
sepp2k has joined #ocaml
RagingDave has joined #ocaml
zpe has quit [Read error: Connection reset by peer]
zpe has joined #ocaml
ttamttam has joined #ocaml
ttamttam has left #ocaml []
tane has joined #ocaml
milosn_ is now known as milosn
ttamttam has joined #ocaml
ttamttam has left #ocaml []
jsvgoncalves has quit [Ping timeout: 245 seconds]
<fds> I don't know if this is a stupid question, but why are <, <=, etc polymorphic, but +, *, etc aren't?
jsvgoncalves has joined #ocaml
<fds> I suppose my question is really "Why aren't +, *, etc polymorphic?" and "Doesn't the answer to that question apply equally to <, <=, etc?".
tani has joined #ocaml
tane has quit [Ping timeout: 256 seconds]
Anarchos has joined #ocaml
UncleVasya has joined #ocaml
jsvgoncalves has quit [Ping timeout: 256 seconds]
jsvgoncalves has joined #ocaml
jsvgoncalves has quit [Ping timeout: 256 seconds]
jsvgoncalves has joined #ocaml
ttamttam has joined #ocaml
emmanuelux has joined #ocaml
ttamttam has left #ocaml []
jbrown has joined #ocaml
bholst has quit [Quit: No Ping reply in 180 seconds.]
smerz_ has joined #ocaml
bholst has joined #ocaml
<gasche> fds: polymorphic comparison operators are ugly hack that we should get rid of
<gasche> the rationale for having them is that you really really often need equality for a wide range of different types
<gasche> morally, equality is "almost total": it works for most datatypes
<gasche> (the structural equalit (=) fails on function closures, and on data that ultimately contain closures; but some languages choose to define it everywhere, using physical equality when no other makes sense)
<gasche> on the contrary, arithmetic operators would be defined only for a small number of datatypes
<gasche> if you type system has no way to express, statically, "I work for only those types", it's not a very good idea to hack to add polymorphism
<darkf> if a function throws an exception is it not total?
<gasche> that's a bit subjective, really
<darkf> it would seem so
<bernardofpc> I guess this is a definition issue ?
<gasche> but the generally understood meaning for "total" is that you always terminate and never raise an exception
<darkf> fair enough
<pippijn> I think structural equality could be defined on closures
<gasche> meh
wwilly has joined #ocaml
<bernardofpc> (+) 3 = (+) 3 ?
<pippijn> yes, but also
<wwilly> bonjour
<bernardofpc> bonsoi
<bernardofpc> r
<pippijn> (let a = 3 in (+) a) = (+) 3
<bernardofpc> pippijn: right, but I guess in both cases you have to go down the closure tree ?
<pippijn> wait, that's the same
<pippijn> let make a = fun b -> a + b
<pippijn> make 3 = make 3
<gasche> I don't think there is a reasonable definition of equality for all closures
<bernardofpc> can't you have a reasonable definition by destructing ?
<gasche> destructing what?
<gasche> I don't understand
<bernardofpc> the AST that represents the closure
<pippijn> oh, no
<pippijn> no AST
<pippijn> physical equality for the function pointers
<fds> gasche: I see. Thanks for your reply.
<pippijn> (fun () -> 3) <> (fun () -> 3)
<bernardofpc> pippijn: right, but we want (+) 3 = make 3 or don't we ?
<pippijn> but if the function pointers are the same, and the captured environment is the same, it can be structurally compared
<pippijn> I don't see how, if the physical function is identical, the envs can be structurally different
<bernardofpc> right, but how do you find the envs ?
<pippijn> they are in a known location in the closure block
<pippijn> just like how they are found when calling the closure
<bernardofpc> hum, what forbids you from making
<bernardofpc> make (fib 4) = make (1 + 1 + 1) ?
<pippijn> nothing, and that's fine, because fib 4 will be evaluated before make is called
<pippijn> gasche: you think my definition is not reasonable?
<pippijn> it's a little conservative, but useful in many cases
<gasche> it may also be a security risk
groovy2shoes has joined #ocaml
<bernardofpc> this is like let rec equal clos1 clos2 = match clos1, clos2 with (f a), (g b) -> equal f g and equal a b
<gasche> currently closures are useful as a black-box
<gasche> sometimes you don't want values to be compared
<gasche> but in any case
<pippijn> that's not a security risk, because I can write a C extension to ocaml that implements exactly what I envision
<gasche> I don't think this definition of equality would be very useful
<gasche> pippijn: you can already with Obj
<pippijn> or obj :)
<gasche> when do we use the equality function, what for?
<gasche> if it's only for, say, storing values in a hashtable bucket, physical equality on closures is fine, no need to do ugly things in the captured environment
<gasche> if you need a finer-grained notion of equality, chances are you need something more fine-grained than this criterion; I find it best to fail when trying to compare closure, and force people to make different representation choices with comparability/serializability in mind
<gasche> in any case, I think we would be better off with an equality type-class
<pippijn> yes
ulfdoz has joined #ocaml
groovy2shoes has quit [Quit: groovy2shoes]
ttamttam has joined #ocaml
darkf has quit [Quit: Leaving]
<companion_cube> gasche: indeed
<companion_cube> and an ord type class
Kakadu has joined #ocaml
ttamttam has left #ocaml []
sepp2k has quit [Remote host closed the connection]
ttamttam has joined #ocaml
IbnFirnas has quit [Ping timeout: 252 seconds]
|jbrown| has joined #ocaml
walter has quit [Quit: This computer has gone to sleep]
IbnFirnas has joined #ocaml
jbrown has quit [Ping timeout: 268 seconds]
Arsenik has quit [Read error: Connection reset by peer]
Arsenik has joined #ocaml
jbrown__ has joined #ocaml
|jbrown| has quit [Ping timeout: 245 seconds]
bartholomew has joined #ocaml
walter has joined #ocaml
Arsenik has quit [Remote host closed the connection]
ttamttam has left #ocaml []
ttamttam has joined #ocaml
|jbrown| has joined #ocaml
ttamttam has left #ocaml []
jbrown__ has quit [Ping timeout: 240 seconds]
jbrown__ has joined #ocaml
|jbrown| has quit [Ping timeout: 268 seconds]
|jbrown| has joined #ocaml
jbrown__ has quit [Ping timeout: 240 seconds]
jbrown__ has joined #ocaml
|jbrown| has quit [Ping timeout: 264 seconds]
walter has quit [Quit: This computer has gone to sleep]
walter has joined #ocaml
awm22 has joined #ocaml
ttamttam has joined #ocaml
ttamttam has left #ocaml []
Anarchos has quit [Ping timeout: 245 seconds]
Anarchos has joined #ocaml
walter|r has joined #ocaml
walter has quit [Ping timeout: 256 seconds]
UncleVasya has quit [Quit: UncleVasya]
Arsenik has joined #ocaml
mjonsson has joined #ocaml
mjonsson has left #ocaml []
yezariaely has quit [Quit: changing servers]
groovy2shoes has joined #ocaml
smerz_ has quit [Ping timeout: 272 seconds]
IbnFirnas has quit [Read error: Operation timed out]
IbnFirnas has joined #ocaml
vpm has quit [Ping timeout: 245 seconds]
Leonidas has quit [Ping timeout: 245 seconds]
Leonidas has joined #ocaml
vpm has joined #ocaml
Nahra has quit [Read error: Connection reset by peer]
Nahra has joined #ocaml
Watcher7|off is now known as Watcher7
ontologiae has joined #ocaml
Kakadu has quit []
arj1 has joined #ocaml
jsvgoncalves has quit [Ping timeout: 252 seconds]
jsvgoncalves has joined #ocaml
adam-- has joined #ocaml
tani has quit [Quit: Verlassend]
Arsenik has quit [Remote host closed the connection]
jbrown__ has quit [Ping timeout: 256 seconds]
RagingDave has quit [Quit: Ex-Chat]
jsvgoncalves has quit [Ping timeout: 264 seconds]
jsvgoncalves has joined #ocaml
ulfdoz has quit [Ping timeout: 245 seconds]
eikke has joined #ocaml
arj1 has quit [Remote host closed the connection]
adam-- has quit [Ping timeout: 272 seconds]
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
arj1 has joined #ocaml
walter|r has quit [Quit: This computer has gone to sleep]
Watcher7 is now known as Watcher7|off
Watcher7|off is now known as Watcher7
walter has joined #ocaml
<wmeyer> pippijn: if you got equality on closures it would mean you solved the halting problem
rwmjones has quit [Read error: Operation timed out]
<ousado> wmeyer: could you elaborate on that?
eikke has quit [Ping timeout: 248 seconds]
<ousado> wmeyer: would that be equality as in semantic equivalence?
<wmeyer> ousado: I don't remember the exact proof of that, but what I am sure, it's impossible to say for any two programs that they will produce the same output for the any data
<wmeyer> that's why Coq is not turing complete and assume that the functions will always terminate
<wmeyer> so you'd need to be sure that both closures will produce for all it's arguments and all possible data always the same result
eikke has joined #ocaml
<ousado> wmeyer: yes, I see
ontologiae has quit [Ping timeout: 240 seconds]
<ousado> wmeyer: so that's not possible in general, I assume, but for certain given programs it should be
<wmeyer> ousado: exactly
<ousado> such as a < b and b >= a
<wmeyer> yes
rwmjones has joined #ocaml
<wmeyer> that's why in Coq you can prove this relations are equivalent
<wmeyer> s/this/these/
<ousado> and there's a proof that it's impossible in the general case?
<wmeyer> should be somewhere
<wmeyer> there is halting problem proof in Coq I think (def-lkb is it on your blog?)
<ousado> I have to admit that this feels counter-intuitive to me. at least when excluding sources of randomness
<wmeyer> to compare the output you have to run the program, but since some of them will not halt ...
eikke has quit [Ping timeout: 268 seconds]
<ousado> I see, so it's kind of an indirect proof
<wmeyer> I remember I figure out this myself at some point, but don't remember my exact thoughs :-)
<wmeyer> the papers by Gregory Chaitin are amazing and help
<ousado> oh man, you're such an heavy-weight champion, wmeyer :)
<ousado> (I mean it !!!)
<wmeyer> ousado: :D
<wmeyer> thanks
<wmeyer> here you go: http://www.google.com/url?q=http://www.cs.auckland.ac.nz/~chaitin/cup.pdf&sa=U&ei=b6p9UcGHIsav0QWi3oHQBQ&ved=0CCEQFjAB&sig2=WVpvCFhwTlLhPsIKZRoflg&usg=AFQjCNHlwldkcKZP7eYqrYKHMKZokGYE9A
paolooo has joined #ocaml
cdidd has quit [Remote host closed the connection]
paolooo_ has joined #ocaml
paolooo has quit [Client Quit]
<ousado> "In this chapter we construct an equation involving only whole numbers and addition, multiplication and exponentiation, with the property that if one varies a paramete rand asks whether the number of solutions is finite or infinite, the answer to this question is indistinguishable from the result of independent tosses of a fair coin"
q66 has quit [Remote host closed the connection]
<wmeyer> yes, it's a difficult paper, and to be honest never fully understood it
<wmeyer> but i felt like a different person after trying it
<ousado> the first sentences of the conclusion are fascinating already
<wmeyer> indeed
<wmeyer> you are reading about diophiantine equations
<wmeyer> which will map into lisp program
<wmeyer> and then he will prove that even in basic arithemtic involving these operations, some of the diophantine equations can have infinit number of solutions
<wmeyer> so they are equvailent lisp program which will not halt
<wmeyer> and assesing for any diophantine equation if it will ever for any parameter will produce infinite number of solutions is not possible
jsvgoncalves has quit [Ping timeout: 276 seconds]
<wmeyer> therefore answering pippijn question here if for given two closures we can in general conclude their equal, would reduce of answering if the two diophantine equations are not even the same - that's easy but will produce the same results for all the parameters
<ousado> :D
<wmeyer> I really enjoy reading it :)
<ousado> this makes me feel good, somehow. I like the world better this way
<wmeyer> you are right, I think i've though about it too :-)
<ousado> and I think this might also be an important result for cryptographic applications
<wmeyer> to build the world there must be some limits. The limits are putting together everything.
<wmeyer> ousado: in practice it affects every corner of the science
<ousado> indeed
<wmeyer> Chaitin is a good writer
<wmeyer> he likes to infect mind with his crazy ideas and proofs
<ousado> it's a good explanation why statistics are so important in all the social sciences, too
<wmeyer> yes, and as always there is no and will be no generic science
<wmeyer> once we generalize the science, we will not be able to measure anything
<ousado> chaos FTW :)
<wmeyer> oh yes, but perhpas there are equivalent theories :)
<ousado> I meant the non scientific chaos, in this case, hehe :)
<ousado> or both, maybe
<wmeyer> yes, it's chaos :)
<wmeyer> because it comes from randomness
milosn_ has joined #ocaml
<wmeyer> more practical theory is more it can measure but at the same time not able to scale to different domain
<wmeyer> this is Godel's incompletness theorem
<wmeyer> exact = specialised = not scale to other phenomena
<wmeyer> which maps to: can't create a formal system which is both consistent and complete
<ousado> I guess many folks over in #haskell have a problem with that idea
<wmeyer> oh definitely it affects: "can/can't" in the language or type system :)
milosn has quit [Ping timeout: 260 seconds]
* wmeyer going to bed
<ousado> wmeyer: good night! and thanks :)
<wmeyer> good night ousado, was a good chat, you can try the paper, you will enjoy it :-)
ousado has quit [Ping timeout: 256 seconds]
ousado has joined #ocaml
paddymahoney has joined #ocaml
darkf has joined #ocaml
<bernardofpc> http://www.math.rutgers.edu/~zeilberg/Opinion125.html -> I would also like that more effort would be put in doing positive proofs than just negative ones (even if the negative show that something shouldn't be pursued, it doesn't really solve a problem but rather say to us that we must rephrase our problem so that it is not so general, but remains practical and useful !)
walter has quit [Quit: This computer has gone to sleep]
<bernardofpc> wmeyer> because it comes from randomness -> oh please, not this... remember the logistic map, and also Poincaré's main motivation for introducing Chaos Theory: to be able to extract information from a system, *not* to throw his hands up and say "I don't know whether the solar system is stable or not"