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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id AB818822AC for ; Fri, 17 Nov 2017 01:50:13 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yawar.amin@gmail.com; spf=Pass smtp.mailfrom=yawar.amin@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f48.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yawar.amin@gmail.com) identity=pra; client-ip=209.85.214.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yawar.amin@gmail.com"; x-sender="yawar.amin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yawar.amin@gmail.com designates 209.85.214.48 as permitted sender) identity=mailfrom; client-ip=209.85.214.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yawar.amin@gmail.com"; x-sender="yawar.amin@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f48.google.com) identity=helo; client-ip=209.85.214.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yawar.amin@gmail.com"; x-sender="postmaster@mail-it0-f48.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AU1/gZxL5oF+XX3PEetmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgXLPTxwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uAQfFxm3Cgtx?= =?us-ascii?q?PePzUtrZgsi20+S705LWagRMwjG6ZOUhAg+xqFDgv9Yfm8NLL6c3gk/Yq2RBYa?= =?us-ascii?q?JfwGJuDV2Wlhf4oMy3+cgwoGxrp/s9+psYAu3BdKMiQOkAAQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CxAwBtMQ5ahjDWVdFcHAEBAQQBAQoBA?= =?us-ascii?q?YNbP24UEweDeIE2mA+BfYJ/jheFSYIRCiWFFgKEWAdAFwEBAQEBAQEBAQESAQE?= =?us-ascii?q?BCAsLCCgvgjgigkUBAgIBIwQZARsdAQMBCwYFCwM0AgIhAQERAQUBHAYTigsBA?= =?us-ascii?q?w0IEJxeQIwNgW0YBQEcgwoFg2MKGScNWIJjAQEBAQEBAQMBAQEBAQEBAQEXAgY?= =?us-ascii?q?SgyJFgUKBVYUUgmskgjaCaIJjBYoEiQOOdz2CN4U5iCGEeYIVYYkvhyOMcTqIc?= =?us-ascii?q?RQFH4EVDxIBgio0ISVeNYIvCYJEH4IRIzYBjAUBAQE?= X-IPAS-Result: =?us-ascii?q?A0CxAwBtMQ5ahjDWVdFcHAEBAQQBAQoBAYNbP24UEweDeIE?= =?us-ascii?q?2mA+BfYJ/jheFSYIRCiWFFgKEWAdAFwEBAQEBAQEBAQESAQEBCAsLCCgvgjgig?= =?us-ascii?q?kUBAgIBIwQZARsdAQMBCwYFCwM0AgIhAQERAQUBHAYTigsBAw0IEJxeQIwNgW0?= =?us-ascii?q?YBQEcgwoFg2MKGScNWIJjAQEBAQEBAQMBAQEBAQEBAQEXAgYSgyJFgUKBVYUUg?= =?us-ascii?q?mskgjaCaIJjBYoEiQOOdz2CN4U5iCGEeYIVYYkvhyOMcTqIcRQFH4EVDxIBgio?= =?us-ascii?q?0ISVeNYIvCYJEH4IRIzYBjAUBAQE?= X-IronPort-AV: E=Sophos;i="5.44,405,1505772000"; d="scan'208,217";a="244922382" Received: from mail-it0-f48.google.com ([209.85.214.48]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Nov 2017 01:50:12 +0100 Received: by mail-it0-f48.google.com with SMTP id y15so2254857ita.4 for ; Thu, 16 Nov 2017 16:50:12 -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=EIbZ2Lr7XiUsNWX8aiQ//oyZdJPpQwbnTsPZAoiVz30=; b=jMc+GczdLB/Z2yd7+zLJamltOXbwpUC7b0i/yTalz+MHAgXxkW+gm1n/aqAknyIri5 msMgLNE6JlctjGvP0Pl/Zxe4lAQ7KRcYJa3kRsLWfUNXZBh4DgPBNNtez2UYCr6eAfzP HIfz9b7j9gkTY17HkZH7LZCvsCbUEo1VJ4rXNZTCP8zK3pL/WxTVZz0XzTHSbVz3PLdj e4J4AAD+zgghn1RGGyN8HSvkUXgwywtcxwoO8UlTbtv+XLigJsggTnvpVla6+Fb6nBph gu7YsmeGBJbQuGb7YTJFVhIlEuQI666loHauQW2pme8A4Qy96qDXSOMyusClutPyaKd+ XpLw== 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=EIbZ2Lr7XiUsNWX8aiQ//oyZdJPpQwbnTsPZAoiVz30=; b=m7OR4IAUrnqGfsseAZT7Kj1hub+HRhF4ERXdxtxNE7qltBs5F6xXodZ20BZOE4y88R FhiHdWh6re+FnsNAOHrghOVkEWsVGzOBehUX3k6+13j1fhwrX8/29YiX8QMHEqS4RPiZ 3ol0gO07KX67VPf6ZHAQ3NKdHG5RxDsVYDSc2drAUO0eWr3L8pZmMUL0zBAjm1pBZx9F KD/h4YgT/dEgf2fytueOpP9LRY4/QaMCzRa6wgQGZpjxlxw1HBFUX+ChOJkARJZ/G3Qf g6uJ3sMKqlTE2DDKfRYAyIib1rVW/zZmcPozSvGmNme/zm2iIahgh7AWQE5mmn3og/Sy 1bEQ== X-Gm-Message-State: AJaThX4Wf96Zoz1t2I4DCiihm/78+V2zFIVIQOAZVw3ft+/lVPkUmWCl YZGwzZc2NaJ8HZUzNNrGmm8Oii8QqgoXk9AePQ== X-Google-Smtp-Source: AGs4zMZi3Ky8rh/YHUVp/u66P0lgj5m7fpW66esphid9c8LRW2jcMG5nrvSUTc1mH72/YJ0ZpLZuYSKgYM0fxicOMg4= X-Received: by 10.36.36.19 with SMTP id f19mr4601865ita.96.1510879810438; Thu, 16 Nov 2017 16:50:10 -0800 (PST) MIME-Version: 1.0 Received: by 10.2.181.19 with HTTP; Thu, 16 Nov 2017 16:49:50 -0800 (PST) In-Reply-To: References: From: Yawar Amin Date: Thu, 16 Nov 2017 19:49:50 -0500 Message-ID: To: Reed Wilson Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary="001a11474b60664c11055e231e6d" Subject: Re: [Caml-list] Subtyping (or something like it) --001a11474b60664c11055e231e6d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Reed, this is maybe not exactly what you specified, but a `private` type abbreviation ( https://caml.inria.fr/pub/docs/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 > --001a11474b60664c11055e231e6d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Reed, this is maybe not exactly what you specified, but= a `private` type abbreviation (=C2=A0https://caml.inria.fr/p= ub/docs/manual-ocaml/extn.html#s-private-types-abbrev ) should work. Yo= u'll have to cast your safe array type to a normal bigarray=C2=A0to get= the indexing and other 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-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 <cedilla@gmail.com> wrote:
A while ago, I made a module which basically extended bigarrays wi= th a few more functions. However, I wanted to have a distinction between re= ad-only and read-write values. The equivalence with bigarrays was irrelevan= t, so my interface just looked like this:

type ro
<= div>type rw
type 'a t
val read_only : 'a t ->= ; ro t
val get : 'a t -> int -> int
val p= ut : rw t -> int -> int -> unit
...

=
Basically, any function that wrote to the type would have to take a &q= uot;rw t", but anything else would take " 'a t". From wh= at I know about C, "ro" behaves like the "const" qualif= ier - not water-proof but it catches some of my common mistakes.
=
Now, however, I want to re-export the equivalence between &#= 39;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 firs= t of which:
* can use the bigarray functions (specifically .{} )<= /div>
* can use all of my new functions
and the second type
* can't use bigarray functions
* can only use a subs= et of my new functions

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

Thanks,
Reed Wilson
=

--
=C3=A7

--001a11474b60664c11055e231e6d--