The Coq mailing list

[Marko Luther <luther AT ares.informatik.uni-ulm.de>]

Hello,

>  Dear Ewen,
>
> > Can the pretty-printing mechanism be changed to prevent `unnecessary'
> > types being shown?
>
>  A rule for Coq output is that what is printed could be re-parsed as
> is. Then, you can avoid `unnecessary' types being shown if a dual
> mechanism allow to automatically deduce these types.

No rule without exception:)

Earlier this year I encountered the following problem with the
printing/parsing mechanism used in Coq:

In the trace below Coq (I think V6.24) prints the expression
'(f (c o))' (explicit term '(f N (c o))') as '(f (o))' which is
original of type 'N'. While re-parsing '(f (o))'
the system infers the explicit term '(f O o)' which is of type 'O'.

The source of the problem is an interaction (or confusion) between the
2 mechanism which generates the Implicit Syntax, namely Argument Synthesis
and Coercion Synthesis.
In my opinion this is not just an implementation bug,
but something which has to be analyzed and formalized in greater detail.
Of course the trivial solution to print all terms fully explicit is not a good
choice for a proof development system which wants to be useful.

At the moment I am working on an advanced (partial) type inference 
algorithm for
our Typelab System (based upon an equivalent calculus as Coq), which
combines Argument Synthesis (including the inference of the type of nil),
Coercion Synthesis and the inference of anonymous type annotations.
Taking Implicit Syntax seriously I have develop a (partial)
erasure algorithm which has the desired feature of being invertible 
with respect
to the elaboration algorithm (every erasure can be elaborated again 
into the same orginal term of the explicitly typed language).
While this work is still unfinished, I'd be very interested to hear what 
people
have to say on the general topic.

Best regards,
   Marko Luther

----------

Trace:

Coq < Implicit Arguments On.

Coq < Variable N:Type.
N is assumed

Coq < Variable O:Type.
O is assumed

Coq < Variable f:(T:Type)(t:T) T.
f is assumed

Coq < Print f.
*** [ f : (T:Type)T->T ]
Position [1] is implicit

Coq < Variable c: O -> N.
c is assumed

Coq < Variable o:O.
o is assumed

Coq < Class N.
N is now a class

Coq < Class O.
O is now a class

Coq < Coercion c:O >-> N.
c is now a coercion

Coq < Check (f (c o)).
(f (o))
     : N

Coq < Check (f (o)).
(f o)
     : O


Marko Luther               phone: +49 731 - 50 24117
Artificial Intelligence    fax:   +49 731 - 50 24119
University Ulm             
mailto:luther AT informatik.uni-ulm.de
D-89069 Ulm                http://www.informatik.uni-ulm.de/ki/luther.html