The Coq mailing list

[Julien Tesson <julien.tesson AT univ-orleans.fr>]

Le 18/07/2011 16:23, AUGER Cedric a écrit :
> Julien Tesson 
> <julien.tesson AT univ-orleans.fr>
>  a écrit :
>> I was looking for an example where it is *not* eliminated *and* it is
>> meaning full. For example
>>    
>>
>>     Definition A : Prop :=  1=1.
>>     Definition a : A.
>>     reflexivity.
>>     Qed.
>>
>>
>>      Definition aList := a::a::a::nil.
>>
>> Here aList is a structure containing elements in Prop, but it is in
>> Set, and at extraction it gives
>>
>>     Extraction aList.
>>
>>
>>     (** val aList : __ list **)
>>     let aList =
>>       Cons (__, (Cons (__, (Cons (__, Nil)))))
>>
>> where __ is a kind of unit. So  I suppose that such structure could
>> be useful, but I am curious to see a real exemple using such things.
>>
> Sorry I misunderstood what you wanted.
> Note that "__" is not really a kind of unit.
> It is a Obj.t, that is, it can be almost anything.
>
> Consider this funny program for instance:
>
> Fixpoint narity n := match n with O => nat | S n => nat -> narity n end.
>
> Fixpoint sum m (k:nat): narity m :=
>   match m as n return (narity n) with
>   | 0 => k
>   | S m0 => fun H : nat => sum m0 (k + H)
>   end.
>
> ==and its extraction==
>
> type __ = Obj.t
>
> type nat =
> | O
> | S of nat
>
> (** val plus : nat -> nat -> nat **)
>
> let rec plus n m =
>   match n with
>   | O -> m
>   | S p -> S (plus p m)
>
> type narity = __
>
> (** val sum : nat -> nat -> narity **)
>
> let rec sum m k =
>   match m with
>   | O -> Obj.magic k
>   | S m0 -> Obj.magic (fun h -> sum m0 (plus k h))
>
> ====
> the "__" is clearly not a unit type!
> In this context, as it replaces a "Prop", you can see it as a unit type
> only if you believe in proof_irrelevance.
>
thank you for this funny and insightful example on the type __ :)

But the type is not really  used, actually if you give this code to ocaml,
the sum function is of type
nat -> nat -> 'a
which is compatible with the

 nat -> nat -> narity

type.  narity is not really used but Ok, it could be.

> Extraction doesn't need proof_irrelevance to be assumed AFAIK.
>
> For your initial question, well, I guess it is never meaningfull to not
> eliminate a "Prop", since you forbid to inspect it.
> The only "Prop" you can inspect are singletons, so they don't need to
> be matched.
>
> BUT, sometimes it is not eliminated for typing reasons.
> For instance in your list example, you cannot remove the "__", since
> the constructor of a list always expect an argument.
Actually, that's why I expected the whole type [list A] to be in Prop when 
[A] is in Prop ...
so that a list of "proofs" would be eliminated at extraction.
That's why I am still curious to see an example where such a list would be 
useful.
it would be extracted as a list of  __ where  __ is the value [let rec f _ = 
Obj.repr f in Obj.repr f]
not the type Obj.t

Your example make me think that, maybe, the examples of polytypic programs 
given in CPDT could use such things.
Unfortunately, I have not the time to explore this more in depth for some 
month ...

thanks again,
Julien.

-- 
Julien Tesson

Doctorant - ATER
Laboratoire d'Informatique Fondamentale d'Orléans
Département Informatique
Université d'Orléans

Tel : 02 38 49 25 81
Fax : 09 56 45 86 27
http://tesson.julien.free.fr/