Does using object types in GADTs get you any more power?

Learning
, ,
11

I gave a thought about how in principle my case could be approached. It seems that we have two distinct methods, which could be employed simultaneously in a single program, with a third emerging as an extension:

  1. Use basic polymorphic variant tagging with encoders in separate signatures or modules hidden by an opaque type. The processors need only be aware of the context they are working with, and the knowledge of all relevant game types need not be declared at the type level as a closed type (thus, non-incrementally).
  2. Use centralized processing functions. Here, it is distinctly possible to take advantage of non-polymorphic type variants. It is easier to work with such approach when the types used for tagging data are closed — which implies that the knowledge of all relevant game types needs to be declared at the type level as a closed type.
  3. However, it is also distinctly possible to create an encoding where the variant types used for tagging data are actually open types. It’s a slightly more complex approach, since we’d need to construct our pattern-matching functions from implementations in several modules, and also we’ll need some additional type arguments to ensure that only the tags known to the processing function are allowed to be given to it.

Now, the implementation techniques for cases (1) and (2) are relatively obvious. A more interesting question is case (3). Could we hope for any efficiency in case we’re constructing our pattern matching from functions in several modules, a la:

  (* somewhere within the processing function *)
  | Int -> do_something_with_int data
  | Float -> do_something_with_float data
  | _ -> try_next data

  (* where `try_next_data` has the form similar to the one above,
     i.e. it is essentially a large pattern-matching expression with
     a functional application (e.g. `try_next_data`) at the tail *)

Could we hope that the compiler would turn this definition into a single pattern-match in the end?

Note how we have an increase in the number of needed type variables in the data tag specifications when we move from (1) to (2) to (3).

  1. In this case, we need a definition of the type 'a t, since the tags are polymorphic, and could easily be subset.
  2. Here, we need an extra type variable to express subsetting, thus ('a , 'b) t, where 'a is a data type, and 'b is probably some polymorphic variant tag type or such (e.g. [> `Int | `Float]).
  3. Here, we need to introduce an additional parameter to prevent inclusion of tags from unknown modules. So, we have ('a, 'b, 'c) t, where 'c designates associated module or modules used in the definition of the specific instance of processing function that uses these tags.

What do you think about these approaches? Are there other methods that you have in mind in addition to those three?