Kopophex has quit [Read error: 110 (Connection timed out)]
Kopophex_ has joined #ocaml
jlouis has quit [Remote closed the connection]
crawfordcomeaux has joined #ocaml
<crawfordcomeaux>
I'm working on an sml project that automates a game called nomic where players can change the rules as they play
sporkmonger has joined #ocaml
<crawfordcomeaux>
I'm trying to figure out how, if a rule creates an object (structure?) and gives it properties (values?), another rule or amendment to the original rule, can add or remove properties/objects to the original object
<crawfordcomeaux>
Something tells me ocaml can easily accomplish that. But I was hoping someone might be able to think of a method for doing that in sml...
<Smerdyakov>
Though your request is vague, I'm pretty sure there is no relevant difference between OCaml and SML.
<crawfordcomeaux>
ok
sporkmonger has quit []
sporkmonger has joined #ocaml
Morphous has joined #ocaml
Morphous_ has quit [Read error: 110 (Connection timed out)]
sporkmonger has quit [Read error: 110 (Connection timed out)]
redocdam has quit []
hsuh has joined #ocaml
hsuh has quit [Remote closed the connection]
sporkmonger has joined #ocaml
ccomeaux has joined #ocaml
bluestorm has quit [Read error: 113 (No route to host)]
<mfp>
did the OCaml 1.0 announcement say he'd win 12 years later? :)
<Yoric[DT]>
Nope, but the French academic world is quite gloomy these days.
<Yoric[DT]>
Reduced research freedom, reduced funding, increased teaching time, increased administration, reduced number of researchers, increased number of PhD students who can't find a job.
<Yoric[DT]>
All with public declarations of the contrary.
<mfp>
:-|
<Yoric[DT]>
Oh, and increased bashing on academics.
<mfp>
anti-intellectualism is alive & well everywhere, isn't it?
<mfp>
Haskell's ivory towers are at least twice as high as OCaml's, so it hurts the former more :P
<Yoric[DT]>
Possibly.
<Yoric[DT]>
From here, Haskell's ivory towers look nicer than OCaml's :)
<mfp>
"The barbarians are at the gates. Hordes of Java programmers are being exposed to generics and delegates (...). The time has come to retreat and climb higher into our ivory tower: we need to design a language that is so devious, so confusing, and so bizarre, it will take donkey’s years for mainstream languages to catch up. Agda, Coq, and Epigram are some approximation of what functional programming might become, but why stop there? I
<mfp>
want strict data, lazy codata, quotient types, and a wackier underlying type theory." > classy
<Yoric[DT]>
I've seen a recent talk about quotient data structures in OCaml.
<Yoric[DT]>
Well, I assume that's what they mean by "quotient" anyway.
<mfp>
ergh wrong chan (or not)
<Yoric[DT]>
Looked actually quite simple.
<mfp>
when they were talking about private abbreviations, right?
<Yoric[DT]>
It was about a simple extension for OCaml which allowed defining "axioms" on data structure, including normalization, equivalence, etc.
<Yoric[DT]>
The extension then generated pseudo-constructors and took advantage of private types to permit pattern-matching.
<Yoric[DT]>
Although I'm not sure how private types help with equivalence.
<adonis28850>
a
<Yoric[DT]>
But then, I may have missed some pre-processing on pattern-matching.
<mattam>
The objects are kept in normal form I think.
<Yoric[DT]>
Yes, but pattern-matching may not be in normal form.
zhoupp has quit []
<mattam>
?
<mattam>
You mean you may write patterns which match non-normal forms?
<Yoric[DT]>
That's what I mean.
<Yoric[DT]>
Now, I don't know if you can actually do that.
<Yoric[DT]>
But if you can write these patterns, you need some rewriting to get them to work at all.
<mattam>
I think they would simply not-match, there's little chance you can "invert" normalization..
<Yoric[DT]>
I assume so.
<Yoric[DT]>
I wasn't thinking about de-normalizing, mind you.
<Yoric[DT]>
Rather about normalizing the pattern-match.
<Yoric[DT]>
Of course, in the general case, that's not possible.
<Yoric[DT]>
But it might be possible to detect patterns which just can't match.
<mattam>
Right.
<bluestorm>
mfp: what do you think may help OCaml getting some hype ?
<bluestorm>
(i'm not sure if hype is that important, but it's right that the Haskell community seems to be efficient on things we could improve)
<jynxzero>
There's a lot of activity in the Haskell community, compared to O'Caml, I'm not sure it's hype. :)
<jynxzero>
I think the thing O'Caml needs most is a full-featured standard base, like Haskell.
<jynxzero>
At the moment, you get O'Caml and it's very sparse, you then need to go get ExtLib, core, a bunch of libraries etc
<jynxzero>
Whereas absolutely tonnes of stuff comes with GHC by default.
guillem has quit [Remote closed the connection]
<mfp>
bluestorm: as jynxzero says, the standard base (OCaml Batteries?), and then somebody like dons ;)
<mfp>
I sort of envy the agility of the hackage devel process
<mfp>
e.g., somebody blogs that CSV parsing is slower in Haskell than in Python, a missing function in ByteString is identified, and 2 days latter it's implemented & the new version released
<mfp>
or somebody realizes that the Haskell sum-file in the shootout is slow, adds a new function to a core library with just the right semantics for that benchmark and releases; GHC becomes the 2nd fastest entry for that benchmark ;)
<mfp>
then said entry is linked to countless times to prove that idiomatic Haskell is ueber fast :))
<bluestorm>
hm
<mfp>
ah and everything is done by the same person hehe
<bluestorm>
rwmjones: have you seen http://user.it.uu.se/~pergu/bitbench/ ? that might be an interesting test (for both elegance and performance) for bitstring
<bluestorm>
mfp: the former (Batteries and such) seems more of a technical issue : i agree it is the most visible (and probably efficient) improvement we can do right now, but i think it is separated from the communication thing
<mfp>
hackage plays a large role too
<bluestorm>
so you're talking about reactivity , and public exposure of the work of the community ?
<rwmjones>
bluestorm, probably more elegance than performance at the moment ...
<mfp>
an easy way for ppl to release things, see what's available (the hump is not very complete), install...
<bluestorm>
couldn't godi play that role ?
<bluestorm>
i've heard the packaging is a bit difficult, but from the end user pov. it's quite handy
<mfp>
packaging for GODI is pretty involved I hear
<mfp>
yeah
<bluestorm>
on the other hand, the META files are easy to create and efficient
<mfp>
it doesn't automate building
<mfp>
ocamlfind could be used to perform the install & manage stuff
<bluestorm>
and ocamlfind is probably not that great for version and conflicts handling
<mfp>
there's a standardized 3-step process to install any lib: runhaskell Setup.lhs configure --prefix=$HOME --user runhaskell Setup.lhs build runhaskell Setup.lhs install
<mfp>
that's not critical, I think (version & conflict handling)
<mfp>
cabal-install was released very recently; the important part is cabal (= standardizing build process + metadata)
Yoric[DT] has quit ["Ex-Chat"]
<bluestorm>
btw
<bluestorm>
i'm planning to try a camlp4 extension for the F# #light syntax
<bluestorm>
do anyone think that would be helpful ?
<mfp>
being able to push a tarball to some site and have it added automatically to the hump, see the extracted documentation & link to its dependencies would be great
<mfp>
#light looked quite good
<bluestorm>
(i was originally interested in mimicking ocaml+twt behavior, but i thought it might be interesting to keep in sync with F# users)
<mfp>
it'll be hard to gain any traction though
<bluestorm>
yeah, i guess the immediate interest would be more in the line of "Hey, we have a #light syntax too !"
munga_ has joined #ocaml
<bluestorm>
(but the camlp4 hacking may be quite fun)
<mfp>
significant whitespaces sounds hard to do with camlp4
<mfp>
playing with the lexer and stuff?
<bluestorm>
yes
<mfp>
or can you get the column from the loc?
<rwmjones>
what is the #light syntax?
<mfp>
rwmjones: an indentation-aware syntax lighter than the std one
<rwmjones>
oh god not another syntax :-(
<bluestorm>
:]
<FoolOfSoul>
is there log4... for ocaml/camlp4?
<bluestorm>
log4 ?
<FoolOfSoul>
like log4j
<bluestorm>
rwmjones: it's not "another" actually, as it's already in use and well-defined in F#
<FoolOfSoul>
the log and the unit are my important libraries
<FoolOfSoul>
so, i can trace the complex execution of ocaml programs
<bluestorm>
you can use #trace in the toplevel
<FoolOfSoul>
bluestorm, i want pick selectly some classified logs
<FoolOfSoul>
s/want/want to
ulfdoz has quit [clarke.freenode.net irc.freenode.net]
rwmjones has quit [clarke.freenode.net irc.freenode.net]
Ugarte has quit [clarke.freenode.net irc.freenode.net]
mbishop has quit [clarke.freenode.net irc.freenode.net]
ccomeaux has quit [clarke.freenode.net irc.freenode.net]
szell has quit [clarke.freenode.net irc.freenode.net]
jdev has quit [clarke.freenode.net irc.freenode.net]
vbmithr_ has quit [clarke.freenode.net irc.freenode.net]
rwmjones has joined #ocaml
vbmithr_ has joined #ocaml
ccomeaux has joined #ocaml
szell has joined #ocaml
mbishop has joined #ocaml
jdev has joined #ocaml
ulfdoz has joined #ocaml
Ugarte has joined #ocaml
adonis28850 has quit [Read error: 110 (Connection timed out)]
m3ga has quit ["disappearing into the sunset"]
Philonous1 is now known as PHilonous
PHilonous is now known as Philonous
Snrrrub has joined #ocaml
jlouis has joined #ocaml
ccomeaux has quit [Client Quit]
guillem has joined #ocaml
mikezackles has joined #ocaml
sponge45 has joined #ocaml
Jedai has joined #ocaml
bpalmer has quit ["ERC Version 5.0 (CVS) $Revision: 1.776 $ (IRC client for Emacs)"]
Proteus_ has joined #ocaml
Proteus has quit [Read error: 113 (No route to host)]
sponge45 has quit [Read error: 110 (Connection timed out)]
marmotine has joined #ocaml
redocdam has joined #ocaml
Cygal has joined #ocaml
Axioplase_ is now known as Axioplase
<asmanur>
Here is a small camlp4 extension to handle haskell's syntaxic sugar for infix operators (for instance (>= 0)) : http://paste.pocoo.org/show/80225/
haveo has joined #ocaml
pango_ has quit [Remote closed the connection]
rwmjones_ has joined #ocaml
pec1 has joined #ocaml
pango_ has joined #ocaml
rwmjones has quit [Read error: 113 (No route to host)]
Linktim has joined #ocaml
<flux>
asmanur, hm, does it also support ( 0 >= ) ?
<flux>
although pretty much all those cases are relatively neatly handled by pa_hole , although some may object ;)
<flux>
(but, look who's talking: I really should take a deep look on camlp4 programming some day..)
<asmanur>
flux: yes it does
Yoric[DT] has joined #ocaml
guillem has quit [Remote closed the connection]
munga_ has quit [Read error: 110 (Connection timed out)]
filp has quit ["Bye"]
TheLittlePrince has joined #ocaml
netx303 has joined #ocaml
mishok13 has quit [Read error: 131 (Connection reset by peer)]
TheLittlePrince has quit [Client Quit]
sporkmonger has joined #ocaml
guillem has joined #ocaml
OChameau has quit [Read error: 113 (No route to host)]
Jedai has quit [Read error: 110 (Connection timed out)]
landonf has joined #ocaml
<landonf>
Dumb question -- what is the >::: and >:: syntax? As in: let test_fixture = "TestSomething" >::: [ ...
<asmanur>
landonf: maybe a user-defined operator ?
<landonf>
Ahh, right. See, dumb question -- thanks!
Linktim has quit ["Quitte"]
Linktim has joined #ocaml
netx303 has left #ocaml []
landonf has quit []
ygrek has joined #ocaml
tomh has joined #ocaml
vbmithr_ has quit ["leaving"]
vbmithr has joined #ocaml
vixey has joined #ocaml
<vixey>
hi
<vixey>
how is type soundness proved given that you may define new data types in ocaml?
<Smerdyakov>
A strange question. I don't see the trouble.
<Smerdyakov>
(The meta answer is that no one has proven type soundness for OCaml, I think.)
<vixey>
okay
<vixey>
why does data not get a good treatment when lambda, exceptions, callcc and everything else does?
pippijn has joined #ocaml
<pippijn>
hi all
<vixey>
hello
<pippijn>
why does ocaml have separate operators for float?
<vixey>
pippijn: the type float is disjoint to integer
<vixey>
I'm sorry I meant int
<pippijn>
vixey: why can't + just be overloaded for int and float?
<bluestorm>
pippijn: overloading does not exist in the base ML type system
<pippijn>
right..
<bluestorm>
you can probably do that with extra care, but OCaml do not
<bluestorm>
and, all in all, it is not so bad
<pippijn>
at least it signifies that this is a floating point operation
<pippijn>
which may be useful in some cases
<bluestorm>
(though it can get a little bit painful, specifically for float computations : there is ongoing work on camlp4 extensions to make it easier)
<mbishop>
you should know the type anyway, so it's not hard to remember
<pippijn>
caml4p is not in debian :-\
<pippijn>
camlp4
<pippijn>
or maybe it is
<pippijn>
I see lots of camlp4 stuff.. is it part of ocaml base?
<pippijn>
never mind.. it's there
<bluestorm>
yes it is
<pippijn>
camlp4 - Pre-Precessor-Pretty-Printer for OCaml
<pippijn>
I want to write a compiler
<pippijn>
I have already done so
<pippijn>
but in C++
<pango_>
actually there's camlp4 and camlp5 (pre-3.10 compatible camlp4)
<pippijn>
pango_: I have ocaml 3.09
<pippijn>
.2
<vixey>
C++ is a different language
<pango_>
hence you should use camlp4 package
<pippijn>
vixey: so I heard (and saw from examples)
<bluestorm>
do you need float operations to write a compiler ?
<pango_>
I guess camlp5 is debian testing only for now
<vixey>
you can read these programs if you are writing a compiler it might help
<pippijn>
Chile`: yacc
<pippijn>
Chile`: the first version was a hand written recursive descent parser but I got annoyed by some minor glitches so I switched to yacc
<pippijn>
vixey: thanks
<pippijn>
A simple arithmetic calculator. It handles addition, subtraction, negation, multiplication and division of integers. <- excellent
<pippijn>
hello world for programming language writers
<bluestorm>
pippijn: do you know the basic notions of OCaml, aka algebraic datatypes and pattern machine ?
<pippijn>
bluestorm: basically, I don't know anything about ocaml, but I know what algebraic datatypes are
<bluestorm>
hm
<pippijn>
I have implemented an extension to C++ which allows the definition and use of them
<bluestorm>
and pattern matching ?
<pippijn>
well
<pippijn>
yeah
<pippijn>
I think I know what that is
<bluestorm>
interesting
<bluestorm>
(pattern matching is when you deconstruct values, binding the inner pats to identifiers)
<pippijn>
matching lists like:
<pippijn>
I have a list with elements (1, 2, 3, 4)
<pippijn>
then I do:
<Chile`>
pippijn: fwiw, there are much better parsers for C++ than yacc these days
<pippijn>
match (l) { (a, b, ...) => { do somethign with a and b; } }
<bluestorm>
yes
<bluestorm>
iirc , there is an existing project providing pattern matching to C++ and Java
<pippijn>
and a and b would be 1 and 2
<Chile`>
pippijn: including ones that are inline in the language (Spirit)
<pippijn>
Chile`: I don't like spirit
<pippijn>
Chile`: it's slow and ugly
* Chile`
shrugs
<pippijn>
but yeah..
<vixey>
camlex and camlyacc are really nice though
<vixey>
ocamllex*
<pippijn>
Chile`: I know yacc and for prototyping, I didn't want to learn another parser generator syntax
<pippijn>
vixey: is there something like a dynamic parser for ocaml where the actual language is defined at runtime?
<pippijn>
so post-facto syntax extensions can be done?
<Smerdyakov>
pippijn, camlp4
<pippijn>
Smerdyakov: not *to* ocaml
<Smerdyakov>
pippijn, I know.
<pippijn>
camlp4?
<Smerdyakov>
Yes.
<pippijn>
interesting
<vixey>
You want to actually extend the parser during compiling?
<pippijn>
so camlp4 can parse arbitrary grammars?
<Smerdyakov>
Yes.
<pippijn>
vixey: either that or right before compiling
<vixey>
are you sure that is necessary?
<Smerdyakov>
Coq uses camlp4 for extensible syntax.
<vixey>
maybe you can just define a more general language
<pippijn>
hm
<pippijn>
it would become much more complex to parse..
<pippijn>
the prototype has no custom operators for one
<pippijn>
it can overload a small set of operators
<pippijn>
which happens to be the set of overloadable operators in C++
<Smerdyakov>
That sounds like a bad sign.
<pippijn>
however, I want to be able to define my own operators (such as set composition operator 'o')
<pippijn>
which would operate as infix operator on the 'set' type
<Smerdyakov>
pippijn, you may have noticed that OCaml lets you define your own operators, with no "syntax extension" needed.
<pippijn>
or as function chaining operator
<pippijn>
(g o f) (3)
<pippijn>
like that
<Smerdyakov>
pippijn, but there are lexical restrictions. You can't use 'o', for one.
<vixey>
well you don't so much define new ones.. as pick them from an infinite set of existing ones
<vixey>
which is what I meant by maybe you can make the parser more general instead of extending it dynamically
<Smerdyakov>
pippijn, however, you can do exactly what you want in OCaml with an arbitrary infix operator. Such operators are just prohibited from starting with letters, at the lexical level.
<pippijn>
vixey: yeah, but o is not necessarily an infix operator
<pippijn>
it may be a function taking three arguments
<Smerdyakov>
pippijn, you might also want to look at SML's handling of infix operators.
<pippijn>
Smerdyakov: I want to write a parser for my own language
<Smerdyakov>
pippijn, it allows _exactly_ what you're asking for, and indeed infix 'o' composition is in the standard library.
<pippijn>
Smerdyakov: I don't want to be tied to ocaml's lexical properties or its type system
<pippijn>
I want \/ to be definable as "or" operator
<Smerdyakov>
pippijn, I know. I'm pointing to SML as an example that supports user infix operators without any "syntax extension" mechanism.
<pippijn>
Smerdyakov: ah, okay
<pippijn>
yeah..
<Smerdyakov>
Standard ML of New Jersey v110.67 [built: Sun Jul 13 19:49:59 2008]
<Smerdyakov>
- infix \/;
<Smerdyakov>
infix \/
<Smerdyakov>
- fun op\/ (a, b) = a orelse b;
<Smerdyakov>
val \/ = fn : bool * bool -> bool
<Smerdyakov>
- true \/ false;
<Smerdyakov>
val it = true : bool
<pippijn>
that's nice
<pippijn>
I want that for my language, as well
<Smerdyakov>
It doesn't interact well with the module system, though. Fixities should be in signatures.
<Smerdyakov>
But I wouldn't be surprised if your language won't have an ML-style module system.
<pippijn>
indeed it won't have that
<pippijn>
probably mostly due to the fact that I developed it not knowing anything about ML
<Smerdyakov>
What is the purpose of the language?
<jlouis>
The ML module system is probably the best module system I've seen yet
<pippijn>
to combine set theory with programming
<jlouis>
pippijn, that sounds almost like prolog ;)
<pippijn>
actually, I want to have a language that can express mathematics in the most natural way
<pippijn>
and I want the language itself to contain as little built-in stuff as possible
<pippijn>
which means for one that operators do not exist
<pippijn>
every operator needs to be defined by the standard library, written in the language itself
<Smerdyakov>
pippijn, I think Coq already satisfies that criterion, and it has tremendous engineering effort behind it already.
<pippijn>
I have looked into coq
<Smerdyakov>
pippijn, it's based around type theory, not set theory. Type theory is superior to set theory for pretty much anything grounded in practical concerns.
<pippijn>
but coq can't really be used as a general purpose programming language
<Smerdyakov>
Absolutely false.
<pippijn>
Smerdyakov: yes, well, type theory.. I wanted to base it around category theory
<Smerdyakov>
Type theory is superior to category theory for pretty much anything grounded in practical concerns. :P
<vixey>
Smerdyakov: it doesn't have a IO library ...
<pippijn>
Smerdyakov: coq wouldn't be the language of choice to write an irc client in
<vixey>
I mean you can't write say, an IRC bot
<Smerdyakov>
vixey, it's trivial to wrap OCaml's standard library once you have a foundation like Ynot.
<Smerdyakov>
pippijn, if so, that would only be because you don't care about expressive types in that domain, not because it wouldn't work out all right.
<vixey>
interesting
<pippijn>
Smerdyakov: tomorrow, I'm having the second part of a meeting with a few other language users and implementers
<Smerdyakov>
pippijn, what is the context of the meeting?
<vixey>
what is a language user?
<pippijn>
I'll mention coq and ask whether they think coq is a basis we could build on
<pippijn>
vixey: a potential user of a language
<pippijn>
which is mostly broken and incomplete right now
<pippijn>
but the ideas are there
<Smerdyakov>
pippijn, what is the context of the meeting?
<vixey>
pippijn: Why are you interested in expressing mathematics in a programming language?
<jlouis>
YNot is interesting as a project.
<vixey>
aeou
<Smerdyakov>
pippijn, did you mean that it's a meeting of users and implementers _of_your_language_?
<pippijn>
not only
<Smerdyakov>
pippijn, then what is the context/purpose of the meeting?
<pippijn>
Smerdyakov: it's about efficiently implementing certain things in mathematics
<Smerdyakov>
pippijn, is this a meeting at a university?
<pippijn>
yes
<Smerdyakov>
pippijn, so all the people in your department with interest in this subject, more or less?
<pippijn>
yes, more or less
<Smerdyakov>
OK. Which university?
<pippijn>
university linz
<pippijn>
it's also about integrating certain CASs with others and interoperability to exploit each CAS's positive sides
* vixey
pippijn: Why are you interested in expressing mathematics in a programming language?
<vixey>
oops
<Smerdyakov>
OK. It's become apparent that you don't know enough about Coq to make an informed choice. Do you think someone else at the meaning _will_ know enough?
<pippijn>
Smerdyakov: possibly
<pippijn>
Smerdyakov: I'll mention it and ask whether anybody knows about it
<Smerdyakov>
pippijn, I'm pretty confident that your work will be irrelevant if you don't build on Coq.
<pippijn>
Smerdyakov: if not, the topic will be deferred until I know more about coq
<pippijn>
vixey: because it aids in formally proving theories
<pippijn>
vixey: which seems to be what coq is doing..
<Smerdyakov>
pippijn, also, there's probably not nearly as much work to do as you've been thinking, if you start with Coq.
<vixey>
what theories ?
<Smerdyakov>
I'm not surprised that you don't know about Coq.
<Smerdyakov>
Hardly anyone outside of programming languages researchers does.
<pippijn>
Smerdyakov: I know maude
<Smerdyakov>
But it's clear to me that any work in formal math that doesn't build on Coq is going to start and stay irrelevant.
<pippijn>
which is also interesting to mathematical proof
<vixey>
how does maude count as a theorem prover?
<pippijn>
maude is used as a model checker
<vixey>
Smerdyakov: I doubt OTT will be irrelevant ..
<Smerdyakov>
vixey, OTT isn't implemented in a production-quality system.
<pippijn>
vixey: one of the group wants to express different types of formal power series in a uniform manner using a programming language
<Smerdyakov>
vixey, my statement is meant to evolve to whatever is the successor to Coq, if there is one.
<bluestorm>
Smerdyakov: aren't there some other proof assistant around, that could be considered : Isabelle and such ?
<Smerdyakov>
vixey, there will never be more than one usable and current system, I predict.
<Smerdyakov>
bluestorm, Isabelle is impractical for a variety of important reasons.
<vixey>
pippijn: oh there are various developments of the constructive reals in Coq
<pippijn>
hm
<pippijn>
I certainly need to learn more about coq
jlouis has quit ["Leaving"]
jlouis has joined #ocaml
<pippijn>
vixey: can you link me to any information on this?
ygrek has quit [Remote closed the connection]
<vixey>
on what?
<pippijn>
formal power series in coq
<vixey>
I read it in a book
<pippijn>
oh
<vixey>
I think the ccorn project is the place to look
<pippijn>
coq constructive repository of nijmegen?
sporkmonger has quit []
pec1 has quit [Read error: 110 (Connection timed out)]
Snark has quit ["Ex-Chat"]
marmotine has quit ["mv marmotine Laurie"]
pec1 has joined #ocaml
marmotine has joined #ocaml
marmotine has quit [Read error: 104 (Connection reset by peer)]
asmanur has quit [Read error: 110 (Connection timed out)]
<jlouis>
Someone must have done extensive formal power series in Coq