Re: [Caml-list] creating GADTs

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> 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 = frame_of_sr_id_chan (samplerate_of_int 3)
> (mpeg_of_int 0, channel_mode_of_int 0);;
> print_samplerate test_frame;;

Here is what I observe on my machine:

# let print_samplerate : type id chan. (id,chan) frame_t -> unit = function
[...]
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
{header_id=MPEG2; header_samplerate=S48000}

# let test_frame = frame_of_sr_id_chan (samplerate_of_int 3)
(mpeg_of_int 0, channel_mode_of_int 0);;
  val test_frame : (mpeg_tag_t, channel_tag_t) frame_t =
  {header_id = MPEG1; header_crc = true; header_samplerate = S22050;
   header_channel_mode = Channel_mono; side_bits = Bits_1_mono <abstr>}

# print_samplerate test_frame;;
Exception: Match_failure ("//toplevel//", 43, -733).

Note that the type of your *_of_int function is not precise enough for
what you want to do:

  val mpeg_of_int : int -> mpeg_tag_t mpeg_t = <fun>
  val samplerate_of_int : int -> mpeg_tag_t samplerate_t = <fun>
  val channel_mode_of_int : int -> channel_tag_t channel_t = <fun>

This means that the mpeg_id returned by mpeg_of_int will have the
imprecise type mpeg_tag_t (basically *either* a MPEG1 or a MPEG2),
instead of having the more precise type you want to guarantee matching
exhaustivity later. This is what Leo described as "still suffer of the
same problem as your original function".

On Sun, Aug 5, 2012 at 12:52 AM, Reed Wilson <cedilla@gmail.com> wrote:
> Thanks for the response!
>
> On Sat, Aug 4, 2012 at 2:21 AM, Leo P White <lpw25@cam.ac.uk> wrote:
>>
>> Hi,
>>
>> The problem with your function
>>
>>
>> let mpeg_of_int = 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 mpeg_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 simple example becomes:
>>
>>
>>  type mpeg1_t;;
>>  type mpeg2_t;;
>>  type _ mpeg_t =
>>  | MPEG1 : mpeg1_t mpeg_t
>>  | MPEG2 : mpeg2_t mpeg_t
>>  ;;
>>
>>  type mpeg_ext_t = Mpeg_Ext: 'a mpeg_t -> mpeg_ext_t;;
>>
>>  let mpeg_of_int = 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 = function
> | (MPEG1, Channel_mono) -> {
> header_id = MPEG1;
> header_crc = true;
> header_samplerate = S48000;
> header_channel_mode = Channel_mono;
> side_bits = Bits_1_mono (1,1);
> }
> | (MPEG1, Channel_stereo) -> {
> header_id = MPEG1;
> header_crc = true;
> header_samplerate = S48000;
> header_channel_mode = Channel_stereo;
> side_bits = Bits_1_stereo (1,1,1,1);
> }
> | (MPEG2, Channel_mono) -> {
> header_id = MPEG2;
> header_crc = true;
> header_samplerate = S24000;
> header_channel_mode = Channel_mono;
> side_bits = Bits_2_mono (1);
> }
> | (MPEG2, Channel_stereo) -> {
> header_id = MPEG2;
> header_crc = true;
> header_samplerate = S24000;
> header_channel_mode = Channel_stereo;
> side_bits = Bits_2_stereo (1,1);
> }
> ;;
>
>
> Then I would create the frame based on the bits in the file:
>
> let id_int = int_of_raw_bits ... in
> let channel_mode_int = int_of_raw_bits ... in
> let frame = 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 maintain your invariants. So your full example would become:
>>
>>  type mpeg_tag_t = [ `Mpeg1 | `Mpeg2 ]
>>
>>  type _ mpeg_t =
>>  | MPEG1 : [< mpeg_tag_t >`Mpeg1] mpeg_t
>>  | MPEG2 : [< mpeg_tag_t > `Mpeg2] mpeg_t
>>  ;;
>>
>>  type _ samplerate_t =
>>  | S48000 : [`Mpeg1] samplerate_t
>>  | S44100 : [`Mpeg1] samplerate_t
>>  | S24000 : [`Mpeg2] samplerate_t
>>  | S22050 : [`Mpeg2] samplerate_t
>>  ;;
>>
>>  type channel_tag_t = [ `Mono | `Stereo ]
>>
>>  type _ channel_t =
>>  | Channel_mono : [< channel_tag_t > `Mono] channel_t
>>  | Channel_stereo : [< channel_tag_t > `Stereo] channel_t
>>  ;;
>>
>>  type (_,_) side_bits_t =
>>  | Bits_1_mono : (int * int) -> ([`Mpeg1], [`Mono]) side_bits_t
>>  | Bits_1_stereo : (int * int * int * int)                       -> ([`Mpeg1], [`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 = {
>>    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 = function
>>  | 0 -> MPEG1
>>  | _ -> MPEG2;;
>>
>> and it still maintains the desired invariant, so that this is allowed:
>>
>>  let good =  { header_id = MPEG1;
>>    header_crc = true;
>>    header_samplerate = S48000;
>>    header_channel_mode = Channel_mono;
>>    side_bits = Bits_1_mono(1, 2); };;
>>
>> but this isn't:
>>
>> let bad =  { header_id = MPEG1;
>>    header_crc = true;
>>    header_samplerate = S48000;
>>    header_channel_mode = Channel_stereo;
>>    side_bits = 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 = [< `Mono | `Stereo > `Stereo ]       The first variant type does not allow tag(s) `Stereo
>>
>> Note that this would still not allow you to write the function:
>>
>>  let mpeg_of_int = 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 = [ `Mpeg1 | `Mpeg2 ]
>
> type _ mpeg_t =
> | MPEG1 : [< mpeg_tag_t > `Mpeg1] mpeg_t
> | MPEG2 : [< mpeg_tag_t > `Mpeg2] mpeg_t
> ;;
>
> type _ samplerate_t =
> | 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 = [ `Mono | `Stereo ]
>
> type _ channel_t =
> | Channel_mono : [< channel_tag_t > `Mono] channel_t
> | Channel_stereo : [< channel_tag_t > `Stereo] channel_t
> ;;
>
> type (_,_) side_bits_t =
> | Bits_1_mono : (int * int) -> ([`Mpeg1], [`Mono]) side_bits_t
> | Bits_1_stereo : (int * int * int * int) -> ([`Mpeg1], [`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 = {
> 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 = function
> | 0 -> MPEG1
> | 1 -> MPEG2
> | _ -> failwith "Bad"
> ;;
>
> let samplerate_of_int = function
> | 0 -> S48000
> | 1 -> S44100
> | 2 -> S24000
> | 3 -> S22050
> | _ -> failwith "Bad"
> ;;
>
> let channel_mode_of_int = 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 = fun sr -> function
> | (MPEG1, Channel_mono) -> {header_id = MPEG1; header_crc = true;
> header_samplerate = sr; header_channel_mode = Channel_mono; side_bits
> = Bits_1_mono (1,1)}
> | (MPEG1, Channel_stereo) -> {header_id = MPEG1; header_crc = true;
> header_samplerate = sr; header_channel_mode = Channel_stereo;
> side_bits = Bits_1_stereo (1,1,1,1)}
> | (MPEG2, Channel_mono) -> {header_id = MPEG2; header_crc = true;
> header_samplerate = sr; header_channel_mode = Channel_mono; side_bits
> = Bits_2_mono (1)}
> | (MPEG2, Channel_stereo) -> {header_id = MPEG2; header_crc = true;
> header_samplerate = sr; header_channel_mode = Channel_stereo;
> side_bits = Bits_2_stereo (1,1)}
> ;;
>
> let print_samplerate : type id chan. (id,chan) frame_t -> unit = function
> | {header_id = MPEG1; header_samplerate = S48000} -> Printf.printf "M1_S48000\n"
> | {header_id = MPEG1; header_samplerate = S44100} -> Printf.printf "M1_S44100\n"
> | {header_id = MPEG2; header_samplerate = S24000} -> Printf.printf "M2_S24000\n"
> | {header_id = MPEG2; header_samplerate = 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 = 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
>
> --
> ç
>
> --
> 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
>