Re: [Caml-list] creating GADTs

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

[-- Attachment #1: Type: text/plain, Size: 1328 bytes --]

2012/08/06 1:11 "Reed Wilson" <cedilla@gmail.com>:
>
> I think I've gotten everything pretty much straightened out now, but
there is something I didn't expect with GADTs and pattern-matching. Using
my previous samplerate_t type:
>
> type mpeg1_t
> type mpeg2_t
> type _ samplerate_t =
> | S48000 : mpeg1_t samplerate_t
> | S44100 : mpeg1_t samplerate_t
> | S24000 : mpeg2_t samplerate_t
> | S22050 : mpeg2_t samplerate_t
>
>
> I can't seem to do something like this:
>
> let samples_per_frame : type id. id samplerate_t -> int = function
> | S48000 | S44100 -> 1152
> | S24000 | S22050 -> 576
>
>
> Instead I have to have each of the constructors use a separate branch:
>
> let samples_per_frame : type id. id samplerate_t -> int = function
> | S48000 -> 1152
> | S44100 -> 1152
> | S24000 -> 576
> | S22050 -> 576
>
>
> even though S48000 and S44100 are the exact same type! OCaml complains:
> Error: This pattern matches values of type mpeg1_t samplerate_t
>        but a pattern was expected which matches values of type
>          id samplerate_t

The error message is not very clear, but the real cause is that currently
it is prohibited to generate GADT constraints in or-patterns.
One would have to check that the generated constraints are identical, which
is not possible at this point.
Future work...

Jacques Garrigue

[-- Attachment #2: Type: text/html, Size: 1708 bytes --]