From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id B0C35822AC for ; Fri, 17 Nov 2017 03:05:08 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cedilla@gmail.com; spf=Pass smtp.mailfrom=cedilla@gmail.com; spf=None smtp.helo=postmaster@mail-wm0-f45.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of cedilla@gmail.com) identity=pra; client-ip=74.125.82.45; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="cedilla@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of cedilla@gmail.com designates 74.125.82.45 as permitted sender) identity=mailfrom; client-ip=74.125.82.45; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="cedilla@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wm0-f45.google.com) identity=helo; client-ip=74.125.82.45; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="postmaster@mail-wm0-f45.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AYZ/RAxwA3R2YS8HXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0uMWIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2TxTor3az9T8fHAnkfUow?= =?us-ascii?q?f7ytW92as8Pi5umt8oebSgBJgnLpcLptJQ/wpADQsOEZhIJjLuA6zR6f8VVSfO?= =?us-ascii?q?ED/25lKRqsnhLn4cH4qJVu/yVUv/sJ+MtJUKG8dKM9G+8LRA86Onw4sZW4/SLI?= =?us-ascii?q?ShGCsz5FCj0b?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0D3AQDzQg5ahi1SfUpcGwEBAQEDAQEBC?= =?us-ascii?q?QEBAYQPC24UEweDeIE2mA+BfYJ/jheFWYIBCiWDOIFeAoRYB0IVAQEBAQEBAQE?= =?us-ascii?q?BARIBAQEICwsIKC+COAUBHgEFgjwBAQEBAgEjBBkBGx0BAwELBgULDRUVAgIhA?= =?us-ascii?q?QERAQUBHAYTigsBAwgFCBCcUECMDYFtGAUBHIMKBYNiChknDViCYwEBAQEBAQE?= =?us-ascii?q?DAQEBAQEBAQEYAgYSgyJFgUKGaYJrJIFEchKCVoJjBYoEKYhaXYU8iF49h3CII?= =?us-ascii?q?YR5ghVhiS+HI4xxOohxFAUfgRUPJoIXNCEIHRVJNYIvCYIaKh+CFCA2AYowgVU?= =?us-ascii?q?BAQE?= X-IPAS-Result: =?us-ascii?q?A0D3AQDzQg5ahi1SfUpcGwEBAQEDAQEBCQEBAYQPC24UEwe?= =?us-ascii?q?DeIE2mA+BfYJ/jheFWYIBCiWDOIFeAoRYB0IVAQEBAQEBAQEBARIBAQEICwsIK?= =?us-ascii?q?C+COAUBHgEFgjwBAQEBAgEjBBkBGx0BAwELBgULDRUVAgIhAQERAQUBHAYTigs?= =?us-ascii?q?BAwgFCBCcUECMDYFtGAUBHIMKBYNiChknDViCYwEBAQEBAQEDAQEBAQEBAQEYA?= =?us-ascii?q?gYSgyJFgUKGaYJrJIFEchKCVoJjBYoEKYhaXYU8iF49h3CIIYR5ghVhiS+HI4x?= =?us-ascii?q?xOohxFAUfgRUPJoIXNCEIHRVJNYIvCYIaKh+CFCA2AYowgVUBAQE?= X-IronPort-AV: E=Sophos;i="5.44,406,1505772000"; d="scan'208,217";a="301161826" Received: from mail-wm0-f45.google.com ([74.125.82.45]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Nov 2017 03:05:07 +0100 Received: by mail-wm0-f45.google.com with SMTP id z3so3626672wme.5 for ; Thu, 16 Nov 2017 18:05:07 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=mMTQPnM+LM70ngc2+4MIEA9KsrRmcxV6H6BOnKUN2Qk=; b=nRSqsvkMg/kDUluu5io+oiiqHQe6BP6DuINmoaP4OCqAqlEQDfDm3oqgpkQGdnchT3 1aTpge6AvNhgUzJCrxmx6LzYr/17oW1GiOls0lKTocJP+W/tnIyw0K6vzmjw3PlwYMzB vOVbHuep4DnG9ZEqW0ksw+Az0+/p4nwahyrUNdKvgEF7IhYbPCP5PJgurepOYuzCRT4Y Pcw6+ZWWhUX3gkhSnkbJXsJe8kzE3z9bSMI3ZoHngL5T9jFFslp9gbjlTPlFKiv4ExGh lAMtbs+mK+GInNHuiMV6sQ1KdnCp1BSvRVn9Wv+hjqSlbMZkJgijdfYxpPAB5wi/Flvy zD3Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=mMTQPnM+LM70ngc2+4MIEA9KsrRmcxV6H6BOnKUN2Qk=; b=SJKeiclHapHBmjeg/m3PyJO5hJ9at7Vx/vw7ipSXdWpP1ftQ/n1WKmwzrgJaQRjks2 cHtu2nNxtI72eMy2EISwN5JFeDIvchHafJpEs2XTiprNn86NI0bYoCiNAb4hdc7WoJ8O tClG7DBwm1qLZDocO9ZZgGjwkFgDJS863GKZT0Ei2z1ZqpDudYbUgcaQ0Toa0M/IvSHV MzXeqArkVJcJe5L6veH+sea6Dvz4xHzyXdCade4ifCin9bNVH5ZE5oM8wZ5kRizot+f2 laO5jNNBQmaCuBfrHrn9zr6DJrmzs3seuOPpKdgk8MUHBvGD4TtE9Ov9wTxnTZqi5D22 CC5g== X-Gm-Message-State: AJaThX4xApR7wNqJtWpvrxr5MBSWXBqWqJ6FnSIWYnJJ5DI99FnbVnP4 GPjz95wYiodwuiwwXvpXnnpAhoTGoY5IM8ChiIc= X-Google-Smtp-Source: AGs4zMa6tGVauwuJKycaYsZSlKYqNBDvvXhXufhjTD5OYj/7GAO3NLP+9oEbwM0LEsBr3nuRhSgyDbCjQDiVaV70bKk= X-Received: by 10.80.139.65 with SMTP id l59mr5328124edl.187.1510884307081; Thu, 16 Nov 2017 18:05:07 -0800 (PST) MIME-Version: 1.0 Received: by 10.80.245.226 with HTTP; Thu, 16 Nov 2017 18:05:06 -0800 (PST) In-Reply-To: References: From: Reed Wilson Date: Thu, 16 Nov 2017 18:05:06 -0800 Message-ID: To: Yawar Amin Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary="94eb2c194a066ba1b3055e242a2f" X-Validation-by: cedilla@gmail.com Subject: Re: [Caml-list] Subtyping (or something like it) --94eb2c194a066ba1b3055e242a2f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable That looks pretty good! One of the things I tried was to use the private type declaration. However, I failed to take the coercion into account, so I thought they couldn't actually be used as bigarrays. I'd still like to avoid casting to bigarrays, but unless a miracle comes along, I think this is how I'll do it. Thanks! On Thu, Nov 16, 2017 at 4:49 PM, Yawar Amin wrote: > Hi Reed, this is maybe not exactly what you specified, but a `private` > type abbreviation ( https://caml.inria.fr/pub/do > cs/manual-ocaml/extn.html#s-private-types-abbrev ) should work. You'll > have to cast your safe array type to a normal bigarray to get the indexing > and other operations, e.g.: > > (my_array : ro t :> (int, int8_unsigned_elt, c_layout) Array1.t).{idx} > > Also, see http://camltastic.blogspot.ca/2008/05/phantom-types.html for a > really cool way to mix phantom types and subtyping. > > Cheers, > > Yawar > > On Thu, Nov 16, 2017 at 4:46 PM, Reed Wilson wrote: > >> A while ago, I made a module which basically extended bigarrays with a >> few more functions. However, I wanted to have a distinction between >> read-only and read-write values. The equivalence with bigarrays was >> irrelevant, so my interface just looked like this: >> >> type ro >> type rw >> type 'a t >> val read_only : 'a t -> ro t >> val get : 'a t -> int -> int >> val put : rw t -> int -> int -> unit >> ... >> >> Basically, any function that wrote to the type would have to take a "rw >> t", but anything else would take " 'a t". From what I know about C, "ro" >> behaves like the "const" qualifier - not water-proof but it catches some= of >> my common mistakes. >> >> Now, however, I want to re-export the equivalence between 'a t and >> bigarrays (mostly for the .{} operator), but also have the >> read-only/read-write distinction. The problem is that if I write: >> type 'a t =3D (int, int8_unsigned_elt, c_layout) Array1.t >> >> then OCaml will see that "ro t" and "rw t" are the same and freely let me >> use "ro t" values in, for example, the "put" function above. >> >> To summarize, is there a way to make two types internally represented by >> bigarrays, the first of which: >> * can use the bigarray functions (specifically .{} ) >> * can use all of my new functions >> and the second type >> * can't use bigarray functions >> * can only use a subset of my new functions >> >> I don't want to have two different versions of each function that I have >> to keep track of. >> >> Thanks, >> Reed Wilson >> >> -- >> =C3=A7 >> > > --=20 =C3=A7 --94eb2c194a066ba1b3055e242a2f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
That looks pretty good! One of the things I tried was to u= se the private type declaration. However, I failed to take the coercion int= o account, so I thought they couldn't actually be used as bigarrays.I'd still like to avoid casting to bigarrays, but unless a miracle co= mes along, I think this is how I'll do it.
Thanks!

On Thu, Nov 16, 2017 at = 4:49 PM, Yawar Amin <yawar.amin@gmail.com> wrote:
Hi Reed, this is maybe not exac= tly what you specified, but a `private` type abbreviation (=C2=A0https://caml.inria.fr/pub/docs/manual-ocaml/extn= .html#s-private-types-abbrev ) should work. You'll have to cas= t your safe array type to a normal bigarray=C2=A0to get the indexing and ot= her operations, e.g.:

(my_array : ro=C2=A0t :> (int, = int8_unsigned_elt, c_layout) Array1.t).{idx}

Also,= see=C2=A0http://camltastic.blogspot.ca/2008/05/phantom-ty= pes.html for a really cool way to mix phantom types and subtyping.

Cheers,

Yawar

On Thu, Nov 16= , 2017 at 4:46 PM, Reed Wilson <cedilla@gmail.com> wrote:
A while ago, I made a module which basically extended big= arrays with a few more functions. However, I wanted to have a distinction b= etween read-only and read-write values. The equivalence with bigarrays was = irrelevant, so my interface just looked like this:

type = ro
type rw
type 'a t
val read_only : '= ;a t -> ro t
val get : 'a t -> int -> int
<= div>val put : rw t -> int -> int -> unit
...
<= br>
Basically, any function that wrote to the type would have to = take a "rw t", but anything else would take " 'a t"= . From what I know about C, "ro" behaves like the "const&quo= t; qualifier - not water-proof but it catches some of my common mistakes.

Now, however, I want to re-export the equivalence b= etween 'a t and bigarrays (mostly for the .{} operator), but also have = the read-only/read-write distinction. The problem is that if I write:
=
type 'a t =3D (int, int8_unsigned_elt, c_layout) Array1.t

then OCaml will see that "ro t" and "rw t&q= uot; are the same and freely let me use "ro t" values in, for exa= mple, the "put" function above.

To summa= rize, is there a way to make two types internally represented by bigarrays,= the first of which:
* can use the bigarray functions (specifical= ly .{} )
* can use all of my new functions
and the seco= nd type
* can't use bigarray functions
* can only u= se a subset of my new functions

I don't want t= o have two different versions of each function that I have to keep track of= .

Thanks,
Reed Wilson

=
--
=C3=A7<= /div>




--
=
=C3=A7
--94eb2c194a066ba1b3055e242a2f--