Error: This expression has type mpeg2_t mpeg_t
but an expression was expected of type mpeg1_t mpeg_t
I'm trying to make mpeg_of_int be the type "int -> 'a mpeg_t" (or something similar), but nothing I do will stick. I don't really think this type is ill-defined since the possible types of 'a are constrained by the definition of mpeg_t.
The main reason I want to use GADTs is that there are some fields in a record I use which change format depending on other fields, but there's no good way to use a variant due to the dependencies... (that's not a great explanation, so here's a longer example:)
I'm making an MP3 parser, and each MP3 frame has a different number of fields depending on the MPEG ID (MPEG1/MPEG2) and the number of channels. This is a simplified version of my GADT types:
type mpeg1_t;;
type mpeg2_t;;
type _ mpeg_t =
| MPEG1 : mpeg1_t mpeg_t
| MPEG2 : mpeg2_t mpeg_t
;;
type _ samplerate_t =
| S48000 : mpeg1_t samplerate_t
| S44100 : mpeg1_t samplerate_t
| S24000 : mpeg2_t samplerate_t
| S22050 : mpeg2_t samplerate_t
;;
type channel_mono_t;;
type channel_stereo_t;;
type _ channel_t =
| Channel_mono : channel_mono_t channel_t
| Channel_stereo : channel_stereo_t channel_t
;;
type (_,_) side_bits_t =
| Bits_1_mono : (int * int) -> (mpeg1_t, channel_mono_t) side_bits_t
| Bits_1_stereo : (int * int * int * int) -> (mpeg1_t, channel_stereo_t) side_bits_t
| Bits_2_mono : int -> (mpeg2_t, channel_mono_t) side_bits_t
| Bits_2_stereo : (int * int) -> (mpeg2_t, channel_stereo_t) 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;
};;
Without the use of GADTs, I can't think of a way to access both header_id and header_channel_mode in frame_t without some big hierarchical structure. The holdup seems to be that some parts of frame_t depend on 'id, some parts on 'chan, and some parts on both. Here's the simplest thing I can think of that will give the same information without GADTs:
type mpeg1_mono_t = {
mpeg1_mono_side_bits : int * int;
};;
type mpeg1_stereo_t = {
mpeg1_stereo_side_bits : int * int * int * int;
};;
type mpeg1_channel_t = MPEG1_channel_mono of mpeg1_mono_t | MPEG1_channel_stereo of mpeg1_stereo_t;;
type mpeg1_samplerate_t = S48000 | S44100;;
type mpeg1_t = {
mpeg1_channel_mode : mpeg1_channel_t;
mpeg1_samplerate : mpeg1_samplerate_t;
}
type mpeg2_mono_t = {
mpeg2_mono_side_bits : int;
};;
type mpeg2_stereo_t = {
mpeg2_stereo_side_bits : int * int;
};;
type mpeg2_channel_t = MPEG2_channel_mono of mpeg2_mono_t | MPEG2_channel_stereo of mpeg2_stereo_t;;
type mpeg2_samplerate_t = S48000 | S44100;;
type mpeg2_t = {
mpeg2_channel_mode : mpeg2_channel_t;
mpeg2_samplerate : mpeg2_samplerate_t;
}
type mpeg_t = MPEG1 of mpeg1_t | MPEG2 of mpeg2_t;;
type frame_t = {
header_id : mpeg_t;
header_crc : bool;
};;
Without GADTs, if I wanted a function to return the number of channels, I'd have to write something like this:
let frame_channels = function
| {header_id = MPEG1 {mpeg1_channel_mode = MPEG1_channel_mono _}} -> 1
| {header_id = MPEG2 {mpeg2_channel_mode = MPEG2_channel_mono _}} -> 1
| {header_id = MPEG1 {mpeg1_channel_mode = MPEG1_channel_stereo _}} -> 2
| {header_id = MPEG2 {mpeg2_channel_mode = MPEG2_channel_stereo _}} -> 2
;;
However, since the number of channels doesn't actually depend on the MPEG ID (MPEG1 or MPEG2), with GADTs I can shorten that to:
let frame_channels : type a b. (a,b) frame_t -> int = function
| {header_channel_mode = Channel_mono} -> 1
| {header_channel_mode = Channel_stereo} -> 2
;;
Now (finally!), the questions:
1. Does it seem like GADTs are the way to go here, or is there a cleaner method?
2. Is there any way of getting mpeg_of_int past the type-checker?
3. If not, is that because I'm doing something unsound, or is it the GADT implementation being too strict?
Thanks for any insights!
--