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

Browse thread
partial application warning unreliable?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2005-12-09 (17:53)
From: Andrej Bauer <Andrej.Bauer@a...>
Subject: Re: [Caml-list] partial application warning unreliable?
It seems unwise to me to try to capture the notion of side-effects via a
type like "0" or "1". Skaller is talking as if the type

  int -> 0

means "a command with side-effects". But "int -> int" can have plenty
side effects, too. A better solution would be to refine types so that
they keep track of which things have side-effects (monads!).

A discussion along the lines "do commands return void or unit?" is
flawed. The type void, in any reasonable semantics (assuming eager
language here), will be inhabited exactly by non-terminating
expressions, whereas "unit" will be inhabited by non-terminating and
terminating ones. Neither of these say anything about side-effects.

I understand ocaml's solution to be as follows: it is understood that
expressions of _all_ types may involve side effects (as well as
exceptions). While the result of a command may be ignored, as it is
uninteresting, the cruical bit is that a command may terminate or not.
This means that its type must posses terminating as well as
non-terminating values, i.e., _unit_ is the right choice. Void would be
the right choice only if all commands were non-terminating, or if all
were terminating.

Andrej Bauer