[Agda] Re: [TYPES] strict unit type

[Andreas Abel]

Hi Bob,

thanks for sending your and Chris' paper.  In

   A Modular Type-checking algorithm for Type Theory with Singleton 
Types and Proof Irrelevance
   http://www.lmcs-online.org/ojs/viewarticle.php?id=598&layout=abstract

we were able to extend the extensional treatment of singleton types to a 
type theory with universes (and of course, Sigma).  Out tool is NBE.

In the presence of computation of the type level (due to universes), the 
phase separation you describe below is no longer possible.  Both phases 
have to interleave since you unravel the structure of types only step by 
step.

We did not require a sophisticated argument for the correctness, it is 
typical model constructions we use.  A PER model to relate values to 
values (extensionally), and a Kripke model to relate terms to values.

Cheers,
Andreas


On 11.05.12 4:31 AM, Robert Harper wrote:
 > the algorithm that stone and i give has a two-phase flavor.  first, a
 > type-directed phase that reduces things to atomic types by
 > elimination forms, then a structural phase that compares the weak
 > head normal forms of the results of the type-directed phase.  (weak
 > head normalization takes care of all beta-like rules.)  the
 > structural phase calls back to the typed phase.  the correctness
 > argument is fascinating (imo) because of the complications introduced
 > by the asymmetries hinted at in thorsten's post having to do with the
 > interaction between sigma's and pi's.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/