The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 10 Oct 2012 16:08:41 +0200,
Gabriel Scherer 
<gabriel.scherer AT gmail.com>
 a écrit :

> 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.

Sorry to disappoint you, what I gave was an example, I do not really
use it. In practice I use a "Inductive type := Nat | Bool." as you said
further. Note however that proof irrelevance is not required if you
work modulo some equivalence relation. And you can admit UIP which is
weaker than proof irrelevance, if I am correct.

> 
> 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.
> 

My initial problem is not affected if you replace "T" with "bool",
"nat" with "true" and "bool" with "false"

> 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 ?