The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  Canonical structures are indeed represented in CiC -- as explicit records 
(i.e., the constructor of a non-indexed Inductive, applied to some 
arguments), or more generally as functions that return an explicit record. 
Declaring any particular record as a Canonical Structure augments the 
unification procedure used by type inference (and by the tactic engine in 
ssreflect and the development version of Coq) with hints that allows it to 
resolve equations of the form
   <projection> <unknown/partly known record> = <projection value>
where <projection> is one of the projectors created by the declaration of the 
type of the record (e.g., x or y in Record point := Point {x : nat; y : 
nat}), and <projection value> is the value of that projection for the record 
being declared canonical.
  These Canonical Projection values are classified by their head constant -- 
Coq will not register a Canonical Projection hint for a value that does not 
have a head constant, nor will it register a second hint for a given 
constant/projection pairs (it just ignores the user command silently in this 
case, which is a bit user-unfriendly). You can get a list of all these pairs 
with the Print Canonical Projections vernacular command, which also gives the 
particular Record value used to resolve each pair. Since Coq 8.2pl1, it is 
also possible to define default projections whose value is one of the 
arguments of the Canonical Structure record-producing function; such hints 
can be used for any right-hand side in the equation above (they are displayed 
as '_' by Print Canonical Projections).
  Like most of the rest of Coq, there is no real documentation of the inner 
workings of Canonical Structures, other than the system code; they are not 
covered in Coq'art, but I know Yves is cooking up some kind of tutorial going 
over some of the design patterns that have emerged from our work. For a basic 
use, the naive semantics given in the Coq documentation are sufficient. 
Advanced use requires some knowledge of how higher-order unification is 
implemented in Coq, as well as the Canonical Structure implementation 
details. Here are a few of them :
 - Coq attempts to use computation (beta-iota reduction), first-order 
unification, Canonical Structure (CS) hints, and constant expansion (delta 
reduction), in that order, and recursively, to resolve unification problems.
 - Because delta-expansion changes the head constant of a term it can change 
which CS hints apply. This can be used to introduce non-determinism into the 
otherwise fully deterministic
CS resolution. Delta expansion can also change or even destroy the projection 
constant; the latter curtails CS resolution, so since version 8.1 Coq defers 
the expansion of projection constants. Beware however that this expansion 
heuristic explicitly excludes unification problems where the record is partly 
known, a situation that arises systematically when the telescope design 
pattern is used; in that case CS resolution can become very fragile.
 - The unification process is slightly more complicated than what I hinted 
above, as the CS record can be a function, and the record type can have 
parameters. In general a CS "record" will have the form
   CR := fun <formals> => R <parameters> ... (C_i <arguments>) ...
and a matching unification problem will have the form
   p_i <actual parameters> <unknown record> == C_i <actual arguments>
This is resolved by replacing <unknown record> with CR <fresh formals>, 
reducing and resolving the residual unification problem, then separately 
resolving the problem
  <unknown record> == CR <fresh formals>
(here, <fresh formals> is a list of new unification variables, same as you 
get with '_'.)
  The first part amounts to replacing <formals> with <fresh formals> in 
<parameters> and <arguments>, then separately resolving the problems
     <parameters> == <actual parameters>
     <arguments> == <actual arguments>
For each of these, the whole unification procedure is invoked recursively, so 
in particular further CS hints may be used. 
  
  Cheers,
Georges Gonthier

-----Original Message-----
From: 
komendantsky AT gmail.com
 
[mailto:komendantsky AT gmail.com]
 On Behalf Of Vladimir Komendantsky
Sent: 18 March 2010 11:38
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Canonical Structure

Hello,

It would be interesting to know whether Canonical Structure has a
formal representation in the CiC. The reference manual describes it as
a type-checker hint. However, canonical structures are complementary
related to implicit coercions that seem to be representable in the
CiC.

Is there a reference on the implementation of canonical structures?

Regards,
Vladimir