Locallypolymorphic exceptions [was: folding over a file]
[
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:  20071004 (08:56) 
From:  Arnaud Spiwack <aspiwack@l...> 
Subject:  Re: [Camllist] Unsoundness is essential 
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 >