Locally-polymorphic exceptions [was: folding over a file]

Locally-polymorphic exceptions [was: folding over a file]

[oleg]

kirillkh wrote
> Is there a way to instantiate an exception with a value of unspecified type
> and then do explicit casting on catch?

Surprisingly, the answer in many (or all?) cases is yes. The answer is
definitely yes in the case when we need to define an exception local
to a polymorphic function. Incidentally, SML permits declarations of
such local exceptions whose type is tied to that of the host
polymorphic function. That feature has been used to implement
delimited continuations. Perhaps unsurprisingly, delimited
continuations can be used to implement such locally-polymorphic
exceptions.

The recent thread gave a good motivation for locally polymorphic
exceptions: writing a library function fold_file. The following code
has been proposed.

> exception Done of 'a
>
>  let fold_file (file: in_channel)
>               (read_func: in_channel->'a)
>               (elem_func: 'a->'b->'b)
>               (seed: 'b) =
>   let rec loop prev_val =
>     let input =
>       try read_func file
>       with End_of_file -> raise (Done prev_val)
>     in
>       let combined_val = elem_func input prev_val in
>       loop combined_val
>   in
>     try loop seed with Done x -> x

Alas, the compiler does not accept the exception declaration, because
the declaration says that the exception should carry a value of all
types. There is no value that belongs to all types (and if it were, it
wouldn't be useful). But we don't actually need the value of all
types. We need the value of our Done exception to have the same type
as the result of the polymorphic function fold_file. We should have
declared the exception Done _inside_ fold_file. And that can be done:
Delimcc.prompt is precisely this type of `local exceptions'.

So, we can implement fold_file, by slightly adjusting the above code:

let fold_file (file: in_channel)
              (read_func: in_channel->'a)
              (elem_func: 'a->'b->'b)
              (seed: 'b) =
  let result = new_prompt () in (* here is our local exn declaration *)
  let rec loop prev_val =
     let input =
       try read_func file
       with End_of_file -> abort result prev_val
     in
       let combined_val = elem_func input prev_val in
       loop combined_val
   in
     push_prompt result (fun () -> loop seed)
;;

(*
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
*)


The analogy between exceptions and delimited continuations is
profound: in fact, delimited continuations are implemented in terms of
exceptions. Abort is truly raise. Well, observationally. The current
delimcc library tried to follow Dybvig, Sabry and Peyton-Jones
interface -- which, being minimalistic, did not include abort as a
primitive. We have to implement abort in terms of take_subcont, which
is wasteful as we save the captured continuation for no good
reason. Internally, the library does have an abort primitive, and it
indeed works in the same way as raise.

Re: Locally-polymorphic exceptions [was: folding over a file]

[kirillkh]

[-- Attachment #1: Type: text/plain, Size: 4039 bytes --]

Hi Oleg,

This looks excellent! I am especially delighted with the fact you don't have
to declare this single-use exception in the global scope anymore.
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?

Also, is there a good manual on delimited continuations for a beginner with
minimum of external references? I have tried to read your papers, but it's
hard to advance because some of the complex stuff is explained elsewhere.

-Kirill

2007/10/3, oleg@pobox.com <oleg@pobox.com>:
>
>
> kirillkh wrote
> > Is there a way to instantiate an exception with a value of unspecified
> type
> > and then do explicit casting on catch?
>
> Surprisingly, the answer in many (or all?) cases is yes. The answer is
> definitely yes in the case when we need to define an exception local
> to a polymorphic function. Incidentally, SML permits declarations of
> such local exceptions whose type is tied to that of the host
> polymorphic function. That feature has been used to implement
> delimited continuations. Perhaps unsurprisingly, delimited
> continuations can be used to implement such locally-polymorphic
> exceptions.
>
> The recent thread gave a good motivation for locally polymorphic
> exceptions: writing a library function fold_file. The following code
> has been proposed.
>
> > exception Done of 'a
> >
> >  let fold_file (file: in_channel)
> >               (read_func: in_channel->'a)
> >               (elem_func: 'a->'b->'b)
> >               (seed: 'b) =
> >   let rec loop prev_val =
> >     let input =
> >       try read_func file
> >       with End_of_file -> raise (Done prev_val)
> >     in
> >       let combined_val = elem_func input prev_val in
> >       loop combined_val
> >   in
> >     try loop seed with Done x -> x
>
> Alas, the compiler does not accept the exception declaration, because
> the declaration says that the exception should carry a value of all
> types. There is no value that belongs to all types (and if it were, it
> wouldn't be useful). But we don't actually need the value of all
> types. We need the value of our Done exception to have the same type
> as the result of the polymorphic function fold_file. We should have
> declared the exception Done _inside_ fold_file. And that can be done:
> Delimcc.prompt is precisely this type of `local exceptions'.
>
> So, we can implement fold_file, by slightly adjusting the above code:
>
> let fold_file (file: in_channel)
>               (read_func: in_channel->'a)
>               (elem_func: 'a->'b->'b)
>               (seed: 'b) =
>   let result = new_prompt () in (* here is our local exn declaration *)
>   let rec loop prev_val =
>      let input =
>        try read_func file
>        with End_of_file -> abort result prev_val
>      in
>        let combined_val = elem_func input prev_val in
>        loop combined_val
>    in
>      push_prompt result (fun () -> loop seed)
> ;;
>
> (*
> 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
> *)
>
>
> The analogy between exceptions and delimited continuations is
> profound: in fact, delimited continuations are implemented in terms of
> exceptions. Abort is truly raise. Well, observationally. The current
> delimcc library tried to follow Dybvig, Sabry and Peyton-Jones
> interface -- which, being minimalistic, did not include abort as a
> primitive. We have to implement abort in terms of take_subcont, which
> is wasteful as we save the captured continuation for no good
> reason. Internally, the library does have an abort primitive, and it
> indeed works in the same way as raise.
>
>

[-- Attachment #2: Type: text/html, Size: 5551 bytes --]

Re: [Caml-list] Re: Locally-polymorphic exceptions [was: folding over a file]

[Daniel de Rauglaudre]

Hi,

> 2007/10/3, oleg@pobox.com <oleg@pobox.com>:
>
> exception Done of 'a
>
>  let fold_file (file: in_channel)
>               (read_func: in_channel->'a)
>               (elem_func: 'a->'b->'b)
>               (seed: 'b) =
> [...]

Personnally, I don't like exceptions because they generally control too
much part of code. I often practice things like:

  match try Some (...) with [ Exception -> None ] with
  [ Some v -> blabla
  | None -> blublu ]

I would write your function like this:

  value fold_file (file : in_channel) (read_func : in_channel -> 'a)
    (elem_func : 'a -> 'b -> 'b) (seed : 'b)
  =
    let rec loop prev_val =
      match try Some (read_func file) with [ End_of_file -> None ] with
      [ Some input ->
          let combined_val = elem_func input prev_val in
          loop combined_val
      | None -> prev_val ]
    in
    loop seed
  ;

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

Re: [Caml-list] Re: Locally-polymorphic exceptions [was: folding over a file]

[kirillkh]

[-- Attachment #1: Type: text/plain, Size: 1748 bytes --]

Hi,

2007/10/3, Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>:
>
> Hi,
>
> > 2007/10/3, oleg@pobox.com <oleg@pobox.com>:
> >
> > exception Done of 'a
> >
> >  let fold_file (file: in_channel)
> >               (read_func: in_channel->'a)
> >               (elem_func: 'a->'b->'b)
> >               (seed: 'b) =
> > [...]
>
> Personnally, I don't like exceptions because they generally control too
> much part of code.


It's easy enough to localize the exception scope in this case and to see
that catching it at the top recursive invocation gets rid of it for sure.
Even the most dreadful beast is harmless, when encapsulated in a cage. (C)

I wonder what are continuations' maintenance properties, though. Any
comments? I'm not fluent in them, yet.

I often practice things like:
>
>   match try Some (...) with [ Exception -> None ] with
>   [ Some v -> blabla
>   | None -> blublu ]
>
> I would write your function like this:
>
>   value fold_file (file : in_channel) (read_func : in_channel -> 'a)
>     (elem_func : 'a -> 'b -> 'b) (seed : 'b)
>   =
>     let rec loop prev_val =
>       match try Some (read_func file) with [ End_of_file -> None ] with
>       [ Some input ->
>           let combined_val = elem_func input prev_val in
>           loop combined_val
>       | None -> prev_val ]
>     in
>     loop seed
>   ;


A similar solution has been proposed in the original discussion ("best and
fastest way to read lines from a file?" thread). But then someone suggested
using a second exception instead, which is better performance-wise, since it
avoids variant allocations on the common code path. What I tried to do with
polymorphic exception is implement a generalized channel fold combinator
based on this idea.

-Kirill

[-- Attachment #2: Type: text/html, Size: 2991 bytes --]

Re: [Caml-list] Re: Locally-polymorphic exceptions [was: folding over a file]

[Daniel de Rauglaudre]

Hi,

On Wed, Oct 03, 2007 at 02:19:56PM +0200, kirillkh wrote:

> But then someone suggested using a second exception instead, which
> is better performance-wise [...]

Is that been checked ? And the two implementations tested ? What are the
results, in time ?

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

Re: [Caml-list] Re: Locally-polymorphic exceptions [was: folding over a file]

[kirillkh]

[-- Attachment #1: Type: text/plain, Size: 1676 bytes --]

2007/10/3, Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>:
>
> Hi,
>
> On Wed, Oct 03, 2007 at 02:19:56PM +0200, kirillkh wrote:
>
> > But then someone suggested using a second exception instead, which
> > is better performance-wise [...]
>
> Is that been checked ? And the two implementations tested ? What are the
> results, in time ?
>

Tested from the top-level on a text file with 11mln lines:
variants:
8.081  8.021  8.072  8.052  8.011  =>  avg=8.0474
exceptions:
7.801  7.902  7.822  7.901  7.832  =>  avg=7.8512
-----------------------------
total: exceptions are 2.44% faster

I'm having troubles with ocamlopt (windows machine), can anyone do a similar
test with it? Here's the code used (it's the pre-combinator version of line
counter):

exceptions (lcex.ml):
exception Done of int;;

let line_count filename =
 let file = open_in filename in
 let rec loop count =
   let _ =
     try
       input_line file
     with End_of_file -> raise (Done count)
   in
     loop (count + 1)
 in
   try loop 0 with Done x -> x
;;

let start_time = Sys.time() in
let count = line_count "c:/kirill/ocaml/test3.txt" in
let diff = Sys.time() -. start_time in
    Printf.printf "count: %d,  time: %f" count diff;;

variants(lcvar.ml):
let readline f =
  try Some (input_line f)
  with End_of_file -> None;;

let line_count filename =
  let f = open_in filename in
  let rec loop count =
    match (readline f) with
      | Some(_) -> loop (count+1)
      | None -> count in
  loop 0;;

let start_time = Sys.time() in
let count = line_count "c:/kirill/ocaml/test3.txt" in
let diff = Sys.time() -. start_time in
    Printf.printf "count: %d,  time: %f" count diff;;


-Kirill

[-- Attachment #2: Type: text/html, Size: 2679 bytes --]

Re: [Caml-list] Re: Locally-polymorphic exceptions [was: folding over a file]

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 2746 bytes --]

Hi,
>
>     > exception Done of 'a
>     >
>     >  let fold_file (file: in_channel)
>     >               (read_func: in_channel->'a)
>     >               (elem_func: 'a->'b->'b)
>     >               (seed: 'b) =
>     >   let rec loop prev_val =
>     >     let input =
>     >       try read_func file
>     >       with End_of_file -> raise (Done prev_val)
>     >     in
>     >       let combined_val = elem_func input prev_val in
>     >       loop combined_val
>     >   in
>     >     try loop seed with Done x -> x
>
In fact, if elem_func is known by the type checker not to raise any
exception,
then the exception need not to be garded by the Done constructor and the
following program is safe:

>  let fold_file (file: in_channel)
>               (read_func: in_channel->'a)
>               (elem_func: 'a->'b->'b)
>               (seed: 'b) =
>   let rec loop prev_val =
>     let input =
>       try read_func file
>       with End_of_file -> raise prev_val
>     in
>       let combined_val = elem_func input prev_val in
>       loop combined_val
>   in
>     try loop seed with x -> x

The only problem is that current type-checker do not treat exception
well and reject this kind of code ....

Just for fun (I could not resist), here is the pml code which is
accepeted, but is useless since pml can not read file yet ;-)

---------- pml code ---------
(* f,a,b are declared type variables,
   a => b is the type of a function that raises no exception
   a -> b | e is the type of a function that raises only exception of
type e
   a -> b is the type of a function with no indication about exceptions *)

val (f,a,b) fold_file:(f => (f -> a | [EOF[]]) => (a=>b=>b) => b => b)
  file read_func elem_func seed =
   let rec loop prev_val =
     let input =
       try read_func file
       with EOF[] -> raise prev_val
     in
       let combined_val = elem_func input prev_val in
       loop combined_val
   in
     try loop seed with x -> x
-------------------------------

So the story is by saying (wrongly) that it is too heavy to anottate
arrow types with exceptions,
making the arrow type a ternary type construct, ML is missing a lot ...

-- 
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
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]

Unsoundness is essential

[skaller]

On Wed, 2007-10-03 at 22:39 +0200, Christophe Raffalli wrote:

> So the story is by saying (wrongly) that it is too heavy to anottate
> arrow types with exceptions,
> making the arrow type a ternary type construct, ML is missing a lot ...

To be bold I propose type theorists have got it totally wrong.

Goedel's theorem says that any type system strong enough to
describe integer programming is necessarily unsound.

All advanced programming languages have unsound type systems
of necessity. Some falsely claim soundness by denying the
expression of certain type information (eg array bounds 
or the type of integers excluding zero).

I want an unsound type system! It much better than the useless
but 'sound' type system of Python, in which the type inference
engine decides all values have type Object and proves
in vacuuo that all programs are type-safe, only to do the 
dependent type checks at run time anyhow -- a cheat known
as dynamic typing.

It is better to admit from the start that type systems
can and MUST be unsound, and allow programmers to write
known correct programs with expressive typing which no type 
system could type check, than to turn programmers off by 
rejecting their valid code.

The cost is some invalid code will be accepted, but there
is no help for it: the type system has to be unsound
or it is of no practical use at all (Ok, I exaggerate,
predicate calculus is complete and useful .. algebraic
typing is the equivalent).

In particular, the ability to write proper type annotations
such as

	divide: int * (int - {0}) -> int

and fail to reject programs which violate the typing is an
essential and useful feature. Later, some programs may
be properly rejected early instead of late when some
smart type theorist extends the capabilities of the compiler,
or the programmer learns how to re-express the typing so
the existing algorithms catch more faults.

Languages like Ocaml make significant advances in type checking
capability, but users and theorists incorrectly laugh at the weak
and unsound type system of C. In fact, the idea of C is the right
one. We know the type system is unsound. It is essential. It is the
very reason C lives on. Newer compilers have better error detection,
in the meantime C doesn't stop you writing your code. C does this
right: you can use a cast to override the type checks OR you can
simply exploit the unsoundness directly. The latter is preferable
because later versions of the compiler may be smart enough to
catch real errors which the casts would always defeat.

It's time to turn type theory on its head. Forget about whether
the typing is sound, give me EXPRESSION first and worry about
checking second. Accept Goedel: the unsoundness is *essential*
and thus must not be an excuse for failure to express. Let me
write:

	divide: int * (int - {0}) -> int

and I may catch a bug using the human brain, or later
the compiler may be improved and catch more bugs automatically.
The fact it will never catch all these bugs is irrelevant 
because unsoundness is an essential requirement of 
expressive type systems. Stop CHEATING by refusing to allow
me to write types you can't check -- because this forces
ME as the programmer to cheat on the type annotations:

	divide: int * int -> int
	hd : 'a list -> 'a



-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[Jacques Carette]

skaller wrote:
> To be bold I propose type theorists have got it totally wrong.
>
> Goedel's theorem says that any type system strong enough to
> describe integer programming is necessarily unsound.
>   
No, that's wrong.  Any *complete* type system that strong is unsound.  
It says nothing about incomplete systems.

My position is that looking for decision procedures everywhere is what 
is blocking real progress.  People doing dependent types have gotten 
over most of that.

> I want an unsound type system! 
No you don't, you want an incomplete one.  You want one where the type 
system will tell you when you are obviously wrong, and will ask you for 
a proof when it's not sure.  If you insist on unsound, then when the 
type system doesn't know, it might let things through anyways, and then 
all bets are off.  I don't want that.

> It much better than the useless
> but 'sound' type system of Python, in which the type inference
> engine decides all values have type Object and proves
> in vacuuo that all programs are type-safe, only to do the 
> dependent type checks at run time anyhow -- a cheat known
> as dynamic typing.
>   
Again, I disagree.  It's much better to do most type checks statically, 
and then to residualize some type checks to run-time if you absolutely 
must. This is roughly what my Master's student Gordon Uszkay did for a 
"scientific computation" language, using CHRs.  Unfortunately, his work 
was already way too ambitious as it was, so all he succeeded in doing is 
an implementation [that works], but no formal proofs.

> In particular, the ability to write proper type annotations
> such as
>
> 	divide: int * (int - {0}) -> int
>
> and fail to reject programs which violate the typing is an
> essential and useful feature. 
I would rather say that what should be done is that run-time type checks 
should be residualized into the program, so that no unsound program 
would be allowed to run to completion, an assertion would be triggered 
first.


> In fact, the idea of C is the right one. 
When I was forced to write a C program (after enjoying Ocaml so much), 
and even with
gcc -W -Wall -Werror -pedantic something.c
I got a clean compile which, when run, core dumped, I was seriously 
unhappy. 

> Stop CHEATING by refusing to allow
> me to write types you can't check -- because this forces
> ME as the programmer to cheat on the type annotations:
>
> 	divide: int * int -> int
> 	hd : 'a list -> 'a
>   
Here we agree.  Both of those types are 'cheating'. 

Jacques

Re: [Caml-list] Unsoundness is essential

[Vincent Aravantinos]

Le 4 oct. 07 à 00:50, skaller a écrit :

> On Wed, 2007-10-03 at 22:39 +0200, Christophe Raffalli wrote:
>
>> So the story is by saying (wrongly) that it is too heavy to anottate
>> arrow types with exceptions,
>> making the arrow type a ternary type construct, ML is missing a  
>> lot ...
>
> To be bold I propose type theorists have got it totally wrong.
> ...
> expressive type systems. Stop CHEATING by refusing to allow
> me to write types you can't check -- because this forces
> ME as the programmer to cheat on the type annotations:
>
> 	divide: int * int -> int
> 	hd : 'a list -> 'a

If you allow everything (such as the "type expressive" C you are  
envisaging), the programmer will be tempted to use this "everything"  
whereas he could achieve the same with a "bounded" language. And in  
this case I bet the programmer won't do things that will ever be  
"type theoretic friendly", whatever progress in type theoretics will be.

To my eyes it looks like many things that appeared in other languages  
to appeal the programmers, but that could be achieved in other (did I  
say better ?) ways. If you allow everything, people will be tempted  
to do anything... And any progress in computer science will never  
catch the gap.

I think it's a good thing to constrain the programmer. How many times  
I thought "that's a pity I can't do this *as I want* in ocaml". And  
then after having been forced to think of another way to achieve my  
goal *within the constraints of ocaml*, I ended with something like  
"woah, actually it's better this way!".

Cheers,
Vincent

Re: [Caml-list] Unsoundness is essential

[Joshua D. Guttman]

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.

Poor old guy.  Worked so hard to be precise, and now
everybody attributes all sorts of things to him.    

        Joshua 
-- 
	Joshua D. Guttman 
	The MITRE Corporation

Re: [Caml-list] Unsoundness is essential

[skaller]

On Wed, 2007-10-03 at 19:13 -0400, Jacques Carette wrote:
> skaller wrote:
> > To be bold I propose type theorists have got it totally wrong.
> >
> > Goedel's theorem says that any type system strong enough to
> > describe integer programming is necessarily unsound.
> >   
> No, that's wrong.  Any *complete* type system that strong is unsound.  
> It says nothing about incomplete systems.

You're right, I have assumed a complete system cannot describe
the integer programming. Is that not so?

> > I want an unsound type system! 
> No you don't, you want an incomplete one.  You want one where the type 
> system will tell you when you are obviously wrong, and will ask you for 
> a proof when it's not sure.  If you insist on unsound, then when the 
> type system doesn't know, it might let things through anyways, and then 
> all bets are off.  I don't want that.

Ah, but that is what I *am* arguing for. The 'reasoning' is simply
that 'the programmer knows best' -- when the type system doesn't.
The evidence is: programming languages with dynamic or unsound
typing eg Python, C, are vastly more popular than those with 
strong typing.

Now, my (quite disputable) claim is that the reason for that 
is that the strong typing people prefer to reject correct 
programs than accept ones which cannot be proven correct, 
but this belief is *demonstrably* fallacious.

As I demonstrated with simple examples, the type system ALREADY
lets incorrectly typed programs through. This fact is hidden
by theoretical mumbo-jumbo. It's time the theorists woke up.
Leaving out (int-{0}) as a type simply because it would make
the type system unsound does not enhance the reliability of
the program: either way, without the annotation and a sound type
system or with the annotation and an unsound system, it is possible
to have a division by 0.

The difference is that the unsound system can be improved,
and the human brain can do type-checking too. So the unsound
system is better because it subsumes the sound one.
Nothing is lost in the unsound system. NEITHER system 
guarantees correctness, and the unsound system still
rejects at least the same set of incorrect programs,
but possibly more.

Ocaml type system is ALREADY unsound: any division by zero
or array bounds check exception provides that conclusively.

Type systems will NEVER be able to prove all programs are
correct. Requiring type safety, i.e. soundness, is simply
an obstacle, not an aid. Correctness and type-safety from
soundness aren't the same thing. It is better to put
more information in the type system, to be more expressive
and declarative and accept unsoundness, than to be limited
in one's declarative description of executable code, so
that in fact the typing is WRONG, in which case the soundness
of the type system is of no use in proving correctness!

I am arguing in favour of a much richer and more expressive
type system, EVEN IF it is not known how to prove type-correctness,
and indeed EVEN IF it CAN be proven that there exist cases
which are undecidable!
 
> Again, I disagree.  It's much better to do most type checks statically, 
> and then to residualize some type checks to run-time if you absolutely 
> must.

I don't see how I disagree with that. Indeed, that is very much
my point! You check what can be checked early, but unless the
compiler can PROVE that the code is incorrect, it should not
reject it. Unsoundness doesn't imply incorrectness.

Any failure caught at runtime by a 'residualised' check
proves the type system is unsound.

So actually you agree with my point. If indeed the type
system were sound there would necessarily not be any need
to generate any such run time checks.

[Note: this does not mean run time type information isn't
required, eg constructor indices, array bounds, etc:
run time type calculations subsume mere type-checks]

> > In particular, the ability to write proper type annotations
> > such as
> >
> > 	divide: int * (int - {0}) -> int
> >
> > and fail to reject programs which violate the typing is an
> > essential and useful feature. 
> I would rather say that what should be done is that run-time type checks 
> should be residualized into the program, so that no unsound program 
> would be allowed to run to completion, an assertion would be triggered 
> first.

I told you: you're agreeing with my claim. However it is slightly
confused: a program can be correct or not, it cannot be unsound.
It is the type system which can be sound or not.

So I am going to assume you mean: a program with suspicious typing
for which a type-safety proof cannot be found at compile time
should have a run time check to ensure the fault consequent
of the unsoundness is caught and diagnosed ASAP at run time.

I don't dispute the ability to generate such checks is useful,
however I raise these issues:

1. What if you cannot generate the checks?
2. Just because the checks pass doesn't mean the program is correct

> > In fact, the idea of C is the right one. 
> When I was forced to write a C program (after enjoying Ocaml so much), 
> and even with
> gcc -W -Wall -Werror -pedantic something.c
> I got a clean compile which, when run, core dumped, I was seriously 
> unhappy. 

And I got a Not_found error in my Ocaml program recently which took
three days to locate. I don't see any qualitative difference.

There is a difference of 'degree' which confusingly is a quality
issue: better diagnostics, earlier detection, etc. But the bottom
line is an uncaught exception in Ocaml and a null pointer dereference
in C both cause an abnormal termination symptomatic of an incorrect
program (not necessarily due to a typing error).

> > Stop CHEATING by refusing to allow
> > me to write types you can't check -- because this forces
> > ME as the programmer to cheat on the type annotations:
> >
> > 	divide: int * int -> int
> > 	hd : 'a list -> 'a
> >   
> Here we agree.  Both of those types are 'cheating'. 

Yes, but your solution might look like this:

	divide: int * (int \ {0}) -> int

with static check on int, and residualised check for a zero
divisor .. and for hd, similar... 

Hey, Ocaml does those checks NOW! SO what's the difference??

The difference is that the system with 

	(int \ {0})

is unsound, but more expressive. My argument is simply that
this is BETTER. Not allowing this has no real utility other
than to allow theorists to argue the type system is sound.
It has no benefits, and many downsides.

Perhaps you see a problem where some typing notation is so hard
it cannot even be checked at run time? This can surely happen.

My answer is: SO WHAT? The programmer is going to code the algorithm
ANYHOW. They will either use CHEAT types, in which case the type
safety provides no benefit OR, MUCH WORSE .. they're go off and
write the program in Python or C instead.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 01:13 +0200, Vincent Aravantinos wrote:
> Le 4 oct. 07 à 00:50, skaller a écrit :

> > To be bold I propose type theorists have got it totally wrong.
> > ...
> > expressive type systems. Stop CHEATING by refusing to allow
> > me to write types you can't check -- because this forces
> > ME as the programmer to cheat on the type annotations:
> >
> > 	divide: int * int -> int
> > 	hd : 'a list -> 'a
> 
> If you allow everything (such as the "type expressive" C you are  
> envisaging), the programmer will be tempted to use this "everything"  
> whereas he could achieve the same with a "bounded" language. 

Yes, this is a valid criticism. Can you please help refine my idea
to take this into account?

What we want is to push the programmer into using the most
checkable form, and only let them 'escape' if it is really
necessary (I hope you agree with that summary!)

But I have no idea how to do that in a coherent way.
A kind of Occam's Razor of programming .. :)

In C++, this is done by encouraging programmers not
to use casts, but still allowing them, and indeed,
providing a more refined and pointed set of casts as well:

	static_cast, dynamic_cast, const_cast, 
	reinterpret_cast

These are long winded (deliberately) and frowned upon so there
is both mechanical (I hate typing) and psychological (peer
pressure, pride, etc) pressure NOT to use casts, and this
is encourage by the fact that C++ needs a LOT LESS casts
than C.

In Ocaml .. Obj.magic is 'evil' and not documented..

But this is a really WEAK form of pressure.

> To my eyes it looks like many things that appeared in other languages  
> to appeal the programmers, but that could be achieved in other (did I  
> say better ?) ways. If you allow everything, people will be tempted  
> to do anything... And any progress in computer science will never  
> catch the gap.

Yes, but the problem now is that all these new languages are
coming out and the designed IGNORE all the good academic work.
Java, Ruby .. to name two examples of *new* rubbish which are
immensely popular, whilst Ocaml and Haskell haven't taken off.

> I think it's a good thing to constrain the programmer.

No dispute. I'm not arguing for NO constraints. In fact
it is the other way around. I'm arguing to allow the programmer
to apply MORE constraints in the form of more expressive types
EVEN IF THESE CONSTRAINTS CANNOT BE ENFORCED.

>  How many times  
> I thought "that's a pity I can't do this *as I want* in ocaml". And  
> then after having been forced to think of another way to achieve my  
> goal *within the constraints of ocaml*, I ended with something like  
> "woah, actually it's better this way!".

Yes. I have to tell you that I use this idea systematically
as a programming technique!

However many things annoy me, some of which I have tried to
fix in Felix. One of them is that modules/functor do not
allow expression of semantic rules: Felix has typeclasses
WITH semantic rules.

Although the rules are limited, Felix can actually generate
a vast battery of axiom checks, and, it currently emits
theorem claims in Why encoding which allows the claims
to be checked by various theorem provers, including Ergo.

None of this comes close to doing what I actually need in
the Ocaml code of the compiler itself, which is a to enforce
invariants of the term rewriting system in the type system.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[skaller]

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

Re: Locally-polymorphic exceptions [was: folding over a file]

[oleg]

> 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.

Re: [Caml-list] Unsoundness is essential

[Brian Hurt]

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

Re: [Caml-list] Unsoundness is essential

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 3140 bytes --]

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
---------------------------------------------


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]

Re: [Caml-list] Unsoundness is essential

[Arnaud Spiwack]

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
>   

RE: [Caml-list] Unsoundness is essential

[David Allsopp]

> Ah, but that is what I *am* arguing for. The 'reasoning' is simply
> that 'the programmer knows best' -- when the type system doesn't.

"the programmer knows best" is one of the founding principles of BCPL!! I'm
not sure I agree, though - IMO Vincent is correct that being forced to
express things "properly" results in better code in the long run. Try
writing any substantial amount of BCPL[*]...

> The evidence is: programming languages with dynamic or unsound
> typing eg Python, C, are vastly more popular than those with 
> strong typing.

I'm not at all convinced that dynamic/unsound typing is the reason for the
popularity of C, etc - I've never met a C programmer whose eyes didn't pop
out on stalks when you explain that Ocaml cannot reference a null pointer
(not that that has ever caused a Damascene-road conversion to the language,
either!). <joke> C and Python's popularity is more down to needing ever more
programmers to debug the work of the previous programmers, right? :o)
</joke> Personally, whenever I go back to C, the novelty of the relaxed type
system is instantly worn away on the first tricky-to-repeat core dump... at
least an Ocaml exception has a cat in hell's chance of being found
systematically!


David


* With apologies and due deference to Martin Richards if he reads this list!

Re: [Caml-list] Unsoundness is essential

[Vincent Hanquez]

On Thu, Oct 04, 2007 at 12:26:53PM +0100, David Allsopp wrote:
> Personally, whenever I go back to C, the novelty of the relaxed type
> system is instantly worn away on the first tricky-to-repeat core dump... at
> least an Ocaml exception has a cat in hell's chance of being found
> systematically!

That's sadly not true. GC bugs in some bindings are usually hard to find !

Cheers,
-- 
Vincent Hanquez

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 10:56 +0200, Arnaud Spiwack wrote:
> Hi everybody,

> 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,

This is my point. Theorists have this all wrong.
I'm a programmer. I do NOT really care if my program is provably
correct. Sure, it would be nice to have such a proof, but the
lack of one will not stop me writing the program!

What I care about is that the program works.

Now, suppose I code some types in my program, and the
type system cannot prove I have respected them. Incompleteness
ensures this can happen (given a sufficiently powerful
type system). Pragmatics indicates this is also possible:
the proof may indeed be constructible but take too long
to construct to be practical.

Should it accept or reject the program? My claim is that
it should accept the program. It should only reject programs
which can be proven incorrect.

Now, I want you to hold on before disputing that claim,
because there is more to the reasoning to come.

The purpose of typing is to assist in showing a program 
is incorrect. We know for sure that in principle and practice
there will be well typed incorrect programs, so there
is no issue of proving all programs correct.

The question is, should we strengthen the type systems
we use to be more descriptive? There is a problem doing this.
If we make the type system descriptive enough, there is a 
possibility we will be able to reject more programs --
this is good! But it is also likely that we will lose
the ability to prove the typing is correct. What should
we do?

If we reject the program, the programmer will be annoyed,
if we accept it, the type system is unsound, because
in accepting it, we risk accepting programs which are
not well typed, and therefore not correct.

Now, please observe that with a stronger type system,
we are going to reject more programs. That is the point.
But we are ALSO going to be unable to decide the well typedness
of many programs, for either incompleteness or pragmatic
reasons.

It simply isn't feasible to reject these programs simply
because a proof of well-typedness cannot be constructed:
and there is no possibility of disputing this claim
because it is what programming languages like Ocaml do
right now: they generate run time checks precisely because
they cannot ensure correctness.

It's already a known fact that today, we cannot ensure
certain things like array bounds and zero division
statically.

So the question is, whether array length and non-zero
integers should be expressible in the type systems 
today.

And my answer is YES PLEASE. A type system with that
expression MUST BE UNSOUND.

I hope this argument is not too hard to follow:
if you make the type system expressive enough, right now,
then it MUST BE UNSOUND because we cannot have the type
system rejecting the many correct programs I can and do
write where I (think I) know I'm never going to divide
by zero, simply because the type system cannot prove
my belief.

There is no issue that the powerful type system must
be unsound. That is not the question or the claim.

The question is: should compiler writers introduce
powerful enough type systems that can express things
like non-zero integers or array index correctness,
KNOWING FOR SURE THAT TO DO SO MANDATES UNSOUNDNESS.

There's no question such powerful type systems have
to be unsound, at least today. That isn't in dispute!

The question is whether we should introduce such rich
and expressible notations anyhow!

My claim is YES WE SHOULD. Because Arnaud is quite wrong
in his belief that 'what we should care about is provability'.
That is what theoreticians care about, but it is NOT the domain
in which programmers operate (unless they're type systems programmers
of course! :)

[PS: of course I do *care* about provability, but I'm not
willing to give up programming just because I can't prove
everything I code is correct]

So finally I will give an example: I cannot write this:

	hd : 'a non-empty-list -> 'a
	divide: int * non-zero-int -> int

in Ocaml at the moment. Should I be able to??

If you say YES, you will note the Ocaml type system would 
become unsound. Ocaml simply cannot prove in all cases that an 
integer value is non-zero, nor that a list is non-empty.

We do not reject programs that apply 'hd' just because of this.
Heck: hd and divide ARE PART OF THE CORE LIBRARY!!!!

My point is: NOTHING IS LOST BY MAKING THE TYPE SYSTEM UNSOUND
WITH THIS EXTENSION. Indeed in SOME cases Ocaml may indeed
be able to prove wrong typing, so we GAIN something from 
the point of view of machine verification. And the human
programmer gains something too, because they too may find
errors, even ones the type system cannot, and it could easily
make the program semantics easier to understand, if the
interface type annotations were richer.

So my belief is that theoreticians are doing the programming
industry a DISSERVICE by insisting on sound typing, because
in so doing they're greatly limiting the expressiveness of 
the type system.

There is no benefit in it. That is the point. A proof of
well-typedness is NOT a proof of correctness in the first
place. I do not care that the type system cannot prove
well typedness because that is not its job: its job is
to prove a program INCORRECT by proving wrong typing.

Making the type system unsound by extending the expressiveness
can be done without failing to reject programs which are
currently rejected. Take Ocaml and add non-zero integers,
and allow it to accept programs where the non-zeroness
cannot be proven, and we are no worse off than now, where
the same fact applies: Ocaml ALREADY allows such programs.

Much as we'd like to be able to guarantee that a program using
non-zero integer type is well typed, it is better to let such
a program pass, than to compromise the expressiveness of
the type system JUST BECAUSE THEORETICIANS ARE SO CONFUSED
ABOUT WHAT THE PURPOSE OF THE TYPE SYSTEM IS THAT THEY REFUSE
TO ALLOW AN UNSOUND ONE (of course I'm definitely not meaning
to be offensive here!)

If you think a type system has to be sound, you do not understand
that the purpose is to catch errors early, and if not diagnose them
late, and we wish to catch as many as possible. We are therefore
COMPELLED to introduce a richer type system, and there is no doubt
such a system, at least today if not always, cannot be sound.

BTW: I am not asking for 'non-zero-int' and 'non-empty-list' as
actual features for Ocaml. There is still a real issue how to make
the extensions to the type system in a general enough way.
For example:

	int \ {0}

looks better because subtraction is a fairly general operator,
but there may be other more useful annotations.

There certainly exist languages where the 'checking' system 
is 'unsound'.

For example Eiffel and Felix both allow pre and post conditions on
functions, and both generate run time checks, which are witness
to unsoundness.

It is merely pride of theoreticians that they claim a precondition
is not type information. There is NO DOUBT in my mind a precondition
is precisely a restriction on the set of input values to a function,
and is definitely type information.

Ocaml does not let you notate this**, although you can write an assert,
but in Felix it is plain it is intended as type information:

	fun divide(x: int where x!=0): ...

even though this is not encoded in the type signature because I do not
know what to do with it. In Felix the typing is unsound, because
it generates the non-zero test at run time.

** of course Ocaml DOES let you notate this now we have private
types we can enforce the constraint in the constructor of a record,
however this semi-abstract type is nominally typed, and not
quite the same as a structural annotation like int \ {0}
which is anonymously typed. However this enforcement is clearly
an unsoundness of typing because the constraint isn't enforced
at compile time. So this is a perfect example of a GOOD
extension of the kind I desire which already introduces an
unsoundness. The key point of the idea is in fact to clearly
and pointedly restrict the unsoundness to the constructor.
Using this, plus smartness of the type system, we may be able to:

	a) reject some programs which are clearly incorrect
	b) optimise away the check in other programs which
		are clearly correct
	c) accept a program where the type system cannot decide
		and generate runtime check as witness to the
		unsoundness

This is GOOD. There should be more of it! The lack of soundness
is not a problem -- it's ESSENTIAL to rejecting even more incorrect
programs because there's no way to eliminate the unsoundness
without eliminating the very expressiveness which allows more
programs to be type checked and thus more to be rejected.
What's more, it leads to better performance too.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

RE: [Caml-list] Unsoundness is essential

[Harrison, John R]

For those who are really interested in what Goedel's theorems
say, or who might enjoy a spirited demolition of various abuses
of them inside and outside logic, let me recommend this book
by the late Torkel Franzen:

http://www.akpeters.com/product.asp?ProdCode=2388

Naturally, I'm not implying that anyone on this thread is guilty
of inappropriate use of the theorems.

John.

Re: [Caml-list] Unsoundness is essential

[Andrej Bauer]

I too have a compulsive obsession to talk about logic, so here is my 
contribution.

Logic is about details. It is only to be expected that in a willy-waving 
competition on a mailing list like ours everyone will get something 
wrong about such a tricky thing as Goedel's theorems (me included). For 
example:

Christophe Raffalli:
> - 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 ...

In logic complete usually means: for every sentence A the system proves 
A or it proves not A. This has nothing to do with being able to 
interpret arithmetic. We can define completeness without reference to 
arithmetic.

(Presumably, a type system is complete if for every (closed) type A,
A is inhabited or A -> void is inhabited. At least this would be the 
reading of completeness under propositions-as-types.)

Christophe Raffalli:
> - The 1st incompleteness theorem states that no theory containing
> arithmetic is complete.

No _sound_ theory interpreting arithmetic is complete.

Arnaud Spiwack wrote:
> 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).

Goedel's theorems say nothing directly about truth. This is a common 
misconception.

Skaller started the discussion with a rerefence to Geodel, which he did 
not attempt to use in a technically correct way. I think it would be 
beneficial for this discussion to move away from explicit references to 
Goedel.

We seem to be talking about two things:

a) Expressiveness of a type system vs. decidability of type-checking.

The main point is that the more expressive the type system the harder it 
is to check types.

b) Safety guarantees for well-typed programs

A typical safety guarantee is expressed with the Preservation Lemma 
("Types are preserved during evaluation") and Progress Lemma ("A typed 
program is either a value or has a next evaluation step"). Together 
these two imply, e.g., that there won't be a segmentation fault.

I think to some extent (b) is what skaller calls "soundness".

If I read skaller correctly, he made three points (please correct me if 
not):

1) The safety properties of well-typed programs in C are none,
but Ocaml is not much better either, since it just pretends that 
exceptions are safe. Therefore, to at least some degree the slogan "the 
Ocaml type system guarantees safety" is not entirely and honestly true.

2) Morally inferior languages such as C and Python are popular because 
people are not willing to write programs with their hands tied to their 
backs by a typing system.

3) Skaller would rather have poor safety guarantees than an inexpressive 
type system that ties his hands.

Goedel is dragged in only because his theorems tell us that the perfect 
world does not exist, i.e., we cannot have decidable type checking of a 
very expressive type system which also has sane safety properties.

Leaving Goedel aside for a moment, we can ask what a good practical 
combination of expressiveness and safety would be. We have to give up at 
least one of the three desired properties (expressiveness, decidability 
of type checking, safety). Various languages make various choices, as 
was already mentioned in this thread. Let me just say that the choice 
made by C, i.e., to give up both expressiveness and safety in return for 
easy type-checking is not as crazy as it may sound (imagine it's 1970, 
your computer has 4kb of memory, everybody around you thinks of types as 
hints to compilers about how many bytes of storage a variable will take, 
and Martin-Lof is just an obscure Scandinavian mathematician and/or 
philosopher that real programmers never heard of).

It seems to me that the evolution of theory-backed languages such as ML 
and Haskell is reaching a point where people are willing to give up 
decidability of type-checking (Haskell has done it). Skaller seems to 
think that the only option is to give up safety, as well, with which I 
disagree. We need _controlled_ unsafety.

My position is this:

i) Insist on good safety properties. If a program compiles without any 
"ifs" and "buts", then it is safe (whatever that means). It the compiler 
thinks the program might be unsafe it should try to compile anyhow, and 
tell us why precisely it thinks it might be unsafe.

ii) Give programmers very expressive type systems so that they can write 
things like

    div : int * {x : int | not (x = 0)} -> int

and much more.

iii) Of course, by combining i) and ii) we must then give up 
decidability of type-checking. We can compensate for that loss by 
_making compilers more interactive_. The current model, where a compiler 
either succeeds on its own or fails completely, is not going to take us 
much further. People from the automated theorem proving community learnt 
a while ago that the interaction between the human and the computer is 
the way to go.

A compiler should be able to take hints on how to check types. The 
result of compilation should be one of:

- everything is ok

- the program contains a grave typing error which prevents
   the compiler from emitting sane code, compilation is aborted

- the compiler generates sane code but also emits a list of assertions
   which need to be checked (by humans or otherwise) in order to
   guarantee safety

If we had compilers like that, they would greatly encourage good 
programming practices.

You can read the above as my manifesto, if you wish.

Best regards,

Andrej

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 14:45 +0200, Vincent Hanquez wrote:
> On Thu, Oct 04, 2007 at 12:26:53PM +0100, David Allsopp wrote:
> > Personally, whenever I go back to C, the novelty of the relaxed type
> > system is instantly worn away on the first tricky-to-repeat core dump... at
> > least an Ocaml exception has a cat in hell's chance of being found
> > systematically!
> 
> That's sadly not true. GC bugs in some bindings are usually hard to find !

I think David's point is that many faults in C are diagnosed,
if at all, by a very hard to analyse output (a core dump).
Whereas in Ocaml more bugs are caught at compile time, and,
often a bug at run time has some simple abstract information
such as an exception constructor name, which help in pinpointing
the problem.

I don't think the claim was *elimination* as much as *improvement*.

However I thin David is missing my argument if he's thinking I am
arguing for a more relaxed type system: on the contrary I want an
even tighter type system. The problem is that the cost is likely
to be unsoundness -- in the process of making the type system
more expressive, we're bound to be forced to let some ill-typed
programs through because it is no longer feasible to prove
well-typedness in all cases.

My argument is that this just isn't a problem to worry about:
the only difference is that existing buggy programs which
were previously judged type correct, are no longer decided
as type correct. In some cases a program will be let through
by BOTH type systems, and in others the more expressive 
system will find the error, so the fact that the type system
is unsound is not a problem: our confidence in the correctness
of the program is *enhanced* despite the unsoundness.

Furthermore, my program which today is accepted may be rejected
tomorrow when a theorist finds some way to reduce the unsoundness
by catching more cases. This is impossible if you don't let me
write the annotations just because you can't prove the well
typedness right now!

BTW: when I say 'type system' and 'soundness' I mean
*static type checking*. I do not consider dynamic typing
as a type system in this sense. Any type test at run time
is instant proof of unsoundness of the type system:
an ill typed program has been allowed to escape to run time.

The fact that a policeman is set to catch the inmate who
escaped from jail does not in any way diminish the fact
the inmate indeed escaped, and the jail security system
was unsound (Ouch .. new season of Prison Break .. :)


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[Andrej Bauer]

At the danger of repeating myself (for which I apologize), I would like 
to convince skaller that he does not want unsound type systems. (What 
skaller calls "sound" I call "safety property" in my previous post.)

Skaller, you want something like this:

(a) expressive power (dependent types, subsets, you-name-it)

(b) soundness, in the following form:
     * the compiler rejects obvious nonsense
     * the result of a compilation is a program and a list of
       assertions which the compiler was unable to verify

This I would call "controlled unsoundness" which at least allows the 
human to see what needs to be verified to guarantee soundness. It's much 
better than the sort of unsoundness that skaller seems to be advocating.

There is actually a new minor point I want to make: you cannot postpone 
all problems with typechecking to runtime. Only very simple conditions, 
such as bounds checks, can be checked at runtime.

It is very easy to come up with preconditions that are computationally 
unverifiable. For example, you might have a numerical method for 
zero-finding which only works if the input is a function satisfying a 
funky condition, e.g., "the function is convex". How are you going to 
check that at runtime?

Or to give you a much more simplistic example:

fun find_zero (f: int -> int where not (forall n:int, f(n) != 0)) {
   int i = 0;
   while (f(i) != 0) { i++; }
   return i;
}

How will you verify the precondition on f at runtime?  In this case I 
would expect the compiler to list all uses of find_zero applied to 
functions which are not known not have a zero. Let the human worry.

Andrej

Re: [Caml-list] Unsoundness is essential

[Lukasz Stafiniak]

A "sound program refuter" will not reject correct programs.

On 10/4/07, skaller <skaller@users.sourceforge.net> wrote:
>
> To be bold I propose type theorists have got it totally wrong.
>
> I want an unsound type system! It much better than the useless
> but 'sound' type system of Python, in which the type inference
> engine decides all values have type Object and proves
> in vacuuo that all programs are type-safe, only to do the
> dependent type checks at run time anyhow -- a cheat known
> as dynamic typing.

Re: [Caml-list] Unsoundness is essential

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 3303 bytes --]

Andrej Bauer a écrit :
> I too have a compulsive obsession to talk about logic, so here is my
> contribution.
>
> Logic is about details. It is only to be expected that in a
> willy-waving competition on a mailing list like ours everyone will get
> something wrong about such a tricky thing as Goedel's theorems (me
> included). For example:
>
> Christophe Raffalli:
>> - 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 ...
> In logic complete usually means: for every sentence A the system
> proves A or it proves not A. This has nothing to do with being able to
> interpret arithmetic. We can define completeness without reference to
> arithmetic.
Sorry, I see now that I was not clear enough :

Complete (at least in french) has many meanings, the one you said and
the fact that something true in every model is provable (which make a
lot of meaning depending to the models you are considering).
The two meanings are unrelated, because arithmetics is complete as is
any first order theory (this is Gödel Completeness theorem for predicate
logic), but incomplete because there are formula A such that neither A
nor not A are provable. This is quite confusing.

But in both case complete means "there are enough rules/axioms in the
system to do what I want". You are just making the "what I want"
more or less strong.

For type systems, if you replace proving by inhabited, they are usually
incomplete, but then, you can look for completeness relative to some
model (like realizability) ... and the answer is yes in some cases. This
is generally a good idea to search for a set of models large enough for
your type system to be complete ... because sometime you realize that
you forgot some usefull typing rules in your type system.

>
> (Presumably, a type system is complete if for every (closed) type A,
> A is inhabited or A -> void is inhabited. At least this would be the
> reading of completeness under propositions-as-types.)
>
> Christophe Raffalli:
>> - The 1st incompleteness theorem states that no theory containing
>> arithmetic is complete.
>
> No _sound_ theory interpreting arithmetic is complete.
Ok, this was implicit.
>
> Arnaud Spiwack wrote:
>> 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).
This is Tarski's result .... (actually Tarski proved that truth can not
even be defined by a formula of arithmetic, which imply that provability
and truth do not coincide because provable formula are definable).

-- 
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
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 17:04 +0200, Andrej Bauer wrote:
[]

Thanks. I think this is a very good interpretation of my intent.

> 3) Skaller would rather have poor safety guarantees than an inexpressive 
> type system that ties his hands.

That's not quite right: it isn't that typing prevents me writing
my programs (it does sometimes, but usually that indicates
a design fault). It's more like the lack of expressiveness prevents
me writing down the invariants and so forth I actually want to.
I have to keep them in my head, or write them as comments where
they're not sanity checked.

In Felix for example the standard library contains this:

// additive symmetric group
typeclass FloatAddgrp[t] {
  inherit Eq[t];
  virtual fun zero: 1 -> t;
  virtual fun add: t * t -> t;
  virtual fun neg: t -> t;
  virtual fun sub(x:t,y:t):t => add (x,neg y);

  reduce id (x:t): x+zero() => x;
  reduce id (x:t): zero()+x => x;
  reduce inv(x:t): x-x => zero();
  reduce inv(x:t): - (-x) => x;
  axiom sym (x:t,y:t): x+y == y+x;
}

typeclass Addgrp[t] {
  inherit FloatAddgrp[t];
  axiom assoc (x:t,y:t,z:t): (x+y)+z == x+(y+z);
  reduce inv(x:t,y:t): x+y-y => x;
}

and here I can encode a LOT more information about the type T
the typeclass describes than Haskell allows. Furthermore,
the 'reduce' axioms have operational semantics (Felix really
does apply these reductions) and the axioms can be tested by
using a statement like 

	check(1,2);

which is how I discovered floating point arithmetic isn't
associative -- an actual regression test failed. What is more
Felix allows a 'lemma' which is an axiom which is made into
a proof goal in Why format for submission to a theorem prover.

This notation is weak, and the Felix compiler cannot really 
prove much with it: for example it does not check instances 
of typeclasses meet their obligations.

But at least the semantics are encoded in the language
and type checked, I can make reasoned arguments based on the
stated semantics, and there is some hope someone will come
along and implement some actual proof procedures and/or
optimisations at a later date.

[I really have proven one trivial lemma using both Ergo
and Simplify.]

Vincent Aravantinos made the important point:

"If you allow everything (such as the "type expressive" C you are  
envisaging), the programmer will be tempted to use this "everything"  
whereas he could achieve the same with a "bounded" language."

and the admission of semantics into the system is the starting
point for allowing one to at least state some of those bounds
(even if there is little or no enforcement the bounds are
formalised).

> Goedel is dragged in only because his theorems tell us that the perfect 
> world does not exist, i.e., we cannot have decidable type checking of a 
> very expressive type system which also has sane safety properties.

Ooops, I am sprung!

>  Skaller seems to 
> think that the only option is to give up safety, as well, with which I 
> disagree. We need _controlled_ unsafety.

Actually I HOPED someone smart enough would dare make such a proposal.
I think I alluded to this idea in the claims that adding unsound
typing to the existing Ocaml type system such as non-zero integers
will not actually compromise safety, but rather enhance it.

However I just do not understand how to say 'It is safe up
to this point, and risky from there on'. I have no mental
concept of 'delimited unsoundness'.

In an analogous context I had no idea how to mix side-effecting
and functional code in a delimited way until I saw how Haskell
does it with Monads.

> My position is this:
> 
> i) Insist on good safety properties. If a program compiles without any 
> "ifs" and "buts", then it is safe (whatever that means). It the compiler 
> thinks the program might be unsafe it should try to compile anyhow, and 
> tell us why precisely it thinks it might be unsafe.

Of course, all pragmatic compilers offer switches to control this
kind of thing.

> iii) Of course, by combining i) and ii) we must then give up 
> decidability of type-checking. We can compensate for that loss by 
> _making compilers more interactive_. The current model, where a compiler 
> either succeeds on its own or fails completely, is not going to take us 
> much further. People from the automated theorem proving community learnt 
> a while ago that the interaction between the human and the computer is 
> the way to go.

Ah.

> A compiler should be able to take hints on how to check types. The 
> result of compilation should be one of:
> 
> - everything is ok
> 
> - the program contains a grave typing error which prevents
>    the compiler from emitting sane code, compilation is aborted
> 
> - the compiler generates sane code but also emits a list of assertions
>    which need to be checked (by humans or otherwise) in order to
>    guarantee safety
> 
> If we had compilers like that, they would greatly encourage good 
> programming practices.
> 
> You can read the above as my manifesto, if you wish.

This is quite good from an industrial viewpoint. The list of
assertions can be reduced by more work in selective areas
as a complement to testing. This gives managers control over risk.

It seems a consequence of this manifesto is that the asserting
of the assertions, if not their proofs, need to be encoded
into the program in an effort to reduce the size of the output
list.

A difficulty here is saying the assertions in a comprehensible
way which is well coupled to the original code. As you said
previously, this probably requires an interactive system.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote:

> Skaller, you want something like this:
> 
> (a) expressive power (dependent types, subsets, you-name-it)
> 
> (b) soundness, in the following form:
>      * the compiler rejects obvious nonsense
>      * the result of a compilation is a program and a list of
>        assertions which the compiler was unable to verify

Yes, I want something like that.

> This I would call "controlled unsoundness" 

As an (eX) motorcyclist I can agree .. riding a bike is like
having one continuous controlled road accident.. :)

> which at least allows the 
> human to see what needs to be verified to guarantee soundness. It's much 
> better than the sort of unsoundness that skaller seems to be advocating.

Sure, but my point does remain: the expressiveness is more or less
paramount. It is not so much that I personally desire it or not,
but that real programmers in the real world go out there and do
whatever is necessary to make programs work.

If you can produce a compiler with an expressive type system
but cannot yet create a complete list of unproven assertions,
that is still better than writing Python. In fact I write a lot
of Python even now. I do not do so in ignorance of the value
of static type checking! There is a good reason I choose it,
for example for the Felix build system.

It is not because I fear writing all the types Ocaml would
require, but because the need for 'dynamic typing' in this
kind of software and the lack of expressiveness in Ocaml
type system makes Ocaml unsuitable. Please note I'm *trying*
to explain the reason, but probably haven't got it right.

The point is, in the manifesto it should go like: expressiveness
first, then generating proof obligations, and also with time,
improving the automatic provers. 

The key thing is not to restrict expressiveness just because
the type system cannot fully cope.. making the typing more
expressive has many benefits by itself.

A stupid one: how can theoreticians test the efficacy of a new
algorithm with real world case data?


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote:

> It is very easy to come up with preconditions that are computationally 
> unverifiable.
[]
> Or to give you a much more simplistic example:
> 
> fun find_zero (f: int -> int where not (forall n:int, f(n) != 0)) {
>    int i = 0;
>    while (f(i) != 0) { i++; }
>    return i;
> }
> 
> How will you verify the precondition on f at runtime?  In this case I 
> would expect the compiler to list all uses of find_zero applied to 
> functions which are not known not have a zero. Let the human worry.

One 'solution' is a timeout. However I would apply the timeout
to the actual find_zero function, not the pre-condition.

The 'convex' example is better, because the pre-condition is not
so obviously closely coupled to the calculation. Also, the
result of a calculation is likely to be simply *wrong*.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[rossberg]

skaller wrote:
>
> All advanced programming languages have unsound type systems
> of necessity. Some falsely claim soundness by denying the
> expression of certain type information (eg array bounds
> or the type of integers excluding zero).

No. Soundness is the absence of /untrapped/ errors. Exceptions are
/trapped/ errors. Huge difference, esp with respect to safety and
security.

- Andreas

Re: [Caml-list] Unsoundness is essential

[Arnaud Spiwack]

> Sure, but my point does remain: the expressiveness is more or less
> paramount. It is not so much that I personally desire it or not,
> but that real programmers in the real world go out there and do
> whatever is necessary to make programs work.
>   
That would be wonderful if they did work... Unfortunately to my 
knowledge, a software is a mere collection of bugs, glued together with 
a couple of features. Or perhaps I'm being a little optimistic here :p .
> A stupid one: how can theoreticians test the efficacy of a new
> algorithm with real world case data?
>   
This is obviously not possible (if I understand the question) since real 
world data don't obey any known law. However they can be modelized for 
further use.

Anyway that is not what you were talking about and I think the 
discussion got confused due to the wild mix of different notions. One 
interpretation of what you suggest is to replace pieces of proof by 
run-time assertions, this sounds a plausible idea, though this is 
probably not a good thing to do for a finished product. It could however 
allow the program to be tested before one tries to prove it. There are 
various other ways to do it, though.

Anyway, just be aware that having a more powerful type system usually 
means much more program that type. Contrary to what you seem to fear.


Arnaud Spiwack

Re: [Caml-list] Unsoundness is essential

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 1641 bytes --]


> On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote:
>
>   
>> It is very easy to come up with preconditions that are computationally 
>> unverifiable.
>>     
> []
>   
>> Or to give you a much more simplistic example:
>>
>> fun find_zero (f: int -> int where not (forall n:int, f(n) != 0)) {
>>    int i = 0;
>>    while (f(i) != 0) { i++; }
>>    return i;
>> }
>>
>> How will you verify the precondition on f at runtime?  In this case I 
>> would expect the compiler to list all uses of find_zero applied to 
>> functions which are not known not have a zero. Let the human worry.
>>     
>
>   
What's the problem ? If you program with the above function and apply it
to a function f,
this means you know f will reach zero (otherwise your program will
loop). But if you know it,
this should mean that you can prove it from the definition of f ?

So the only reason to have today programming language that gives not
enough safety is because the cost
of the formal proof is still to big (by cost, I mean cost to write
proof, but also the cost of learning how
to write proof ...)

-- 

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
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 19:56 +0200, rossberg@ps.uni-sb.de wrote:
> skaller wrote:
> >
> > All advanced programming languages have unsound type systems
> > of necessity. Some falsely claim soundness by denying the
> > expression of certain type information (eg array bounds
> > or the type of integers excluding zero).
> 
> No. Soundness is the absence of /untrapped/ errors. 

Fair ..

> Exceptions are /trapped/ errors. 

I chose not to accept that definition. I use instead
"trapped at compile time", meaning "in advance of running
the program".

Otherwise you could say dynamically typed languages were
strongly typed and sound.

I'm not saying that it is a bad thing to emit code to
generate diagnostics at run time, if you can't prove
safety at compile time .. I AM saying that doing that
means the type system is unsound, because by type system
I mean "static type checking".

The point is that static checks are hopefully rigorous:
what ever properties they ensure they ensure them 
for certain, once and for all time.

Whereas dynamic checks prove only, in some cases,
that there is a bug and thus you have to actually
test the program with good coverage, and even then
you learn little UNLESS there is a bug :)

Also note, specified exceptions are not suitable traps:
this is a conformance issue and not really related,
but it is worth noting that if a catchable exception
is specified, the condition that caused it to be raised
isn't necessarily an error:

	try:
		x = "Bad" +42
	except:
		print "Python WILL print this"

This code is perfectly well defined and contains no
errors, not even a type error. Adding a string to an integer
raises TypeError in Python, and this is mandatory, so this
behaviour is well defined and can be used as a programming
technique (and it is!), there is no 'trapped' error here.

C/C++ does this right: if a program is 'ill-formed' then
a diagnostic must be issued. Throwing an exception silently
is NOT allowed. [C/C++ doesn't mandate diagnostics always because
some are too hard to detect]



-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[Ken Rose]

skaller wrote:
> It seems a consequence of this manifesto is that the asserting
> of the assertions, if not their proofs, need to be encoded
> into the program in an effort to reduce the size of the output
> list.
>
> A difficulty here is saying the assertions in a comprehensible
> way which is well coupled to the original code. As you said
> previously, this probably requires an interactive system.
>
>   
I think that in an industrial system, the assertions are going to have 
to travel with the code.  I can't imagine that a system that needs a 
particular, highly trained programmer (the one who wrote the thing) to 
cajole the compiler into generating code will ever be satisfactory to 
any business that writes code.

 - ken

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 20:17 +0200, Arnaud Spiwack wrote:
>  
> That would be wonderful if they did work... Unfortunately to my 
> knowledge, a software is a mere collection of bugs, glued together with 
> a couple of features. Or perhaps I'm being a little optimistic here :p .

Lol! The one I hear is that a program is defined to be the tracks
left by thousands of bugs.

In the case of Ocaml, we might say that when many messages
of the form: "This expression has type SquarePeg but is here
used with type RoundHole" have been fixed by sandpapering
off the edges of those pegs .. the program is the residual sawdust
that remains on the floor after thousands of curses.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 13:02 -0700, Ken Rose wrote:
> skaller wrote:
> > It seems a consequence of this manifesto is that the asserting
> > of the assertions, if not their proofs, need to be encoded
> > into the program in an effort to reduce the size of the output
> > list.
> >
> > A difficulty here is saying the assertions in a comprehensible
> > way which is well coupled to the original code. As you said
> > previously, this probably requires an interactive system.
> >
> >   
> I think that in an industrial system, the assertions are going to have 
> to travel with the code.  I can't imagine that a system that needs a 
> particular, highly trained programmer (the one who wrote the thing) to 
> cajole the compiler into generating code will ever be satisfactory to 
> any business that writes code.

There is a such a system, I can't remember its name. The proofs and
types etc do travel with the code, but the 'language' is designed with
holes to fill in interactively, and the compiler fills them out
partially then prompts for the balance. After supply, more holes
are filled in by the same process.

So for export, you get a complete linear representation of 
the conventional kind but you use a GUI to develop it.
Perhaps someone can provide a link (it's quite well known
very advanced category theory based system).


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[rossberg]

skaller wrote:
>
>> Exceptions are /trapped/ errors.
>
> I chose not to accept that definition. I use instead
> "trapped at compile time", meaning "in advance of running
> the program".

As a definition for what?

> Otherwise you could say dynamically typed languages were
> strongly typed and sound.

In fact, technically, they are. People have used the term "unityped" for it.

> C/C++ does this right: if a program is 'ill-formed' then
> a diagnostic must be issued. Throwing an exception silently
> is NOT allowed. [C/C++ doesn't mandate diagnostics always because
> some are too hard to detect]

This paragraph sounds like a contradiction in itself.

More importantly, an OCaml program performing div 0 isn't "ill-formed", it
has a perfectly well-defined, safe semantics (in precisely the same way as
adding a string in Python). See the library docs.

- Andreas

Re: [Caml-list] Unsoundness is essential

[skaller]

On Thu, 2007-10-04 at 23:07 +0200, rossberg@ps.uni-sb.de wrote:
> skaller wrote:
> >
> >> Exceptions are /trapped/ errors.
> >
> > I chose not to accept that definition. I use instead
> > "trapped at compile time", meaning "in advance of running
> > the program".
> 
> As a definition for what?

What trapped means.

> > Otherwise you could say dynamically typed languages were
> > strongly typed and sound.
> 
> In fact, technically, they are. People have used the term "unityped" for it.

That isn't what I meant at all. Python is statically unityped, but
dynamically it has integers, reals, strings, etc. Type errors
in Python are not 'trapped' .. they're impossible.

> > C/C++ does this right: if a program is 'ill-formed' then
> > a diagnostic must be issued. Throwing an exception silently
> > is NOT allowed. [C/C++ doesn't mandate diagnostics always because
> > some are too hard to detect]
> 
> This paragraph sounds like a contradiction in itself.

Yes, but it isn't. If the specification was to throw
a catchable exception, then that would be a requirement
on implementation which would permit programmers to divide
by zero deliberately. In that case, a divide by zero error
is impossible to detect because it can't be distinguished
from the legitimate division by zero for the purpose
of raising an exception.

> More importantly, an OCaml program performing div 0 isn't "ill-formed", it
> has a perfectly well-defined, safe semantics (in precisely the same way as
> adding a string in Python). See the library docs.

I didn't claim otherwise: I claim it is a very bad idea
to permit a program to do obvious bullshit like divide by zero
(for integers I mean).

Note I'm NOT saying Ocaml *implementation* shouldn't raise an exception,
just that the language specification should not require it do so.
The difference is in one case the operation is semantically well defined
and thus definitely not detectable as an error, whereas in the other
it is not defined, and so is unequivocably an error.

Oh well this was fun but I'm off interstate without a computer for
a week.. hope my Airbus doesn't divide any empty lists by zero ..

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Unsoundness is essential

[Arnaud Spiwack]

> In the case of Ocaml, we might say that when many messages
> of the form: "This expression has type SquarePeg but is here
> used with type RoundHole" have been fixed by sandpapering
> off the edges of those pegs .. the program is the residual sawdust
> that remains on the floor after thousands of curses.
>   
^_^

You might really be interested in toying around with interactive 
systems. I would probably advise Adga2 ( 
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php ) or Epigram 1 ( 
http://www.e-pig.org/ ).

Interactive programming tends to save quite a few weird error messages. 
The type systems of these are of the sort we were discussing on this thread.


Arnaud Spiwack

Re: Unsoundness is essential

[Bárður Árantsson]

skaller wrote:

> On Thu, 2007-10-04 at 23:07 +0200, rossberg@ps.uni-sb.de wrote:
>> skaller wrote:
>>>> Exceptions are /trapped/ errors.
>>> I chose not to accept that definition. I use instead
>>> "trapped at compile time", meaning "in advance of running
>>> the program".
>> As a definition for what?
> 
> What trapped means.
> 
>>> Otherwise you could say dynamically typed languages were
>>> strongly typed and sound.
>> In fact, technically, they are. People have used the term "unityped" for it.
> 
> That isn't what I meant at all. Python is statically unityped, but
> dynamically it has integers, reals, strings, etc. Type errors
> in Python are not 'trapped' .. they're impossible.
> 

$ python
Python 2.5.1 (r251:54863, Oct  1 2007, 21:44:24)
[GCC 4.1.2 (Gentoo 4.1.2)] on linux2
Type "help", "copyright", "credits" or "license" for more information.
 >>> 1 + "a"
Traceback (most recent call last):
   File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'int' and 'str'

-- 
Bardur Arantsson
<bardurREMOVE@THISscientician.net>

- I may not have morals, but I do have standards.