Accueil     Ŕ propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis ŕ jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml ŕ l'adresse ocaml.org.

Locally-polymorphic exceptions [was: folding over a file]
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-10-04 (15:04) From: Andrej Bauer Subject: Re: [Caml-list] Unsoundness is essential
```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

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

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

```