The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

On 30 Sep 2021, at 11:24, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Why is it costly to maintain typing information?

with eta for unit for example, to decide whether x = y : P n for some variables x and y and predicate P, 

you need to check whether P n  is convertible to unit or not. Which means coarsely computing 

the weak-head normal form of  'P n’.

In a system without tactics, where only answering "yes" must quick, this may be acceptable.

But with tactics, answering “no” quickly is also very important because (of backtracking for instance)

many unsuccessful tests for conversion are triggered. 

Also you need it to allow eta for products in particular unit types and other decidable aspects of extensionality.

You can implement eta for (non-empty) products in an untyped setting using records with primitive projections. 

Only unit cannot be dealt with this way because it corresponds to a projection without arguments. 

For unit however, there is a workaround by defining it in a definitionally proof irrelevant sort (SProp in Coq, Prop in Agda),

in which case you get extensionality by the property of the sort, instead of the type. 

Amicalement,  

— Nicolas

 

Cheers,

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of nicolas tabareau <nicolas.tabareau AT inria.fr>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Thursday, 30 September 2021 at 09:47
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Convertibility with η-equivalence

 

Hi Thorsten, 

 

I completely agree with you that η should be thought of as an equivalence and not a reduction.  

And its natural specification is in a typed setting. 

 

However, when it turns to implementing an efficient type checker, it makes sense to 

try to decide this equivalence without relying on typing information, which are costly to maintain.

 

So what is important then is to show that the untyped implementation meets the typed specification.

 

This is not a formalist game but rather a developer concern. 

 

Best, 

 

— Nicolas

 

On 30 Sep 2021, at 10:34, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

 

Just some comments: the eta rule is a way to implement extensionality for pure functions, hence it is not really a form of computation unlike beta. Hence we shouldn’t think of it as a form of reduction it is an equivalence and reduction isn’t the best way to decide it. Also it makes very little sense on untyped terms, this seems to be rather some formalist game.

 

Thorsten

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.