<twobitsprite>
sad the stdlib has String.iter but no String.map...
Snark has joined #ocaml
PhyuckYiu has quit [Read error: 104 (Connection reset by peer)]
joshcryer has quit [Client Quit]
m3ga has joined #ocaml
SnarkBoojum has joined #ocaml
Snark has quit [Read error: 110 (Connection timed out)]
SnarkBoojum is now known as Snark
Morphous has joined #ocaml
Amorphous has quit [Read error: 110 (Connection timed out)]
Skal has joined #ocaml
<Demitar>
twobitsprite: That's what extlib is for. ;-)
_JusSx_ has joined #ocaml
bluestorm has joined #ocaml
rillig has joined #ocaml
rillig has quit [Client Quit]
m3ga has quit ["disappearing into the sunset"]
_JusSx_ has quit ["leaving"]
Morphous is now known as Amorphous
Smerdyakov has joined #ocaml
dylan has quit ["Lost terminal"]
dylan has joined #ocaml
Skal has quit [Remote closed the connection]
<twobitsprite>
gah! camlp4 is so confusing!
ski has quit [Read error: 110 (Connection timed out)]
ski has joined #ocaml
ski_ has joined #ocaml
ski has quit [Nick collision from services.]
ski_ is now known as ski
tspier2 has joined #ocaml
<tspier2>
Hi, I have a question about parsing user input. Does anyone have some free time?
<Smerdyakov>
The cardinal rule of IRC: Ask the question, wait for answer; never ask to ask.
<tspier2>
Well, this is what I want to do...
<tspier2>
I want to have a prompt that just has the symbol ">". Then the user can enter input. If the user enters print('Hello World'); then it would print Hello World on the next line. Whatever the user puts in ('') will be printed on the next line. Can someone please help me write a simple program on how to do this?
<tspier2>
Example:
<tspier2>
> print('Hello World');
<tspier2>
> Hello World
<Smerdyakov>
If your language will get any more complicated, you should use a parsing tool like ocamlyacc or camlp4.
<Smerdyakov>
However, if you don't know how to parse 'print' statements with constant arguments, then you have a bigger, language-independent problem. (If you know how to do it but don't want to do that tedious work, that's another issue, and one that parsing tools ameliorate.)
<tspier2>
Well, I'm trying to find a language that I can use to create a simple language for education purposes. I'm interested in OCaml, but I haven't gotten too far into the tutorial, because reading bores me. I need to see actual source of something I will use in order to gain an interest in it.
<Smerdyakov>
Do you know how to complete your task in any other programming language?
<tspier2>
I started doing it in Pascal, but then I got rid of my source, because I decided that Pascal is slowly dying out, and OCaml would be a great candidate.
<Smerdyakov>
So you don't know to perform this basic regular-language parsing task in any programming language?
<tspier2>
Not really, because I don't do too much console-based programming anymore. Normally I stick to GUI.
<tspier2>
Or little scripts for IRC in perl here and there
<Smerdyakov>
So you are stuck on the input aspect, not how to parse a string once you have it?
<tspier2>
The only thing needed for the output to be presented would be the basic print('');
<Smerdyakov>
s/will such/will find such/
<tspier2>
Oh
<bluestorm>
(basically, why not just use (o)caml as a teaching language ?)
<tspier2>
I've forgotten a lot of programming I did over the years, but I want to get back into it now. OCaml looks like it could be a good language for me to learn. How long would it take for the average person to learn?
<Smerdyakov>
bluestorm, where did that come from?
<Smerdyakov>
tspier2, that depends how polluted you are by time with other, imperative languages.
<tspier2>
Hmm
<Smerdyakov>
tspier2, starting with OCaml, an academic semester's time should certainly be enough to get comfortable with it.
<Smerdyakov>
tspier2, coming from most mainstream languages, many people need years to get over the handicaps they carry.
<tspier2>
Oh
<Smerdyakov>
I'll only say that good programmers (or people with the potential to become good programmers) find OCaml very easy to learn and use.
<tspier2>
Okay
<dylan>
O'
<dylan>
er
<dylan>
O'Caml's great for a lot of tasks, and seems quite elegant. But I would not advise trying to do multitasking network applications in it, or CGI-like things in it.
* dylan
's first experience with ocaml was writting a CGI utility library, and then trying to implement a wiki.
<flux__>
what tool is better for those?
<dylan>
Erlang kills at network applications.
<Smerdyakov>
dylan, the ML world has everything Erlang has, plus static typing, so it must be the static typing that bothered you...?
<dylan>
No other language / platform has anything comparable to mnesia.
<flux__>
not having static typing wasn't much of a bane?
<dylan>
Smerdyakov: ML does not have mnesia.
<Smerdyakov>
dylan, mnesia is just a web server built on lightweight threads, right?
<dylan>
Smerdyakov: Erlang's process model is slightly different than Concurrent ML's.
<dylan>
Smerdyakov: Mnesia is a relational database.
<Smerdyakov>
Ah, I misremembered.
<Smerdyakov>
dylan, how is the process model different?
<dylan>
Erlang with static typing would be cool.
<flux__>
how much better could ocaml be made by just writing libraries?
<flux__>
for those tasks
<dylan>
Smerdyakov: I lack enough experience with either to say. But it dervices from the untyped mailbox that each process has.
<flux__>
I'm just wondering what it is in the language that makes it better
<Smerdyakov>
flux__, stay tuned; I'm working on the best web application framework ever, based on the ML approach. ;)
<dylan>
flux__: If Event was made more efficient, ocaml would be almost as useful.
<flux__>
smerdyakov, but it's only web?-)
<Smerdyakov>
dylan, I'm curious, do the inefficiencies you imply also exist in MLton's CML?
<flux__>
(I'm intereseted nevertheless)
<Smerdyakov>
flux__, there are many good features that apply elsewhere, but web applications are my focus.
<dylan>
Smerdyakov: Dunno. I prefer ocaml's syntax to SML's.
<flux__>
they do say erlang is excellent for network applications, so maybe there's some truth to that
<dylan>
flux__: some features of erlang would be difficult in ocaml. Like reloading code without dropping connections.
<flux__>
I've never heard anyone explicitly say that ocaml is great for network applications ;)
<Smerdyakov>
flux__, I'm not yet aware of linguistic issues that don't put Concurrent ML on the same footing.
<flux__>
so all we'd need is a killer library
<dylan>
Trying to get per process mailboxes (Event.channels) that stay polymorphic (how do I explain? hmm...) would require magic similar to lablgtk...
<Smerdyakov>
I don't know. I'm not clear on what is missing from Concurremt ML implementations today.
<Smerdyakov>
dylan, I understand. You want dynamic typing. :P
<dylan>
Smerdyakov: Not entirely, no.
<Smerdyakov>
dylan, I won't accept your assertion that you need this feature; I want an example of an application where this is important.
<dylan>
It should be possible to express that within a type system, although maybe not ocaml's.
<dylan>
Smerdyakov: I will not accept your assertion that monkey lives in my nose.
<Smerdyakov>
Are you calling monkey a liar?
<flux__>
I guess the simplest way to see why dynamic typing is so convenient in this case would be to have such an application.. and then port it to ml
<dylan>
Perhaps.
* dylan
has been doing that.
<flux__>
and then also consider other factors such as how easy are they to expand afterwards
<dylan>
Friend of mine wrote a chat server in erlang. I'm trying to port it to ocaml. It's a pain.
<dylan>
My design works, but the erlang is actually easier to add features to.
<Smerdyakov>
dylan, literal line-by-line porting doesn't show anything but how well a language supports a kind of development.
<Smerdyakov>
s/but/about
<dylan>
Smerdyakov: it's not line by line.
<dylan>
I wrote a spec for this chat protocol, and I try to implement the spec in ocaml.
<Smerdyakov>
Any "porting" that involves trying to use the same basic design has the same problem.
<flux__>
yeah, actually I didn't mean 'port' but 'reimplement'
<dylan>
my design's different, as I said. And harder to work with.
<flux__>
great, so we can just blame the developer, not the tool.. ;)
<dylan>
Mostly this a failing of libraries available, and the type system not being smarter.
<dylan>
I know something is wrong when I ponder doing it in haskell...
mikeX has joined #ocaml
<Smerdyakov>
I think we'd be interested to hear about details, and I'm sure you'll understand if we don't believe that you have a point without them.
<dylan>
the ocaml one (my baby) is far less complete than the erlang one. I'm not sure if it even works right now.
<Smerdyakov>
No, I don't want to read your code. I want to read a detailed but thoughtful critique that involves minimally-sized examples that illustrate the issues. :P
<dylan>
Oh. Appologizes. I prefer reading code to english, most of the time.
<Smerdyakov>
Notice I mentioned minimally-sized examples, which are definitely code.
<Smerdyakov>
But probably not literal code from your implementation.
<dylan>
I would consider the erlang version to be as minimally sized as would warrant a valid comparison
<dylan>
anyway, off hand I'd say ocaml needs an in-memory relation database that gets along with the type system,
<dylan>
a way to watch
<Smerdyakov>
haver_worker.erl is looong.
<dylan>
a way to watch CML threads (a supervisor model)
<dylan>
and (hard to do) a way of replace code at runtime (in the bytecode VM) if the type signatures match.
<Smerdyakov>
That last one I definitely disagree with. You just need dynamic loading of code, if your program is architected properly.
<dylan>
769 for that server seems reasonable to me.
<Smerdyakov>
I guess my objection is similar to the usual one for inheritance in OO: there are no semantic constraints that child classes satisfy the specifications associated with their parents, but the construct is designed to lead you into a false belief of that.
<dylan>
it is really useful to replace functions in the running server, without dropping all the clients.
<Smerdyakov>
Same with modifying code at runtime: you believe that you have put something compatible in, in a way that preserves your program-wide invariants, but nothing checks that for you.
<Smerdyakov>
You're better off using an explicit hand-off protocol that you design with the issues in mind.
<Smerdyakov>
You can update software without dropping clients or replacing code.
<dylan>
Erlang is quite pragmatic, though. It has code reloading because people needed it to get their job done.
<Smerdyakov>
You just switch to calling a new, dynamically-loaded function at one place where you used to call another. (And maybe the old code is GC'd.)
<Smerdyakov>
I will never agree that code reloading is necessary.
<dylan>
that is what Erlang does.
<Smerdyakov>
You can always just switch to calling _different_ code.
<dylan>
Except for old connections, remain using the old code. Only effects new connections.
<Smerdyakov>
I believe Alice ML supports this, then.
<dylan>
Alice ML is inspired by Oz, I believe, which itself has some ideas from Erlang. :)
<ski>
(didn't know that last)
<dylan>
Last I looked at Oz, I found it depressing and tasting of fish. Perhaps I'll try Alice. :)
gim_ has joined #ocaml
<tspier2>
How can I get input in OCaml? I know in Python it is, "int(raw_input("Enter input:"))".
<Smerdyakov>
tspier2, prepare to see me repeat a message I already sent you!
<Smerdyakov>
If you are not able to read documentation, then ML is not for you.
<tspier2>
Wow, I am lost already.
<dylan>
if you are not able to read documentation, no language is for you.
<dylan>
Except perhaps subtext...
<tspier2>
No. I just can't read this, because there is hardly any commenting.
<Smerdyakov>
tspier2, I didn't mean to imply that the page I linked should explain it to someone unfamiliar with ML.
<Smerdyakov>
tspier2, you should read the tutorial in the manual first.
<tspier2>
Oh
* dylan
remembers running the ocaml toplevel for the first time, typing in a few math expressions, and then wondering why variables were immutable.
<ski>
val read_line : unit -> string
<ski>
Flush standard output, then read characters from standard input until a newline character is encountered. Return the string of all characters read, without the newline character at the end.
<ski>
e.g.
<ski>
so you'd call 'read_line ()' to get a string
<tspier2>
Oh
slipstream-- has joined #ocaml
Snark has quit ["Leaving"]
slipstream has quit [Read error: 110 (Connection timed out)]
tspier2 has quit ["Leaving"]
* Demitar
would like to switch to standard ml, if there just weren't so many thing he'd miss from OCaml... :)
<Smerdyakov>
Like?
<Demitar>
Labeled arguments, object oriented gtk bindings, and a solid sdl binding.
<Demitar>
On the other hand I'd just love being able to compile things with mlton. :)
<Demitar>
Oh, and marshalling is something I'd lack in mlton (currently at least).
<Demitar>
And I do like those polymorphic variants. :)
<Demitar>
I have so far found the ML Basis structure a bit confusing. At least after all the ocaml auto linking and ocamlfind.
<Smerdyakov>
I don't use any of the features you mentioned, and have gripes about some of them. :)
<Smerdyakov>
Anyway, forget this OCaml vs. SML; just program in Coq.
<Demitar>
Object orientation I presume? :) I'm not really a fan, just need a good gtk binding really. :)
<Smerdyakov>
But you said it had to be OO.....
<Demitar>
Well, in ocaml I prefer OO for the syntax really. :)
<Smerdyakov>
I also don't like labeled arguments, since they are easy to get with records and thus only complicate the language; and polymorphic variants, since they are far too fast-and-loose to mesh with my view of the general ML philosophy.
<Smerdyakov>
I bet part of the rationale for labeled arguments in OCaml is that you don't have anonymous record types; SML does.
<Demitar>
Smerdyakov: There we go. :) My argument was that { Module.Foo.Bar.Baz.label = ...; } would be quirky. :)
<Demitar>
Also, polymorphic variants are the same argument, and really just a minor nag at most.
<Demitar>
Smerdyakov: What nice ffi generation tools exist for SML?
<Smerdyakov>
Demitar, MLton basically allows you to include ML-ized C prototypes in code and then call the C functions easily. Do you mean a tool that would do that kind of thing automatically from a .h file?
<Demitar>
Yes, I'm lazy. :) (I found ml-nffigen btw.)
<Smerdyakov>
Right. The SML/NJ NLFFI is very nice in that respect.
<Smerdyakov>
Generates everything automatically, and with ML types.
<Demitar>
But incompatible with mlton I take it?
<Smerdyakov>
I think it works with MLton these days, too.
<Demitar>
Woo.
<Smerdyakov>
At least, ml-nlffigen seems to be mentioned in the MLton docs under "other tools included." :)
<Demitar>
How pure is SML in regards to imperative programming? There are still things I'd rather not do in a functional manner.
<Smerdyakov>
The only significant differences in that area that I know of are: associativity rule for the ';' operator requires more parentheses in SML, and SML has no mutable record arguments (though they're easy to simulate with refs).
<Demitar>
No let updated_record = { foo_record with bar = "newval"; } in syntax?
<Smerdyakov>
Right, though that's not an imperative feature, and SML/NJ has a similar extension.
<Demitar>
Yes, not imperative, just saving a lot of hassle. :)
<Demitar>
I probably should attempt porting the current little application I have been working on then. :) (I would benefit massively from just a bit of inlining (I use an abstract type for vectors).)
<Smerdyakov>
Is this something you could code in Coq? :)
<Smerdyakov>
(It's easy to output SML code from Coq, I think.)
<Demitar>
You mean Coq has evolved from a theorem solver into a terrifying general programming language? :)
<Smerdyakov>
My thesis work is in programming program analysis tools with Coq.
<Smerdyakov>
Coq has been a superset of an ML-like programming language from the start.
<Demitar>
Would this require me to actually remember all that algebra and logic I've long forgotten? :) My current argument for using OCaml (and ML in general) is that it allows me to write sloppy code and get away with it. :)
<Smerdyakov>
When you use ML, you can write sloppy code and get away with it if you only make errors that ML's type system can characterize.
<Smerdyakov>
When you use Coq, you can write sloppy code and get away with it if you make any error that mathematics can characterize. :)
<Smerdyakov>
(Fixing your errors is significantly more work in Coq, though. ;)
<Demitar>
This is quite interesting I must say. Using a tool written in ocaml to output sml. All while porting an application originally written in ocaml.
<twobitsprite>
Is coq mostly good for working with program source code, or is it useful at all as a language in its own right?
<Smerdyakov>
twobitsprite, modulo syntactic sugar, Coq is at least as useful a programming language as ML.
<Smerdyakov>
twobitsprite, since ML is a subset, more or less.
<twobitsprite>
I see... so you're saying the Coq just isn't an pretty as ocaml, essentially?
<Smerdyakov>
twobitsprite, but you also gain arbitrary mathematical power.
<Smerdyakov>
twobitsprite, yes.
<twobitsprite>
Smerdyakov: think it'd be easier to work with ternary numbers in coq? :P
<Smerdyakov>
twobitsprite, only if you are interested in proving program correctness.
<Demitar>
Smerdyakov: Now, could you give me an example of rendering an opengl scene from Coq? ;-)
<twobitsprite>
i.e. I'm currently trying to tackle camlp4 so that I can introduce a septemvigesimal (base-27) litteral syntax... would this be simpler in coq?
<Smerdyakov>
Demitar, it would look more or less like doing the same in Haskell.
<Smerdyakov>
twobitsprite, no; Coq uses camlp4, and I think camlp4 was developed with use in Coq as a main goal. :)
<Demitar>
There we go, another language I've only briefly looked at. I'm not sure I have time for another larval stage right now... :)
<twobitsprite>
Demitar: you having problems understand camlp4 too?
<Demitar>
twobitsprite: No, with Coq and Haskell. :)
<twobitsprite>
ahh
<Demitar>
twobitsprite: And, yes camlp4 is confusing to me as well but that's nothing I need to worry about right now. :)
<Smerdyakov>
(Coq can also output Haskell.)
<Demitar>
Smerdyakov: More specifically, where should I look if I want to generate an actual program in Coq?
<Smerdyakov>
I use camlp4 at a shallow level to extend Coq with new tactics and such.
<twobitsprite>
camlp4 just seems to have too many non-othognal syntaxes involved for me to really grok
<twobitsprite>
orthogonal*
<Smerdyakov>
Demitar, the Coq manual? :)
<Smerdyakov>
Demitar, or the Coq'Art book.
<Smerdyakov>
Demitar, if you want to use only the ML subset, you can more or less just start writing code with a handy table mapping OCaml to Coq syntax.
<Smerdyakov>
(I don't know of one. ;)
<Demitar>
Smerdyakov: I find it a tad difficult to find an actual example of a file and a command which will generate an actual program which will do something. :)
<Demitar>
Smerdyakov: I meant generating a standalone executable which will actually display something on screen.
<Smerdyakov>
That gives you OCaml code, which I assume you know how to compile.
<Demitar>
If I just wanted cryptic coq code I'd look in the tutorial. :)
<Demitar>
Oh?
<Demitar>
Oooh...
<Demitar>
So, definition is one of the important keywords. :)
<Smerdyakov>
It's like 'let' in OCaml.
<Smerdyakov>
(Like the form of 'let' without 'in'. 'let'/'in' has a different counterpart in Coq.)
<Demitar>
Smerdyakov: If I actually get past this barrier writing programs in coq will hopefully be like my switch from python to ocaml. :)
<Demitar>
Say I would like to call a function, for instance print_endline.
<Demitar>
Where should I look?
<Smerdyakov>
You need to implement a monadic version in Coq, and then declare the relevant types and values as parameters in Coq.
<Smerdyakov>
Er, implement in _OCaml_.
<Demitar>
Is there a trivial example of something like this somewhere?
* Demitar
would love to have the colission detection written in coq. :)
khaladan_ has joined #ocaml
<Smerdyakov>
I don't know of any document like that.
<Smerdyakov>
It's all very avant-garde, you see. :)
<twobitsprite>
I see mention of "ocpp" in the ocaml-list archives, but no where on the actual site... any links?
<Demitar>
Yes, but if you have been working on this I was assuming you had some examples, difficult or not isn't really the point here, just something to get me started. :)
<Smerdyakov>
Bloody hell. SourceForge web CVS is acting up.
<Smerdyakov>
(I was going to point you to an implementation of a generic model checker in Coq.)
<twobitsprite>
why do I need to keep .cm* files around after running ocamlmktop? is there a way to statically link them?
<Demitar>
Smerdyakov: Am I correct if I guess that Coq will generate a rather straightforward model of what it has proven? Which in turn mlton can optimize into silliness. :)
<Smerdyakov>
Demitar, Coq's logic is defined so that typing clearly defines what should actually exist at runtime and what is part of a specification/proof.
<Demitar>
So, basically it's already optimized (at source level at least)? (No need to get into specifics if I'm wrong. :)
<Demitar>
In the sense that Coq has already proven so much that most dead code elimination is no longer relevant.
<Smerdyakov>
I don't know about that.
<Smerdyakov>
There is nothing similar to traditional compiler optimization.
<Demitar>
It's an adventure then. :)
<Demitar>
Now, the ability to prove that no object will pass through another would be neat, although I doubt that's actually possible with IEEE floats. :)
<Demitar>
(Thinking collision detection here.)
<Smerdyakov>
Coq helps you prove correctness properties. It doesn't do anything for performance optimization, nor is there even a clear idea of what performance of a Coq program is.
<Demitar>
Well, can't really get worse than the current performance of my game application, it's horribly unoptimized. :)
<Demitar>
Is it promising that Coq code still looks about as confusing as when I first looked at OCaml? :)
<Smerdyakov>
BTW, here's a person who has worked a lot on formal verification of floating point using Isabelle, a tool with much in common with Coq: http://www.cl.cam.ac.uk/~jrh/
<Demitar>
I can pick out identifiers and keywords but it all blurs into a big pile in the end. :)
* Demitar
goes to have a look.
<Smerdyakov>
My usual answer is that the asymptotic difficulty of learning Coq for experienced programmers is the same as that of learning programming for a non-programmers, though there may be a more favorable constant. :)
<zmdkrbou>
there are persons working on formal verification of floating point using coq too :)
<Demitar>
Well, I do need to brush up my algebra anyway. :)
<Smerdyakov>
zmdkrbou, OK, but they are not the chair for IJCAR'06, leading me to follow their home page links. :)
khaladan has quit [Connection timed out]
khaladan_ is now known as khaladan
<Demitar>
Smerdyakov: Should I expect Coq to include the Asm library or where would I find that?
<Smerdyakov>
Demitar, elsewhere in the same CVS repository on SF. That is not a particularly good example to use to follow along with. :)
<Demitar>
Ah, but if I intend to interact with real-world sources I assume I'll have to know about bits in the end, no? :)
<Smerdyakov>
I wasn't talking about that aspect. I was talking about the complexity of that file even by itself.
<Demitar>
Ah, well right now, I'm just browsing at random trying to get a feel for the language in another way. :)
<Demitar>
Question is, will programs developed in Coq have higher development time? (Of course, I already gladly accept the lower maintenance burden of an ocaml program in contrast to the short startup high maintenance of a python application. :) )
<Smerdyakov>
I am unaware of any significant use of Coq today in everyday programming, nor any guide targeted to that use. This is really more or less a new direction that I am proposing.
<Smerdyakov>
Maybe you would like to look up the Epigram project, which has documentation aimed more towards this.
<Demitar>
Well, it does adress a number of issues I have with ocaml as it is, mainly related to dataflow analysis (pre/post conditions and all that).
<Demitar>
Smerdyakov: Does anonymous records mean you can actually have named return types as well in SML? (Which is something I've been feeling would be nice from time to time.)
<Demitar>
Also, are epigram really seriously meaning they have multiline constucts? (Faked from a lexical perspective or not. :)
<Smerdyakov>
Demitar, what do you mean by "named return types"?
<Smerdyakov>
Epigram's notation unnerves me as well. :)
<twobitsprite>
Smerdyakov: familiar with Clean? (while we're on the topic of other languages)
<Smerdyakov>
twobitsprite, no. I only know that it uses uniqueness types for controlled imperativity.
<twobitsprite>
ahh... I was wondering you knew what I would be missing from Ocaml if I started using it...
<twobitsprite>
and there's noone in #clean
bluestorm has quit [Remote closed the connection]
<Demitar>
In general I suspect most languages simply lack polish of libraries. :)
<twobitsprite>
Demitar: yeah... I only really need some basic networking and some way to interface to some primitive graphics for now...
<Smerdyakov>
twobitsprite, why would you choose Clean over Haskell?
<twobitsprite>
(at least in terms of libraries)
<twobitsprite>
Smerdyakov: I'm just window shopping a bit, mostly... is Haskell generally superior to Clean?
<Smerdyakov>
twobitsprite, Haskell is _much_ more popular, with a much larger community.
<ski>
Smerdyakov : 'controlled imperativity' ?
<Smerdyakov>
ski, implementation of things that would be done with imperative constructs in other languages.
<Smerdyakov>
ski, while keeping referential transparency.
<ski>
(if you consider monads to also be 'controlled imperativity', then i think we agree)
<ski>
right
<ski>
(or rather, the monads used for common imperative things)
<twobitsprite>
Smerdyakov: maybe I just never gave it enough of a chance... and the fact that after searching far and wide, the only documents on doing i/o in Haskell have been mind boggling thesis papers... not much in the way of practical documentation for haskell
<ski>
twobitsprite : i/o in haskell is not very hard, i think
<Smerdyakov>
twobitsprite, I didn't find that to be the case.
<twobitsprite>
Smerdyakov: again... I probably just gave up too quickly... know of any good practical tutorials?
<ski>
(twobitsprite : search for 'Yet Another Haskell Tutorial pdf')
<Demitar>
Smerdyakov: Interestingly I seem to be having trouble coming up with a case where something I want to prove is something I actually know how to implement in Coq. ;-)
<Smerdyakov>
Demitar, I will try again to emphasize what a big leap it is to using Coq from OCaml. You should really read some documentation from start to finish, and you will need to learn a lot about logic and proving.
<twobitsprite>
can one extend the syntax of Haskell easily?
<twobitsprite>
er... maybe I should just join #haskell
<Demitar>
Smerdyakov: I have gone through the tutorial previously. I suspect it's just that my mind is set on writing solutions, no specifying properties.
<Demitar>
Just like the typesystem was working against me when I first started with OCaml but now is working for me.
<Smerdyakov>
Get ahold of the Coq'Art book.
<Demitar>
It's not availible online I take it? (Looking about the page.)
<Demitar>
Well what do you know, the book exists at exactly two university libraries... :)
<Smerdyakov>
I don't think it's available online.
<zmdkrbou>
nope, it's not
<Demitar>
Hah, look at that. A NaN leaked through to the front a bank currency calculator. :)
<Demitar>
A book which actually annotates four levels of competence makes for interesting reading. Ö=
<Demitar>
I make a prediction that before Coq is really useful for real-world applications a lot of data input validation is needs to be automated...
<Smerdyakov>
Can you elaborate on what you mean?
JKnecht has quit ["leaving"]
<Demitar>
Let's take the game as an example. I need to load level data, receive user input and all that, and once I feed this into my coq program I will most likely have to assert a number of preconditions so that I do not invalidate all the proofs I have built up. (I may be wrong in all this of course.)
<zmdkrbou>
(people don't use coq as a compiler/interpreter for real programs ... they use extraction)
<Demitar>
zmdkrbou: Still, the proven modules are only good as long as the preconditions are met.
<Smerdyakov>
You can write input validation code in Coq, and even generate it automatically with proof search.
<Demitar>
I take it there is no implicit pattern matching like "let (x, y) = point1 in" in definitions ("Definition add (x : R, y : R) ... = ... .")?
<Smerdyakov>
No, though 'let' supports that to a limited extent.
<Demitar>
Is this as convenient as the syntax is at the moment or did I miss something?
<Demitar>
(*let add (x1, y1) (x2, y2) =
<Demitar>
(x1 +. x2), (y1 +. y2)*)
<Demitar>
Definition add (p1 : R * R) (p2 : R * R) : (R * R) :=
<Demitar>
match p1 with
<Demitar>
| pair x1 y1 =>
<Demitar>
match p2 with
<Demitar>
| pair x2 y2 =>
<Demitar>
((x1 + x2), (y1 + y2))
<Demitar>
end end.
<Smerdyakov>
let (x1, y1) := p1 in let (x2, y2) := p2 in (x1 + x2, y1 + y2)
<Demitar>
Thanks. Where do I find out the naming of types for instance the List module in the standard library has no comment in the reference manual. Is the current answer to use the source? (I'm writing in CoqIde atm.
<Demitar>
Oooh, Print Module. :)
<Demitar>
On the other hand I should probably use a Set here... (implementing sum.)
<Demitar>
Smerdyakov: How do you view your use of Coq currently? As a poweful programming tool, or is it a tad to experimental to be really useful right now?
<Smerdyakov>
More than a tad experimental.
<flux__>
more useful or more experimental than a tad experimental?-)
<Smerdyakov>
More experimental
<Demitar>
So you're telling me that if I go with Coq I'll never actually produce this game within a useful timeframe? :) (Not that I mind too much.)
<Smerdyakov>
Probably not.
<flux__>
I wonder what kinds of proofs could be used while developing a game..
* zmdkrbou
didn't read what was going on here ... are you trying to code a game using coq ??
<flux__>
"proof for the game being fun" ;)
<Demitar>
flux__: Physics, collision detection and rendering could benefit greatly, the rest probably already is handled well enough by the ML type system already. :)
<Demitar>
(*Could* there are no guarantees it will. :)
<flux__>
coq allows some more interesting types than ocaml, right?
<flux__>
so maybe those could be useful in some programming constructs
<Smerdyakov>
flux__, that's an understatement ("some" more interesting types). :D :D
<Demitar>
It allows more fine grained restrictions on types if nothing else. Consider the int range type etc
<Smerdyakov>
The Coq type system can encode more or less all of math.
<Demitar>
Is this really correct?
<Smerdyakov>
Which?
<flux__>
is coq's type system decidable?
<zmdkrbou>
nope
<Smerdyakov>
flux__, yes, but type inference isn't.
<Smerdyakov>
(Meaning that type _checking_ is decidable)
<Demitar>
Smerdyakov: I wonder what caml it's really outputting.
<Smerdyakov>
Demitar, eh? You can always run Extraction and see for yourself..
<flux__>
I imagine it does some Obj.magic
<Smerdyakov>
flux__, for what?
<Demitar>
Smerdyakov: No, I'm looking at the caml output and it doesn't look quite right. :)
<zmdkrbou>
Smerdyakov: coq can't encode all of math ... it's still intuitionnistic
<flux__>
for expressing things that aren't expressable in ocaml
<Smerdyakov>
zmdkrbou, you can add the law of the excluded middle as an axiom, though I hear there are bad consequences of this. :)
<Demitar>
Coq doesn't use the language native types for many operations?
<zmdkrbou>
Smerdyakov: :D
<Smerdyakov>
Demitar, right. More precisely, it never does unless you ask it to explicitly.
<Demitar>
That explains the ordering of the fold_left arguments. :)
<zmdkrbou>
(and the extraction process produces lots of Obj.magic)
<Demitar>
But still, if that caml is to compile it will need an open ...;; statement or three at the top.
<Smerdyakov>
zmdkrbou, "lots"? I don't remember _lots_.
<Smerdyakov>
Demitar, use "Recursive Extraction" and I think you will find that the code is complete.
<Demitar>
Ah.
<flux__>
are there any plans to make Coq self-hosting?-)
<flux__>
or is it, atleast partially?
<flux__>
I understand it's written in O'caml?
<Demitar>
Hrm...
<Demitar>
let r0 =
<Demitar>
failwith "AXIOM TO BE REALIZED"
<Smerdyakov>
flux__, Xavier Leroy said that he had a student working on something along those lines.
<Smerdyakov>
flux__, namely, an extraction procedure written in Coq with a soundness proof.
<flux__>
that would be nice. after all, who knows what kinds of bugs are lurking in the extraction procedure ;)
<Smerdyakov>
Demitar, how did you define r0?
<Demitar>
So... The real type is not declared?
<Demitar>
Back to the manual. :)
<Smerdyakov>
It shouldn't be surprising that you can't get executable code from a development over the real numbers.
<Smerdyakov>
Since the real numbers don't have computable operations.
<Smerdyakov>
(Even constructive real numbers, maybe? Or at least they're nasty.)
<Demitar>
I wasn't expecting to be able to prove anything using reals, just produce code. I suspected the best way would be to actually switch to ints eventually.
<Demitar>
(s/best/simplest/)
<Demitar>
I wonder if Coq is the right path for me anyway, I've always preferred intuitive proof over formal anyway. :)
<Demitar>
Smerdyakov: I'm confused, how am I supposed to define r0? Isn't it defined in the Reals module?
<Smerdyakov>
Demitar, you can't extract code to OCaml that uses reals.
<Smerdyakov>
Demitar, reals don't have computable operations.
<Demitar>
Ah, now I understand what you're saying. :)
<Demitar>
So the basic datatypes I can extract are integers, sets and lists (all in various forms, shapes and colors).
<Smerdyakov>
You can't extract any "basic datatypes" directly.
<Smerdyakov>
They're all defined from scratch with inductive types.
<Smerdyakov>
There are ways to say that an inductive type should be extracted to use a particular OCaml type, including built-in types.
<Demitar>
Ah.
* Demitar
is slowly starting to grasp how this is supposed to work.
<Smerdyakov>
In fact, there is no good support in mainline Coq for extracting programs that use primitive types. I had to patch it for my own work.