Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
* Caml-list Digest, Vol 28, Issue 11
@ 2007-10-04  8:56 caml-list-request
  0 siblings, 0 replies; only message in thread
From: caml-list-request @ 2007-10-04  8:56 UTC (permalink / raw)
  To: caml-list

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain; charset="us-ascii", Size: 18579 bytes --]

Send Caml-list mailing list submissions to
	caml-list@yquem.inria.fr

To subscribe or unsubscribe via the World Wide Web, visit
	http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
or, via email, send a message with subject or body 'help' to
	caml-list-request@yquem.inria.fr

You can reach the person managing the list at
	caml-list-owner@yquem.inria.fr

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Caml-list digest..."


Today's Topics:

   1. Re: Unsoundness is essential (skaller)
   2. Re: Locally-polymorphic 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: [Caml-list] Unsoundness is essential
To: "Joshua D. Guttman" <guttman@mitre.org>
Cc: caml-list@inria.fr
Message-ID: <1191462724.7542.76.camel@rosella.wigram>
Content-Type: text/plain

On Wed, 2007-10-03 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: [Caml-list] Re: Locally-polymorphic exceptions [was: folding
	over a	file]
To: kirillkh@gmail.com
Cc: caml-list@inria.fr
Message-ID: <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
> general-purpose library instead of the imperative-style 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 multi-prompt delimited
continuations. One may even say that if a type system supports
reference cells, it shall support multi-prompt 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 self-contained paper on delimited
continuations is

        A static simulation of dynamic delimited control
        by Chung-chieh Shan
        http://www.cs.rutgers.edu/~ccshan/recur/recur-hosc-final.pdf

I have heard some people have found the introduction section of
	http://okmij.org/ftp/Computation/Continuations.html#context-OS
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: [Caml-list] Unsoundness is essential
To: skaller <skaller@users.sourceforge.net>
Cc: "Joshua D. Guttman" <guttman@mitre.org>, caml-list@inria.fr
Message-ID: <Pine.LNX.4.64.0710032230000.28993@localhost>
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed



On Thu, 4 Oct 2007, skaller wrote:

> On Wed, 2007-10-03 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 non-primitive recursion.  So 
Ocaml's type system, which is not Turing complete, is gaurenteed to 
terminate eventually (it may have regretable big-O behavior, including an 
nasty non-polynomial 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@univ-savoie.fr>
Subject: Re: [Caml-list] Unsoundness is essential
To: skaller <skaller@users.sourceforge.net>
Cc: caml-list@inria.fr
Message-ID: <47049A6D.6020201@univ-savoie.fr>
Content-Type: text/plain; charset="iso-8859-1"

skaller a écrit :
> On Wed, 2007-10-03 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 type-system 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 Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.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 non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
Url : http://yquem.inria.fr/cgi-bin/mailman/private/caml-list/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: [Caml-list] Unsoundness is essential
To: caml-list@inria.fr
Message-ID: <4704AAA8.9080602@lix.polytechnique.fr>
Content-Type: text/plain; charset=ISO-8859-1; 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 non-zero, 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 0-valued integer (at each 
application). And curry-howard 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, 2007-10-03 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 type-system 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 ;-)
>
>   
> ------------------------------------------------------------------------
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>   



------------------------------

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


End of Caml-list Digest, Vol 28, Issue 11
*****************************************


^ permalink raw reply	[flat|nested] only message in thread
only message in thread, other threads:[~2007-10-04 14:11 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2007-10-04  8:56 Caml-list Digest, Vol 28, Issue 11 caml-list-request

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox