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/
troydm has quit [Ping timeout: 248 seconds]
talzeus has joined #ocaml
emmanuelux has quit [Quit: emmanuelux]
Watcher7 is now known as Watcher7|off
troydm has joined #ocaml
Watcher7|off is now known as Watcher7
<pippijn> MarcWeber: filter?
<pippijn> MarcWeber: you mean syntax extension?
<pippijn> ah
<pippijn> you mean camlp4 filter
<pippijn> that's nice
<MarcWeber> Right now I want tagging ..
talzeus has quit [Remote host closed the connection]
<pippijn> tagging?
<pippijn> whitequark: I like the namespaces
<MarcWeber> tag files.
<pippijn> MarcWeber: for editors?
<MarcWeber> sure
<pippijn> why?
<pippijn> what do you need?
<MarcWeber> pippijn: I need "tell me definition of Camlp4.Sig.AstFilters"
<pippijn> anything you can't do with .annot files?
<MarcWeber> How do you do this?
<pippijn> hum
<pippijn> MarcWeber: ocaml toplevel :)
<MarcWeber> Let me try
<pippijn> MarcWeber: what library is that module in?
<MarcWeber> ocaml distribution
<pippijn> what library?
<pippijn> camlp4lib.cma?
<MarcWeber> Camlp4 could have told you. No idea. I could use grep.
<MarcWeber> But let me try .annot first
<pippijn> camlp4 can tell me?
<pippijn> how can it tell me where a module is defined?
<pippijn> MarcWeber: https://paste.xinu.at/L1gEq8/
<MarcWeber> I have the source.
<MarcWeber> I just want to goto it faster ..
<pippijn> ah
<pippijn> well, the annot doesn't tell you what file it is defined in, I think
<MarcWeber> module type AstFilters = sig
cthuluh has joined #ocaml
<MarcWeber> That looks close.
<pippijn> there are several AstFilters
<pippijn> there is otags
<MarcWeber> There is ocamltags (emacs, written in lisp)
<pippijn> and ocamltags
<pippijn> yeah
<MarcWeber> There is otags, which requires me to know whethere I have to use revised syntax and which syntax extensions?
<MarcWeber> I don't know.
<MarcWeber> So for now simple regex for ctags will do probably.
troydm has quit [Ping timeout: 248 seconds]
yacks has quit [Ping timeout: 264 seconds]
<MarcWeber> http://dpaste.com/1269300/ is what I use for now
<MarcWeber> ~/.ctags
<MarcWeber> then ctags -R .
<MarcWeber> ctags is "exuberant ctags"
<MarcWeber> It may not be perfect, but with some luck it works for most cases I care about.
troydm has joined #ocaml
<MarcWeber> That was missing 'value'
jcao219 has joined #ocaml
introom has joined #ocaml
<Drup> pippijn: annot can't tell you, but .cmt (with ocamlspot) can.
<Drup> probably merlin too
<MarcWeber> Thanks
breakds has joined #ocaml
csakatoku has joined #ocaml
<MarcWeber> Drup: Which of the buildsystems allow to easily use those tools?
<MarcWeber> Can I use ocamake --with-ocmal-spot or the like?
darkf has joined #ocaml
<Drup> hum, I was not clear enough, sorry
<Drup> ocamlspot is a tool to browse .cmt files, .cmt files are generated by the -bin-annot command line option in the compiler
<Drup> so ocamlspot is used by the editor, not the compiler.
<MarcWeber> Can you find a similar one sentence explains it all description for merlin?
<Drup> merlin use cmt files for other file than the current end the current file is browsed using a custom top level that allow annot-like feature without recompilation
<Drup> s/end/and
<Drup> I'm really bad with build systems so you will have to look at the documentation to see how to add the -bin-annot option
<MarcWeber> :)
<pippijn> wmeyer: ping
<pippijn> or anybody else doing coq
<MarcWeber> Is 4.00 likely to be compatible to 3.x code?
<pippijn> wmeyer: I have this: | Repeat : regex -> nat -> regex
breakds has quit [Quit: Konversation terminated!]
<pippijn> wmeyer: I want to say "nat that is >= 1"
<pippijn> wait..
<pippijn> nat is already >= 1 :)
<pippijn> never mind
<MarcWeber> def-lkb_: I've seen that merlin also works with Vim. Vim users may want to have a look at github.com/MarcWeber/vim-addon-ocamldebug
breakds has joined #ocaml
<Tobu> blerp, ocaml 4.00.1doesn't build with -j in MAKEFLAGS
breakds has quit [Remote host closed the connection]
<pippijn> ok, now I need help
<pippijn> it doesn't like my recursive call
<MarcWeber> I guess you have to talk more if you want others to help you ..
<pippijn> the fixpoint is_empty_language has the following match case: | Not (Intersect r1 r2) => is_empty_language (Not r1) && is_empty_language (Not r2)
pootler__ has quit [Ping timeout: 255 seconds]
pootler_ has quit [Ping timeout: 240 seconds]
<pippijn> or the simpler one:
<pippijn> | Not (Repeat r n) => is_empty_language (Not r)
Drup has quit [Quit: Leaving.]
<MarcWeber> I'll take a nap. If you want me to try to help you (my knowledege is still limited) then you should paste a block of code. I don't understand your case yet.
madroach has quit [Ping timeout: 248 seconds]
<pippijn> MarcWeber: do you know coq?
Neros has quit [Ping timeout: 246 seconds]
madroach has joined #ocaml
<amiller_> ok so now i want to use ocamlprof with my compiler-libs-hack compiler
<amiller_> there's no driver/compilep.ml or anything like that
<pippijn> oh
<pippijn> nat is not >= 1
<pippijn> meh :\
<pippijn> "The constructor O is zero"
dsheets has joined #ocaml
<MarcWeber> pippijn: Not much. How do you run that code?
<pippijn> I don't run it
<pippijn> I try to compile it
talzeus has joined #ocaml
Neros has joined #ocaml
<MarcWeber> pippijn: Do you mind pasting the command line you use for "compiling" it?
<bernardofpc> Error: Cannot find library Types in loadpath => meh
yacks has joined #ocaml
<pippijn> bernardofpc: https://paste.xinu.at/vTTeN3/
<pippijn> MarcWeber: coqc Types.v; coqc Language.v
<MarcWeber> Now I have a {Types,Language}.vo files.
<MarcWeber> And what was causing trouble to you?
<pippijn> the commented out code
<pippijn> the de morgan rules
<pippijn> or
<pippijn> MarcWeber: try uncommenting the Repeat case
<pippijn> | Not (Repeat r n) => is_empty_language (Not r)
<MarcWeber> I should start by understanding the working code first :)
<MarcWeber> double_negation is commented, too?
<bernardofpc> pippijn: I guess that you should unfold the Not
<pippijn> :\ ok
<bernardofpc> I am also learning Coq, but I guess it cannot prove that your transformation is "reducing the complexity of the formula"
<pippijn> yeah
<pippijn> I was hoping it could
<pippijn> or I could somehow prove it
<pippijn> especially in | Not (Intersect r1 r2) => is_empty_language (Not r1) && is_empty_language (Not r2)
<bernardofpc> can't you just do Not X -> not (is_e_l X) ?
<pippijn> the recursive call only has one of the two r1 or r2
<MarcWeber> pippijn: Why is the first choice always indented by tab?
<pippijn> bernardofpc: no, because that is wrong
<bernardofpc> ok
<pippijn> MarcWeber: ah.. because I started coq today, and I haven't set up my editor well, yet
<MarcWeber> pippijn: You could use a gist ..
<bernardofpc> Oh, I see
<pippijn> bernardofpc: what do you see?
<bernardofpc> "that is wrong"
<pippijn> yeah
<pippijn> https://paste.xinu.at/pf1/ <- this is the ocaml implementation
<MarcWeber> pippijn: regex = regular expression? What is Phi and Epsilon?
<pippijn> Phi is the empty language, Epsilon the empty word
<pippijn> they are not created by user input
<pippijn> but they come from derivatives
<bernardofpc> Phi is something like an impossible match ?
<pippijn> d/da (Letter a) = Epsilon
<pippijn> d/da (Letter b) = Phi
<pippijn> d/da (Epsilon) = Phi
<bernardofpc> oh
<bernardofpc> what's a derivative in this sense ?
<pippijn> the regular expression that matches at a state
<MarcWeber> pippijn: So you want to proof something about regular expression matching?
<pippijn> MarcWeber: potentially
<bernardofpc> given a transition da ?
<pippijn> yes
<pippijn> transition on a
<MarcWeber> You have a working ocaml implementation and want to reimplement that using coq - proofing some properties?
<pippijn> MarcWeber: yes
<MarcWeber> The ocaml implementation is missing Types again.
<pippijn> why do you want to compile the ocaml code?
<MarcWeber> not really.
<MarcWeber> I want to practise reading ocaml :)
<pippijn> the first thing I wanted to do is implement some of the basic support functions in coq
<pippijn> eventually, I would like to prove that a "simplify regex" function is correct
<bernardofpc> pippijn: why Not (Star _) is not the empty language ?
<pippijn> in that L(r) = L(simplify r)
<pippijn> bernardofpc: ~(a*) matches something that is not a*
<pippijn> for example "hello"
<pippijn> hello is not a*
<bernardofpc> well, yeah, but ~(.*) matches nothing, right ?
<bernardofpc> . = Choice a (Choice b ( ...))
<pippijn> hmm
<bernardofpc> (finite alphabet)
<pippijn> that is true
<pippijn> but
<pippijn> is_empty_language is an approximation
<pippijn> it's only used to throw away dead states
<bernardofpc> I see
<bernardofpc> perhaps then this should be Prop and not bool
<pippijn> oh
<bernardofpc> where you construct a proof that something is an empty language by accumulating your arguments to it ;-)
<bernardofpc> (so you don't care about the false, only the true ones)
<pippijn> ok, I don't know about that, yet
<pippijn> I don't know anything :)
<pippijn> I need a book..
<bernardofpc> well, your multi-| match surprised me
<pippijn> it's 4:25am, and I just felt like playing with it
<pippijn> why?
<pippijn> ocaml has that
<bernardofpc> I didn't know ;-)
<pippijn> ok
* bernardofpc only knows a bit of C, and trying to learn OCaml here :D
<pippijn> :)
<pippijn> good
<pippijn> nullable should be bool, though
<pippijn> I guess??
<pippijn> -?
<bernardofpc> as for a book, I heartly recommend Pierce's SF
<bernardofpc> I learnt all Coq I know from it
<pippijn> because.. nullable is total and exact?
<pippijn> whether a regex is nullable is well-defined
<bernardofpc> I don't really know that much about regexps
<pippijn> it's used to decide how to handle a pair of regex
weie has joined #ocaml
<pippijn> r1 r2
<pippijn> if r1 is nullable, then either r1 or r2 can consume the input
<pippijn> if r1 is not nullable, only r1 can consume it
<bernardofpc> but an idea I got from http://www.cis.upenn.edu/~bcpierce/sf/toc.html is that most things you should do in Prop
<bernardofpc> and if you can, do also in bool-way
<pippijn> what do you mean, also?
<pippijn> ok then, now both are Prop
<bernardofpc> for instance, you construct Prop's for all the things you'd like to prove
<bernardofpc> kind of establishing the language
<pippijn> can I use Props in code?
<bernardofpc> Not sure how this translates back into OCaml that might become a program
<pippijn> like, "match nullable foo with True => blah | False => bloh end"?
<bernardofpc> oh, no, I don't think so
<bernardofpc> a Prop has no "value" like False
<bernardofpc> (again, as far as I understand)
<pippijn> ok
<bernardofpc> you can only destruct it using the constructs you gave
<pippijn> then I need one that returns bool
sclv__ has joined #ocaml
sclv has quit [Ping timeout: 268 seconds]
sclv__ is now known as sclv
oriba has quit [Quit: oriba]
lusory has joined #ocaml
<MarcWeber> pippijn: I know de morgan from boolean laws.
<MarcWeber> Thinking about whether this applies to regular expressions is over my head right now
breakds has joined #ocaml
<pippijn> MarcWeber: it does
<pippijn> MarcWeber: these are boolean operators on languages (and regular expressions)
pootler__ has joined #ocaml
pootler_ has joined #ocaml
<pippijn> and DFAs
Neros has quit [Read error: Operation timed out]
Neros has joined #ocaml
<MarcWeber> pippijn: Somhow I still have trouble with the wording you use.
<MarcWeber> for me a regex is a pattern matching some input
<MarcWeber> Let me get a paper..
<pippijn> MarcWeber: and it is
dsheets has quit [Read error: Operation timed out]
watermind has joined #ocaml
<pippijn> MarcWeber, bernardofpc: do you know how to use Coq.Lists.ListSet?
<pippijn> I'm trying to do set_map
<pippijn> it needs a compare function
<pippijn> (I think)
Watcher7 is now known as Watcher7|off
<pippijn> Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y}) (f : A -> B) (x : set A) : set B
<pippijn> equality/inequality
ygrek has joined #ocaml
<bernardofpc> pippijn: i guess that Aeq_dec stands for "equality decidable")
<bernardofpc> not sure what the {} + {} notation means)
<pippijn> I think I know
<MarcWeber> http://adam.chlipala.net/cpdt/ Maybe this could be of interest ..
<bernardofpc> oh, sumbool
<bernardofpc> never seen, ok
yacks has quit [Quit: Leaving]
jcao219 has quit [Ping timeout: 248 seconds]
<pippijn> bernardofpc: do you know how "decide equality" works?
<pippijn> https://paste.xinu.at/Xkf/coq <- this works
watermind has quit [Quit: Konversation terminated!]
<pippijn> but I don't know how to make it work if Moo is ascii -> moo
<pippijn> ok, I got it
breakds has quit [Read error: Connection reset by peer]
<amiller_> i think i'm not sure how to use Gc.allocated_bytes correctly
<amiller_> does it show the largest allocation ever attained
<amiller_> since the process began
<amiller_> or does it keep counting *reallocations* of the same amount of space
gnuvince has quit [Ping timeout: 255 seconds]
justdit has joined #ocaml
Watcher7|off is now known as Watcher7
ggole has joined #ocaml
<gasche> ggole: did you have a look at the GADT-without-polymorphic-variants snippet?
ttamttam has joined #ocaml
ttamttam has left #ocaml []
Watcher7 is now known as Watcher7|off
<ggole> Yes
<ggole> I should have thanked you for putting that up: made interesting reading
ygrek has quit [Ping timeout: 246 seconds]
<ggole> I think polymorphic variants are the way to go in the end
<ggole> But it was an interesting experiment
<xenocons> is there an ocaml bot for irc?
<xenocons> (like haskell has lambdabot)
q66 has joined #ocaml
lenstr has quit [Read error: Connection reset by peer]
csakatok_ has joined #ocaml
csakatoku has quit [Ping timeout: 256 seconds]
ulfdoz has joined #ocaml
ggole has quit []
ygrek has joined #ocaml
justdit has quit [Ping timeout: 264 seconds]
justdit has joined #ocaml
introom has quit [Remote host closed the connection]
<orbitz> xenocons: i have a partially completed framework of an IRC bot in Ocaml
<xenocons> orbitz: how are you handling the evaluation of code? lexing the user input from IRC then compiling with ocaml, or cheating and redirecting std\in\out to ocamls repl
ulfdoz has quit [Ping timeout: 246 seconds]
zpe has joined #ocaml
Snark has joined #ocaml
chrisdotcode has quit [Ping timeout: 256 seconds]
<orbitz> xenocons: you misunderstand, i have a farmework for an IRC Bot
<orbitz> I never said it evaluates code:)
<orbitz> adding it woudl be easy, the hardest part is figuring out how to restrict the pgrograms
<xenocons> oh right
<xenocons> orbitz: yeah
<orbitz> at one point there was such a bot in here, I don't know what happened to it
<xenocons> ah
ygrek has quit [Ping timeout: 240 seconds]
<orbitz> i spent a little while trying to get a library to work that shuts off various syscalls but didn't have any luck with it
<xenocons> tricky problem
<orbitz> seccomp2 is supposed to solve it
ggole has joined #ocaml
gnuvince has joined #ocaml
ollehar has joined #ocaml
<xenocons> easiest is probably a vm that dies each evaluation
<xenocons> connected over serial or something
<orbitz> I think seccomp2 is easier (if it works)
<xenocons> i think thats how the guy in #rust on irc.mozilla.net does it
<xenocons> ah is seccomp2 available?
<orbitz> I have a library that implements it, i'm just not sure the kernel i am running supports it
<xenocons> ah
<orbitz> I'll play with it in the next few weeks hoepfully
<xenocons> nice
ollehar has quit [Ping timeout: 240 seconds]
yacks has joined #ocaml
ollehar has joined #ocaml
ollehar has quit [Ping timeout: 248 seconds]
djcoin has joined #ocaml
raichoo has joined #ocaml
hkBst has joined #ocaml
skchrko has quit [Quit: Leaving]
mika1 has joined #ocaml
UncleVasya has joined #ocaml
justdit has quit [Ping timeout: 256 seconds]
justdit has joined #ocaml
<xenocons> orbitz: i wonder if someone has written a paper\blog about dynamic compilation as a service and the security implications
<flux> but how about dynamic compliation + proof-carrying code, should be secure, right?
<flux> or maybe not. it could mislead the user into doing something he doesn't believe he is doing..
<xenocons> heh, could be a problem
chrisdotcode has joined #ocaml
<xenocons> its i guess about balance between offering nice features without crippling the user, but also not letting them break the world
<xenocons> i can think of a few approaches, outside of the language
<xenocons> but DSL might be best approach
<xenocons> or at least the nicest sounding
ggole has quit [Read error: Connection reset by peer]
<gasche> have a look at xavierbot
<gasche> it's in perl, but implements reasonable security for code execution
<xenocons> hmm, ok will do
skchrko has joined #ocaml
ontologiae_ has joined #ocaml
troydm has quit [Ping timeout: 248 seconds]
<xenocons> nice its not too man loc
thomasga has joined #ocaml
derek_c has joined #ocaml
introom has joined #ocaml
talzeus has quit [Remote host closed the connection]
ggole has joined #ocaml
introom has quit [Remote host closed the connection]
<gasche> amiller_: are you trying to figure out the peak memory consumption of your OCaml program?
<gasche> for that I simply use "/usr/bin/time -v"
<companion_cube> hey, the idea of making !r a lvalue is neat
<companion_cube> :]
<companion_cube> howdy gasche!
<gasche> amiller_: then http://ygrek.org.ua/p/code/pmpa to know where the bulk of the allocation comes from
talzeus has joined #ocaml
<gasche> companion_cube: meh
<gasche> I think it would make sense, but I like the fact that (!) and (:=) can be defined as functions on top of the primitive mutable record fields
<gasche> that's how I teach references to my students, and they get it easily
<gasche> I show them the declaration "type 'a myref = { mutable contents : 'a }", and ask them to implement (my_get : 'a myref -> 'a) and (my_set : 'a myref -> 'a -> unit)
<companion_cube> gasche: sure, it would be even better to have a general notion of reference values
<gasche> you mean having ('a ref) as a primitive?
<gasche> that's hard without either boxing or delicate type system and runtime considerations
<companion_cube> hmmm, being able to return a reference to some values, yeah
<gasche> well the question is: would the reference point to a valid block header that is just before the referenced value?
<gasche> if yes, that requires boxing (which could get ridden of locally, as in fact it already is done)
<companion_cube> I see, you fear that the reference would be alive but not the reference it points to
<gasche> hm no
<gasche> but hm
<gasche> say you have a record of three fields, the last one being mutable
<gasche> and you want to somehow return that field as a ('a ref) without changing to a boxed representation
<gasche> then if you store this ('a ref) somewhere, what will the GC do when traversing it?
<companion_cube> yeah, exactly
<companion_cube> or you have to save a pair ('a ref, offset-in-block)
chrisdotcode has quit [Ping timeout: 256 seconds]
<gasche> hm add a different kind of blocks that is used to point to memory internal to a valid block, with additional metadata for the GC
<gasche> (so you box the adress, not the pointed-to value)
justdit has quit [Ping timeout: 268 seconds]
<companion_cube> that probably makes references less useful
troydm has joined #ocaml
<gasche> in any case, you see there are hard runtime problems underlying "first-class primitive references"
<companion_cube> sure
<gasche> which is why we don't have them
<companion_cube> I just said it would be nice :)
justdit has joined #ocaml
derek_c has quit [Quit: Lost terminal]
<gasche> I think Daniel's remark that improving error messages should be a priority is full of good sense
<gasche> the other think I deduce from Arthur's suggestion being "we really want implicits or type-classes", which is not news
iZsh has quit [Excess Flood]
iZsh has joined #ocaml
ygrek has joined #ocaml
<adrien> which one is easier, hmmmm
<adrien> hmmmm
<adrien> I really don't know :D
<gasche> adrien: which one of which choices?
<gasche> because I don't think it makes sense to compare "improve error messages" and "add implicits or type-classes"; it's not the same person that would do the work in any case, and they can be done in parallel
<adrien> my TODO list has an entry telling me to reread such things because many of them can be improved
<adrien> well, parallel, yes, up to the number of available workers ;-)
<gasche> I think few people would spontaneously decide to implement implicits or type-classes for OCaml
<companion_cube> lolilol
<gasche> Grégoire Henry is one canonical choice right now, but even he is busy with other things
<gasche> on the contrary, improving error messages seems like a more reasonable contribution target
<gasche> and can be partly distributed once the basic blocks are in place
talzeus has quit [Remote host closed the connection]
* adrien wants gettext support ='(
<gasche> I believe there is a patchset floating around for spanish-language error messages
<gasche> I don't personally care much for those
<gasche> but it's very much orthogonal to giving more information in error messages
<adrien> I want to be able to have "beginner", "intermediate", "expert" error messages
<gasche> when does it make sense?
<adrien> for beginners :P
<gasche> do you have a concrete example?
<adrien> redefinition of a type named "t" in the toplevel
<gasche> (in my experience, beginners are already much too good at ignoring the part of the messages that they don't (want to try to) understand)
<adrien> well, then make it better suited at beginners
<gasche> adrien: what's the problem with hinting at a possible cause for all levels?
<adrien> I really need to move my ass to work
talzeus has joined #ocaml
<adrien> gasche: I don't want my screen to be flooded with many lines
<adrien> I'd do C++ if I did /o\
<def-lkb_> adrien: making the error messages less confusing is worthwile for all users, not only beginners
* adrien -> []
introom has joined #ocaml
ttamttam has joined #ocaml
<adrien> def-lkb_: there's "less confusing", and there's "giving hints"
<gasche> I think trying to hide hints for pros is premature optimization
malo has joined #ocaml
<adrien> I agree some of the messages can be improved for everyone but I doubt it will always fit everyone
<adrien> gasche: hmmm, not really hide hints for pros
<adrien> but ocaml is used for teaching
<gasche> I think you can be both clear and concise, even for beginners
<adrien> and that means that sometimes (very) detailled error messages can be good
<gasche> (in a way that wouldn't repel non-beginners)
<def-lkb_> and modifying messages based on level and language would make search engine much less useful to find similar problems :P
<adrien> heh
<adrien> well, -> work
<gasche> we could organize a Sprint for improvement of OCaml error messages?
<ggole> <gasche> hm add a different kind of blocks that is used to point to memory internal to a valid block
<adrien> I have another sprint coming first (x-compilation)
<ggole> There have been gcs which have this
<adrien> but, yeah
<gasche> but for this one you're alone adrien :-'
<ggole> It's additional complexity, but it allows some nice efficient things
<gasche> ggole: did you have a look at the GADT-without-polymorphic-variants example?
<ggole> Yes :)
<ggole> I answered that before
<gasche> I'm sorry, it must have been too far in my logs
<ggole> Thanks for that btw
<ggole> (I think that was during whitequark's ruby rant, and it didn't get the attention it deserved)
<ggole> My conclusion was that the technique was interesting, but polymorphic variants are probably the way to go
<gasche> I was considering writing a blog post about it
<ggole> I've also come to agree with your suggestion that polymorphic variants as GADT arguments is not a good idea
<gasche> but I still don't see why polymorphic variants would be better or how they would actually work for this problem
<gasche> ah
<gasche> you mean polymorphic variants to classify values, rather than as phantom types
<ggole> The alternative is just plain polymorphic variants
<ggole> Yes
<gasche> that sounds saner, indeed
<ggole> As phantom types they just don't work out
<gasche> well
<ggole> I had high hopes for GADTs
<gasche> we believed they did when we have "do it yourself" phantom types before GADTs
<gasche> I only understood the variance problem after GADTs were introduced
<gasche> s/we have/we had/
<ggole> I still don't understand the problem exactly
<gasche> if you have
<ggole> Not that soundness problems tend to be particularly clear
<gasche> type _ t = A : [ `A ] t | AB : [ `A | `B ] t
<gasche> it is unsound to claim that ('a t) is covariant
<gasche> and therefore that you can silently cast a [ `A ] t into a [ `A | `B ] t
<gasche> as you are tempted to do when you use polymorphic variants as phantom types to mention "possible cases"
<ggole> The part which confused me is that explicit variance annotations were being discarded
<gasche> it may be possible to do related things using row polymorphism instead of subtyping
<gasche> ggole: do you have an example of silently discared annotations? that's probably a bug
<ggole> I would annotate something [< 'A | 'B] and it would be generalised as ['A | 'B]
<gasche> ah
<gasche> that's not a variance annotation
<ggole> Discarded isn't the right word
<ggole> Uh
<ggole> Whatever the terminology is there
ontologiae_ has quit [Quit: WeeChat 0.4.0]
ontologiae has joined #ocaml
<ggole> I doubt it is a bug: it was certainly surprising, though
<gasche> "variance" refers to subtyping
<gasche> [< and [> are not related to subtyping
<gasche> in fact there is no terminology to denote them in the OCaml manual, besides calling [> "open variants" and [< "closed variants"
<gasche> so I guess you could say "openness annotations"
<ggole> Hmm
<gasche> (no sure that's a very good terminology because I would be tempted to call the simple "[" case, which is "exact variant" in the manual, "closed", as it is not instantiable anymore)
ollehar has joined #ocaml
<gasche> but to come back to your remark, yes, typing of polymorphic variants is an advanced topic
<gasche> I actually think that GADTs are probably easier to understand and use (were it not for their terrible error messages)
<ggole> Yes, I've often been surprised
<ggole> The type variable you sometimes need to add can be particularly odd
<ggole> (I think I understand it now)
justdit has quit [Read error: Connection reset by peer]
<ggole> I used to think that allowing subsets of regular variants would be a nice language extension
<ggole> The complexities of GADTs and polymorphic variants have me thinking that might not be a good idea
<ggole> It is often the case that you want to be able to say "this case should not happen", but the complexity of doing it statically is unfortunate
ollehar has quit [Ping timeout: 256 seconds]
sclv__ has joined #ocaml
sclv has quit [Ping timeout: 276 seconds]
sclv__ is now known as sclv
mcclurmc has quit [Ping timeout: 240 seconds]
kakadu has joined #ocaml
ollehar has joined #ocaml
ggole_ has joined #ocaml
ggole has quit [Ping timeout: 240 seconds]
gnuvince has quit [Ping timeout: 268 seconds]
ollehar1 has joined #ocaml
mcclurmc has joined #ocaml
ollehar has quit [Ping timeout: 246 seconds]
ollehar1 has quit [Ping timeout: 255 seconds]
gautamc has quit [Read error: Connection reset by peer]
thelema_ has quit [Ping timeout: 246 seconds]
thelema has joined #ocaml
Drup has joined #ocaml
gautamc has joined #ocaml
dsheets has joined #ocaml
ollehar has joined #ocaml
yacks has quit [Ping timeout: 268 seconds]
yacks has joined #ocaml
Drup has quit [Ping timeout: 248 seconds]
Drup has joined #ocaml
csakatoku has joined #ocaml
csakatok_ has quit [Ping timeout: 246 seconds]
talzeus has quit [Remote host closed the connection]
csakatoku has quit [Remote host closed the connection]
malo has quit [Remote host closed the connection]
_andre has joined #ocaml
<adrien_oww> :-)
<adrien_oww> we're talking a lot about issues with ocaml on windows but we don't usually mention how much everything has improved in the last few years =)
ollehar has quit [Ping timeout: 255 seconds]
_andre has quit [Quit: Lost terminal]
_andre has joined #ocaml
so has quit [Ping timeout: 268 seconds]
so has joined #ocaml
so has quit [Ping timeout: 268 seconds]
so has joined #ocaml
gnuvince has joined #ocaml
yacks has quit [Quit: Leaving]
breakds has joined #ocaml
<ggherdov> Hi all. Disclaimer: not affiliated. I have just seen that o'reilly is offering 50% cut on Yaron Minsky book "Real World Ocaml" "early release" , http://shop.oreilly.com/product/0636920024743.do?code=WKERRLS . But the author, in the beta release at https://realworldocaml.org/ , says "It has all the chapters except for first-class modules, packaging/build and
<ggherdov> Async/RPC". Question: does o'reilly early release include those chapters? I tweeted him but no reply so far https://twitter.com/_GGhh_/status/349486784595492868
<Tobu> ggherdov: early release gets you every update, from the current state (probably close to the beta) to the completed book
ollehar has joined #ocaml
<ggherdov> Tobu: ah good! i didn't know that. thanks a lot
sclv has quit [Ping timeout: 246 seconds]
yacks has joined #ocaml
ygrek has quit [Ping timeout: 268 seconds]
sclv has joined #ocaml
ollehar has quit [Ping timeout: 256 seconds]
pootler__ has quit [Ping timeout: 256 seconds]
pootler_ has quit [Ping timeout: 256 seconds]
UncleVasya has quit [Ping timeout: 246 seconds]
adrien_o1w has joined #ocaml
zopt has joined #ocaml
noplamodo_ has joined #ocaml
snarkyboojum has joined #ocaml
hnrgrgr_ has joined #ocaml
darkf has quit [Quit: Leaving]
travisbrady has joined #ocaml
tizoc` has joined #ocaml
tchell has quit [*.net *.split]
adrien_oww has quit [*.net *.split]
hnrgrgr has quit [*.net *.split]
cokesme has quit [*.net *.split]
tizoc has quit [*.net *.split]
noplamodo has quit [*.net *.split]
smango has quit [*.net *.split]
snarkyboojum_ has quit [*.net *.split]
tizoc` is now known as tizoc
tizoc has quit [Changing host]
tizoc has joined #ocaml
tchell has joined #ocaml
smango has joined #ocaml
noplamodo_ is now known as noplamodo
noplamodo has quit [Changing host]
noplamodo has joined #ocaml
ygrek has joined #ocaml
tchell has quit [*.net *.split]
smango has quit [*.net *.split]
drwhom has joined #ocaml
tchell has joined #ocaml
smango has joined #ocaml
mehdid_ has joined #ocaml
asmanur_ has joined #ocaml
|jbrown| has joined #ocaml
breakds has quit [Quit: Konversation terminated!]
djcoin has quit [*.net *.split]
cdidd has quit [*.net *.split]
mehdid has quit [*.net *.split]
jbrown has quit [*.net *.split]
asmanur has quit [*.net *.split]
hkBst has quit [Quit: Konversation terminated!]
thomasga1 has joined #ocaml
thomasga has quit [Ping timeout: 264 seconds]
fasta has quit [Read error: Connection reset by peer]
ohama has quit [Ping timeout: 264 seconds]
ohama has joined #ocaml
othiym23 has quit [Ping timeout: 244 seconds]
othiym23 has joined #ocaml
cdidd has joined #ocaml
djcoin has joined #ocaml
raichoo has quit [Quit: leaving]
adrien_o1w is now known as adrien_oww
mort___ has joined #ocaml
mort___ has left #ocaml []
pootler_ has joined #ocaml
pootler__ has joined #ocaml
travisbrady has quit [Quit: travisbrady]
travisbrady has joined #ocaml
pootler_1 has joined #ocaml
pootler_2 has joined #ocaml
pootler__ has quit [Ping timeout: 245 seconds]
pootler_ has quit [Ping timeout: 245 seconds]
chrisdotcode has joined #ocaml
jcao219 has joined #ocaml
kakadu has quit [Quit: Konversation terminated!]
quelu_ has joined #ocaml
jcao219 has quit [Read error: Connection reset by peer]
wagle_ has joined #ocaml
olasd_ has joined #ocaml
f6g5gw has joined #ocaml
mika1 has quit [Quit: Leaving.]
Drup has quit [Read error: Connection reset by peer]
fds_ has joined #ocaml
Drup has joined #ocaml
f6g5gw has quit [Client Quit]
jcao219 has joined #ocaml
jave has joined #ocaml
whitequark has quit [*.net *.split]
Tobu has quit [*.net *.split]
alang has quit [*.net *.split]
olasd has quit [*.net *.split]
vpm has quit [*.net *.split]
zorun has quit [*.net *.split]
wagle has quit [*.net *.split]
quelu has quit [*.net *.split]
jave_ has quit [*.net *.split]
fds has quit [*.net *.split]
nicoo has quit [Ping timeout: 248 seconds]
olasd_ is now known as olasd
thomasga1 has quit [Ping timeout: 248 seconds]
ygrek has quit [Ping timeout: 246 seconds]
bobry has quit [Ping timeout: 251 seconds]
rixed has quit [Quit: zzzzzz]
Neros has quit [Ping timeout: 240 seconds]
Neros has joined #ocaml
whitequark has joined #ocaml
Tobu has joined #ocaml
alang has joined #ocaml
zorun has joined #ocaml
vpm has joined #ocaml
rgrinberg1 has joined #ocaml
fasta_ has joined #ocaml
ttamttam has quit [Ping timeout: 276 seconds]
sgnb` has joined #ocaml
drwhom_ has joined #ocaml
q66_ has joined #ocaml
rwmjones_ has joined #ocaml
Jenza2 has joined #ocaml
foo303_ has joined #ocaml
chrisdotcode has quit [Read error: Operation timed out]
montik has joined #ocaml
rgrinberg has quit [Ping timeout: 264 seconds]
rwmjones has quit [Ping timeout: 264 seconds]
drwhom has quit [Ping timeout: 264 seconds]
q66 has quit [Ping timeout: 264 seconds]
SuperNoeMan has quit [Ping timeout: 264 seconds]
Leonidas has quit [Ping timeout: 264 seconds]
foo303 has quit [Ping timeout: 264 seconds]
Jenza has quit [Ping timeout: 264 seconds]
The_third_man has quit [Ping timeout: 264 seconds]
sgnb has quit [Ping timeout: 264 seconds]
Jenza2 is now known as Jenza
SuperNoeMan has joined #ocaml
Leonidas has joined #ocaml
ontologiae has quit [Ping timeout: 256 seconds]
The_third_man has joined #ocaml
mehdid_ is now known as mehdid
introom has quit [Remote host closed the connection]
nicoo has joined #ocaml
pootler_2 has quit [Ping timeout: 260 seconds]
<amiller_> okay so
pootler_1 has quit [Ping timeout: 252 seconds]
<amiller_> i want to read a Marshal'd object from a channel
<amiller_> however i also want to take a hash of the serialized string of the object!
<amiller_> right now i basically unmarshal then remarshal the thing i just unmarshaled
<amiller_> that sucks obviously
<amiller_> but what else might i do
<amiller_> one thing i tried is doing marshal to string
<amiller_> and then marshalling the string
<amiller_> but that leads to a lot of bloat/overhead because of the doubly-encoded data on the wire
<amiller_> i think the right approach would be to do marshal.to_string and then basically write the string directly to a file
<amiller_> er well this is only for reading i care about so
<amiller_> basically i know that the way marshal.from_channel works is that it first reads a fixed-size header containing the size of the data and then it reads the indicated number of bytes
<amiller_> so i could just replicate this manually
<amiller_> to avoid duplicating work what i'd really prefer is just if there was an option to Marshal.from_channel that gave me access to the whole string it read but i don't think there is one
<amiller_> is there anything canonical for this i'm overlooking?
pootler__ has joined #ocaml
pootler_ has joined #ocaml
<transfinite> amiller_: marshal to string and then just output the string on the channel, don't re-marshal it
<amiller_> but what about reading
<transfinite> if you have no other data on the channel you can just read until EOF. otherwise, send a (marshaled) length first
<ggole_> Can't you get the extent of the thing with Marshal.header_size/.total_size, slurp + hash that many bytes, then seek back to the position and unmarshal?
<transfinite> seeking won't work if the channel is a pipe or network connection
<ggole_> Yeah, true
introom has joined #ocaml
ttamttam has joined #ocaml
osnr has joined #ocaml
osnr has quit [Changing host]
osnr has joined #ocaml
osa1 has joined #ocaml
ollehar has joined #ocaml
introom has quit [Ping timeout: 252 seconds]
ollehar has quit [Ping timeout: 252 seconds]
drwhom_ is now known as drwhom
drwhom has left #ocaml []
ttamttam has left #ocaml []
weie_ has joined #ocaml
gautamc1 has joined #ocaml
mcclurmc has quit [Ping timeout: 256 seconds]
MarcWebe1 has joined #ocaml
ohama has quit [Disconnected by services]
Snark_ has joined #ocaml
Neros_ has joined #ocaml
lusory_ has joined #ocaml
ohama has joined #ocaml
<flux> pretty cool and nice copy-paste installation instructions: http://www.algo-prog.info/spoc/web/index.php - if you're into GPGPU that is
Neros has quit [*.net *.split]
cdidd has quit [*.net *.split]
gautamc has quit [*.net *.split]
skchrko has quit [*.net *.split]
Snark has quit [*.net *.split]
lusory has quit [*.net *.split]
weie has quit [*.net *.split]
bkpt has quit [*.net *.split]
MarcWeber has quit [*.net *.split]
djcoin has quit [Quit: WeeChat 0.4.0]
skchrko has joined #ocaml
bkpt has joined #ocaml
raichoo has joined #ocaml
cdidd has joined #ocaml
pootler__ has quit [Remote host closed the connection]
pootler_ has quit [Remote host closed the connection]
ollehar has joined #ocaml
travisbrady has quit [Quit: travisbrady]
Snark_ is now known as Snark
bobry has joined #ocaml
Kakadu has joined #ocaml
pootler_ has joined #ocaml
pootler__ has joined #ocaml
pootler_1 has joined #ocaml
travisbrady has joined #ocaml
Drup has quit [Ping timeout: 245 seconds]
tane has joined #ocaml
ygrek has joined #ocaml
skchrko has quit [Quit: Leaving]
thomasga has joined #ocaml
UncleVasya has joined #ocaml
ollehar has quit [Ping timeout: 276 seconds]
ggole_ has quit []
kuahsds has joined #ocaml
Drup has joined #ocaml
derek_c has joined #ocaml
kuahsds has quit [Quit: Page closed]
wagle_ is now known as wagle
Watcher7|off is now known as Watcher7
skchrko has joined #ocaml
derek_c has quit [Quit: Lost terminal]
<hcarty> gasche: You keep mentioning sprints - maybe something should be organized around the OUD meeting in September?
<hcarty> gasche: Physical presence may help keep things focused. Or prevent focus... it should be fun either way.
skchrko has quit [Quit: Leaving]
ollehar has joined #ocaml
Ptival has joined #ocaml
Ptival has quit [Client Quit]
ygrek has quit [Ping timeout: 264 seconds]
Neros_ has quit [Ping timeout: 252 seconds]
_andre has quit [Quit: leaving]
stevej has joined #ocaml
<adrien_oww> (physical, hmmmm ='( )
Neros has joined #ocaml
ttamttam has joined #ocaml
ttamttam has quit [Quit: ttamttam]
<pippijn> wmeyer: you there?
<pippijn> bernardofpc: I solved the is_empty_language thing
<pippijn> bernardofpc: https://paste.xinu.at/nWZEPG/
dsheets has quit [Ping timeout: 256 seconds]
<wmeyer> pippijn: yes
<Drup> is there a good method to find back the actual function from gprof's output ?
<pippijn> wmeyer: never mind, I killed pattern repeat
<pippijn> my problem was
<pippijn> | Repeat e (S n) => Repeat e n
<pippijn> in all other cases, it's e that decreases
<pippijn> but in the Repeat case, n has to decrease and finally, when n is 1, e is gone
stevej has quit [Quit: ["Textual IRC Client: www.textualapp.com"]]
<wmeyer> no, you shoul say in opposite
<wmeyer> | Repeat e n => Repeat e (S n)
<pippijn> why?
<wmeyer> because then reduction will lead to decreasing term
<pippijn> then it increases
<pippijn> it's about pattern^n
<pippijn> for example a^3
<wmeyer> ah sorry
<pippijn> matching aaa
<wmeyer> yep
<wmeyer> my brain is not working
<pippijn> ok
<wmeyer> so it's pattern match, not a type definition of (course different arrow)
<wmeyer> and no constructor syntax
<wmeyer> so it looks good
<wmeyer> but I don't understand what you want to do
<pippijn> ok
breakds has joined #ocaml
<wmeyer> pippijn: in general this code should look the same as in OCaml
* wmeyer getting worse in explanations these days.
<pippijn> that is of course not possible in coq
<wmeyer> beautiful, you writing your regexp engine in Coq?
<pippijn> wmeyer: just for fun
<pippijn> might not finish
<pippijn> so
<pippijn> that ocaml code is impossible in coq
<pippijn> but how can I implement repeat in coq
<wmeyer> http://adam.chlipala.net/cpdt/html/MoreDep.html <- search for regexp matcher
<wmeyer> probably you hit the not well founded recursion problem
<wmeyer> aka structural termination check
<pippijn> I know
introom has joined #ocaml
<wmeyer> | Repeat (e, 1) → derive l e
<wmeyer> looks wrong to me
<pippijn> that's totally right
<pippijn> and valid in coq, too
<wmeyer> you having infinite loop here (if I see that correctly)
<pippijn> no
<pippijn> you see it incorrectly
<pippijn> the unprovable termination is in the second case
<whitequark> I can't understand how let rec list = 1 :: list;; can ever work
<wmeyer> ah see
<whitequark> either I'm dumb or this is a special form matched by the compiler
<wmeyer> pippijn: you have two structuraly decreasing arguments
<pippijn> yes
<pippijn> only in Repeat
<pippijn> in the rest, I have one
<wmeyer> hmm
<wmeyer> but usually it causes troubles
<Drup> whitequark: what's the problem with that ? you're going to have trouble to traverse it, but that's all
<pippijn> no shit :)
<wmeyer> pippijn: Coq *is* a sophisticated tool. And still haven't learned wf stuff
<wmeyer> :)
<whitequark> Drup: well. I know that letrec can be implemented with mutable bindings if your language has that, but OCaml doesn't
<whitequark> Drup: or you can whip out an y combinator
<whitequark> but that won't work for data structures
introom has quit [Ping timeout: 252 seconds]
Neros has quit [Ping timeout: 256 seconds]
<Drup> afaik, let rec on static structures is implemented exactly like that
<whitequark> plus, in this case even mutable bindings won't help, because you need to construct a cell referring to itself. you can't put it in an environment unless you already constructed it
<whitequark> and you can't construct it unless you can refer to it
<whitequark> and it's immutable.
<whitequark> Drup: well, y combinator works because it constructs two structurally identical functions which call each other
<Drup> the implementation mutate a pointer to loop
<whitequark> but here, it's just a single cell
<whitequark> Drup: I understand that it can mutate a pointer if you need two mutually recursive functions
<whitequark> but not how that will help with a data structure
<whitequark> or why would anyone want to construct it anyway :)
<Drup> it's indeed quite useless like this
<wmeyer> pippijn: did that help?
<Drup> whitequark: but you can actually do some stuff with it, on very corner cases
<whitequark> Drup: I'm really interesting which
<whitequark> it seemingly violates an invariant built in to the language?
<whitequark> because cells are supposed to be immutable, and there's no way to make a cyclic data structure if it's immutable
<whitequark> *really interested
<pippijn> wmeyer: telling me that coq is a sophisticated tool?
<pippijn> wmeyer: no
<pippijn> I knew that
<Drup> huum, I don't have any example now, you can try to search the caml list (or ask gasche, I'm sure he have an example :D)
<pippijn> and I knew about the recursion thing
<whitequark> doesn't seem like ocaml has user-accessible set-cdr
<pippijn> I still don't know how to solve it
<pippijn> whitequark: that would make list a non-persistent data structure
<whitequark> pippijn: right
<whitequark> see above about invariants and cycles
<pippijn> ah
<pippijn> well
<pippijn> :)
<pippijn> the ocaml runtime and compiler can do anything they want
<pippijn> so can you, if you cheat
<whitequark> well, you have to take care when cheating, because someone, somewhere, is relying on that invariant ;)
<pippijn> yes
def-lkb_ is now known as def-lkb
<pippijn> probably many people
Neros has joined #ocaml
<Drup> pippijn: repeat after me, "The Obj module is not part of the ocaml language" :]
<pippijn> hehe
<pippijn> it is, and I love it
<whitequark> oooh the Obj module
<whitequark> so much neatness inside
* whitequark has a look on his face like he just got a new toy
<whitequark> I can break so much things with it
<pippijn> Drup: without it, my parser generator wouldn't work
<pippijn> it could, but only if the user explicitly stated all the types, and then we're at C :\
<Drup> pippijn: I don't want to know how it works, I have seen far too much Obj when looking at Eliom's client-server communication code.
<Drup> ;)
<whitequark> pippijn: nah, not at C. at least the compiler isn't actively trying to break your code.
<pippijn> Drup: menhir and probably ocamlyacc both use Obj.magic
<pippijn> or, actually
<pippijn> I use Obj.obj and Obj.repr, they probably do the same
<whitequark> Obj.magic ?
<Drup> pippijn: I know it's useful, I just prefer not to have to see it :)
Kakadu has quit []
<pippijn> then don't look at the generated code
<pippijn> wmeyer: I could use your help
<pippijn> wmeyer: fun (a, b) => (a, b) doesn't work in coq?
<pippijn> how do tuples work?
<pippijn> oh, I see
<pippijn> let '(a, b) := tuple in
<pippijn> wmeyer: it doesn't work in fun (..)?
<pippijn> > Check ((f ∘ f) 0).
<pippijn> > ^^^^^
<pippijn> Error: Unknown interpretation for notation "_ ∘ _".
<pippijn> wmeyer: what's wrong with that?
tane has quit [Quit: Verlassend]
dsheets has joined #ocaml
Snark has quit [Quit: leaving]
wdmeyer2 has joined #ocaml
* wdmeyer2 testing irc on android
wdmeyer2 has quit [Remote host closed the connection]
<hcarty> adrien_oww: Physical presence isn't required for the actual activity, but it may help encourage people who are at the meeting to take part.
<pippijn> wmeyer: do you know how equality works?
zpe has quit [Remote host closed the connection]
<Drup> what is "caml_modify" in gprof output ?
<pippijn> Drup: mutating reference record/array fields
<pippijn> reference as in "not int/bool/char"
<Drup> ok
<Drup> pippijn: and I suppose that caml_compare is the polymorphic comparaison function ?
<pippijn> yes
mcclurmc has joined #ocaml
osa1 has quit [Quit: Konversation terminated!]
<pippijn> wmeyer: transition_eq doesn't work
<pippijn> wmeyer: Error: congruence failed.
<whitequark> why is it not possible to reimplement functions like polymorphic comparison in plain ocaml?
<whitequark> does the type inferencer have a problem with that?
<pippijn> whitequark: it's not?
<pippijn> I think it is possible
<whitequark> pippijn: realworldocaml says it isn't
<pippijn> show me
<pippijn> if they don't say why, then I don't believe it
<pippijn> if they say "Obj is not part of plain ocaml" then yes
<whitequark> oh, that explains it
ollehar has quit [Remote host closed the connection]
<whitequark> well, why can't you do it without obj?
<pippijn> because you can't do anything with 'a
<pippijn> you can't inspect 'a
<pippijn> it's opaque
<pippijn> like void* in C
<whitequark> oh, ocaml doesn't specialize functions
<whitequark> I get it.
<pippijn> whether it does or not doesn't matter
<whitequark> doesn't expose specialization to ocaml code.
<whitequark> is what I meant
<pippijn> I don't know what that means
<pippijn> if you mean overloading, then yeah
<pippijn> it doesn't do overloading
<pippijn> 'a is *really* like void*
<pippijn> implemented as void*, too
raichoo has quit [Quit: leaving]
<whitequark> it's not like overloading
<whitequark> but I see what you mean
<whitequark> interesting.
<pippijn> you want to dispatch functions over a type?
<pippijn> choose a different comparison function based on the type of an argument?
<pippijn> or what does specialisation do?
fds_ is now known as fds
<whitequark> yes, this is probably the closest match for it in ocaml
<Drup> I think this it what whitequark means
<Drup> this is*
<whitequark> duh, easier to explain in terms of my own compiler :) it's based on CPA, if you know what it is
<whitequark> (cartesian product algorithm)
<pippijn> I don't know
<whitequark> every time a compiler tries to translate a call to function with type 'a -> 'a, or something like that, it looks at the type of argument, then duplicates the function and substitutes 'a for the type of the argument
<whitequark> thus 'specialization'
<pippijn> Drup: and yeah, it's too bad that ocaml doesn't specialise functions for int, but it might potentially have to generate a lot of functions
<whitequark> you can then use other techniques to dispatch over the type, once it's inside
<whitequark> e.g. latent predicates
<Drup> pippijn: oh I don't have any real opinion on this, I was just trying to ease communication ;)
<pippijn> whitequark: so basically it's C++ templates
q66_ has quit [Remote host closed the connection]
<whitequark> yes, similar
ollehar has joined #ocaml
zpe has joined #ocaml
ollehar has quit [Ping timeout: 276 seconds]
breakds has quit [Quit: Konversation terminated!]
<whitequark> so, ocaml sometimes generates specialized versions of polymorphic functions
<whitequark> according to Drup's link
<whitequark> neat
<pippijn> it does?
<pippijn> can you quote the part that says so?
<pippijn> because I read that as it doesn't
zpe has quit [Ping timeout: 246 seconds]
<whitequark> >All we need to do is to hint to the OCaml compiler that the arguments are in fact integers. Then OCaml will generate a specialised version of max which only works on int arguments:
<Drup> whitequark: since you're into this sort of things, you should read this : http://www.ocamlpro.com/blog/2013/05/24/optimisations-you-shouldn-t-do.html
<pippijn> no
<pippijn> whitequark: then it will generate one for int
<pippijn> but there won't be one for 'a
<whitequark> pippijn: hm?
<pippijn> how do you hint to the compiler that the arguments are integers?
stevej has joined #ocaml
<whitequark> there's an example in the article:
<whitequark> let max (a : int) (b : int) = if a > b then a else b
<whitequark> (Ctrl+F, "Polymorphic types" and scoll one page down)
<whitequark> Drup: thanks
<whitequark> I'm not that concerned of performance of my compiler, though. (yet? :D)
gautamc1 has quit [Read error: Connection reset by peer]
<pippijn> right
<pippijn> so now max "a" "b" doesn't work anymore
<whitequark> sure
<pippijn> so it's not specialisation
<pippijn> it's just defining a function with a type
gautamc has joined #ocaml
<whitequark> yes, you're right.
<gasche> still when you write
<gasche> let max a b = if a > b then a else b
<gasche> and
<gasche> let max (a : int) b = if a > b then a else b
<gasche> the compiler does not pick the same meaning for (>)
<gasche> in the second case, the polymorphic comparison has been specialized
travisbrady has quit [Quit: travisbrady]
<gasche> regarding value recursion, it can be useful to define (mutable) doubly-linked lists for example
<gasche> or in the implementation of some prime number sieves
<gasche> or to represent some recursive closure values in a language runtime implemented in OCaml
<gasche> they have
mehdid has quit [Read error: Operation timed out]
mehdid has joined #ocaml
tchell has quit [*.net *.split]
smango has quit [*.net *.split]
hnrgrgr_ is now known as hnrgrgr
zpe has joined #ocaml
<whitequark> gasche: I think if the linked list is mutable, you don't need value recursion?
<whitequark> as in, you do not need that special form of let rec
chrisdotcode has joined #ocaml
emmanuelux has joined #ocaml
<bernardofpc> pippijn: nice, but that's quite of a hack ;-)
<bernardofpc> (mostly because it's a total function, where it is not because of Not Star _)
<bernardofpc> I'll try to writ something that makes sense in "Prop"
zpe has quit [Ping timeout: 264 seconds]
<bernardofpc> Not sure exactly how this translates into a real program, but I guess this is a recursive definition that might work
tchell has joined #ocaml
smango has joined #ocaml
zpe has joined #ocaml
breakds has joined #ocaml
emmanuelux has quit [Quit: emmanuelux]
emmanuelux has joined #ocaml
dsheets has quit [Ping timeout: 252 seconds]
zpe has quit [Ping timeout: 246 seconds]
dsheets has joined #ocaml
yacks has quit [Ping timeout: 268 seconds]
so has quit [Ping timeout: 268 seconds]
yacks has joined #ocaml
so has joined #ocaml
yacks has quit [Ping timeout: 246 seconds]
oriba has joined #ocaml
zpe has joined #ocaml
gnuvince has quit [Ping timeout: 268 seconds]
zpe has quit [Ping timeout: 240 seconds]
darkf has joined #ocaml
UncleVasya has quit [Quit: UncleVasya]
so has quit [Ping timeout: 268 seconds]