A pattern for using GADTs to subset cases

[s.t.s]

At the type level, I think object types could be employed to allow for extensibility and even some record masking and private fields setup (cf. this part of the manual for some interesting ideas about private row types). Consider this code in Owi for inspiration.

With object types, I think, the whatever relevant desired notions of inheritance could be simulated.

The more interesting question, though, is whether we may construct the types for tagging data without enumerating all cases in some centralized location. Could we distribute the definition of tagged data throughout the modules, and to actually process this data with functions that were not defined at the same time that the centralized data representation has been defined?

@blement

Are you aware of extensible type definitions ? It allows for adding new constructors (but not deleting them though), at the price of having to add a default case to every pattern matching:

type t = ..
type t += A | B
let f1 (x:t) = match x with | A -> 1 | B -> 2 | _ -> 0
type t += C
let f2 (x:t) = match x with | A -> 1 | B -> 2 | C -> 3 | _ -> 0

There are some pitfalls with using these open types, since it’s distinctly possible to construct cases that would result in the invocation of the refutation clause even if GADTs and type tags are involved.