monochrom has quit ["Don't talk to those who talk to themselves."]
mrsolo has joined #ocaml
mrsolo has quit [Remote closed the connection]
mrsolo has joined #ocaml
CosmicRay has quit ["Leaving"]
fab__ has joined #ocaml
mfurr has joined #ocaml
_fab has quit [Read error: 110 (Connection timed out)]
Nutssh has quit [Read error: 110 (Connection timed out)]
Nutssh has joined #ocaml
salo has joined #ocaml
<salo>
can someone see what i intend with "type 'a state = 'a | false;;" and tell me how to do it correctly?
<Smerdyakov>
type 'a state = true of 'a | false
<Smerdyakov>
Or, probably even better, type 'a state = 'a option
<salo>
can you elaborate? i am a total noob. what does "true of 'a
<salo>
" mean?
<Smerdyakov>
I think you should read a tutorial.
<salo>
thanks
<mfurr>
note that it must be True of 'a | False (constructors must start with a capital)
<Smerdyakov>
I wonder why bool doesn't have construtcors True and False.
<mfurr>
language constructs can bind the rules?.... *shrug*\
<mfurr>
err s/bind/bend/
<salo>
perhaps my intent is not clear. i would like state to be either of type 'a, or false.
<mfurr>
the above type will work for that...
<avlondono>
I've never used that ... it sucks, you're overriding true.
<Smerdyakov>
avlondono, mfurr explained why you can't.
* avlondono
tries it
* avlondono
can't use true anymore.
<avlondono>
I can't even let a = true
<Smerdyakov>
Oh, apparently true and false are hardwired to be constructors.
<avlondono>
I wonder why would it make sense at all, no matter if the lenguage let you do such thing.
<mfurr>
it still works for me...
<Smerdyakov>
It makes sense to avoid special cases.
<Smerdyakov>
It's sort of unsavory that true and false are special cases to begin with, though.
<mfurr>
oh, uncapitalized... wierd
<Smerdyakov>
Yet another reason why OCaml is a disgrace. :P
<avlondono>
hehehe
<Smerdyakov>
I'm going to start a list, so I remember all these reasons.
<avlondono>
anyway, /me is off
<avlondono>
and post the list in the topic Smerdyakov :-)
GreyLensman has quit ["Leaving"]
<mfurr>
it makes sense for 'true' and 'false' to be primitive values, but why you can use them as a constructor is definately wierd
<avlondono>
but should be symmetric
<avlondono>
yeah, that's weird, and bad practice also
<Smerdyakov>
No, it makes sense for 'True' and 'False' to be primitive values.
<Smerdyakov>
And I don't mean that.
<Smerdyakov>
It makes sense to have this code always executed:
<Smerdyakov>
type bool = False | True
<Smerdyakov>
Maybe some later code can shadow it, like you can with any other variant type, but 'if' and others always refer to the original.
<Smerdyakov>
That is the SML way.
mfurr has quit ["Leaving"]
salo has quit []
fab__ has quit [Remote closed the connection]
Nutssh has quit ["Client exiting"]
<vincenz>
Anyone here?
<Smerdyakov>
So yeah!
<vincenz>
eoh :)
<vincenz>
hi
<vincenz>
how would I read 4-byte integers from a file written by a c++ program (binary-file)
<vincenz>
and how would I represent numbers in the 0-2**32-1 range (aka unsigned ints)
<Smerdyakov>
For the latter, use Int32.
<vincenz>
I thought it was signed
<Smerdyakov>
For the former, you could always read it a byte at a time and assemble it.
<Smerdyakov>
Oh yeah. I'm not sure what the best way to do that is, then. Int64 would certainly work.
<vincenz>
hmm
<Smerdyakov>
It's Word32 in SML. ;)
<vincenz>
are int64 immediate?
<Smerdyakov>
I think IntXX are always boxed.
* vincenz
nods
<vincenz>
alright, thank you :)
<vincenz>
I have this analysis script in python
<vincenz>
but it's taking 50 minutes
<vincenz>
gonna port to ocaml
<vincenz>
and then work on ocaml from now on
<vincenz>
I originally used python as I thought others might need to fiddle and I wasn't sure as to their preparedness for using ocaml, but my newer scripts will be purely for self-use
vezenchio has joined #ocaml
<vincenz>
so if I'm reconstructing ints...
<vincenz>
I read a byte, shift, read a byte, right?
<vincenz>
first byte is highest byte?
<pango>
that's what I used to process bitmaps, too, don't know if it's optimal...
<vincenz>
so I have two uint64 (fixed-heap-id and block-size) as keys
<vincenz>
anyways
<vincenz>
I was hoping to put the hashedtype module definition inside the class
<vincenz>
but that doesn't work :/
mlh has joined #ocaml
malte has joined #ocaml
malte has left #ocaml []
<vincenz>
How big is the performance hit for using a class that derives from a virtual class?
jrosdahl has quit [Read error: 60 (Operation timed out)]
<Herrchen>
sorry vincenz, had a connection problem ...
<Herrchen>
coudn't connect to my box having irc-client running
<vincenz>
no prob :)
grom358 has joined #ocaml
<grom358>
anyone here?
<vincenz>
hmm
<vincenz>
Herrchen: I need an efficient thingy....
<vincenz>
basically I have a set of active-blocks
<grom358>
hey, do you know if there is an ocaml binding for wxWidgets around?
<vincenz>
where a block spans from a begin-addr to an end-addr
<vincenz>
grom358: there should be, never used them though
<vincenz>
Herrchen: blocks can be added or removed
<vincenz>
Herrchen: and I want an easy way to find out to which block an address belongs
<vincenz>
that last function (lookup) is called OFTEN, and I typically have around a few thousand blocks
<vincenz>
hmm
<vincenz>
nm
<vincenz>
got
<grom358>
are many people using ocaml on windows?
<vincenz>
... got it (damn I'm tired)... I'll use a binary tree, know an implementation of a btree?
<vincenz>
grom358: I used to once, but it's been a whiel
* vincenz
works on linux now
<grom358>
yeah... I wish everyone would switch from windows to linux. Then wouldn't have to worry about writing apps to work on windows
tea has joined #ocaml
<vincenz>
Whats the big diff between hash and map?
<grom358>
in ocaml??
<vincenz>
yeah
<vincenz>
I mean conceptually
<vincenz>
I know one is a btree and the other uses bins
<gl>
hashtbl is not a functionnal structure
<vincenz>
?
<vincenz>
how do you mena?
<vincenz>
..mean
grom358 has quit []
<vincenz>
small question
<vincenz>
I have an array containing tuples
<vincenz>
is it best to do
<vincenz>
match a.(i) with (c,d) -> a.(i) <- (c+1, d)
<vincenz>
given they're tuples of ints
<vincenz>
or
<vincenz>
match a.(i) with (c,d) -> incr c
<vincenz>
given they're tuples of refs to ints
docelic has quit ["goin' home"]
CosmicRay has joined #ocaml
mlh has quit [Client Quit]
srv_ has joined #ocaml
srv has quit [Read error: 232 (Connection reset by peer)]
jrosdahl has joined #ocaml
mayhem has joined #ocaml
<mayhem>
hi
<mayhem>
anyone experienced in Chu spaces ?
mayhem has quit ["Fermeture du client"]
<vincenz>
what are they?
<det>
vincenz: Map is a persistent data structure, Hash is not
<vincenz>
det: ?
<vincenz>
in what sense?
<Smerdyakov>
Let's try that again.
<Smerdyakov>
Maps are immutable. Hash tables are mutable.
<Smerdyakov>
Get it yet?
<vincenz>
oh!
<vincenz>
persistent implies something else
<vincenz>
or my cs terminology knowhow is limited
<Smerdyakov>
It means the same thing in FP parlance.
<det>
vincenz: with a Hash, adding an element mutates the hash, the old version no longer exists, with a Map, adding an element creates a new map that shares parts of the old map, but the old map can still exist
<vincenz>
I know, I know, I get it now :)
<vincenz>
just caugt me offguard with 'persistent'
<det>
I see
<det>
I was trying to make clear the advantages of a Map, rather than the implementation
monochrom has joined #ocaml
<vincenz>
thnx :)
<vincenz>
anyways
<vincenz>
(sorry didn't sleep, worked all night so my iq at the moment is quite low)
<vincenz>
anyways I ported an analysis script I ahd built from python to ocaml
<vincenz>
it took 50 minutes in python
<vincenz>
it takes 2 minutes in ocaml
<vincenz>
:)
<mellum>
vincenz: now try FORTRAN :)
<det>
yeah
<det>
python is teh slow
pangoaway is now known as pango
<Herrchen>
re
<Herrchen>
arg - wlan at uni was really bad today
<Herrchen>
returned home - and away - bye
Herrchen has quit ["bye"]
pango has quit ["Leaving"]
gpciceri has joined #ocaml
pango has joined #ocaml
<jason__>
vincenz: 90% of the bottlenecks in analysis code exists in the semantics themselfs, and not in the compiler.
<jason__>
Or the language. :P
gpciceri has quit ["Leaving"]
<vincenz>
jason__: I didn't change the semantics
<jason__>
.. It's hard not to :p
<jason__>
I've made programs in Ruby that have performed better than Ocaml code I've produced to do similar things. Mostly because a mistake was made between one or the other.
<jason__>
I don't think Ocaml is 25X faster than Python. Probably more like 10, or 15.
<jason__>
Depending on the problem.
mrsolo has quit [Read error: 60 (Operation timed out)]
pattern has quit [Remote closed the connection]
<mattam>
haha, you must have IO-bound problems then
cjohnson has joined #ocaml
tea has quit [Remote closed the connection]
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
_fab has joined #ocaml
mrsolo has joined #ocaml
vezenchio has quit ["None of you understand. I'm not locked up in here with you. YOU are locked up in here with ME!"]
mrsolo_ has joined #ocaml
jason__ is now known as TheDracle
Niccolo has joined #ocaml
<TheDracle>
Hm, val opendbm : string -> open_flag list -> int -> t
<TheDracle>
I give the function the permissions '644' and it for some reason sets the permissions incorrectly on creation.
<TheDracle>
Is it translating the Ocaml 31-bit integer 644 into a 32-bit integer aprorpiately before applying it?
<CosmicRay>
You probably meant 0o644
<CosmicRay>
those bits are usually given in octal
<TheDracle>
Ah.
mrsolo_ has quit [Operation timed out]
<TheDracle>
Okay. How do you know this?
<CosmicRay>
hmm.
<TheDracle>
Just convention?
<CosmicRay>
that's one of those things I've known for so long, I don't remember where I picked it up
<TheDracle>
Lol, okay.
<CosmicRay>
maybe chmod(1)
<TheDracle>
I'm used to using "rw+" or something like that in C/C++
<CosmicRay>
ah yes, chmod(1)
<CosmicRay>
A numeric mode is from one to four octal digits (0-7), derived by
<TheDracle>
Alright.
<TheDracle>
Yeah, with chmod there is usually an enum with different permissions.
<TheDracle>
Okay, thanks :)
<CosmicRay>
yes, there may be one in the Unix module as well
<TheDracle>
Yeah, I was looking around for that.
<TheDracle>
Hm, still giving me the same problem.
<CosmicRay>
you did recompile, right? :-)
<TheDracle>
I can less the db file created, but when I run the program to open it again it throws an exception saying it can't open it.
<TheDracle>
Yeah I did.
<TheDracle>
Before I couldn't do touch on the file.
<CosmicRay>
what reason does it give?
<TheDracle>
Fatal error: exception Dbm.Dbm_error("Can't open file test.db")
<CosmicRay>
bah
<CosmicRay>
can you delete the file and try again?
<TheDracle>
Lol, yeah.
<TheDracle>
Hm, nope. It create it just fine.
<CosmicRay>
At least it's not one of those messages I used to see so often from Perl programmers: "Failure opening foo: Success"
<TheDracle>
Access: (0644/-rw-r--r--)
<TheDracle>
Lol, yeah.
<CosmicRay>
ok, and then can it open it again?
<TheDracle>
It creates it with the right permissions.
<TheDracle>
When I run the executable again, once the file exists, I get that exception.
<TheDracle>
I wouldn't touch perl with a 10 foot pole.
<CosmicRay>
show me the line of code that opens it
mrsolo has quit [No route to host]
<TheDracle>
let myDataBase = opendbm "test.db" [Dbm_rdwr;Dbm_create] 0o644
<CosmicRay>
try removing Dbm_create
<CosmicRay>
you may have discovered a bug in the docs or the implementation if that works
<TheDracle>
Yeah, I tried that, it doesn't work still.
<CosmicRay>
maybe they are mapping Dbm_create to O_CREAT *AND* O_EXCL instead of just O_CREAT
<CosmicRay>
hmm.
<CosmicRay>
that is weird.
<TheDracle>
Yeah, it is.
<CosmicRay>
and you are the user that owns the file?
<TheDracle>
Yes.
<TheDracle>
I can touch and less it.
<CosmicRay>
well I'm out of ideas
<CosmicRay>
try posting to caml-list
<TheDracle>
Yeah, I'll try screwing around with it a bit.
<TheDracle>
Thanks for your help.
<CosmicRay>
oh, try strace
<CosmicRay>
it may tell you what the problem is
<TheDracle>
How good is Dbm as a db?
<TheDracle>
Ah, good idea.
<CosmicRay>
depends on what you're trying to do
<CosmicRay>
what are you trying to do? :-)
<TheDracle>
Hm, maybe because I didn't write anything to it.
<TheDracle>
Since the file is empty throws that exception.
<CosmicRay>
oh, also did you properly close it?
<TheDracle>
Somewhat misleading.
<TheDracle>
No.. My program basically consists of that line.
<TheDracle>
Lol.
<CosmicRay>
Try adding a call to the Dbm close statement :-)
<TheDracle>
Heh, I will.
<TheDracle>
Store a large set of data in a .db file.
<TheDracle>
Like, maybe 16 megs in raw ascii format.
<TheDracle>
So, not huge.
<avlondono>
you need the extension, .db
<avlondono>
to open it
<CosmicRay>
avlondono: no, that gets added automatically
<CosmicRay>
and the extension is not always .db
<TheDracle>
The first argument is the name of the database (without the .dir and .pag suffixes)
<TheDracle>
Right?
<CosmicRay>
that depends on what backend it was compiled with
<CosmicRay>
you are right, thedracle
<avlondono>
well, I always need to _open_ the .db
<TheDracle>
CosmicRay: How good is the access time and such in comparison to say, MySQL?
<avlondono>
but yes, your error is different. so ignore me.
<CosmicRay>
TheDracle: for this, it'll probably be better
<TheDracle>
CosmicRay: Oo..
<CosmicRay>
TheDracle: dbm/gdbm is a very efficient little system
<CosmicRay>
TheDracle: of coruse, it also doesn't have the same power as mysql
<CosmicRay>
TheDracle: you have one key and one value, and both must be strings
<TheDracle>
Right.
<CosmicRay>
TheDracle: there is no sql ehre, etc.
<TheDracle>
Yeah, sql is overrated anyways :p
<CosmicRay>
and of course, this'll be far lighter on resource requirements than any sql system, since you don't have networking code, new processes, SQL engines, etc.
<CosmicRay>
you may also be interested in ocaml-sqlite
<TheDracle>
Yeah.. What about Sqlite?
<TheDracle>
Lol, okay.
<CosmicRay>
heh
<TheDracle>
Yeah, I'll check it out.
<CosmicRay>
I hear it's also very fast
<CosmicRay>
probably not AS fast
<CosmicRay>
but then it does support SQL
<TheDracle>
Yeah, I'm very impressed with the pcre bindings for Ocaml.
<TheDracle>
Ah, good, close does the trick.
<CosmicRay>
now that one *was* documented :-)
<TheDracle>
Believe it or not, this data is for an atmospheric calibration system for a cosmic-ray detector :)
<Niccolo>
hmm, i rewrote myself in ocaml, what do you think?
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
Nutssh has joined #ocaml
Nutssh has left #ocaml []
menace has joined #ocaml
salo has joined #ocaml
Nutssh has joined #ocaml
<salo>
can paramaterized types have more than one paramater? i want "type 'a 'b myType = {foo: 'a; bar: 'b}
cedricshock has joined #ocaml
<Nutssh>
Yup.... 'type ('a,'b) mytype = ....'
<cedricshock>
Anything in ocaml like qt's signals and slots? Say I have Object A. Objects b and c both want to know when object a changes, so they do something like, "yo object a, tell us when you've changed", and object a has something where it can say "Tell everyone who wants to know it that I've changed"
<salo>
nutssh: thanks!
<cedricshock>
Or should I code this up myself since its kind of small?
<Nutssh>
I don't know of any prepackaged library for that. It might be part of the utility functions for gtk.
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
<CosmicRay>
you could just maintain a list of functions to call
<CosmicRay>
and use List.iter to tell them
<cedricshock>
CosmicRay: Oooh - list of functions is better. thanks.
<cedricshock>
I was doing list of objects, and expecting a certain member function. It was preventing me from having objects of a different type subscribe.
lmbdwar has joined #ocaml
<lmbdwar>
hey
<cedricshock>
Stupid newbie question: how do I call a function, throw away its result, then call another function and return its result?
<cedricshock>
Like: (imagine c) printf(blah) ; x = 1 + 3
<Demitar>
Unless f1 actually only returns the unit value in which case ignore is irrelevant.
<cedricshock>
"call a function, throw away its result" -- this ought to tell me it's not a function. Otherwise not calling it would be equivalent.
<cedricshock>
I've spent too much time in #haskell
<cedricshock>
Is unit [] ? Or is there something different from nil for it?
<Demitar>
() : unit
CosmicRay has quit ["Client exiting"]
<cedricshock>
What's wrong with this:?
<cedricshock>
method notify l = match l with
<cedricshock>
[] -> []
<cedricshock>
| head :: tail -> ignore (head); notify tail
<Demitar>
s/method/let/
<cedricshock>
It's in an object.
<Demitar>
Ah.
<cedricshock>
Error is "unbound value notify"
<Demitar>
First of all you're not calling head if you wanted to do that. You'd need to pass it an argument.
<cedricshock>
Unit?
<Demitar>
Whatever you want it to recieve.
<Demitar>
Second you need to make a local recursive function inside the method.
<Demitar>
let rec notify l = ...
<cedricshock>
Why? Methods can't be recursive, or they arn't called this way from in an object, or both?
<Demitar>
I can't recall ever seing a recursive method.
<Demitar>
Third you don't want to do it like that at all. Use List.iter: method notify l = List.iter (fun f -> f <argument>) l
<cedricshock>
Is this correct for list construction: let l = head :: tail ?
<TheDracle>
Hm, yeah, I don't believe you can make recursive methods.
<TheDracle>
I think it makes sense in a way.
<TheDracle>
Since a method is indeed a message being passed to an object.. Message passing recursively is somewhat a misnomer..
<TheDracle>
Just let rec blah val = will do the trick internally.
<TheDracle>
What do you mean cedric? That's one way to construct a list.
<TheDracle>
let l = [head;tail];; would also work.
deknos has joined #ocaml
<TheDracle>
Except it's more like let l = head :: [tail];;
deknos has quit [Client Quit]
<cedricshock>
method subscribe o = subscribers <- o :: subscribers
<cedricshock>
Then later:
<cedricshock>
a#subscribe b
<cedricshock>
Error: The expresion has type (type of b) but here it is used with type unit->unit
<cedricshock>
How did o get restricted to type unit -> unit ?
<cedricshock>
Subscribers was initialized as type unit.
cjohnson has quit [Connection timed out]
<TheDracle>
subscribers <- o returns unit.
<TheDracle>
I wouldn't combine the operations like that.
<TheDracle>
You want to append o to subscribers right?
cjohnson has joined #ocaml
<TheDracle>
Do, (subscribers := o :: subscribers).
<cedricshock>
Which one is cheap, append or prepend?
<TheDracle>
Prepend.
<TheDracle>
Append has to search the list for the last index.
<cedricshock>
That's what I thought. That's what I'm doing.
<TheDracle>
Wait, dereference the list first right.
<TheDracle>
subscribers := o :: !subscribers;;
<cedricshock>
Why do we need to go around dereferencing things?
<cedricshock>
Error: This expression has type 'a list but is here used with type 'b ref
<cedricshock>
I must be doing something subtly wrong:
<cedricshock>
class changingobject name_init =
<cedricshock>
object(self)
<cedricshock>
val mutable subscribers = []
<cedricshock>
val name = name_init
<cedricshock>
method subscribe o = subscribers := o :: !subscribers;
<cedricshock>
method notify l = List.iter (fun f -> f ()) l
<cedricshock>
method changed u = print_endline name; self#notify subscribers
<cedricshock>
end;;
<cedricshock>
<cedricshock>
let a = new changingobject "a";;
<cedricshock>
let b = new changingobject "b";;
<cedricshock>
a#subscribe b#changed;;
<cedricshock>
a#changed;;
<TheDracle>
Hm, I was thinking of it as a ref.
<cedricshock>
It does the same thing with or without the !.
<cedricshock>
[o;subscribers] != o :: subscribers ?
menace has quit [Read error: 110 (Connection timed out)]
<TheDracle>
Well, I think that first one makes subscribers a sublist.
<cedricshock>
That was my guess. And that's what the docs say.
<TheDracle>
I guess the class definition can't have undetermined types.
<cedricshock>
That's the error I get now with things the way i think they should be.
<cedricshock>
How do you explicitly specify a type in something like o ( like unit -> unit )
<cedricshock>
yay !
<cedricshock>
It worked with a bunch of explicit typing added.
<TheDracle>
Right.
<cedricshock>
What does ocaml call templates (classes where types are undetermined, but provided later)?
<TheDracle>
Basically just val mutable subscribes: int list
<TheDracle>
Is the only typing you need to provide.
<TheDracle>
It doesn't really have 'templates' per se. It has generics kindof.
<TheDracle>
It's different than templates though.
<TheDracle>
Templates are more a preprocessor type of action.
mrsolo_ has joined #ocaml
<cedricshock>
Oh darn. I forgot. Functions arn't first class objects in any functional programming language. Oops.
cjohnson has quit [Read error: 110 (Connection timed out)]
cjohnson has joined #ocaml
<TheDracle>
Hm..
<TheDracle>
Objects are very strange.
<TheDracle>
I'd expect that it would check the let statement below the object definition to determine the type of the subscribers list.
<TheDracle>
But it doesn't.
<TheDracle>
let myObj = new changingobject "Hello" in myObj#subscribe 5;
<cedricshock>
this works:
<cedricshock>
class ['a] messenger =
<cedricshock>
object(self)
<cedricshock>
val mutable subscribers = []
<cedricshock>
method subscribe o = subscribers <- (o :: subscribers)
<cedricshock>
method send (m : 'a) = List.iter (fun f -> f m) subscribers
<cedricshock>
end;;
<cedricshock>
<TheDracle>
It still complains that it doesn't know the type of the list.
<cedricshock>
let a = new messenger;;
<cedricshock>
a#subscribe print_endline;;
<cedricshock>
a#subscribe print_endline;;
<cedricshock>
a#subscribe print_endline;;
<cedricshock>
a#send "Hello world";;
<cedricshock>
I followed up on your generics.
<TheDracle>
Hm.
<TheDracle>
Right.
<cedricshock>
It seems silly, since ['a] is only used once - it ought to be able to figure it out
<cedricshock>
I would have guessed that it would go through the object, and for each new type it met add a new type generic thingy to the object. There's no reason it couldn't
<TheDracle>
You basically generify the subscribers list.
<TheDracle>
So that it will replace it with the provided type on creation.
<TheDracle>
But, I would also expect the original to work, and the compiler to be able to determine the type by its use later in the code.
<cedricshock>
I would too. I'd even say its a bug that the language doesn't assign new types to each thing it encounters in an object of undetermined type and try to determine them later, just like it does when I explicitly state that there are undetermined types, and you'll figure them out later.
<TheDracle>
Will infer the type of myList to be an 'int list' by the use of it.
<TheDracle>
Since I append 5 to it, by the later use in the code it is able to determine the type.
<cedricshock>
Here's what really bugs me:
<cedricshock>
print_endline = print_endline;;
<TheDracle>
.. Where is this?
<cedricshock>
No way around this garbage without making a new class of functions and building the whole language again inside itself.
<cedricshock>
Oops. I take it all back. It works with ==
monochrom has quit ["Don't talk to those who talk to themselves."]
<TheDracle>
Hm, There has to be some way around this..
<TheDracle>
It's just stupid that the type inferance mechanism doesn't figure out the type via the method call later.
<TheDracle>
Maybe if I included it in a separate module or something.
<cedricshock>
I agree. I'd say it's a bug. Suggested fix: for each undetermined type, treat it as iff it was specified alla class ['a] .... later explicit decleration. Replace error message with warning at compile time.
<TheDracle>
I'll have to look into this further, maybe there's a reason.
<cedricshock>
Is there a function return this list with this member removed ?
<cedricshock>
Like drop(list, item)?
<TheDracle>
Um, they're linked lists.
<TheDracle>
Look in the "List" module.
<cedricshock>
I know. It would scan the list till it found a match, then drop it.
<cedricshock>
Oh well. I can write it myself.
<TheDracle>
Well, technically they aren't mutable lists.
GreyLensman has joined #ocaml
<TheDracle>
Probably grab the sublist to that element, and the sublist after than element and use @.
<cedricshock>
We add to lists, and they arn't mutable. It's done by constructing a new list.
<cedricshock>
What's with this:?
<cedricshock>
let rec drop l i =
<cedricshock>
match l with
<cedricshock>
[] -> []
<cedricshock>
| i :: tail -> tail
<cedricshock>
| head :: tail -> head :: drop tail i;;
<cedricshock>
Warning: this match case is unused.
<cedricshock>
Case highlighted is head :: tail
<cedricshock>
Many lists can't match either [] or i :: tail, unless i is an unbound variable.
<Smerdyakov>
Patterns don't check equality with existing variables.
<Smerdyakov>
Every variable occurrence declares a new pattern variable.
<cedricshock>
Then what use are they?! They only check against the anonymous variable and constants, but not existing variables!?
<Smerdyakov>
Pattern matching in OCaml is syntactic sugar over a very basic case analysis construct.
<Smerdyakov>
Its only function is to deconstruct variant types.
<cedricshock>
And to assign to unassigned variables, if I have my guessing right.
<Smerdyakov>
Deconstruction includes getting access to the values contained within constructors.
<cedricshock>
But it doesn't do comparison against existing non-constants because of the subtle difference between = and == and = is what everyone would guess, but isn't meaningful for all types because the language (and all other functional languages if found) doesn't treat functions as first class objects, right?
<cedricshock>
s/if/I've
<pango>
because the "usual meaning" of two functions being equal isn't always computable
<pango>
so better not give the false impression isn't doable
<Smerdyakov>
Pattern matching is syntactic sugar for the absolute minimal language support needed to read variants.
<Smerdyakov>
Equality checking with existing values is not needed for this.
<cedricshock>
I know. In fact it's uncomputable (simple proof from halting problem - got some guys name that starts with an R associated with it)
<pango>
but you can use | x :: tail when x = i -> or | x :: tail when x == i ->, etc.
<cedricshock>
Fun thing to do is use the algorith - proof isomorphism to show that either his proof is wrong or his proof is trivial. The correct interpretation IMHO is that both his porrf and the whole issue of the halting problem are trivial.
<Smerdyakov>
cedricshock, can you be more specific about what you mean?
<cedricshock>
pango: Yeah, I guess seperating out the boolean logic is alright.
<cedricshock>
Here: I'll give you the theorem and the proof:
<Smerdyakov>
cedricshock, I know the theorem and I know the proof.
<cedricshock>
The theorem is that no program can be made that will determine something non trivial about any other program.
<cedricshock>
Cool!
<Smerdyakov>
cedricshock, I'm interested in what you mean about applying "the algorith - proof isomorphism."
<Smerdyakov>
(I know what the Curry-Howard Isomorphism is. It's central to my research.)
<cedricshock>
It's not really an isomorphism, it's a misnomer.
<Smerdyakov>
How not?
<cedricshock>
It's the proof that if you have a proof of something, it is the same as having a program that will do it, and vica-versa.
cjohnson has quit [Read error: 110 (Connection timed out)]
cjohnson has joined #ocaml
<Smerdyakov>
How is there not an isomorphism?
<cedricshock>
So we accept for a moment that any proof is also a list of instructions for demonstrating something, and a list of instructions for doing something is a proof that it can be done.
<Smerdyakov>
There is a one-to-one, onto correspondence between proofs and programs.
<cedricshock>
I highly doubt that it can be written in a 1-1 and onto manner. It's probably a *morphism, but I highly doubt, that in my non-rigourous interpretation it is an isomorphism.
<cedricshock>
Cool!
<cedricshock>
So we start here:
<Smerdyakov>
I take it you've never used Coq.
<cedricshock>
A proof: No program can determine anything non trivial about another program.
<Smerdyakov>
Oh, no, that's far too informally specified.
<cedricshock>
Yeah, in a finite amount of time, etc, and what non-trivial means.
<Smerdyakov>
No. You have to define what a "program" is, as well.
<Smerdyakov>
You need a model of computation.
<cedricshock>
Give me your formal version.
<Smerdyakov>
Slightly more formal, but good enough for me: No Turing Machine can determine anything non-trivial about Turing Machines it is given as input.
<cedricshock>
Ok. Now let's take that statement.
<Smerdyakov>
The Curry-Howard Isomorphism, on the other hand, deals with, say, ML programs.
<cedricshock>
It is a proof, so there must be some turing-machine program that it is.
<Smerdyakov>
Not Turing Machines.
<cedricshock>
But we can show that any ML program can be made into a turing machine program, no?
<Smerdyakov>
But not every TM can be made into an ML program
<Smerdyakov>
In a suitable way.
<Smerdyakov>
It's the typechecking in the source language that makes C-H work.
<Smerdyakov>
TM's just don't cut it.
<cedricshock>
That's ok. I think I only need to go the one way.
<Smerdyakov>
Multiple ML programs can be made into the same TM.
<cedricshock>
So we can rewrite (Read's?) theorem as a turing machine program.
<Smerdyakov>
OK.
<Smerdyakov>
(Rice's)
<cedricshock>
Now it is a turing machine that looks at other turing machines and determines about them "You do not say anything non-trivial about other turing machine programs."
GreyLensman has left #ocaml []
<Smerdyakov>
And such a TM exists.
<Smerdyakov>
It's trivial.
<Smerdyakov>
It always outputs "NO."
<cedricshock>
Exactly
<cedricshock>
That's why I'm claiming that Rice's theorem is trivial.
<cedricshock>
Otherwise it violates itself.
<Smerdyakov>
Something is not right here
<cedricshock>
Nope.
<cedricshock>
A turing machine that always outputs no is trivial.
<Smerdyakov>
That is correct.
<Smerdyakov>
But that does not correspond with Rice's Theorem in any meaningful way.
<cedricshock>
That's all Rice's theorem is. Rice's theorem tells us something thats not obvious, but, using its own definition of trivial, is trivial.
<Smerdyakov>
But every theorem is trivial, using your definition, which shows me that your definition of "trivial" is useless.
<cedricshock>
It's definition of trivial would say that knowing anything that is true is trivial, no matter how interesting or surprising it is to us.
<Smerdyakov>
I don't see how the Curry-Howard Isomorphism figures into this at all.
<Smerdyakov>
Rice's Theorem immediately lets us see that the language of TM's deciding the halting problem is trivial.