The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 06/03/2013 03:42 PM, Kevin Sullivan wrote:

On Mon, Jun 3, 2013 at 12:38 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:
universes

I can see that if you can define types as sets of elements satisfying arbitrary specifications, then to solve the particular equality problem I used as an example, in general, would be to   solving program equivalence. Bzzzt. That said, I'd be happy with just name or syntactic equivalence. I think what you are saying is that even that level of computation with types as values is out of reach in Coq. Correct?

Right.  The feature that prevents analysis of types is often presented as a big advantage of type theories.  It's often called "parametricity" and said to underlie abstract datatypes and abstraction via modules or classes.

Coq lacks functionalities to "destruct/inspect" and/or "construct" type definitions.

Well, I'd say Coq's logic Gallina lacks case analysis over types, but certainly allows very rich forms of constructing new types from old ones.

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.