flux changed the topic of #ocaml to: Discussions about the OCaml programming language | http://caml.inria.fr/ | OCaml 4.01.0 http://bit.ly/1851A3R | http://www.ocaml.org | Public logs at http://tunes.org/~nef/logs/ocaml/
<j0sh> is opam working?
<j0sh> can't update or install new packages
<j0sh> or is it just me?
<companion_cube> looks like it works for me
<j0sh> hm, alright
ollehar has quit [Ping timeout: 260 seconds]
ygrek has joined #ocaml
Xenasis has quit [Quit: WeeChat 0.4.2]
kyrylo has quit [Read error: Operation timed out]
mcclurmc has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
mcclurmc has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
kyrylo has joined #ocaml
talzeus has quit [Remote host closed the connection]
jwatzman|work has quit [Quit: jwatzman|work]
ygrek has quit [Ping timeout: 252 seconds]
yacks has joined #ocaml
talzeus has joined #ocaml
NoNNaN has quit [Ping timeout: 240 seconds]
kyrylo has quit [Quit: Hi, Rob!]
ygrek has joined #ocaml
kyrylo has joined #ocaml
kyrylo has quit [Client Quit]
kyrylo has joined #ocaml
kyrylo has quit [Read error: Operation timed out]
NoNNaN has joined #ocaml
x4i has joined #ocaml
manizzle is now known as WeLoveCP
WeLoveCP is now known as manizzle
kyrylo has joined #ocaml
watermind has joined #ocaml
watermind has quit [Client Quit]
philtor has joined #ocaml
talzeus has quit [Remote host closed the connection]
talzeus has joined #ocaml
manizzle has quit [Ping timeout: 272 seconds]
cesar_ has joined #ocaml
cesar_ is now known as Guest95236
skchrko has quit [Quit: Leaving]
kyrylo has quit [Ping timeout: 272 seconds]
Eyyub has quit [Ping timeout: 248 seconds]
bicgena has joined #ocaml
mcclurmc has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
Eyyub has joined #ocaml
mcclurmc has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
gambogi has joined #ocaml
lostcuaz has joined #ocaml
Eyyub has quit [Read error: Operation timed out]
yacks has quit [Read error: Connection reset by peer]
yacks has joined #ocaml
x4i has quit [Ping timeout: 248 seconds]
x4i has joined #ocaml
mreca has quit [Quit: Textual IRC Client: www.textualapp.com]
lostcuaz has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rand000 has joined #ocaml
mcclurmc has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
philtor has quit [Read error: Operation timed out]
Guest95236 has quit [Remote host closed the connection]
csakatoku has joined #ocaml
cesar_ has joined #ocaml
skchrko has joined #ocaml
cesar_ is now known as Guest4152
Guest4152 has quit [Remote host closed the connection]
ygrek has quit [Ping timeout: 248 seconds]
mcclurmc has quit [Remote host closed the connection]
mort___ has joined #ocaml
ggole has joined #ocaml
nikki93 has quit [Remote host closed the connection]
axiles has joined #ocaml
mort___ has quit [Quit: Leaving.]
ulfdoz has joined #ocaml
mcclurmc has joined #ocaml
ollehar1 has joined #ocaml
tristero has quit [Ping timeout: 246 seconds]
tristero has joined #ocaml
ulfdoz has quit [Ping timeout: 252 seconds]
mcclurmc has quit [Ping timeout: 260 seconds]
ulfdoz has joined #ocaml
dant3 has joined #ocaml
yacks has quit [Quit: Leaving]
tristero has quit [Ping timeout: 272 seconds]
ygrek has joined #ocaml
tristero has joined #ocaml
dant3 has quit [Remote host closed the connection]
dant3 has joined #ocaml
Kakadu has joined #ocaml
ulfdoz has quit [Ping timeout: 272 seconds]
x4i has quit [Quit: Lingo - http://www.lingoirc.com]
nikki93 has joined #ocaml
nikki93 has quit [Ping timeout: 272 seconds]
Thooms has joined #ocaml
mcclurmc has joined #ocaml
jao has quit [Ping timeout: 272 seconds]
zRecursive has left #ocaml []
mcclurmc has quit [Ping timeout: 246 seconds]
talzeus_ has joined #ocaml
talzeus has quit [Read error: Connection reset by peer]
talzeus has joined #ocaml
cago has joined #ocaml
csakatoku has quit [Remote host closed the connection]
csakatoku has joined #ocaml
talzeus_ has quit [Ping timeout: 260 seconds]
AltGr has joined #ocaml
AltGr has left #ocaml []
AltGr has joined #ocaml
csakatoku has quit [Ping timeout: 272 seconds]
csakatoku has joined #ocaml
wobster has joined #ocaml
Thooms has quit [Quit: WeeChat 0.3.8]
Thooms has joined #ocaml
nikki93 has joined #ocaml
nikki93 has quit [Ping timeout: 272 seconds]
mika1 has joined #ocaml
tristero has quit [Ping timeout: 272 seconds]
dant3 has quit [Remote host closed the connection]
dant3 has joined #ocaml
dant3 has quit [Ping timeout: 264 seconds]
martintrojer has quit [Read error: Connection reset by peer]
martintrojer has joined #ocaml
blAckEn3d has joined #ocaml
tristero has joined #ocaml
blAckEn3d has quit [Quit: Computer has gone to sleep.]
blAckEn3d has joined #ocaml
blAckEn3d_ has joined #ocaml
blAckEn3d has quit [Ping timeout: 245 seconds]
Atheist has joined #ocaml
Atheist is now known as Guest43493
Guest43493 has quit [Read error: Connection reset by peer]
dant3 has joined #ocaml
skchrko has quit [Quit: Leaving]
dant3 has quit [Ping timeout: 252 seconds]
dant3 has joined #ocaml
Simn has joined #ocaml
blAckEn3d_ has quit [Quit: Computer has gone to sleep.]
blAckEn3d_ has joined #ocaml
zpe has joined #ocaml
blAckEn3d_ has quit [Ping timeout: 252 seconds]
blAckEn3d has joined #ocaml
mort___ has joined #ocaml
jonludlam has joined #ocaml
avsm has joined #ocaml
dant3 has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
dant3 has joined #ocaml
Tamae has joined #ocaml
talzeus has quit [Remote host closed the connection]
thomasga has joined #ocaml
avsm has quit [Ping timeout: 248 seconds]
mcclurmc has quit [Ping timeout: 252 seconds]
_andre has joined #ocaml
_andre has quit [Read error: No route to host]
_andre has joined #ocaml
talzeus has joined #ocaml
ollehar1 has quit [Ping timeout: 260 seconds]
talzeus has quit [Remote host closed the connection]
blAckEn3d has quit [Quit: Computer has gone to sleep.]
talzeus has joined #ocaml
talzeus has quit [Remote host closed the connection]
talzeus has joined #ocaml
ocp has joined #ocaml
talzeus has quit [Read error: Connection reset by peer]
talzeus has joined #ocaml
ontologiae has joined #ocaml
ocp has quit [Quit: Leaving.]
ocp has joined #ocaml
tutak has joined #ocaml
<tutak> Hello guys
<tutak> I'm supposed to do a project in Ocaml, could be something like an implementation of Bellman-Ford algorithm.
csakatoku has quit [Remote host closed the connection]
<companion_cube> the graph distance thing, right?
<tutak> I have zero knowledge or ocaml or any other functional language. I do have programming background
<tutak> Yes
<companion_cube> tutak: you didn't have any lectures on ocaml?
<companion_cube> weird
<tutak> companion_cube, actually I'm doing this as an optional exam
<companion_cube> well, if you don't know ocaml at all, that might be tough.
<tutak> Is there any video short tutorial which could get me up and running a lil quickly than a say a complete book?
<companion_cube> http://ocaml.org/learn/ you may start here
<companion_cube> I don't think video tutorials are any good...
<companion_cube> follow the tutorial
<tutak> ok...
<companion_cube> good luck ^^
<tutak> thanks :D
<companion_cube> you can ask questions here if you're stuck
avsm has joined #ocaml
<tutak> companion_cube, What kind of areas is Ocaml used outside the diddatic area? I mean what kind of jobs is it associated with if any? I read it currently doesnt have widespread adoption
<companion_cube> it's used by a few companies (including a trading one), and by many researchers
baldandgoateed is now known as MacNuggard
skchrko has joined #ocaml
<companion_cube> but if you don't know a functional language, learning it will anyway be beneficial for you
<tutak> Ya, it would be interesting to have another outlook of programming rather than the usual OOP
<tutak> companion_cube, what do you think about this tutorial? http://try.ocamlpro.com/
<companion_cube> it should be nice too (you can use the online repl to follow the other tutorial, also)
amirmc has joined #ocaml
dant3 has quit [Remote host closed the connection]
Kakadu has quit [Ping timeout: 272 seconds]
mcclurmc has joined #ocaml
Kakadu has joined #ocaml
rand000 has quit [Ping timeout: 272 seconds]
mcclurmc has quit [Ping timeout: 265 seconds]
testcocoon has quit [Quit: Coyote finally caught me]
ontologiae has quit [Ping timeout: 252 seconds]
avsm has quit [Quit: Leaving.]
testcocoon has joined #ocaml
dsheets has quit [Ping timeout: 264 seconds]
dant3 has joined #ocaml
talzeus has quit [Remote host closed the connection]
tutak has quit [Ping timeout: 264 seconds]
nikki93 has joined #ocaml
nikki93 has quit [Read error: Operation timed out]
dsheets has joined #ocaml
amirmc has quit [Quit: Leaving.]
amirmc has joined #ocaml
thomasga has quit [Quit: Leaving.]
<Kakadu> What do you think, should some OCaml courses will be presented on www.coursera.org ?
blAckEn3d has joined #ocaml
zxqdms has quit [Quit: leaving]
amirmc has quit [Quit: Leaving.]
dant3 has quit [Remote host closed the connection]
dant3 has joined #ocaml
mcclurmc has joined #ocaml
mcclurmc has quit [Ping timeout: 246 seconds]
<hcarty> Does ctypes provide a way to create custom blocks, along the lines of http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual033.html#toc150 (section 19.9 in the manual)
<hcarty> ?
<hcarty> Kakadu: A well designed OCaml course would be nice to have on Coursera. I think it could help in promoting the language.
zxqdms has joined #ocaml
<Kakadu> hcarty: I think that too
<hcarty> Something based on OCaml From The Very Beginning or RWO, depending on the audience you want to target.
<NoNNaN> any idea about the proposed course topics?
<companion_cube> algorithmics ? :p
<Kakadu> Creating compilers using OCaml?
ontologiae has joined #ocaml
<pippijn> OFTVB is not a nice acronym
amirmc has joined #ocaml
<NoNNaN> Peter Sestoft, IT University of Copenhagen has some good courses on programming language concepts & compiler topic (eg.: http://www.itu.dk/courses/BPRD/E2013/),and the course use fsharp as the base/implementation language
<companion_cube> f# -_-
amirmc has quit [Ping timeout: 252 seconds]
ygrek has quit [Ping timeout: 272 seconds]
thomasga has joined #ocaml
mort___ has quit [Quit: Leaving.]
thomasga has quit [Client Quit]
kyrylo has joined #ocaml
<bernardofpc> Kakadu> What do you think, should some OCaml courses will be presented on www.coursera.org ? -> if you have a *really* good one, then sure yes
<bernardofpc> (if not, this is a good motivation to create such a good course :d)
<bernardofpc> as OCaml is not like "Lin Algebra" or "Philosophy 101" (a mandatory course for lots of people), having a "not top-notch course" might do more harm than good in promoting "this is a hard language, besides, nobody uses it"
<bernardofpc> otoh, if the course gets people doing fun stuff (my takes: matching, polymorphic functions, recursive algorithms on recursive data structures) then it will encourage people finding more and more about it
tianon has quit [Ping timeout: 260 seconds]
tianon has joined #ocaml
Thooms has quit [Ping timeout: 272 seconds]
<nicoo> hcarty: Regarding basing it on RWO, we would have to choose between OCaml/Core and OCaml. (And RWO is frustrating w.r.t. not specifying what is syntax extensions and what is vanilla OCaml)
<Drup> (in all cases, we need a cute camel drawing)
<hcarty> bernardofpc: Agreed
<hcarty> nicoo: Agreed too.
<companion_cube> Drup: ^^
<Drup> (for thos who don't know, this is the reference : http://learnyouahaskell.com/)
<nicoo> Drup: Yes, LYAH is just *great*
yacks has joined #ocaml
blAckEn3d has quit [Quit: Computer has gone to sleep.]
amirmc has joined #ocaml
amirmc has quit [Ping timeout: 252 seconds]
thomasga has joined #ocaml
amirmc has joined #ocaml
wobster has left #ocaml []
avsm has joined #ocaml
nbb_ has joined #ocaml
nikki93 has joined #ocaml
<nbb_> hi, a newcomer to React here. i have a problem where using S.value seems to have a side effect.
<nbb_> adding this line: List.map (fun _ -> None) (S.value state_s) |> ignore;
darkf has quit [Quit: Leaving]
<nbb_> changes the rest of the program. with the line it runs as intended, without it seems to hang.
<nbb_> should this be possible?
* adrien_oww would say "why not?"
nikki93 has quit [Ping timeout: 252 seconds]
<nbb_> well, the function does not do anything, except reading the value of the signal
<nbb_> i was assuming that only if the signal changes, there can be side effects.
<adrien_oww> one possible thing is that some stuff gets garbage-collected without this line
<adrien_oww> which usually translates by an absence of events
<adrien_oww> (or new signal values)
<companion_cube> nbb_: there is a combinator of type 'a S.t -> 'a E.t, that returns an event triggered every time the signal changes
<nbb_> hmm, ok. but the line does not define new values. so doing a garbage collection directly after the line should kill the effect again?
<companion_cube> val changes : 'a React.signal -> 'a React.event
<nbb_> companion_cube: yes, i am using that in fact at another place: S.changes state_s
skchrko has quit [Remote host closed the connection]
<nbb_> but S.value should not trigger the 'changes' event, right?
<companion_cube> reading from a signal or event doesn't change (nor affect in any way) the signal or event
<companion_cube> just be careful with the Gc
<nbb_> companion_cube: yes that's what i thought and that's why i am confused: the line in question should not really do _anything_ ?
<adrien_oww> nbb_: ocaml will not reclaim values as long as they are "in scope"
<nbb_> i just tired Gc.full_major () after the line and it did not change the behavior.
<adrien_oww> put the line of code you pasted into an intermediate function
<adrien_oww> that might change
Thooms has joined #ocaml
<nbb_> adrien_oww: ok, i tried the following:
<companion_cube> nbb_: hmmm, S.value seems to re-compute the current state of the signal, if needed, I guess
<nbb_> let ff () = let _ = List.map (fun _ -> None) (S.value state_s) |> ignore in () in ff ();
<nbb_> this has the same effect as the line by itself.
mcclurmc has joined #ocaml
<companion_cube> and how can this typecheck? S.value doesn't return a list
<adrien_oww> (* you could let ff () = ignore (List.map (fun _ -> None) (S.value state_s)) *)
<companion_cube> oh, t he value is a list
<companion_cube> -_-
<nbb_> yes, sorry, its 'a list
<adrien_oww> uncommon; but well, should work
<adrien_oww> nbb_: hmm, need to see the full code
<nbb_> yeah thanks anyway. i'll try to condense it and then post it to a mailing list probably?
Yoric has joined #ocaml
<companion_cube> if you need to perform side-effects on elements of an event or a signal, the iter functions are what you need
mort___ has joined #ocaml
<adrien_oww> and store your events in a data structure to make sure they're kept around
avsm has quit [Quit: Leaving.]
<nbb_> adrien_oww: yes, actually a list of signals/events may be better than a signal that is a list for garbage collection safety.
<adrien_oww> well, that's as you prefer
<adrien_oww> the golden rule with react is: keep it simple
<adrien_oww> and if you ever have 'a event event or 'a signal signal or any combination, you need to change it :P
blAckEn3d has joined #ocaml
dant3 has quit [Remote host closed the connection]
<nbb_> companion_cube: ok. the line i posted was just an example of some function; at first i was printing the state_s, but doing nothing was enough
<nbb_> anyway, i'll check that events are stored properly and try again.
rand000 has joined #ocaml
nbb_ has left #ocaml []
dant3_ has joined #ocaml
ontologiae has quit [Ping timeout: 265 seconds]
skchrko has joined #ocaml
ygrek has joined #ocaml
Thooms has quit [Ping timeout: 245 seconds]
avsm has joined #ocaml
FreeArtMan has joined #ocaml
avsm has quit [Quit: Leaving.]
FreeArtMan has quit [Quit: main.lv]
Yoric has quit [Ping timeout: 252 seconds]
shinnya has joined #ocaml
dant3_ has quit [Remote host closed the connection]
<thomasga> how do you turn-on binannot with oasis ?
Yoric has joined #ocaml
skchrko has quit [Quit: Leaving]
<thomasga> johnelse: does it work for 3.12.1 ?
<thomasga> (ie. is that converted to -annot ?)
<johnelse> thomasga: nope :( that's the drawback
<thomasga> hum
<johnelse> you could probably make a flag for it
<thomasga> thx
<johnelse> np
<thomasga> and I guess it's not possible to enable that option for all the libraries defined in an _oasis file
<thomasga> (ie. I have to copy it in every "libray" section)
<johnelse> if you can, I haven't figured out how :)
<thomasga> well copy/paste should be ok for now on …
avsm has joined #ocaml
mye has joined #ocaml
ocp has quit [Ping timeout: 265 seconds]
Eyyub has joined #ocaml
cago has left #ocaml []
lostcuaz has joined #ocaml
Eyyub has quit [Ping timeout: 252 seconds]
dant3 has joined #ocaml
cesar_ has joined #ocaml
cesar_ is now known as Guest15896
Guest15896 has quit [Remote host closed the connection]
dant3 has quit [Ping timeout: 272 seconds]
dant3 has joined #ocaml
mika1 has quit [Quit: Leaving.]
skchrko has joined #ocaml
dant3 has quit [Ping timeout: 245 seconds]
S11001001 has joined #ocaml
avsm has quit [Quit: Leaving.]
S11001001 has quit [Changing host]
S11001001 has joined #ocaml
nikki93 has joined #ocaml
saml has joined #ocaml
mocrunsthecity has joined #ocaml
avsm has joined #ocaml
bholst has joined #ocaml
mocrunsthecity has quit [Read error: Connection reset by peer]
nikki93 has quit [Ping timeout: 272 seconds]
mocrunsthecity has joined #ocaml
FreeArtMan has joined #ocaml
FreeArtMan has quit [Read error: Operation timed out]
Eyyub has joined #ocaml
FreeArtMan has joined #ocaml
lostcuaz_ has joined #ocaml
amirmc has quit [Quit: Leaving.]
Eyyub has quit [Ping timeout: 272 seconds]
FreeArtMan has quit [Read error: Connection reset by peer]
lostcuaz has quit [Ping timeout: 272 seconds]
Eyyub has joined #ocaml
Thooms has joined #ocaml
shinnya has quit [Ping timeout: 260 seconds]
ontologiae has joined #ocaml
Eyyub has quit [Ping timeout: 245 seconds]
cesar_ has joined #ocaml
cesar_ is now known as Guest83108
Guest83108 has quit [Remote host closed the connection]
FreeArtMan has joined #ocaml
shadynasty has joined #ocaml
Eyyub has joined #ocaml
FreeArtMon has joined #ocaml
<shadynasty> hello. what is the difference between "module Foo : sig ... end = struct ... end" vs "module Foo = struct ... end" ?
<companion_cube> shadynasty: one is a type declaration (put this in the .mli), the other is a concrete definition for Foo
<companion_cube> (put in the .ml, where the real code goes)
<shadynasty> isn't the first one a declaration and a definition?
<adrien_oww> it's not a "definition" like in C though
<adrien_oww> you add constraints on the interface of the module which is implemented inside "struct ... end"
<companion_cube> shadynasty: no, it just says "this module contains a module Foo with this signature"
<adrien_oww> that way you can add fields or restrict signatures
FreeArtMan has quit [Ping timeout: 245 seconds]
<shadynasty> aha
<fds> Regarding the earlier conversation on Coursera: I'd love to see a "writing theorem provers in OCaml" course taught by John Harrison. :-D
<companion_cube> oh dear
<companion_cube> oh dear
pminten has joined #ocaml
<companion_cube> is he the one who wrote the book on theorem proving, with ocaml samples?
<fds> Yeah
<shadynasty> does this channel have an eval bot?
<companion_cube> shadynasty: sadly not
<companion_cube> I don't know if such a bot exists
<companion_cube> that would be interesting though
<bernardofpc> there's an online repl ;-)
nikki93 has joined #ocaml
<shadynasty> neat, it even adds the trailing ;; for you :)
S11001001 is now known as S11001010
<companion_cube> but you're right, we should have this
<shadynasty> yeah, eval bots are great
<adrien_oww> xavierbot is an eval bot
<adrien_oww> bots tend to be frowned upon because they spam
<adrien_oww> just make a type error with objects or polymorphic variants and you'll end up with a long error message
<companion_cube> that's just a matter of limiting output
<gambogi> opam question: I have a package (ExtLib) installed, but when I try to open it in utop (or any program) I get an unbound module exception
<gambogi> any common causes for this?
<companion_cube> gambogi: did you #require "extlib";; ?
FreeArtMon has quit [Quit: main.lv]
<gambogi> companion_cube: so ExtLib does apear, but the submodule(?) ExtUTF8 doens't seem to be there
nikki93 has quit [Ping timeout: 252 seconds]
<companion_cube> are there other modules in Extlib you can access?
S11001010 is now known as S11001001
<gambogi> yeah
<companion_cube> are you sure this module is still in current versions of Extlib?
<companion_cube> hmmmm, Extlib.UTF8 does exist
Kakadu has quit [Quit: Page closed]
Eyyub has quit [Read error: Operation timed out]
zarul has quit [Remote host closed the connection]
FreeArtMan has joined #ocaml
zarul has joined #ocaml
avsm has quit [Quit: Leaving.]
FreeArtMan has left #ocaml []
<companion_cube> fds: that's a pretty interesting idea you had, still
AltGr has left #ocaml []
AltGr has joined #ocaml
yacks has quit [Quit: Leaving]
dant3 has joined #ocaml
avsm has joined #ocaml
avsm has quit [Client Quit]
avsm has joined #ocaml
zarusky has joined #ocaml
zarul has quit [Ping timeout: 245 seconds]
avsm has quit [Ping timeout: 260 seconds]
<jpdeplaix> gasche: Do you currently subscribe to the pgocaml mailing-list ?
jwatzman|work has joined #ocaml
travisbrady has joined #ocaml
AltGr has left #ocaml []
AltGr has joined #ocaml
Kakadu has joined #ocaml
mort___ has quit [Quit: Leaving.]
thomasga has quit [Read error: Operation timed out]
tobiasBora has joined #ocaml
pminten has quit [Remote host closed the connection]
<gambogi> so I have ~/.opam/4.01.0/lib/extlib/uTF8.cmi
<gambogi> and the .mli
<gambogi> but for some reason utop still doesn't see the module
<companion_cube> gambogi: try just using Extlib.UTF8
<companion_cube> once you #require'd it
<gambogi> doesn't work
<companion_cube> strange
<Kakadu> Why I don't have uTF8.cmi?
<Kakadu> I just install extlib via opam
jonludlam has quit [Remote host closed the connection]
<companion_cube> I don't have it either, actually
<companion_cube> but Extlib.UTF8.empty (say) works
<Kakadu> I look at build directory and it seems that uTF8.ml was not built
<gambogi> I did a build from source and it asked whether or not to include uTF8
<Kakadu> opam uses `make minimal=1 build` command
<fds> companion_cube: I'm glad you think so. :-)
<Kakadu> this command doesn't builds UTF8
<companion_cube> interesting
<companion_cube> ooooh
<fds> My OCaml skills are still very basic, but it's ML's theorem-proving pedigree which has brought me here.
<Kakadu> README >
<Kakadu> `minimal=1` will exclude from build several modules (namely Unzip UChar UTF8) potentially conflicting with other
nikki93 has joined #ocaml
<companion_cube> my bad, I had batteries loaded
<companion_cube> and it shadows Extlib
<companion_cube> fds: you're interested in automated theorem proving? :>
<fds> Yeah, I'm interested in automated and interactive theorem proving. Pen and paper theorem proving too!
nikki93 has quit [Ping timeout: 245 seconds]
nikki93 has joined #ocaml
mort___ has joined #ocaml
AltGr has left #ocaml []
mort___ has quit [Remote host closed the connection]
rand000 has quit [Ping timeout: 246 seconds]
nikki93 has quit []
tobiasBora has quit [Quit: Konversation terminated!]
tobiasBora_ has joined #ocaml
Yoric has quit [Ping timeout: 245 seconds]
tobiasBora_ has quit [Ping timeout: 252 seconds]
ggole has quit []
rand000 has joined #ocaml
Thooms has quit [Quit: WeeChat 0.3.8]
troydm has quit [Quit: What is hope? That all of your wishes and all of your dreams come true? (C) Rau Le Creuset]
arjunguha has joined #ocaml
arjunguha has quit [Client Quit]
mocrunst_ has joined #ocaml
manizzle has joined #ocaml
mocrunst_ has quit [Client Quit]
mocrunst_ has joined #ocaml
mocrunsthecity has quit [Ping timeout: 272 seconds]
mocrunst_ has quit [Client Quit]
mocrunsthecity has joined #ocaml
malvarez has joined #ocaml
ollehar has joined #ocaml
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
dant3 has quit [Remote host closed the connection]
dsheets has quit [Ping timeout: 246 seconds]
dant3 has joined #ocaml
troydm has joined #ocaml
tobiasBora_ has joined #ocaml
ygrek has quit [Ping timeout: 265 seconds]
ontologiae has quit [Ping timeout: 245 seconds]
willb2 has quit [Ping timeout: 252 seconds]
dant3 has quit []
blAckEn3d has quit [Quit: Lingo - http://www.lingoirc.com]
Eyyub has joined #ocaml
tobiasBora_ has quit [Ping timeout: 264 seconds]
tobiasBora_ has joined #ocaml
mocrunsthecity has quit [Remote host closed the connection]
<MacNuggard> fds, pen and paper theorem proving seldom seems to be "formal" though.
<MacNuggard> I would take the position that anything other than a formal proof is pseudoscience and I think it's funny how extremely defensive everyone gets over it if their favourite academic disciple is called a pseudoscience.
_andre has quit [Quit: leaving]
willb1 has joined #ocaml
xkb_ is now known as Xebia
Xebia is now known as xkb
tobiasBora_ has quit [Quit: Konversation terminated!]
Anarchos has joined #ocaml
Eyyub has quit [Ping timeout: 252 seconds]
dsheets has joined #ocaml
Eyyub has joined #ocaml
<bernardofpc> Well, if you start calling people names, it is fairly understandable that they get defensive ;-)
willb1 has quit [Read error: Operation timed out]
<bernardofpc> (pseudoscience being outright aggressive, at least if you want what you're doing to BE science)
<adrien> if we invented computers through science and couldn't do science before we had computers, how did we do it?
<companion_cube> :)
<bernardofpc> maybe we did not invent computers through science ?
<bernardofpc> (maybe we didn't even INVENT computers !)
<companion_cube> maybe it's the illuminati from the future :p
<bernardofpc> (maybe the matrix gots us)
<bernardofpc> </brain needs rest>
<adrien> but who built the machines that built the matrix?
Eyyub has quit [Ping timeout: 240 seconds]
<MacNuggard> bernardofpc, where am I calling people names?
<MacNuggard> Besides, formal proofs existed before computers, it just happens that computers are such a great tool constructing and verifying them that doing it without them nowadays is insanity.
Eyyub has joined #ocaml
<Anarchos> companion_cube don't feed the troll....
<bernardofpc> MacNuggard: in fact, "science" as defined by philosophy is not formalism, rather the cycle "hypothesis -> model -> forecasts -> experiments"
<bernardofpc> (so Math, and maybe Computer "Science" are not sciences since they don't admit falsifiable hypothesis through experiments
<MacNuggard> bernardofpc, well, maybe, but formalism is the only thing that meets Popper's criteria.
<MacNuggard> It is the only thing that is purely objective and reproducible and free from human interpretation
<bernardofpc> of falsifiability ?
<MacNuggard> Of reproducibility actually.
<bernardofpc> Oh
<adrien> ls
<adrien> ergh
<MacNuggard> The point of non formalism is that there can exist debate on how to interpret things because well, there is human interpretation
<bernardofpc> This is IRC, Not zsh ;-)
<adrien> tired brain
<MacNuggard> And formal proofs also have this amazing property of not really being disprovable.
<bernardofpc> ribht
<asmanur_> MacNuggard: uh?
<bernardofpc> so you disjoin falsifiability from reproducibility
<asmanur_> have you been away for the last century ?
<bernardofpc> therefore ther's no science
<MacNuggard> asmanur_, such as?
rand000 has quit [Ping timeout: 272 seconds]
<MacNuggard> bernardofpc, if we add the criterion of empirical I would submit to that
<asmanur_> MacNuggard: I'm not sure what you mean by a proof being "disprovable"
<asmanur_> but a formal proof is no assurance of the "truth" of the statement
<bernardofpc> truth is just a formal value anyway ;-)
<MacNuggard> asmanur_, what is this "truth" of which you speak?
<bernardofpc> it bears no relation to the Universe
<MacNuggard> All I know is following from the axioms by the rules of inference.
<bernardofpc> of course, one might object to the purpose of doing something absolutely disconnected from reality by fiat
<asmanur_> yes MacNuggard but what the point of writing overly formal proof in a system where you have no guarantee on the soundness of the system?
<MacNuggard> asmanur_, well, clearly proofs are not disprovable, that makes them proofs.
<MacNuggard> If they were disprovables they wouldn't be proofs.
<MacNuggard> Proving the negation does not disprove the proof, it just proves the inconsistenty of the system
<MacNuggard> asmanur_, I never spoke of use or points or truthfulness.
<MacNuggard> I'm saying what it is, not if we should do it or if it's useful.
<asmanur_> MacNuggard: uh, you were saying that without formal proofs, no science is possible
<MacNuggard> which is more or less the jumps in logic many people tend to make when I call thnigs pseudosciences, that they are not useful or I dislike them or dislike the people that practice them or whatever, people seem to have a very hard time keeping those things disjoint
<MacNuggard> indeed
<bernardofpc> well, you were the one calling "pseudoscience", which is a very negative word, at least as people interpret it
<bernardofpc> if you just say "empirical science" or "interpreted science", this is much more precise, and also will not invoke flames on you
<bernardofpc> even though human interpretation might be a very bad thing for science, it's the way most people (if not all) interact
<MacNuggard> bernardofpc, therein lies the problem more or less.
<MacNuggard> People's disposition to use terms more as value judgements rather than descriptive.
<MacNuggard> Like ehh "terrorist" and "freedom fighter" ultimately they mean the same thing, it just communicates if you agree with their cause or not.
<MacNuggard> And then you have people who actually say "No, we're not terrorists, we're fredeom fighters!"
<bernardofpc> well, that's a different issue, because "pseudoscience" is not well defined, nor your definition of science is common to everybody
<bernardofpc> most people don't even know Popper's criteria
<MacNuggard> I'm just taking popper's criteria literally in this case.
<MacNuggard> But I usually qualify it as "accordingly popper's criteria, everything but formalism is a pseudosciecne"
<MacNuggard> Or at least not a science.
<MacNuggard> Where a pseudoscience is something that claims to be a science but isn't.
Yoric has joined #ocaml
<adrien> popper was an idiot then
<Drup> bernardofpc: very brave of you to try to convince a troll not to use an abrasive, I admire the effort, though I find it pointless.
<MacNuggard> More like popper didn't intend people to take his criteria literally.
<Drup> abrasive term*
tane has joined #ocaml
<MacNuggard> or "strictly" rather
rand000 has joined #ocaml
rand000 has quit [Client Quit]
tlockney has quit [Quit: I may return, one day...]
Yoric has quit [Ping timeout: 252 seconds]
mocrunsthecity has joined #ocaml
malvarez has quit [Remote host closed the connection]
talzeus has joined #ocaml
tlockney has joined #ocaml
tlockney has quit [Client Quit]
tlockney has joined #ocaml
shadynasty_ has joined #ocaml
thomasga has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-20131020]: i've been blurred!]
mocrunsthecity has quit [Remote host closed the connection]
ocp has joined #ocaml
lostcuaz_ has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<shadynasty_> what is the difference between a functor and a function of type module -> module?
shadynasty_ has quit [Quit: Page closed]
<companion_cube> aww
<shadynasty> hi
<shadynasty> :)
<companion_cube> shadynasty: a functor is, indeed, a function from modules to modules :)
<companion_cube> most of the time called at compile time, but sometimes also at runtime
<companion_cube> let module M = Map.Make(....) in
<shadynasty> functors seem to take as argument a non-first-class module though
<companion_cube> indeed
<companion_cube> I think that's an artifact of the type system
<companion_cube> which separates modules and values
<companion_cube> and provides way to convert between them, the "first class modules", indeed
Yoric has joined #ocaml
nikki93 has joined #ocaml
<MacNuggard> companion_cube, a functor is a function from module to module?
<MacNuggard> I always thought it was more from type to module
Yoric has quit [Client Quit]
Yoric has joined #ocaml
<companion_cube> MacNuggard: no, it takes a module as an argument
mocrunsthecity has joined #ocaml
<companion_cube> argument that may contain several types and values
thomasga has quit [Quit: Leaving.]
Kakadu has quit []
<MacNuggard> companion_cube, can't a functor take pretty much any value as argument which needn't be a module?
<companion_cube> no, a functor takes a module as argument and returns a module
<companion_cube> if you want to give it a simple value, wrap it in a module :p
FreeArtMan has joined #ocaml
<MacNuggard> THen I am verily confused
<MacNuggard> oh well
<MacNuggard> I'mretarded anyway
axiles has quit [Remote host closed the connection]
<companion_cube> nah
<MacNuggard> companion_cube, well, maybe not that bright.
<MacNuggard> I'm good at StarCraft II though.
malvarez has joined #ocaml
<MacNuggard> I play every race and every matchuyp is my finest.
<nicoo> l
<dsheets> starcraft ii is basically ocaml, you should be fine
<nicoo> :D
<nicoo> dsheets: What is the OCaml equivalent of zerglings ?
<dsheets> boxes
zpe has quit [Remote host closed the connection]
<MacNuggard> integers, clearly.
<dsheets> when you transform your town center, it is a functor application
zpe has joined #ocaml
<dsheets> when you transform a unit, it is a function
<companion_cube> MacNuggard: then you should write bots for starcraft 2, in OCaml
<companion_cube> and win the championships :>
<MacNuggard> I don't think SC2 has an exposed API, only BW.
<companion_cube> ah, right
<tautologico> there was a competition a couple of years ago for StarCraft 1 AIs
ontologiae has joined #ocaml
<adrien> BW doesn't have an exposed API either
<adrien> it's RE iirc
mocrunsthecity has quit [Remote host closed the connection]
<MacNuggard> Well, not by Blizzard, but someone made BWAPI.
<tautologico> yeah I don't think they have an official API
<MacNuggard> It's not official, it just exists.
<MacNuggard> And Blizzard has been kind enough to let AI competitions happen
zpe has quit [Read error: No route to host]
ontologiae has quit [Ping timeout: 248 seconds]
FreeArtMon has joined #ocaml
FreeArtMan has quit [Ping timeout: 252 seconds]
willb1 has joined #ocaml
mye has quit [Quit: mye]
<adrien> anyone know someone (nick)named "gallais"? (doing coq)
<asmanur_> guillaume allais ?
Yoric has quit [Ping timeout: 245 seconds]
<adrien> just saw that, yeah
<adrien> and apparently he's in scotland
<adrien> poor soul :P
<companion_cube> must drown his pain in whisky
<adrien> (and he does agda)
travisbrady has quit [Quit: travisbrady]
travisbrady has joined #ocaml
FreeArtMan has joined #ocaml
FreeArtMan has quit [Client Quit]
FreeArtMon has quit [Remote host closed the connection]
Eyyub has quit [Read error: Operation timed out]
Eyyub has joined #ocaml
Simn has quit [Ping timeout: 252 seconds]
Sim_n has joined #ocaml
Yoric has joined #ocaml
tnguyen1 has quit [Quit: tnguyen1]
<MacNuggard> companion_cube, explain to me how a functor is a function from module to module.
<MacNuggard> Is module a type?
<MacNuggard> are modules typed/
<companion_cube> ocaml contains a language for modules
<companion_cube> where you have modules and module types
<companion_cube> and functors which are, really, functions from modules of a certain type, to modules of another type
sgnb has quit [Read error: Connection reset by peer]
sgnb has joined #ocaml
<nicoo> companion_cube: You can have also equality constraints tying these modules together
<nicoo> )types insides these modules*)
<companion_cube> indeed
<companion_cube> there are links between the values world and the module world
zpe has joined #ocaml
Eyyub has quit [Ping timeout: 264 seconds]
Eyyub has joined #ocaml
<Drup> nicoo: the modules themself too
ollehar1 has joined #ocaml
tane has quit [Quit: Verlassend]
jao has quit [Read error: Operation timed out]
Eyyub has quit [Ping timeout: 248 seconds]
Eyyub has joined #ocaml
Yoric has quit [Ping timeout: 245 seconds]
Sim_n is now known as Simn
Eyyub has quit [Read error: Operation timed out]
mcclurmc has quit [Remote host closed the connection]
Eyyub has joined #ocaml
<nicoo> Drup: True, but I wanted to begin with the most common exemple
mcclurmc has joined #ocaml
mcclurmc has quit [Remote host closed the connection]
dant3 has joined #ocaml
ocp has quit [Ping timeout: 260 seconds]
saml has quit [Quit: Leaving]
thomasga has joined #ocaml
darkf has joined #ocaml
S11001001 has quit [Quit: ERC Version 5.3 (IRC client for Emacs)]
thomasga has quit [Quit: Leaving.]
thomasga has joined #ocaml
dant3 has quit [Remote host closed the connection]
dant3 has joined #ocaml
nikki93 has quit [Remote host closed the connection]
mcclurmc has joined #ocaml
<MacNuggard> companion_cube, so is it possible to make a function char -> module?
<Drup> it is now, since we have first class modules, yes
<MacNuggard> since when do we have this?
<MacNuggard> those*
<Drup> I don't remember if it's
<Drup> 3.12 or 4.00.0
<Drup> so 3.12
<MacNuggard> How exactly does this work with lexical scope though?
<MacNuggard> If a module exists at runtime and potentially even depend on user input.
<Drup> wat with lexical scope ?
<Drup> It doesn't change anything
mcclurmc has quit [Ping timeout: 272 seconds]
<Drup> module type S = sig val x : char end ;;
<Drup> let f x = let module M = struct let x = x end in (module M : S) ;;
<Drup> here is a simple example
<MacNuggard> Well, if modules are first class then it is only decidable at runtime what bindings they define no?
<MacNuggard> Well, it's not decidable at all in fact then
<Drup> you have to provide the type if you want to use a module as value
<malvarez> Drup: I think he means you can't bind names to values at compile time
<MacNuggard> at runtime rather
<Drup> you still now what's in the scope
<Drup> know*
<MacNuggard> but the type of the module basically encorporates all its bindings and their types?
<Drup> yes
<MacNuggard> Well, that solves it I guess.
<Drup> yes =)
<MacNuggard> Makes for some very inflexible first class modules though.
<MacNuggard> I thought it was more something like how python modules functioned
<Drup> there is no such things as "python modules", call them by their names : they are dictionaries.
<malvarez> As I understand it, it's basically like passing around a record
<malvarez> Perhaps with existential types if you have abstract types in your module
<malvarez> But I could be terribly wrong
<MacNuggard> Drup, oh please, that's just a definition war.
<MacNuggard> They are called modules in python nomenclature, Ocaml functions are technically not functions either.
<Drup> MacNuggard: you mean, like pseudoscience ? :p
<ousado> MacNuggard: inflexible in what way?
<MacNuggard> Drup, I didn't make the definition, I just took the one everyone swears by and for kicks and funs poibnt out that when you take it strictly only formalism falls under it.
<MacNuggard> inflexible in that they aren't dictionaries that grossly violate static scope
<MacNuggard> I have no idea how python's scoping model works, I feel guido wants us to not worry about how it works at all and just hack stuff together having no idea what we are doing.
thomasga has quit [Quit: Leaving.]
<ousado> you mean "... that don't circumvent the type system" ?
<Drup> (also, MacNuggard, python modules really *are* exactly the same as python's dictionaries)
<Drup> (you can manipulate them in the same way ... like adding stuff in another module at runtime)
<MacNuggard> Isn't that extremely expensive, to hash every time you just want to access a binding?
<MacNuggard> Python has no type system
<MacNuggard> I reserve my right to call dynamic typing untyped.
<Drup> I will let the implementation details to python people, but you can do the same stuff with both.
<MacNuggard> Though I suppose you can argue that a > b > c in python constitutes a form of static typing.
<ousado> static typing happens at compile time
<ousado> .. and I assumed "they" referred to ocaml modules, in your above sentence
sillyotter has joined #ocaml
<MacNuggard> The gripe people have with the term "dynamic typing" is more that it is a completely unrelated concept to static typing and in fact not something special.
<MacNuggard> Static typing is investigating the structure of a datum and deciding based on it what the return value of a procedure must bee.
sillyotter has quit [Client Quit]
<Drup> huh, no, that's inference.
<MacNuggard> Ehh
<MacNuggard> dynamic typing is ...*
<MacNuggard> I'm basically saying there is no real difference between investigating the "tag" of a datum and investigating the first character of a string.
<MacNuggard> In fact, internally many dynamic types are implemented as vectors whose first element is some special value
<Drup> and ?
<MacNuggard> And therefore dynamic typing doesn't really exist, there is no hard definition of what a "dynamic type" would be,.
<MacNuggard> And what would make it different from simply the first character of a string.
<Drup> you like to redefine words to your own definition, don't you ?
<flux> actually he is following the definitions used in research about.. types?
cesar_ has joined #ocaml
<MacNuggard> I am.
cesar_ is now known as Guest60476
<flux> the type of any value in a dynamically typed language is the one and same, universal type
<MacNuggard> In type theory python's grammar would be called untyped or unityped.
<flux> how it behaves depends completely on what is done at runtime, so you cannot pick a fragment of code in isolation and see what it means type-wise, you must execute it
<MacNuggard> Also, all languages almost have some form of dynamic typing. that ( > ) in OCaml fails on two functions int -> int is arguably dynamic typing.
<MacNuggard> flux, well, I wouldn't call it a "type" or at the very least it's something fundamentally different from the types of expressions in a recursive langauge.
<MacNuggard> And I don't think it's even been formalized what a "dynamic type" would be given that it's not really magical, it's just part of the structure of a datum much like the first character of a string.
travisbrady has quit [Quit: travisbrady]
Simn has quit [Quit: Leaving]
Guest60476 has quit [Remote host closed the connection]
lostcuaz has joined #ocaml
<ousado> pythons grammar wouldn't be called anything in type theory, grammar is about syntax
<MacNuggard> static typing is very much about grammar.
<MacNuggard> In fact, it's basically a hack to keep calling a langauge context free when it actually isn't.
skchrko has quit [Quit: Leaving]
<ousado> uhm.. this is getting weird
willb1 has quit [Ping timeout: 264 seconds]
<MacNuggard> Not at all.
<MacNuggard> That's what it is. The grammar for OCAM would say something like <lambda> := fun <id> + -> <exp>; or whatever which is a context free grammar because a context free grammar can't express the limitatins to <exp> that would be required, that would be context sensitive.
<MacNuggard> But then we just say that it is "grammatical, but wrongly typed" in some cases which means that because we call it grammatical, it's still a context free grammar, if we said it was ingrammatical it would not be a context free grammar but ultimately that would change nothing as far as partioning the kleene set of symbols into compilable and uncompitable ocaml programs.
<MacNuggard> We could just as well say that wrongly typed programs are "ingrammatical" and arrive at the same accept/reject partitioning but then the langauge's grammar is no longer context free.
madroach has quit [Ping timeout: 252 seconds]
dant3 has quit [Remote host closed the connection]
dant3 has joined #ocaml
dant3 has quit [Remote host closed the connection]
madroach has joined #ocaml
willb1 has joined #ocaml
csakatoku has joined #ocaml
mcclurmc has joined #ocaml
Eyyub has quit [Ping timeout: 240 seconds]
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
Eyyub has joined #ocaml