Re: [Caml-list] creating GADTs

[Reed Wilson <cedilla@gmail.com>]

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

--
ç