The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

I would be interested to hear a bit more about how you use those
types. From what I understand, dependent elimination as in exp and
GADT-like type equalities as in exp_ are not always equivalent; for
example, the latter form tend to require axioms of irrelevance of
equality proofs (eg. K) to work correctly in practice, while the
former do not (I'm no expert on this topic but this is what I got from
the comparison between Agda and Coq systems, and Pierre Boutillier
explanations); in the cases where both style can be chosen, I thought
the former was preferred for this reason.

I thought the expected way to define those types was to have a
dependency (as in your first example), but not on a type, rather on a
base value (eg. an "Inductive tag := Nat | Bool"; the reason being the
need to have stronger equalities: at the type level you can't prove
for example iirc. that (nat * bool) is different from nat. While (nat
<> bool) should be provable and make your particular example work
correctly, I would expect more general examples of GADTs to fail if
formulated in this way because the theory of type inequalities is
weaker than what you have in, say, OCaml or Haskell.

On Tue, Oct 9, 2012 at 6:30 PM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> Hi all, I think there is no real work around for my problem here, but I
> still ask to the list.
>
> Imagine, I have an AST, like this one:
>
> Inductive exp : Type → Type :=
> | Nat : nat → exp nat
> | Bool : bool → exp bool
> | Plus : exp nat → exp nat → exp nat
> | If : exp bool → exp nat → exp nat → exp nat.
>
> I find it cumbersome to have to deal with dependant types directly, so
> I use parameters in stead of indice:
>
> Inductive exp_ (T : Type) : Type :=
> | Nat_ : T=nat → nat → exp_ T
> | Bool_ : T=bool → bool → exp_ T
> | Plus_ : T=nat → exp_ nat → exp_ nat → exp_ T
> | If_ : T=nat → exp_ bool → exp_ nat → exp_ nat → exp_ T.
>
> With that, I do not require inversion tactic any more (at least for
> 'exp_'), since there is no dependance. But inserting all these
> equalities in the definition is ugly, the version with dependant types
> is a lot nicer. So I wanted to trick Coq using notations.
>
> Definition app (U : Type) : (Type → Type) → (Type → Type) :=
>   λ p t, (U=t → p t).
>
> Reserved Notation "[ e ∷ t ]". (* := (app t e _).*)
>
> Inductive exp__ (T : Type) : Type :=
> | Nat__ : nat → [exp__ ∷ nat] T
> | Bool__ : bool → [exp__ ∷ bool] T
> | Plus__ : exp__ nat → exp__ nat → [exp__ ∷ nat] T
> | If__ : exp__ bool → exp__ nat → exp__ nat → [exp__ ∷ nat] T
> where "[ e ∷ t ]" := (app t e).
>
> This works, and I find it a lot better than exp_. But there are
> trailing 'T's which seem rather strange. So I would rather write
>
> Inductive exp__ (T : Type) : Type :=
> | Nat__ : nat → [exp__ ∷ nat]
> | Bool__ : bool → [exp__ ∷ bool]
> | Plus__ : exp__ nat → exp__ nat → [exp__ ∷ nat]
> | If__ : exp__ bool → exp__ nat → exp__ nat → [exp__ ∷ nat]
> where "[ e ∷ t ]" := (app t e T).
>
> but it does not work, since T is not known to the system at this place
> (sad thing), and putting '_' instead of 'T' does not work either as
> the type system is not able to infer it.
>
> There are mainly two reasons, the first one is that it would require to
> reduce "app" before finding that 'T' is the only possibility, and the
> second one is that even in some basic case, such as "Inductive list
> (A:Type) : Type := nil : list _ | cons : A → list A → list _." it does
> not work even if the '_' cannot be filled with anything else than A.
>
> Do you think some feature request should be sent, or do you have some
> workaround ?