The Coq mailing list

[Vladimir Voevodsky <(e29315a54f%hidden_head%e29315a54f)vladimir(e29315a54f%hidden_at%e29315a54f)ias.edu(e29315a54f%hidden_end%e29315a54f)>]

I am thinking about including these reductions in the design of a universe 
polymorphic type system which I am working on but I plan to study the paper 
by Abel, Coquand and Pagano before making a definite choice.

V.



On May 6, 2012, at 6:29 PM, Andrej Bauer wrote:

>>>>> 2. Prod x : T , Pt reduces to Pt,
>>>>> 
>>>>> 3. Prod x : Pt , T reduces to T.
>>> 
>>> I would qualify this as *very* agressive! Extraction, just to mention
>>> one feature, will not survive this extension.
>> 
>> Unless it is implemented in the target language...
> 
> Some years ago Chris Stone and I used a realizability interpretation
> to extract programs from from a first-order logic over dependent
> types. We had a type much like the suggested Pt. We systematically
> removed all occurrences of Pt. For example Pt -> T and Pt * T were
> converted to T. It's doable, although some care needs to be taken, and
> my feeling is that such things are better done through manipulation of
> extracted code rather than in the original logic/type-system, because
> a lot is known about optimization of programs and a little less about
> optimization of logic.
> 
> It was cool to see lots of proof-irrelevant stuff disappear in the
> extracted code (we worked on the assumption that equality was
> proof-irrelevant).
> 
> With kind regards,
> 
> Andrej