The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

Hi Kevin,

The usual way around this is to define syntax for types e.g.,:

Inductive tipe : Set := 
  | Nat : tipe
  | Pair : tipe -> tipe -> tipe
  | Arrow : tipe -> tipe -> tipe.

and then an interpretation of your syntax back into semantics:

Fixpoint interp(t:tipe) : Set := 
  match t with 
  | Nat => nat
  | Pair t1 t2 => (interp t1) * (interp t2)
  | Arrow t1 t2 => (interp t1) -> (interp t2)
  end%type.

Then you can define equivalence on tipes e.g.:

Definition tipe_eq : forall (t1 t2:tipe), {t1=t2}+{t1<>t2}.
  decide equality.
Defined.

This gets trickier when you have complicated types (e.g., 
polymorphism or dependent types).  

-Greg

On Jun 3, 2013, at 3:42 PM, Kevin Sullivan 
<sullivan.kevinj AT gmail.com>
 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? Coq lacks functionalities to 
> "destruct/inspect" and/or "construct" type definitions. E.g., to write a 
> function that takes a type and returns a type that is a composition of that 
> type with some new type information. Have I basically got this right?
> 
> 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?
> 
> Kevin 
>