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 4109EBB83 for ; Mon, 29 May 2006 22:52:08 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k4TKq7jI026414 for ; Mon, 29 May 2006 22:52:07 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id WAA25003 for ; Mon, 29 May 2006 22:52:06 +0200 (MET DST) Received: from fmsmga101.fm.intel.com (mga05.intel.com [192.55.52.89]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k4TKq5mr022011 for ; Mon, 29 May 2006 22:52:06 +0200 Received: from fmsmga001.fm.intel.com ([10.253.24.23]) by fmsmga101.fm.intel.com with ESMTP; 29 May 2006 13:52:04 -0700 Received: from orsmsx332.jf.intel.com (HELO orsmsx332.amr.corp.intel.com) ([192.168.65.60]) by fmsmga001.fm.intel.com with ESMTP; 29 May 2006 13:52:04 -0700 X-IronPort-AV: i="4.05,184,1146466800"; d="scan'208"; a="43989735:sNHT14984207" Received: from orsmsx409.amr.corp.intel.com ([192.168.65.58]) by orsmsx332.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.211); Mon, 29 May 2006 13:52:04 -0700 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] Re: immutable strings (Re: Array 4 MB size limit) Date: Mon, 29 May 2006 13:52:01 -0700 Message-ID: <196F1D996F92CD46A542EA519DB8CE4703CCAACC@orsmsx409> Thread-Topic: [Caml-list] Re: immutable strings (Re: Array 4 MB size limit) thread-index: AcaANXWbIX3Vuj9PTaSxNQrQZotXagCd4rVwAC0Ty2A= From: "Harrison, John R" To: "Martin Jambon" , "Caml List" Cc: "Harrison, John R" X-OriginalArrivalTime: 29 May 2006 20:52:04.0130 (UTC) FILETIME=[BD84C820:01C68361] X-Miltered: at nez-perce with ID 447B5EF7.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 447B5EF5.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; johnh:01 ocaml:01 const:01 well-typed:01 mutable:01 caml-list:01 arbitrary:01 abstract:01 functions:01 functions:01 immutable:01 strings:01 strings:01 artificial:01 theorem:02 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 Hi Martin, | OK, but let's be pragmatic: what kind of interface and implementation do | you have in mind? I did indeed have a very specific example in mind, my theorem prover HOL Light. I have an OCaml type of typed lambda-terms: type term =3D Var of string * hol_type | Const of string * hol_type | Comb of term * term | Abs of term * term The type "term" is private, and the abstract type interface only permits you to construct well-typed terms, via interface functions like "mk_var" and "mk_comb". For example, the call "mk_comb(s,t)" gives "Comb(s,t)" provided the types agree, and fails otherwise. I would like the user to be able to write "mk_var(x,ty)" and the net result to be just one cons "Var(x,ty)" with "x" and "ty" identical to the input arguments. But with mutable strings, it is possible in principle for the string "x" inside that object to get modified by other code. Of course, it's a bit artificial, but I would like it to be impossible, given that the principle of LCF provers is that the user should be able to use arbitrary programs while having soundness enforced by the ML type system. Of course, I can use my own private type of strings, but then I need to convert every time I use standard library functions, pattern matching is a bit less convenient, etc. John.