The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

And the answer is to build my own type system within Coq and to use its types, rather than Coq types, to do what I want?

Quite possibly, though we'd need more context to give advice at that level of detail.

FWIW, here's the context. In "design theory" it's standard practice to model a design space as a vector of design parameters: a "parameterization". This is like a simple product type. A state in the design space represented by a value of this type. 

A less simplistic representation of a design space is as a subset type of a product type: the subset of tuples that satisfy some additional constraints -- a state invariant. 

So, a modest insight, possibly not new: we can and perhaps should recast traditional design space thinking in the setting of type theory. A simple design space is given by a "design type." 

Now we can talk about design evolution in this setting, in terms of transitions between values of a design type. 

In reality, though, not only the "value" of a design changes over time (through changes to the values of its constituent parameters), but its very parameterization changes from time to time (as do the invariants), as well. 

In other words, not only the "value" of a design, but also its "type" changes from state to state as the system evolves. 

I'm interested in modeling design evolution in a setting that unifies evolution both within fixed types and also across (evolutionarily related) "design types."

So, in this context, having types as first class values is helpful. For example, I can say that the state of a design is a value of this kind of pair:

Inductive design : Type := mk_designState {

  design_type: Set;

  design_value: design type 

}.

The next step is to look at graphs in which [design] values of this kind are at the nodes, and where edges represent changes between designs. These changes can include changes in both or either design_value and design_type. 

Moving further along, one looks at operations that produce such transitions. It's this sort of "design evolution operator" that I'm really interested in modeling.

For example, a simple operator is one that adds a new parameter to the parameterization of a design space, i.e., a new dimension/field to whatever product type it already had, along with a value for this new parameter. (E.g., we add a new "persistence" field, maybe of an enumerated

type, and a value, such as "MySQL" for this field.)

One could also imaging putting guards on such transitions predicated on properties of the the types at the origin nodes. That would require somehow being able to "introspect" types. 

Kevin Sullivan