From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <fernando@gatech.edu>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled 
	version=3.1.3
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by yquem.inria.fr (Postfix) with ESMTP id 702ABBC69
	for <caml-list@yquem.inria.fr>; Fri, 16 Nov 2007 20:32:54 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgAAAHd/PUeCz6Woi2dsb2JhbACPDQEBAQgEBg8a
X-IronPort-AV: E=Sophos;i="4.21,428,1188770400"; 
   d="scan'208";a="4340595"
Received: from deliverator6.gatech.edu ([130.207.165.168])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 16 Nov 2007 20:32:53 +0100
Received: from deliverator6.gatech.edu (localhost [127.0.0.1])
	by localhost (Postfix) with SMTP id BD6CC1821;
	Fri, 16 Nov 2007 14:32:52 -0500 (EST)
	(envelope-from fernando@gatech.edu)
Received: from mailprx3.gatech.edu (mailprx3.prism.gatech.edu [130.207.171.17])
	(using TLSv1 with cipher EDH-RSA-DES-CBC3-SHA (168/168 bits))
	(Client CN "smtp.mail.gatech.edu", Issuer "RSA Data Security, Inc." (verified OK))
	by deliverator6.gatech.edu (Postfix) with ESMTP id CE4551807;
	Fri, 16 Nov 2007 14:32:26 -0500 (EST)
	(envelope-from fernando@gatech.edu)
Received: from localhost (gato.physics.und.nodak.edu [134.129.186.227])
	(using TLSv1 with cipher EDH-RSA-DES-CBC3-SHA (168/168 bits))
	(No client certificate requested)
	(sasl: method=PLAIN, username=gtg783d@mailprx3.gatech.edu, sender=n/a)
	by mailprx3.gatech.edu (Postfix) with ESMTP
	id A376121B5; Fri, 16 Nov 2007 14:32:25 -0500 (EST)
	(envelope-from fernando@gatech.edu)
Date: Fri, 16 Nov 2007 13:32:19 -0600
From: Fernando Alegre <fernando@gatech.edu>
To: David Allsopp <dra-news@metastack.com>
Cc: 'caml-list' <caml-list@yquem.inria.fr>
Subject: Re: [Caml-list] Compiler feature - useful or not?
Message-ID: <20071116193219.GB22392@gato.physics.und.nodak.edu>
References: <20071116181024.GA15777@gato.physics.und.nodak.edu> <00a701c82885$726915b0$017ca8c0@countertenor>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <00a701c82885$726915b0$017ca8c0@countertenor>
User-Agent: Mutt/1.5.9i
X-Spam: no; 0.00; compiler:01 compile-time:01 trivial:01 ocaml:01 run-time:01 ocaml:01 sml:01 equality:01 hacks:01 imho:01 wrote:01 exception:01 exception:01 ints:01 caml-list:01 

On Fri, Nov 16, 2007 at 07:18:18PM -0000, David Allsopp wrote:

> optimisation but permission_of_int (or whatever conversion construct you
> came up with) would need to raise an exception on invalid input.

And that is why "permission_of_int" would not be considered part of
the core language.

However, things like what I proposed earlier, such as

(x :> n finite), whenever x and n are known at compile-time

or

(int :> even), if the encoding of an even number 2*n is given by n

will never raise an exception, are sound and could be part of the core
language. The first case is straightforward, but extending it safely
(i.e. no code, only type equations) is not obvious. The second case
needs some way to specify the encoding along with a proof that it is
sound, and this is not trivial either. However, both extensions seem
theoretically possible and in line with the philosophy of the Caml type
system.

> Consider string_of_int (error-free - all ints can be represented as strings)
> vs. int_of_string which raises an exception if the string is not a
> recognised representation of an int.
> 
> > While exceptions are needed for I/O, no core expression should raise an
> > exception.
> 
> compare = compare;;
> 
> (though cf. SML equality types)
> 
> Good code using permission_of_int (as with good code using int_of_string)
> would ensure that the int is valid before ever calling permission_of_int but
> the permission_of_int itself needs to be able to raise the exception to
> fulfil the contract of its type (int -> permission).

Exactly. And that is the reason why, IMHO, we may never see such an
extension to OCaml language, since it is primarily a research language
for type checking. (And so run-time "usefulness", or hacks, are
secondary to the OCaml team.)

Thanks,
Fernando