The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 20 mai 2010 à 17:43, Chris Casinghino a écrit :

> Hello Yves,
> 
>> You should look at the pattern-matching constructs (for instance the value
>> of hlist_rect), the fact that the parameter does not occur among the
>> constructors' arguments plays a role.
> 
> I am confused.  Before sending my initial email, I observed that
> hlist_rect doesn't change if I make A an index and an argument to each
> constructor.  That is, this alternate version of hlist is given
> an identical hlist_rect (up to alpha-conversion):
> 
> Inductive hlist : Type -> Type :=
> | HNil  : forall A : Type, hlist A
> | HCons : forall A : Type, forall B, A -> hlist B -> hlist A.
> 
> This was the source of my confusion, since I thought the point of
> parameters was to get the nicer hlist_rect, as you suggest.  Am I
> missing something?

Hi Chris,

  one nice thing about non-uniform parameters is that you don't need dependent
elimination/inversion to use them, only substitution is needed. To see this, 
the
non-uniform parameter instance must depend on the initial parameter though. 
Also you can avoid raising universe levels using parameters instead of 
arguments.
As a slightly contrived example:

Inductive powlist (A : Type) := 
| pownil 
| powcons (a : A) (l : powlist (A * A)) : powlist A.

Inductive powlistarg : Type -> Type := 
| powargnil A : powlistarg A 
| powargcons A : forall (a : A) (l : powlist (A * A)), powlistarg A.

(* Now, if you pattern-match on a powlist (A * B) returning an A, you can 
do:*)

Definition powlista (p : powlist (nat * bool)) : option nat := 
  match p return option nat with
    | pownil => None
    | powcons (a, b) _ => Some a
  end.

(* While using an p : powlistarg (A * B) this won't typecheck: *)

Definition powlistarga (p : powlistarg (nat * bool)) : option nat := 
  match p return option nat with
    | powargnil _ => None
    | powargcons A' a l => Some (fst a)
  end.

You lose the information that A' = A * B here... so you'd need type 
equalities to make this work, or write a more generic definition on a 
"general" instance "powlistarg X". Of course, same goes for the recursive [l] 
argument which gets an overly general [powlistarg (A' * A')] type in the 
second case.

Another interest of non-uniform type parameters is that they are readily 
extractible to Haskell/OCaml which support polymorphic recursion. They are 
also used in the FingerTree contrib.

Hope this helps,
-- Matthieu