<ppsmimou>
associativity of multiplication must be part of the stdlib
<ppsmimou>
err commutativity
<ppsmimou>
mult_comm
<ppsmimou>
I would do something like
<ppsmimou>
intro m.
<ppsmimou>
apply (mult_comm m (S n)).
<ppsmimou>
hum not apply, exact.
<lmbdwr>
ppsmimou, it is indeed but I want to proove it by myself
<ppsmimou>
(I haven't touched coq for ages)
<ppsmimou>
Lemma mult_comm : forall n m, n * m = m * n.
<ppsmimou>
Proof.
<ppsmimou>
intros; elim n; intros; simpl in |- *; auto with arith.
<ppsmimou>
elim mult_n_Sm.
<ppsmimou>
elim H; apply plus_comm.
<ppsmimou>
Qed
<ppsmimou>
(sorry for the flood)
<ppsmimou>
its the proof of the stdlib
AJC has left #ocaml []
b00t has joined #ocaml
<lmbdwr>
ppsmimou,
<lmbdwr>
Ive seen it
<lmbdwr>
but as I mentioned
<lmbdwr>
it uses a nice
<lmbdwr>
auto with arith
<lmbdwr>
:)
<lmbdwr>
so this proofs is based on the hints of the stdlib already
ktne has joined #ocaml
<ktne>
hello
b00t has quit [Remote closed the connection]
batdog|gone is now known as batdog
Leonidas has joined #ocaml
<dbueno>
Is there anything like SML's CM in the works for OCaml
<dbueno>
?
* dbueno
hopes so.
<ktne>
what is sml's cm?
<ktne>
sorry, i'm a beginner :)
mikeX has quit [Read error: 145 (Connection timed out)]
jewel has quit [Read error: 110 (Connection timed out)]
mikeX has joined #ocaml
<ktne>
i have a question
<ktne>
i have defined a max function like this:
<ktne>
let max x y = if x>y then x else y;;
<ktne>
max 2 3.0 is wrong
<ktne>
but is this detected at runtime or compile time?
<ktne>
does ocaml compile two versions automatically? one for integers and one for floats?
<mikeX>
ktne: at compile time
<ktne>
i see
<ktne>
how one question
<ktne>
what's the type of ( > ):
<mikeX>
ktne: ocaml is very strictly typed, so passing ints and floats at the same time will cause a type error
<flux__>
ktne, you can ask ocaml
<flux__>
( > );;
<mikeX>
i suppose 'a 'a -> 'a
<ktne>
why?
<ktne>
oh
<mikeX>
oh bool, yes
<ktne>
huh
<ktne>
got it now :)
<mikeX>
- : 'a -> 'a -> bool = <fun>
<ktne>
why isn't + the same?
<mikeX>
it is : )
<ktne>
why you need a separate + and +. when you could have + as 'a -> 'a?
<mikeX>
+ does not work for floats
<mikeX>
oh, that's not the same
<ktne>
why it doesn't work for floats?
<mikeX>
lol (stupid mode on today i guess)
<flux__>
ktne, because then the type system would accept (fun _ -> ()) + (fun _ -> ())
<ktne>
(+);; is int->int->int
<ktne>
flux__ hmm, what's wrong with that?
<flux__>
ktne, you can't add functions together
<flux__>
or network sockets or threads or..
<ktne>
but you can compare functions?
<ktne>
like fun > fun?
<flux__>
actually that's a runtime error
<flux__>
but, yes
<ktne>
yes i get an exception at runtime
<ktne>
i find this confusing
<ktne>
why aren't they consistently treated?
<flux__>
so you would rather + work on everything?
<ktne>
no, but i would have > and >.
<ktne>
or 2.> :)
<flux__>
well, I suppose you will want to compare many things to each other
<flux__>
while I think only functions are something you cannot compare
<dbueno>
ktne: How would you define function comparison?
<dbueno>
Or pick an "easier" problem: how would you define equality on functions?
<flux__>
well, I suppose you could just do physical comparison
<ktne>
if for same input they have same output
<flux__>
ktne, unfortunately that's not possible to decide
<dbueno>
ktne: How would you test the function (+)?
<dbueno>
Run it on every integer?
<ktne>
if funa > funb then funa takes all arguments funb takes and more
<ktne>
the < is the reverse
<ktne>
but this is not ordered i guess
<dbueno>
As fluk__ says, these are undecidable questions. See: halting problem.
<dbueno>
flux__, sorry. =]
<dbueno>
Unrelated question, for anyone: is there a way to get parameter names into ocamldoc html output generated from an .mli file?
duncanm has joined #ocaml
<duncanm>
has anyone looked into F# here?
chessguy has joined #ocaml
<duncanm>
actually
<duncanm>
i can't figure out how to use the option type
<dbueno>
duncanm: Ask a specific question.
<duncanm>
i have something like
<duncanm>
let x = None;
<duncanm>
x = Some(3);;
<duncanm>
that doesn't work, how do i fix that?
<dbueno>
You can't assign to x.
<dbueno>
In OCaml, if you want to assign to a variable, it must have a "ref" type.
<duncanm>
and i use the !x to get its value, right?
<dbueno>
let x = ref None;;
<dbueno>
x := Some 3;;
<duncanm>
ah
<dbueno>
Yes.
ktne has quit []
kryptt has joined #ocaml
lmbdwr is now known as mayhem
<pango>
actually ktne asked a good question, those polymorphic inequality functions are hackish
<pango>
you can't overload them for your own types (if their default behavior doesn't satisfy your needs), so at that point you'll need to pass your own relation definition around...
<dbueno>
pango, Agreed. I had to define an AST comparator recently, to test whether two ASTs were structurally similar.
<dbueno>
It would have been nice to overload (=) and split out the cases where it barfs due to "abstract value" (I am using bignums).
chessguy has quit [" HydraIRC -> http://www.hydrairc.com <- IRC for those that like to be different"]
<flux__>
I suppose it would be performance issue if every object just had a comparator function attached..
<pango>
they probably thought that requiring functorized interfaces, ala Set.Make, was too heavyhanded for simple uses... at the expense of language/implementation purity :/
<pango>
flux__: actually there's a huge cost attached to those polymorphic comparators (dynamic typing, anyone ?)
<flux__>
that true, but the cost I mentioned would be there even if you never used them?
<flux__>
atlest 4 bytes extra for each object?
TaXules has quit [Remote closed the connection]
<pango>
You don't need such things in types are defined thru modules instead of objects, no ?
<flux__>
if the objects you want to compare aren't of type 'a, you can compare efficiently
TaXules has joined #ocaml
<pango>
like, declare a module of signature OrderedType for each different type you want to use inequality functions on
<flux__>
would sort : 'a list -> 'a list then work, efficiently?
<flux__>
or do you mean that each such function would be first instantiated from their module with your OrderedType-parameter?
<pango>
I guess that that would be the price to pay, yes
<flux__>
well, you can always redefine (<) if you want :)
<flux__>
although I suppose it would be risky, if you have a missing 'open' and you'll fall back into using ocaml's (<) ..
<pango>
also you can't redefine it for existing modules
<pango>
I'm not sure they're examples in standard lib however
<flux__>
true
<flux__>
but it's unrealistic to expect they would just work anyway with that new model
<flux__>
;)
<pango>
Sets are functorized, List.sort and Array.sort ask for the comparator to use,..
<flux__>
some kind of module-inference would be nice
<flux__>
if would automatically construct the modules you need ;)
<pango>
actually, the standard library is open for functorized use
<pango>
Char, Int32, Int64, Map, Nativeint, Set, all have a compare : t -> t -> int function
<pango>
(where is float btw ?)
<flux__>
int and bool are missing too?
<pango>
int = Nativeint
<flux__>
oh, right
<flux__>
hmm, really?
<flux__>
native ints are something like 42n
<pango>
mmmh
<pango>
so int is missing too ? :/
<flux__>
I think Char is there by coincidence, a place to have .code .code etc :)
<pango>
"almost consistant by coincidence" :)
Smerdyakov has quit ["Leaving"]
smimou has joined #ocaml
mikeX_ has joined #ocaml
mikeX has quit [Read error: 145 (Connection timed out)]
Nutssh has joined #ocaml
DRMacIver has left #ocaml []
jajs has joined #ocaml
postalchris has joined #ocaml
Leonidas has quit ["An ideal world is left as an exercise to the reader"]
shawn has joined #ocaml
mayhem is now known as maayhem
pango has quit ["Leaving"]
pango has joined #ocaml
duncanm has quit [Read error: 110 (Connection timed out)]
bluestorm has joined #ocaml
mikeX has joined #ocaml
duncanm has joined #ocaml
chessguy has joined #ocaml
mikeX_ has quit [Connection timed out]
jajs has quit ["Leaving"]
duncanm_ has joined #ocaml
duncanm has quit [Read error: 104 (Connection reset by peer)]
_fab has quit [Read error: 104 (Connection reset by peer)]
_fab has joined #ocaml
_JusSx_ has joined #ocaml
_JusSx_ has quit ["leaving"]
Snark has quit [Remote closed the connection]
<duncanm_>
anyone looked into F# here?
duncanm_ is now known as duncanm
<duncanm>
i tried 'let x = ref None;;'
<duncanm>
and it says
<duncanm>
error: FS0030: Value restriction. Type inference has inferred the signature
<duncanm>
val x : 'a option ref
<duncanm>
but its definition is not a simple data constant. Either define 'x' as a simple data term, make it a function, or add a type constraint to instantiate the type parameters.
<dbueno>
What type of data are you going to put in the option?
<Poopsmith>
duncanm: See, it can't infer what type the option is.
<Poopsmith>
Since None doesn't indicate what the 'a becomes.
<Poopsmith>
(Since the option type is defined polymorphically.)
<Poopsmith>
So you can either make it explicit by adding a type signature, or write enough code that you use the Some type and it can do inference properly./
<Poopsmith>
"It" being the compiler.
<dbueno>
duncanm: Try: let : Form option = None
<Poopsmith>
let x : Form option = None, he means. ;)
<dbueno>
Exactly that. =] Thanks, Poopsmith.
<dbueno>
Hm... never thought I'd say those words.
<duncanm>
error: FS0001: This expression has type
<duncanm>
Form option
<duncanm>
but is here used with type
<duncanm>
'a ref
<pango>
dbueno: you forgot the 'ref'
<kryptt>
n
<dbueno>
let x : Form option ref = ref None
<pango>
let x = ref (None : Form option)
<Poopsmith>
Ooh, yeah.
<Poopsmith>
Or let x : Form option = ref None
<Poopsmith>
Forgot about that part.
<Poopsmith>
this is nice. It's like collaborative coding.
<dbueno>
Poopsmith: Form option ref.
<Poopsmith>
I'll write one line and ten people will eventually realize what I meant and debug me.
<Poopsmith>
Yes, that!
<duncanm>
heh
<Poopsmith>
It's worth noting that I just spent ages debugging a function in F# that, it turned out, I'd accidentally used the type name instead of the variable name of a given argument in.
<Poopsmith>
*sigh*
jajs has joined #ocaml
<duncanm>
ah
<duncanm>
Poopsmith: you're toying with F# too?
<Poopsmith>
duncanm: Actually, using it for work. :)
<duncanm>
oh nice
<Poopsmith>
Yeah.
<duncanm>
so, let graph : Form option ref = None?
<Poopsmith>
It's certainly robust enough for production use, IMO.
<duncanm>
error: FS0001: This expression has type 'a option
<duncanm>
but is here used with type Form option ref
<Poopsmith>
You still have to do ref None
<duncanm>
ha
<duncanm>
and then later, graph := Some(new Form())
<Poopsmith>
# let x : int option ref = ref None;;
<Poopsmith>
val x : int option ref = {contents = None
<duncanm>
oh, that's kinda annoying, cuz by doing that
<duncanm>
everytime i wanna access something in the form, i have to do !x
<duncanm>
i suppose i could cop out and just say let x = null
<Poopsmith>
Well, that's the problem with using refs.
<Poopsmith>
IF it's a problem.
<duncanm>
how do i go from 'a option back to 'a?
<Poopsmith>
You can do pattern matching on it.
<duncanm>
!x just gets rid of the ref
<duncanm>
oh
<Poopsmith>
Right.
<duncanm>
is that the only way?
<Poopsmith>
Like match x with Some(y) -> use y
<Poopsmith>
| None -> flip out because we don't want to be here
<Poopsmith>
Well, why would you not want to match on it? What if it happens to be a None? :)
<Poopsmith>
As far as I know, there is no other way, but more importantly, why would you want there to be?
<Poopsmith>
I don't think you could do it any other way and be typesafe.
<Poopsmith>
The type signature doesn't guarantee which constructor was used, after all.
<Poopsmith>
So you have to match all possible constructors (well, you don't, but the compiler will warn you if you aren't).
<Poopsmith>
So I guess you could do it explicitly (like, "I know this is a Some so give me the value").
<Poopsmith>
You could even write a function that does it.
<Poopsmith>
let getVal (Some(x)) = x
<Poopsmith>
But, again, what about runtime matching errors now?
<Poopsmith>
(So scratch what I said about typesafety, because you can do it.)
<Poopsmith>
(And there may be a built-in function that does the above. I don't really know.)
<pango>
that will raise a matching failure exception
<Poopsmith>
Right.
<pango>
and with ocaml you'll get a warning at compile time, too
<Poopsmith>
I said that. :)
<Poopsmith>
That's why you want to use matching whenever you want to get the value out of an option type. Because otherwise, why are you using the option type?
<Poopsmith>
Unless you'd rather throw an exception and use exception handling for control flow, but that's slow.
<pango>
I shouldn't be switching between IRC and other tasks ;)
clog has joined #ocaml
<romildo>
I have been told that ocaml compiled programs are very efficient, some times as efficient as or more efficient than C programs.
<Poopsmith>
Stylistically, they're good when you want a separate function to handle the error of this function, somewhere farther down the call stack, and you don't want to guarantee that it'll know to check for some sort of error-indicating return value (like -1).
<Poopsmith>
But I'm sort of getting a bit pedantic.
<Poopsmith>
romildo: Of course it all depends on the program, but I've been told the same thing.
jajs has quit [Read error: 110 (Connection timed out)]