The Coq mailing list

[Andrej Bauer <(e29315a54f%hidden_head%e29315a54f)andrej.bauer(e29315a54f%hidden_at%e29315a54f)andrej.com(e29315a54f%hidden_end%e29315a54f)>]

>>>> 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