Avoiding extra matching with extensible GADTs

[s.t.s]

@K_N

So, from my understanding, extensible GADTs are a bad fit here, since as @nojb said, one can always extend the type from anywhere, in a manner you cannot predict and therefore your pattern matching has to account for that unknown case. For instance one could create type (_, _) Data_tags.t += Bad : ([>Int], int) tand passBadto your inspect function, which would trigger theassert false`.

Agreed.

@K_N

But you don’t want full extensibility, <…>

Once again, agreed.

@K_N

Wouldn’t it be “simpler” (conceptually) to split your files between Game_data_typ and Game_sprite_typ (for instance) containing only type definitions,

Sure. Especially considering that these types already exist, and the issue that I have come across is more about tagging the types rather than organization of the game data itself.

@K_N

then create a central Data_tags module containing all the cases

This is what I am trying to conceptually avoid as much as possible. Ideally, all the types related to sprites should be editable through sprite-related modules, and the generic modules should be aloof about their presence.

There’s a certain difference between freely tagging the data, like e.g. `Sprite of Game_sprite.t and defining a type case like type t += Sprite of Game_sprite.t. The use of polymorphic variants is in principle acceptable. However, my problem is not entirely solved, since I still need to find a scheme to tag the data, and thus to translate from `Tag into `Tag of data_type within a function that does the tagging. The attempted use of GADTs that allow simple type-mapping seemed like a nice trick, but perhaps I need to consider an entirely different approach.

@K_N

If your Data_tags.t is not extensible anymore but finite, you may be able to remove completely unneeded cases in pattern matching. Of course this is not perfect and may not scale well if you have several such modules.

The solution would probably involve partial matching through the use of GADTs and phantom labels. For me it’s more of a last-resort solution, since it breaks conceptual modularity (by relying on the centralized all-encompassing data-type that contains all relevant tags), and it seems that we’re missing some opportunity that may already have been in existence.

@K_N

As an aside (and somewhat unrelated) the way to extend the behavior of functions such as inspect in the presence of polymorphic variants (or extensible variants) would be for it to take as extra argument the default case handler:

let inspect (type a t) ?(default=(fun _ -> assert false)) (tag : (a, t) Data_tags.t)  =
    match tag with
    | Data_tags.Int -> "Int"
    | Data_tags.Float -> "Float"
    | x -> default x

This means you can extend the behavior of inspect after its definition (by passing a suitable function to handle the cases that are not covered, but of course, the default behavior is still assert false and is still reachable.

The conceptual problem for me with this approach is that it creates a landmine of sort. Someone could deliberately feed an input to my program that would “crash” it – which is the effect of assert false statement. I seek to avoid that. In the future, I may be the one inadvertently triggering that assert false case. It’s a fate that I wish to avoid as a software developer responsible for the codebase.

@s.t.s

@K_N

If your Data_tags.t is not extensible anymore but finite, you may be able to remove completely unneeded cases in pattern matching. Of course this is not perfect and may not scale well if you have several such modules.

The solution would probably involve partial matching through the use of GADTs and phantom labels. For me it’s more of a last-resort solution, since it breaks conceptual modularity (by relying on the centralized all-encompassing data-type that contains all relevant tags), and it seems that we’re missing some opportunity that may already have been in existence.

I also feel that this breaks abstraction, where we have slighly different modi (pl. of modus) of encoding type values in the different parts of the game, and it is appropriate for them to use their own data-types, albeit very similar. The aim I try to achieve is to eliminate code duplication involved in handling the cases that are common to all these types.