From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 1F6B47EEBF for ; Fri, 24 Jul 2015 17:34:43 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of ilitzroth@gmail.com) identity=pra; client-ip=209.85.220.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ilitzroth@gmail.com"; x-sender="ilitzroth@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of ilitzroth@gmail.com designates 209.85.220.178 as permitted sender) identity=mailfrom; client-ip=209.85.220.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ilitzroth@gmail.com"; x-sender="ilitzroth@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-qk0-f178.google.com) identity=helo; client-ip=209.85.220.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ilitzroth@gmail.com"; x-sender="postmaster@mail-qk0-f178.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BdAQAQWrJVlLLcVdFcDoREBrBBkn8CgT0HTAEBAQEBARIBAQEBBwsLCR8whCMBAQEDARIRBBkBGx0BAwELBgULDSoCAiIBEQEFARwGEwgXA4d2AQMKCKp9gSw+MYs/gWyCeYsmChknDVeEWAEBAQEBAQEDAQEBAQEXAQUOiz+FBweCaYFDBYxBiCKMPIFFk36CFxIjgRUXg05APDGCSwEBAQ X-IPAS-Result: A0BdAQAQWrJVlLLcVdFcDoREBrBBkn8CgT0HTAEBAQEBARIBAQEBBwsLCR8whCMBAQEDARIRBBkBGx0BAwELBgULDSoCAiIBEQEFARwGEwgXA4d2AQMKCKp9gSw+MYs/gWyCeYsmChknDVeEWAEBAQEBAQEDAQEBAQEXAQUOiz+FBweCaYFDBYxBiCKMPIFFk36CFxIjgRUXg05APDGCSwEBAQ X-IronPort-AV: E=Sophos;i="5.15,538,1432591200"; d="scan'208";a="171533580" Received: from mail-qk0-f178.google.com ([209.85.220.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 24 Jul 2015 17:34:42 +0200 Received: by qkbm65 with SMTP id m65so16420296qkb.2 for ; Fri, 24 Jul 2015 08:34:41 -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; bh=DPCabOyoHlXIOl4qzThpppCDQ4xPqhSkpxSyKibyIHY=; b=kOsYSZbVZ6dtwsOwXfnSF71SPk87WD4TKKyoAKe9VRXBZPqKUEPO8M3MqXwadnd+/N lbNkiRgO7feon20JOi4VGzh5TV+h43qbgE2kWpv0ItWg5O4u0jucGd3ajimhvmI84CPY XzCw/zegpIR+9PU2oOMRb05388O5NKw2eFeCYySNgccgVK4ffFfdQ5Q9EWj9OPYl7aLB o9ffmm0A7NSV7oJ0J7UzRkuGNOc+xflTNbXYDpHUJ4ThPToPmS/6MItBSupoDkpBmSps yTmEs9kszj3wwUl22TGf2HdnnLQeURdMGh/R82HAVZO3S68hLu+lRWdu+KYemLJaf9uZ 1G2g== X-Received: by 10.140.146.205 with SMTP id 196mr22248325qhs.27.1437752080985; Fri, 24 Jul 2015 08:34:40 -0700 (PDT) MIME-Version: 1.0 Received: by 10.96.205.97 with HTTP; Fri, 24 Jul 2015 08:34:21 -0700 (PDT) In-Reply-To: <25270BD4-F9E4-45A2-8190-F91B937D8BB1@math.nagoya-u.ac.jp> References: <25270BD4-F9E4-45A2-8190-F91B937D8BB1@math.nagoya-u.ac.jp> From: immanuel litzroth Date: Fri, 24 Jul 2015 17:34:21 +0200 Message-ID: To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: multipart/alternative; boundary=001a11353c700ff557051ba0be24 Subject: Re: [Caml-list] Question on private type abbreviations --001a11353c700ff557051ba0be24 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Yes, I found that explicitly adding the conversion function works works but then I got into some currying problem -- sorry I'm relatively new to ocaml: let conversion_test =3D test_conversions (fun (x : uint8) -> (x:>int)) in conversion_test uint8 1 I want to just define the conversion test inside the body of the let so I can reuse the name for the other types. That doesn't seem to work? Immanuel On Fri, Jul 24, 2015 at 4:44 PM, Jacques Garrigue < garrigue@math.nagoya-u.ac.jp> wrote: > On 2015/07/24 23:04, immanuel litzroth wrote: > > > > I have a question related to private type abbreviations > > I'm interfacing C++ and ocaml and I want to make sure that the ranges of > integer types are correct and reflect them in the ocaml interface. > > > > So I define > > type uint8 =3D private int > > and > > type int8 =3D private int > > same for the other sizes/signedness > > and the appropriate functions to do range checking (those are external > and use > > std::numeric limits) > > external uint8 : int -> uint8 =3D "make_uint8" > > ... > > this gives typesafety and avoids boxing/unboxing and makes sure that the > user can > > only pass values that are range checked at the earliest opportunity. > > > > Now I wanna check my code > > for all the types I wanna use 1 checking function something like this: > > > > let test_conversions (the_fun : int -> 't) (the_val : int) =3D > > try > > let the_t =3D the_fun the_val in > > Printf.printf "Numbers are %d\n" (the_t : 't :> int) > > with > > | Invalid_argument str -> Printf.printf "Error: %s" str > > > > let () =3D test_conversions uint8 1 -> will work > > .. > > let () =3D test_conversions uint64 (-1) -> will print Error... > > > > Now this doesn't typecheck because the type var 't in the signature is > too general. > > what I need to put there is "a type coercible to int" > > Is that possible? Is there some way to achieve this? > > I see no way to do that implicitly. > Namely, subtyping is only checked for coercions, so if you don=E2=80=99t = write a > coercion for > each of your types, this won=E2=80=99t work. > This means you need to add another parameter: > > let test_conversions (coerce : =E2=80=99t -> int) (the_fun : int -> 't) > (the_val : int) =3D > try > let the_t =3D the_fun the_val in > Printf.printf "Numbers are %d\n=E2=80=9D (coerce the_t) > with > | Invalid_argument str -> Printf.printf "Error: %s=E2=80=9D str > > let from_uint8 x : uint8 :> int =3D x > let from_uint64 x : uint64 :> int =3D x > > let () =3D test_conversions from_uint8 uint8 1 > .. > let () =3D test_conversions from_uint64 uint64 (-1) > > Jacques Garrigue > > --001a11353c700ff557051ba0be24 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Yes,=C2=A0
I found that explicitly adding the conversi= on function works works but then I got
into some currying problem= -- sorry I'm relatively new to ocaml:

le= t conversion_test =3D test_conversions (fun (x : uint8) -> (x:>int)) = in
=C2=A0 =C2=A0 conversion_test uint8 1

I want to just define the conversion test inside the body of the let= so I can reuse the name
for the other types. That doesn't se= em to work?
Immanuel

On Fri, Jul 24, 2015 at 4:44 PM, Jacques Garrigue = <garrigue@math.nagoya-u.ac.jp> wrote:
On 2015/07/2= 4 23:04, immanuel litzroth wrote:
>
> I have a question related to private type abbreviations
> I'm interfacing C++ and ocaml and I want to make sure that the ran= ges of integer types are correct and reflect them in the ocaml interface. >
> So I define
> type uint8 =3D private int
> and
> type int8 =3D private int
> same for the other sizes/signedness
> and the appropriate functions to do range checking (those are external= and use
> std::numeric limits)
> external uint8 : int -> uint8 =3D "make_uint8"
> ...
> this gives typesafety and avoids boxing/unboxing and makes sure that t= he user can
> only pass values that are range checked at the earliest opportunity. >
> Now I wanna check my code
> for all the types I wanna use 1 checking function something like this:=
>
> let test_conversions=C2=A0 =C2=A0(the_fun : int -> 't)=C2=A0 (t= he_val : int) =3D
>=C2=A0 =C2=A0try
>=C2=A0 =C2=A0 =C2=A0let the_t =3D the_fun the_val in
>=C2=A0 =C2=A0 =C2=A0Printf.printf "Numbers are %d\n" (the_t := 't :> int)
>=C2=A0 =C2=A0with
>=C2=A0 =C2=A0| Invalid_argument str -> Printf.printf "Error: %s= " str
>
> let () =3D test_conversions uint8 1 -> will work
> ..
> let () =3D test_conversions uint64=C2=A0 (-1) -> will print Error..= .
>
> Now this doesn't typecheck because the type=C2=A0 var 't in th= e signature is too general.
> what I need to put there is "a type coercible to int"
> Is that possible? Is there some way to achieve this?

I see no way to do that implicitly.
Namely, subtyping is only checked for coercions, so if you don=E2=80=99t wr= ite a coercion for
each of your types, this won=E2=80=99t work.
This means you need to add another parameter:

let test_conversions=C2=A0 (coerce : =E2=80=99t -> int)=C2=A0 (the_fun := int -> 't)=C2=A0 (the_val : int) =3D
=C2=A0 try
=C2=A0 =C2=A0 let the_t =3D the_fun the_val in
=C2=A0 =C2=A0 Printf.printf "Numbers are %d\n=E2=80=9D (coerce = the_t)
=C2=A0 with
=C2=A0 | Invalid_argument str -> Printf.printf "Error: %s=E2=80=9D = str

let from_uint8 x : uint8 :> int =3D x
let from_uint64 x : uint64 :> int =3D x

let () =3D test_conversions from_uint8 uint8 1
..
let () =3D test_conversions from_uint64 uint64=C2=A0 (-1)

Jacques Garrigue


--001a11353c700ff557051ba0be24--