From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 1806FBB9C for ; Fri, 9 Dec 2005 18:53:13 +0100 (CET) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jB9HrBFk006133 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Fri, 9 Dec 2005 18:53:12 +0100 Received: from localhost ([127.0.0.1] ident=andrej) by haka.fmf.uni-lj.si with esmtp (Exim 4.50) id 1EkmQS-0001Pj-25; Fri, 09 Dec 2005 18:52:56 +0100 Message-ID: <4399C477.6030606@andrej.com> Date: Fri, 09 Dec 2005 18:52:55 +0100 From: Andrej Bauer User-Agent: Debian Thunderbird 1.0.2 (X11/20050331) X-Accept-Language: en-us, en MIME-Version: 1.0 To: skaller Cc: Andreas Rossberg , caml-list@yquem.inria.fr Subject: Re: [Caml-list] partial application warning unreliable? References: <1134009551.10435.24.camel@rosella> <20051208.121012.49167263.garrigue@math.nagoya-u.ac.jp> <1134092611.8940.57.camel@rosella> <439976E0.305@ps.uni-sb.de> <1134148648.8940.167.camel@rosella> In-Reply-To: <1134148648.8940.167.camel@rosella> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 127.0.0.1 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com X-SA-Exim-Scanned: No (on haka.fmf.uni-lj.si); SAEximRunCond expanded to false X-Miltered: at concorde with ID 4399C487.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 refine:01 monads:01 semantics:01 terminating:01 ocaml's:01 terminate:01 terminating:01 posses:98 partial:01 exceptions:01 int:01 int:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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