From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q397C7KL022041 for ; Mon, 9 Apr 2012 09:12:07 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtoBAHOKgk/RVdK2mGdsb2JhbABCp2CRVAgiAQEBAQEICQ0HFCeCCQEBAQICEgITGQEbEgsBAwwGBQsNDSEiAREBBQEKEgYTEhCHXQEDCwugLQqMGYJxhDwKGScDCleBDgEFC5BPBJVsgRGNRT2EDA X-IronPort-AV: E=Sophos;i="4.75,393,1330902000"; d="scan'208";a="153236308" Received: from mail-iy0-f182.google.com ([209.85.210.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 Apr 2012 09:12:01 +0200 Received: by iahk25 with SMTP id k25so9031370iah.27 for ; Mon, 09 Apr 2012 00:12:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=bAsT8E3mG0elt0CFJzJ6RMz2ltSRwKZFbc7mrZ7aJVE=; b=cEbEuNO4hLR1kU0j1P3EfFXj01QIVErpjmv5piMylRrxDJY7XaKDSORlODXwFFA0p2 CW6FbjzZSt3mjVFCtoPLPh7pS04Wj19prt/jrsRStnYSAJ/Z7NsyJkvkkCxyrseOdxDL 7QqE5xg4Y98DobaKzuPm/OComi4fnuseqwAq7LFXFujLXO2Tpb/3YQbm7xy0OXRmEPv9 gG2rinhKYBbpyicuCoamJgyOyDzqs0aOgziaYk5loJDXL2pMAnXKV1jX+tE4ei9Ic5EN 5/0T9VASRSkZRvixNyQhKJm/q54zZdgA/Hu5eZvonTc99oG4HREMS0smtlv4C8aKxB61 h8Vw== Received: by 10.50.219.199 with SMTP id pq7mr4012041igc.70.1333955520561; Mon, 09 Apr 2012 00:12:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.140.100 with HTTP; Mon, 9 Apr 2012 00:11:20 -0700 (PDT) In-Reply-To: <20120409065143.GO13251@kerneis.info> References: <20120407151452.GA12887@siouxsie> <1333949868.9770.2.camel@Nokia-N900> <20120409065143.GO13251@kerneis.info> From: Gabriel Scherer Date: Mon, 9 Apr 2012 09:11:20 +0200 Message-ID: To: Gabriel Kerneis Cc: Cedric Cellier , caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q397C7KL022041 Subject: Re: [Caml-list] Articles on using types for enhancing sw-quality? In the next OCaml version, you will be able to do that more cleanly with GADTs. That is actually one of the advantages of having GADTs in the language; while the typing effects can be (more or less awkwardly) encoded in existing constructions, such encodings tends to rely on higher-order constructions and are not very efficient at runtime. By contrast, with plain GADTs, you get the usual algebraic datatypes (which are very efficiently handled by the compiler), with some additional goodness due to type-informed dead clause removal. type 'a li = | Nil | Cons of 'a * 'a li let head (Cons (hd, _tl)) = hd (* ocamlopt -dlambda: (let (head/1037 (function param/1068 (if param/1068 (field 0 param/1068) (raise (makeblock 0 (global Match_failure/16g) [0: "test.ml" 5 4]))))) *) (* size-indexed lists *) type z type 'n s type ('a, _) gli = | GNil : ('a, z) gli | GCons : 'a * ('a, 'n) gli -> ('a, 'n s) gli let ghead : type a n . (a, n s) gli -> a = fun (GCons (hd, _tl)) -> hd (* ocamlopt -dlambda: (let (ghead/1051 (function param/1069 (field 0 param/1069))) *) On Mon, Apr 9, 2012 at 8:51 AM, Gabriel Kerneis wrote: > On Mon, Apr 09, 2012 at 07:37:48AM +0200, Cedric Cellier wrote: >> > - Chung-chieh Shan and Oleg's "Lightweight Static Capabilities" >> > presents several examples of phantom types and a general design method >> > to use them to enhance program safety: >> >   http://okmij.org/ftp/papers/lightweight-static-capabilities.pdf >> >> I attempted to read this one out of curiosity, >> and it raised a question: is there a way to write >> these unsafe functions (List.Unsafe.tail/head...) in pure OCaml? > > It depends on what you call "pure OCaml".  Using the evil Obj module: > > let head (l : 'a list) : 'a = Obj.obj (Obj.field (Obj.repr l) 0) ;; > > which relies on the underlying representation (use at your own risks) and > generates a call to caml_array_unsafe_get: >    L1: const 0 >        push >        acc 1 >        ccall caml_array_unsafe_get, 2 >        return 1 > > Similarly: > let tail (l : 'a list) : 'a list = Obj.obj (Obj.field (Obj.repr l) 1) ;; > > Best, > -- > Gabriel > > -- > Caml-list mailing list.  Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >