Camllist Digest, Vol 28, Issue 11
 camllistrequest@y...
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  camllistrequest@y... 
Subject:  Camllist Digest, Vol 28, Issue 11 
Send Camllist mailing list submissions to camllist@yquem.inria.fr To subscribe or unsubscribe via the World Wide Web, visit http://yquem.inria.fr/cgibin/mailman/listinfo/camllist or, via email, send a message with subject or body 'help' to camllistrequest@yquem.inria.fr You can reach the person managing the list at camllistowner@yquem.inria.fr When replying, please edit your Subject line so it is more specific than "Re: Contents of Camllist digest..." Today's Topics: 1. Re: Unsoundness is essential (skaller) 2. Re: Locallypolymorphic exceptions [was: folding over a file] (oleg@pobox.com) 3. Re: Unsoundness is essential (Brian Hurt) 4. Re: Unsoundness is essential (Christophe Raffalli) 5. Re: Unsoundness is essential (Arnaud Spiwack)  Message: 1 Date: Thu, 04 Oct 2007 11:52:04 +1000 From: skaller <skaller@users.sourceforge.net> Subject: Re: [Camllist] Unsoundness is essential To: "Joshua D. Guttman" <guttman@mitre.org> Cc: camllist@inria.fr MessageID: <1191462724.7542.76.camel@rosella.wigram> ContentType: text/plain On Wed, 20071003 at 19:28 0400, Joshua D. Guttman wrote: > skaller <skaller@users.sourceforge.net> writes: > > > Goedel's theorem says that any type system strong enough > > to describe integer programming is necessarily unsound. > > Are you sure that's what it *says*? I thought I remembered > it stated differently. I paraphrased it, deliberately, in effect claiming an analogous situation holds with type systems.  John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net  Message: 2 Date: Wed, 3 Oct 2007 19:16:49 0700 (PDT) From: oleg@pobox.com Subject: [Camllist] Re: Locallypolymorphic exceptions [was: folding over a file] To: kirillkh@gmail.com Cc: camllist@inria.fr MessageID: <20071004021649.96554A99F@Adric.metnet.fnmoc.navy.mil> > Could you be more specific regarding the continuations' performance impact? > Would it matter in practice? Would you recommend using this function in a > generalpurpose library instead of the imperativestyle implementation that > was suggested? For use in practice (including ocamlopt  the case delimcc does not yet support: I should really fix that) one should probably `inline' the implementation of abort into the code of fold_file. The result will _literally_ be the following: exception Done (* could be hidden in a module *) let fold_file (file: in_channel) (read_func: in_channel>'a) (elem_func: 'a>'b>'b) (seed: 'b) = let result = ref None in let rec loop prev_val = let input = try read_func file with End_of_file > result := Some prev_val; raise Done in let combined_val = elem_func input prev_val in loop combined_val in try loop seed with Done > (match !result with Some x > x  _ > failwith "impossible!") ;; (* val fold_file : in_channel > (in_channel > 'a) > ('a > 'b > 'b) > 'b > 'b = <fun> *) let line_count filename = let f = open_in filename in let counter _ count = count + 1 in fold_file f input_line counter 0;; (* val line_count : string > int = <fun> *) let test = line_count "/etc/motd";; (* val test : int = 24 *) It should be noted the differences from the previous imperative solutions: the reference cell result is written only once and read only once in the whole folding  namely, at the very end. The reference cell is written to, and then immediately read from. The bulk of the iteration is functional and tail recursive. The use of mutable cell is the trick behind typing of multiprompt delimited continuations. One may even say that if a type system supports reference cells, it shall support multiprompt delimited continuations  *and vice versa*. > Also, is there a good manual on delimited continuations for a beginner with > minimum of external references? Perhaps the most comprehensive and selfcontained paper on delimited continuations is A static simulation of dynamic delimited control by Chungchieh Shan http://www.cs.rutgers.edu/~ccshan/recur/recurhoscfinal.pdf I have heard some people have found the introduction section of http://okmij.org/ftp/Computation/Continuations.html#contextOS helpful. Please note Christopher Strachey's quote on the above page. It was said back in 1974! Here's another quote from the same Strachey and Wadsworth's paper: Those of us who have worked with continuations for some time have soon learned to think of them as natural and in fact often simpler than the earlier methods. Christopher Strachey and Christopher P. Wadsworth, 1974.  Message: 3 Date: Wed, 3 Oct 2007 22:35:57 0400 (EDT) From: Brian Hurt <bhurt@spnz.org> Subject: Re: [Camllist] Unsoundness is essential To: skaller <skaller@users.sourceforge.net> Cc: "Joshua D. Guttman" <guttman@mitre.org>, camllist@inria.fr MessageID: <Pine.LNX.4.64.0710032230000.28993@localhost> ContentType: TEXT/PLAIN; charset=USASCII; format=flowed On Thu, 4 Oct 2007, skaller wrote: > On Wed, 20071003 at 19:28 0400, Joshua D. Guttman wrote: >> skaller <skaller@users.sourceforge.net> writes: >> >>> Goedel's theorem says that any type system strong enough >>> to describe integer programming is necessarily unsound. >> >> Are you sure that's what it *says*? I thought I remembered >> it stated differently. > > I paraphrased it, deliberately, in effect claiming an analogous > situation holds with type systems. > I'm not sure that's correct I thought it was that any type system sufficiently expressive enough (to encode integer programming) could not be gaurenteed to be able to be determined in the general case that the type checking algorithm could not be gaurenteed to halt, in other words, and the computing equivelent of Godel's theorem is the halting problem. The dividing line, as I understand it, is nonprimitive recursion. So Ocaml's type system, which is not Turing complete, is gaurenteed to terminate eventually (it may have regretable bigO behavior, including an nasty nonpolynomial cost algorithm for unification, but it will complete if you let it run long enough, which may be decades...). Haskell's type system, by comparison, is Turing complete, so it's not gaurenteed to ever halt/terminate in the general case. One advantage Haskell has over Ocaml is that Haskell has a Turing complete type system on the other hand, one advantage Ocaml has over Haskell is that Ocaml doesn't have a Turing complete type system... :) I am not an expert, tho. Brian  Message: 4 Date: Thu, 04 Oct 2007 09:46:53 +0200 From: Christophe Raffalli <christophe.raffalli@univsavoie.fr> Subject: Re: [Camllist] Unsoundness is essential To: skaller <skaller@users.sourceforge.net> Cc: camllist@inria.fr MessageID: <47049A6D.6020201@univsavoie.fr> ContentType: text/plain; charset="iso88591" skaller a écrit : > On Wed, 20071003 at 19:28 0400, Joshua D. Guttman wrote: >> skaller <skaller@users.sourceforge.net> writes: >> >>> Goedel's theorem says that any type system strong enough >>> to describe integer programming is necessarily unsound. > > I paraphrased it, deliberately, in effect claiming an analogous > situation holds with type systems. > Not unsound, incomplete ! you mixup first and second incompleteness theorem. Let's clarify ?  first if a type system does not contain arithmetic nothing can be said (this implies ML), but in this case, the meaning of complete needs to be clarified. Indeed, there are complete type system ...  The 1st incompleteness theorem states that no theory containing arithmetic is complete. This means that there will always be correct programs that your type system can not accept. However, I thing a real program that is not provably correct in lets say ZF, does not exists and should be rejected. you do not accept a program whose correctness is a conjecture (do you ?)  The second incompleteness theorem, states that a system that proves its own consistency is in fact inconsistent. For type system (strong enough to express arithmetic, like ML with dependant type, PVS, the future PML, ..). This means that the proof that the system is consistent (the proof that "0 = 1 can not be proved") can not be done inside the system. However, the proof that your implementation does implement the formal system correctly can be done inside the system, and this is quite enough for me.  The soundness theorem for ML can be stated as a program of type "int" will  diverge  raise an exception  or produce an int I think everybody except LISP programmers ;) want a sound type system like this. OK replace everybody by I if you prefer ... For PML, we are more precise : exception and the fact the a program may diverge must be written in the type.  ML type system is sometimes too incomplete, this is why the Obj library is here. However, the use of Obj is mainly here because ML lacks dependant types. In fact, the main use of Obj is to simulate a map table associating to a key k a type t(k) and a value v:t(k).  All this says that a typesystem only accepting proved programs is possible and a good idea (it already exists). The question for researcher is how to produce a type system where the cost of proving is acceptable compared to the cost of debugging, and this stars to be the case for some specific application, but we are far from having to remove the word "bug" from our vocabulary ;)  Christophe Raffalli Universite de Savoie Batiment Le Chablais, bureau 21 73376 Le BourgetduLac Cedex tel: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univsavoie.fr www: http://www.lama.univsavoie.fr/~RAFFALLI  IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature. The public key is stored on www.keyserver.net   next part  A nontext attachment was scrubbed... Name: signature.asc Type: application/pgpsignature Size: 252 bytes Desc: OpenPGP digital signature Url : http://yquem.inria.fr/cgibin/mailman/private/camllist/attachments/20071004/2148e899/signature.pgp  Message: 5 Date: Thu, 04 Oct 2007 10:56:08 +0200 From: Arnaud Spiwack <aspiwack@lix.polytechnique.fr> Subject: Re: [Camllist] Unsoundness is essential To: camllist@inria.fr MessageID: <4704AAA8.9080602@lix.polytechnique.fr> ContentType: text/plain; charset=ISO88591; format=flowed Hi everybody, Christophe already said much of what I have to do, but it's compulsively impossible to me to avoid posting on such a thread. My own psychopathologies coerce me into meddling into here. First of all, as some sort of an introductory thing, I'd like to mention that Java is probably the currently most popular language among programmers, and it's strongly typed. Indeed, there are quite a few unsafe feature (null pointers, down casting), but they are gradually removed (well, I guess null pointers won't ever): since the addition of generics wild downcasting to use generic structures is largely deprecated, if one would provide with a primitive ternary guarded cast operator, one wouldn't have to resort to write it by hand "if (blah.isClass...", etc... Anyway, back to Mr. Gödel and his theorem. What he stated indeed is that truth and provability never coincide (provided we're talking of something at least as expressive as arithmetic). That is, as some people already mentionned: either everything can be proved, or there is at least a statement A such that neither A is provable neither its negation. Still there is something peculiar in the interpretation of Gödel theorem, since if we are in a classical logical system (where ~~A (not not A) and A are equivalent). If neither A nor ~A are provable, then both can be "the real one". By that I mean that both can be chosen as true, without impacting the consistency of the system (quick proof sketch : A > ~A is equivalent to A > (A > False) which is equivalent to A&A > False wich is equivalent to ~A). A conclusion I can draw from that is that we don't care about what is true, we care about what is provable, since it is at least welle defined, where truth is very much unclear (an example of such weirdness is the axiom of choice, which is a very pratical axiom in classical mathematics, and widely accepted. Except when you are doing probabilities where it is very convenient to have the "measurability axiom" stating that "everything is mesurable" (more or less) and which contradicts the axiom of choice). Now let's move to programming again. Type systems can be arbitrarily complex, see for instance, Coq, Agda2, Epigram, PML and many other that I'm less familiar with. In this language, evidences show that everything one needs to prove for proving a program (partially) correct, is provable. There we must draw a clear line between two concept which have been a bit mixed up in this thread : provability and decidability. Of course, it is not possible to decide in all generality that whoever integer is nonzero, thus a type system able to express (int > int{0} > int) as a type for division cannot decide type checking without extra information. The extra information is no more than a proof that we never provide an 0valued integer (at each application). And curryhoward isomorphism allows to stick it inside the type system. That's what Type Theorist yearn for (by the way that is cool because many runtime check consume time unneedlessly, and time is money, and money is precious). Of course, there is still a lot of work to do around these. But this is more than promissing, and one should be able to never need unsafe features (though there actually is a more or less unsafe feature inherently in these type systems, it's called "axioms", since you can generaly enhance the theory with any additional claim. However axioms are usually kept out of very sensitive areas). At any rate, this does not say anything about the mostly untype languages. It is a different issue, typed vs untyped or decidable type inference vs more expressiveness in type system. The untyped world has its perks, especially C, which allow quite a few low level manipulation which are very useful. What I mean here is that if we need types (and I believe that a vast majority of programming application do), then we should have as expressive typing as possible, and not need to rely on unsafe feature which give headaches and segfaults. I realize that I got lost in my way, so I'll stop here, but I may be back (this is a much more prudent claim than that of another AS) in followups ;) . Arnaud Spiwack Christophe Raffalli a écrit : > skaller a écrit : > >> On Wed, 20071003 at 19:28 0400, Joshua D. Guttman wrote: >> >>> skaller <skaller@users.sourceforge.net> writes: >>> >>> >>>> Goedel's theorem says that any type system strong enough >>>> to describe integer programming is necessarily unsound. >>>> >> I paraphrased it, deliberately, in effect claiming an analogous >> situation holds with type systems. >> >> > > Not unsound, incomplete ! > you mixup first and second incompleteness theorem. Let's clarify ? > >  first if a type system does not contain arithmetic nothing can be said > (this implies ML), but in this case, the meaning of complete needs to be clarified. > Indeed, there are complete type system ... > >  The 1st incompleteness theorem states that no theory containing > arithmetic is complete. This means that there will always be correct programs > that your type system can not accept. However, I thing a real program that > is not provably correct in lets say ZF, does not exists and should be rejected. > you do not accept a program whose correctness is a conjecture (do you ?) > >  The second incompleteness theorem, states that a system that proves its own > consistency is in fact inconsistent. For type system (strong enough to express > arithmetic, like ML with dependant type, PVS, the future PML, ..). This means > that the proof that the system is consistent (the proof that "0 = 1 can not be proved") > can not be done inside the system. However, the proof that your implementation > does implement the formal system correctly can be done inside the system, and > this is quite enough for me. > >  The soundness theorem for ML can be stated as a program of type "int" will >  diverge >  raise an exception >  or produce an int > I think everybody except LISP programmers ;) want a sound type system like this. > OK replace everybody by I if you prefer ... For PML, we are more precise : exception > and the fact the a program may diverge must be written in the type. > >  ML type system is sometimes too incomplete, this is why the Obj library is here. > However, the use of Obj is mainly here because ML lacks dependant types. In fact, > the main use of Obj is to simulate a map table associating to a key k a type t(k) and > a value v:t(k). > >  All this says that a typesystem only accepting proved programs is possible and > a good idea (it already exists). The question for researcher is how to produce a > type system where the cost of proving is acceptable compared to the cost of debugging, > and this stars to be the case for some specific application, but we are far from > having to remove the word "bug" from our vocabulary ;) > > >  > > _______________________________________________ > Camllist mailing list. Subscription management: > http://yquem.inria.fr/cgibin/mailman/listinfo/camllist > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/camlbugs >  _______________________________________________ Camllist mailing list. Subscription management: http://yquem.inria.fr/cgibin/mailman/listinfo/camllist Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/camlbugs End of Camllist Digest, Vol 28, Issue 11 *****************************************