From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 4DC52BB9C for ; Fri, 9 Dec 2005 19:51:31 +0100 (CET) Received: from smtp06.web.de (smtp06.web.de [217.72.192.224]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jB9IpUED001494 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 9 Dec 2005 19:51:31 +0100 Received: from [84.165.182.142] (helo=wiko) by smtp06.web.de with smtp (WEB.DE 4.105 #340) id 1EknL8-0001Mv-00 for caml-list@yquem.inria.fr; Fri, 09 Dec 2005 19:51:30 +0100 Message-ID: <002c01c5fcf1$f791e9e0$15b2a8c0@wiko> From: "Andreas Rossberg" To: 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> Subject: Re: [Caml-list] partial application warning unreliable? Date: Fri, 9 Dec 2005 19:54:21 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 6.00.2800.1506 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1506 Sender: AndreasRossberg@web.de X-Sender: AndreasRossberg@web.de X-Miltered: at nez-perce with ID 4399D232.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; rossberg:01 caml-list:01 andrej:01 monads:01 semicolon:01 wrote:01 sourceforge:01 partial:01 andreas:01 andreas:01 int:01 int:01 seems:03 unit:03 implicit:03 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 "skaller" wrote: > Felix allows > > f: int -> 0 > > but not > > g: 0 -> int Then your "0" is not a proper type in the usual formal sense. Even less is it the type-theoretic 0. As Andrej Bauer points out, void vs unit has nothing to do with side effects. If you want to capture side effects properly in a type system the known approaches are effect systems or monads. In fact, your 0 looks somewhat like a monad type with implicit injection and semicolon as a kind of forgetting bind operator. But it seems sufficiently adhoc to make any type-theoretic interpretation difficult. - Andreas