[Agda] Re: [TYPES] strict unit type

[Robert Harper]

hello everyone,

there is no problem to decide equivalence in the presence of extensionality axioms such as eta and xi, nor for unicity conditions such as the one stating that all maps to 1 are equal.  my work with chris stone on singleton types shows how to handle sigma's and pi's and unit (actually much more than just unit, but including it as a special case), which specializes to arrow and cross as well.  generally the method works well for negative types, but cannot be made to scale to positive types, which require some form of induction.  so, for example, there is no problem with the "iota" (i.e., beta) rules for inductive types, since these are purely computational, and we can handle extensionality conditions for negative types, but one cannot expect something as strong as the coproduct universal condition for sums, merely the beta-like rule of reduction.

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.

as an aside, would someone please explain to me as concisely as possible what is the problem with universes in coq?  this came up in discussion here yesterday, and i drew the impression, perhaps mistaken, that the problem is that coq does not implement the solution that pollack and i worked out in 1988.  if i am right, the problem is already solved, but was apparently not used in the coq implementation for some reason.  i can explain separately what pollack and i did and how it works.  it sounded as though it would address many of the problems that have arisen, but i'm not completely certain until i learn more about them.

best,
bob

On May 10, 2012, at 11:41 AM, Altenkirch Thorsten wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> 
> On 10/05/2012 00:04, "Vladimir Voevodsky" <vladimir at ias.edu> wrote:
> 
>> 
>> On May 1, 2012, at 5:24 AM, Altenkirch Thorsten wrote:
>> 
>>> In general we shouldn't expect to decide eta equality by untyped
>>> reduction. eta equality isa form of decidable extensionality and does
>>> not
>>> correspond well to computation to a normal form.
>>> 
>>> Clearly, the case of the unit type shows that we need to know the type
>>> to
>>> check equality.
>>> 
>>> Trying to decide eta equalities by reduction is very non-modular. This
>>> is
>>> basically the point of Vladimir's email.
>>> 
>>> However, if we implement it as a type directed decision procedure things
>>> are much better. E.g. to terms f,g : Pi x:A.B x are convertible if f x
>>> and
>>> g x : B x are convertible (whewre x is a fresh variable) after beta
>>> reduction. Similarily, two terms p,q : Sigma x:A.B x are convertible if
>>> p.1 and q.1 : A are convertible after beta reduction and p.2 and q.2 : B
>>> p.1 (or B q.1) are convertible after beta reduction. (The and here has
>>> to
>>> be read sequentially, and the choice B p.1 or B p.2 actually causes some
>>> technical problems).
>> 
>> Why just after beta reduction and not say iota-reduction or even some
>> internal eta-reduction?
> 
> When I say beta I also mean beta for product and inductive types. The Coq
> people seem to call this iota reduction.
> 
> What do you mean by internal eta-reduction.
> 
> Btw, I don't think you need to reduce under a lambda (which is also a form
> of extensionality). So what I mean is to execute the purely computational
> rules (these are the once used by any functional programming language).
> 
> 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 send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.
> 
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.