The Coq mailing list

[Chris Casinghino <ccasin AT cis.upenn.edu>]

Hello Hugo and Matthieu,

Thank you both for the thoughtful examples.  I now understand some of
the ways that I have underestimated the usefulness of parameters!  The
pattern matching example is particularly compelling.

--Chris

On Thu, May 20, 2010 at 12:33 PM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
>
> 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
>