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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id CAB047ED5C for ; Sun, 5 Aug 2012 00:53:18 +0200 (CEST) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of cedilla@gmail.com) identity=pra; client-ip=209.85.160.54; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="cedilla@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of cedilla@gmail.com designates 209.85.160.54 as permitted sender) identity=mailfrom; client-ip=209.85.160.54; receiver=mail1-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 (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-pb0-f54.google.com) identity=helo; client-ip=209.85.160.54; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="postmaster@mail-pb0-f54.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnUFADanHVDRVaA2jWdsb2JhbABFhXuyOwR8CCIBAQEBBwsLCRIGI4IgAQEBAwESAg8EGQEbHgMMBgULDQICJgICIgERAQUBHBkbB4dbAQMGBpwtCQOLVE+CcYQvChknDVeIcQEFDIEViikyhUCBEgOITYx8ji8+hB4 X-IronPort-AV: E=Sophos;i="4.77,714,1336341600"; d="scan'208";a="169090512" Received: from mail-pb0-f54.google.com ([209.85.160.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 05 Aug 2012 00:52:54 +0200 Received: by pbbro2 with SMTP id ro2so4201703pbb.27 for ; Sat, 04 Aug 2012 15:52:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; bh=Ii5kUjb7v8Kl/TvT//CL4mj0l+IHI7J8iK17Sa+jW5E=; b=VkInkjLmqiAkWn95jgOm51JpBKYliTt0jZ+yR/oXAgh320Z/+tiTwQFdMOJPX9GAtk uqgbyY34VP/JLTt73DcezEpdIp04ohDe0Z9C9gXX7PZGLRyWwUoXY58AFKhp3SBUHb2N /xCP/+NR2PiA0a4JJa2NfNfxUa1wCdVbJWk4WKKDpwull59DuE06+X7hRqIqwyXSsExU OUpMHLLNZegA+U+Mwij3VqNxGWs+2OoiE9rsTuODxIKRHniAUaHJCiQMIOnUeXMr9d/3 uKXXQ2n6YyIWa5V1ly+MA1zHYM/wBvIrJptnhJFI9p8d4/xNvz6rkszIaonckEyImn7z jCrw== MIME-Version: 1.0 Received: by 10.66.75.229 with SMTP id f5mr8034758paw.47.1344120773310; Sat, 04 Aug 2012 15:52:53 -0700 (PDT) Received: by 10.142.173.15 with HTTP; Sat, 4 Aug 2012 15:52:53 -0700 (PDT) In-Reply-To: References: Date: Sat, 4 Aug 2012 15:52:53 -0700 Message-ID: From: Reed Wilson To: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Validation-by: cedilla@gmail.com Subject: Re: [Caml-list] creating GADTs Thanks for the response! On Sat, Aug 4, 2012 at 2:21 AM, Leo P White wrote: > > Hi, > > The problem with your function > > > let mpeg_of_int =3D function > | 0 -> MPEG1 > | _ -> MPEG2 > ;; > > is that it cannot have type int -> 'a mpeg_t becuase that would mean that= you could use it to create any values with any mpeg_t type (e.g. string mp= eg_t). I thought that looked like a funny type for a function, but shouldn't it be clear from the definition of mpeg_t that the function can't return string mpeg_t? I thought that's one of the things GADTs were supposed to solve. > > > I can think of two possible solutions to your problem. > > The first is to use an existential type via another GADT, so that your si= mple example becomes: > > > type mpeg1_t;; > type mpeg2_t;; > type _ mpeg_t =3D > | MPEG1 : mpeg1_t mpeg_t > | MPEG2 : mpeg2_t mpeg_t > ;; > > type mpeg_ext_t =3D Mpeg_Ext: 'a mpeg_t -> mpeg_ext_t;; > > let mpeg_of_int =3D function > | 0 -> Mpeg_Ext MPEG1 > | _ -> Mpeg_Ext MPEG2 > ;; This does work, but unfortunately it doesn't seem to work for my purpose, since I still can't get mpeg1_t or mpeg2_t "out" of it. (I apologize for my continued use of nonstandard terminology - I've never used any of these advanced typing features before) Basically, in the end I'd build a function that creates a ('id,'chan) frame_t, with 'id and 'chan depending on the bits stored in the MP3's header. So something like this: let frame_of_id_and_chan : type id chan. (id mpeg_t * chan channel_t) -> (id,chan) frame_t =3D function | (MPEG1, Channel_mono) -> { header_id =3D MPEG1; header_crc =3D true; header_samplerate =3D S48000; header_channel_mode =3D Channel_mono; side_bits =3D Bits_1_mono (1,1); } | (MPEG1, Channel_stereo) -> { header_id =3D MPEG1; header_crc =3D true; header_samplerate =3D S48000; header_channel_mode =3D Channel_stereo; side_bits =3D Bits_1_stereo (1,1,1,1); } | (MPEG2, Channel_mono) -> { header_id =3D MPEG2; header_crc =3D true; header_samplerate =3D S24000; header_channel_mode =3D Channel_mono; side_bits =3D Bits_2_mono (1); } | (MPEG2, Channel_stereo) -> { header_id =3D MPEG2; header_crc =3D true; header_samplerate =3D S24000; header_channel_mode =3D Channel_stereo; side_bits =3D Bits_2_stereo (1,1); } ;; Then I would create the frame based on the bits in the file: let id_int =3D int_of_raw_bits ... in let channel_mode_int =3D int_of_raw_bits ... in let frame =3D frame_of_id_and_chan (mpeg_of_int id_int, channel_of_int channel_mode_int) in ... If hiding the mpeg_t type inside mpeg_ext_t, I wouldn't be able to use it to create a frame of the right type. > > > The second is to use polymorphic variants instead of abstract types to ma= intain your invariants. So your full example would become: > > type mpeg_tag_t =3D [ `Mpeg1 | `Mpeg2 ] > > type _ mpeg_t =3D > | MPEG1 : [< mpeg_tag_t >`Mpeg1] mpeg_t > | MPEG2 : [< mpeg_tag_t > `Mpeg2] mpeg_t > ;; > > type _ samplerate_t =3D > | S48000 : [`Mpeg1] samplerate_t > | S44100 : [`Mpeg1] samplerate_t > | S24000 : [`Mpeg2] samplerate_t > | S22050 : [`Mpeg2] samplerate_t > ;; > > type channel_tag_t =3D [ `Mono | `Stereo ] > > type _ channel_t =3D > | Channel_mono : [< channel_tag_t > `Mono] channel_t > | Channel_stereo : [< channel_tag_t > `Stereo] channel_t > ;; > > type (_,_) side_bits_t =3D > | Bits_1_mono : (int * int) -> ([`Mpeg1], [`Mono]) side_bits_t > | Bits_1_stereo : (int * int * int * int) -> ([`Mp= eg1], [`Stereo]) side_bits_t > | Bits_2_mono : int -> ([`Mpeg2], [`Mono]) side_bits_t > | Bits_2_stereo : (int * int) -> ([`Mpeg2], [`Stereo]) side_bits_t > > ;; > > type ('id,'chan) frame_t =3D { > header_id : 'id mpeg_t; > header_crc : bool; > header_samplerate : 'id samplerate_t; > header_channel_mode : 'chan channel_t; > side_bits : ('id,'chan) side_bits_t; > };; > > This allows you to write your function as before: > > > let mpeg_of_int =3D function > | 0 -> MPEG1 > | _ -> MPEG2;; > > and it still maintains the desired invariant, so that this is allowed: > > let good =3D { header_id =3D MPEG1; > header_crc =3D true; > header_samplerate =3D S48000; > header_channel_mode =3D Channel_mono; > side_bits =3D Bits_1_mono(1, 2); };; > > but this isn't: > > let bad =3D { header_id =3D MPEG1; > header_crc =3D true; > header_samplerate =3D S48000; > header_channel_mode =3D Channel_stereo; > side_bits =3D Bits_1_mono(1, 2); };; > > Error: This expression has type ([ `Mpeg1 ], [ `Mono ]) side_bits_t > > but an expression was expected of type > ([ `Mpeg1 ], [< channel_tag_t > `Stereo ] as 'a) side_bits_t > Type [ `Mono ] is not compatible with type > 'a =3D [< `Mono | `Stereo > `Stereo ] The first variant typ= e does not allow tag(s) `Stereo > > Note that this would still not allow you to write the function: > > let mpeg_of_int =3D function > | 0 -> S48000 > | _ -> S24000;; > > which suffers from the same problem as your original function. That helps a lot! I think I got it working with polymorphic variants. I basically added < mpeg_tag_t > to all the samplerate definitions, which seems to let everything work. The result is this: type mpeg_tag_t =3D [ `Mpeg1 | `Mpeg2 ] type _ mpeg_t =3D | MPEG1 : [< mpeg_tag_t > `Mpeg1] mpeg_t | MPEG2 : [< mpeg_tag_t > `Mpeg2] mpeg_t ;; type _ samplerate_t =3D | S48000 : [< mpeg_tag_t > `Mpeg1] samplerate_t | S44100 : [< mpeg_tag_t > `Mpeg1] samplerate_t | S24000 : [< mpeg_tag_t > `Mpeg2] samplerate_t | S22050 : [< mpeg_tag_t > `Mpeg2] samplerate_t ;; type channel_tag_t =3D [ `Mono | `Stereo ] type _ channel_t =3D | Channel_mono : [< channel_tag_t > `Mono] channel_t | Channel_stereo : [< channel_tag_t > `Stereo] channel_t ;; type (_,_) side_bits_t =3D | Bits_1_mono : (int * int) -> ([`Mpeg1], [`Mono]) side_bits_t | Bits_1_stereo : (int * int * int * int) -> ([`Mpeg1], [`Stereo]) side_bit= s_t | Bits_2_mono : int -> ([`Mpeg2], [`Mono]) side_bits_t | Bits_2_stereo : (int * int) -> ([`Mpeg2], [`Stereo]) side_bits_t ;; type ('id,'chan) frame_t =3D { mutable header_id : 'id mpeg_t; mutable header_crc : bool; mutable header_samplerate : 'id samplerate_t; mutable header_channel_mode : 'chan channel_t; mutable side_bits : ('id,'chan) side_bits_t; };; let mpeg_of_int =3D function | 0 -> MPEG1 | 1 -> MPEG2 | _ -> failwith "Bad" ;; let samplerate_of_int =3D function | 0 -> S48000 | 1 -> S44100 | 2 -> S24000 | 3 -> S22050 | _ -> failwith "Bad" ;; let channel_mode_of_int =3D function | 0 -> Channel_mono | 1 -> Channel_stereo | _ -> failwith "Bad" ;; All the types seem to work out, with one fairly contrived exception... If I write a few test functions: let frame_of_sr_id_chan : type id chan. id samplerate_t -> id mpeg_t * chan channel_t -> (id,chan) frame_t =3D fun sr -> function | (MPEG1, Channel_mono) -> {header_id =3D MPEG1; header_crc =3D true; header_samplerate =3D sr; header_channel_mode =3D Channel_mono; side_bits =3D Bits_1_mono (1,1)} | (MPEG1, Channel_stereo) -> {header_id =3D MPEG1; header_crc =3D true; header_samplerate =3D sr; header_channel_mode =3D Channel_stereo; side_bits =3D Bits_1_stereo (1,1,1,1)} | (MPEG2, Channel_mono) -> {header_id =3D MPEG2; header_crc =3D true; header_samplerate =3D sr; header_channel_mode =3D Channel_mono; side_bits =3D Bits_2_mono (1)} | (MPEG2, Channel_stereo) -> {header_id =3D MPEG2; header_crc =3D true; header_samplerate =3D sr; header_channel_mode =3D Channel_stereo; side_bits =3D Bits_2_stereo (1,1)} ;; let print_samplerate : type id chan. (id,chan) frame_t -> unit =3D function | {header_id =3D MPEG1; header_samplerate =3D S48000} -> Printf.printf "M1_= S48000\n" | {header_id =3D MPEG1; header_samplerate =3D S44100} -> Printf.printf "M1_= S44100\n" | {header_id =3D MPEG2; header_samplerate =3D S24000} -> Printf.printf "M2_= S24000\n" | {header_id =3D MPEG2; header_samplerate =3D S22050} -> Printf.printf "M2_= S22050\n" ;; I was happy to notice that this did not complain about being incomplete, correctly seeing that the samplerates can only be used with a matching header_id; However, if I then I make an invalid frame using the *_of_int functions: let test_frame =3D frame_of_sr_id_chan (samplerate_of_int 3) (mpeg_of_int 0, channel_mode_of_int 0);; print_samplerate test_frame;; This accepts the input (even though samplerate_of_int 3 is `Mpeg2, and mpeg_of_int 0 is `Mpeg1). However, this will print M1_S44100, which is definitely not what I specified (samplerate_of_int 3 is S22050)! There must be something I don't get with this typing. Any ideas what? In the end, though, I will not actually use a function like frame_of_sr_id_chan, so using polymorphic variants should do exactly what I want. Thanks again, Reed -- =C3=A7