[Agda] Fin n -> Fin n extensional?

Tue Feb 24 10:44:01 CET 2015

They should be neither – the identity type Id_A should have the same polarity as the type A.

Thorsten

From: Gabriel Scherer <gabriel.scherer at gmail.com<mailto:gabriel.scherer at gmail.com>>
Date: Tue, 24 Feb 2015 08:59:35 +0000
To: Dan Doel <dan.doel at gmail.com<mailto:dan.doel at gmail.com>>
Cc: agda list <agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>>
Subject: Re: [Agda] Fin n -> Fin n extensional?

In general my understanding of type theory is that, in natural deduction calculi (all typed lambda-calculi) negative types (functions and records-with-projections) are easy to eta-expand, and positives (sums) are hard. I'm not sure whether identity types can be given a polarity, but it certainly would not be negative : their introduction rule is not inversible.

On Tue, Feb 24, 2015 at 1:30 AM, Dan Doel <dan.doel at gmail.com<mailto:dan.doel at gmail.com>> wrote:
I imagine Agda doesn't do eta expansion of the identity type because it doesn't do eta expansion of any inductive type. It only does it for records and functions.

If the identity type were a builtin, and all indexed types were expected to be defined by making reference to the identity type (or at least, were considered sugar for such), it would probably enable special treatment; it's probably how Epigram would have worked (they were considering other judgmental rewrites as well, like functor and monad axioms). Detecting which indexed inductive types are sufficiently identity-like to eta expand, or blessing only one (which I guess could be done since there are already pragmas informing Agda of the identity type for use in `rewrite`) would be difficult in the first case (probably) and weird in both.

On Mon, Feb 23, 2015 at 3:05 PM, Jon Sterling <jon at jonmsterling.com<mailto:jon at jonmsterling.com>> wrote:
Andrea,

Out of curiosity, is the reason that Agda does not do eta expansion at
the identity type because it would cause false identifications to become
true judgementally in an open term?

Kind regards,
Jon

On Mon, Feb 23, 2015, at 10:50 AM, Andrea Vezzosi wrote:
> As a side note, Agda doesn't actually do any eta expansion at the Id
> type, e.g. two postulated equalities won't be judgementally equal.
>
> However without postulates (or primTrustMe) it is still the case that
> every proof of equality in a closed context will evaluate to refl.
> Axiom K actually computes away as soon as the proof becomes refl, so
> it's not making this any harder.
>
>
> Cheers,
> Andrea
>
> On Mon, Feb 23, 2015 at 4:38 PM, Neelakantan Krishnaswami
> <n.krishnaswami at cs.bham.ac.uk<mailto:n.krishnaswami at cs.bham.ac.uk>> wrote:
> > -----BEGIN PGP SIGNED MESSAGE-----
> > Hash: SHA1
> >
> > Hello,
> >
> > Definitional equality including Axiom K (uniqueness of identity proofs)
> > remains decidable.
> >
> > The reason is that you can split the implementation of judgemental
> > into two alternating phases -- weak-head normalization and
> > type-directed eta-expansion. Just as with eta for unit, this means
> > that when you compare terms at equality type, you can simply succeed.
> >
> > Concretely, if you have proofs p and q at type Id[X](e,e') such that
> > p,q :  Id[X](e,e'), then you can eta-expand to p ==> refl and
> > q ==> refl, and then refl will be judged to be equal to itself.
> >
> > If you restrict "computation" to mean beta-reduction, then equality
> > proofs do not all have to *reduce* to refl. However, they all can
> > *eta-expand* to refl.
> >
> > IMO, a very good reference on this is Andreas Abel's habilitation
> > thesis. If you're in a hurry, then his FOSSACS 2011 paper with Gabriel
> > Scherer "On Irrelevance and Algorithmic Equality in Predicative Type
> > Theory" was a relatively accessible introduction to this approach.
> >
> >
> > Best,
> > Neel
> >
> > On 19/02/15 20:54, Abhishek Anand wrote:
> >> Thanks Jason. Your argument is convincing. Already at the second
> >> line,  (\_ → 0) and (\_ → 1)  being definitionally equal
> >> contradicts my understanding of Coq's definitional equality. Are
> >> your assumptions valid in Agda with K? In other words, is it true
> >> that in Agda with K, any proof of equality (Id) of closed terms
> >> computes down to refl?
> >>
> >>
> >> Thanks, -- Abhishek http://www.cs.cornell.edu/~aa755/
> >>
> >> On Wed, Feb 18, 2015 at 12:06 PM, Jason Gross
> >> <jasongross9 at gmail.com<mailto:jasongross9 at gmail.com>> wrote:
> >>
> >>> Here's one, I think, for showing impossibility of inhabiting the
> >>> type (f g : Void → ℕ) → Id f g: Assuming the type theory is
> >>> strongly normalizing on terms of identity type, the only closed
> >>> proof of equality of two closed functions must be refl.  Thus, if
> >>> (\_ → 0) and (\_ → 1) are equal, they must be definitionally
> >>> equal in a strongly normalizing type theory.  From (Id f g), we
> >>> can obtain (x : Void) → Id (f x) (g x); it's behavior is to send
> >>> refl to refl.  Thus, when we plug in refl : Id (\_ → 0) (\_ → 1),
> >>> we get a proof of Void → Id 0 1 which reduces to \_ → refl.  But
> >>> this is a contradiction, for refl does not prove Id 0 1.
> >>>
> >>> On Wed, Feb 18, 2015 at 11:37 AM, Abhishek Anand <
> >>> abhishek.anand.iitg at gmail.com<mailto:abhishek.anand.iitg at gmail.com>> wrote:
> >>>
> >>>> Unprovability of void-ext has been known to be the reason why
> >>>> one cannot (in Coq) code up natural numbers as W Types.
> >>>>
> >>>> Here is a quote : "This is because one cannot prove that there
> >>>> is only a unique function from the empty set to the set of
> >>>> natural numbers without using extensional equality." from
> >>>> https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes
> >>>>
> >>>> However, I don't know a formal (meta-theoretical) proof of
> >>>> unprovability of void-ext. I'd be grateful if someone can point
> >>>> us to such a  proof.
> >>>>
> >>>>
> >>>> -- Abhishek http://www.cs.cornell.edu/~aa755/
> >>>>
> >>>> On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata <drl at cs.cmu.edu<mailto:drl at cs.cmu.edu>>
> >>>> wrote:
> >>>>
> >>>>> Can you even do this (without otherwise assuming function
> >>>>> extensionality)?
> >>>>>
> >>>>> For example, for Fin 0, isn't it the same as saying "any
> >>>>> function from 0 to A is abort":
> >>>>>
> >>>>> data Id {A : Set} (a : A) : A → Set where refl : Id a a
> >>>>>
> >>>>> data Void : Set where
> >>>>>
> >>>>> abort : {A : Set} → Void → A abort ()
> >>>>>
> >>>>> void-ext : {A : Set} → (f : Void → A) → Id f abort void-ext f
> >>>>> = {!!}
> >>>>>
> >>>>> (void-ext is sufficient; is it necessary?) and if so, can you
> >>>>> prove that?  I don't see how off the top of my head.
> >>>>>
> >>>>> -Dan
> >>>>>
> >>>>> On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor <
> >>>>> J.P.PizaniFlor at uu.nl<mailto:J.P.PizaniFlor at uu.nl>> wrote:
> >>>>>
> >>>>> Not yet (couldn't find it anywhere), but I will probably need
> >>>>> it for my Ph.D project, so maybe it will come in some
> >>>>> time...
> >>>>>
> >>>>> Cheers,
> >>>>>
> >>>>> João Pizani, M.Sc <j.p.pizaniflor at uu.nl<mailto:j.p.pizaniflor at uu.nl>> Promovendus -
> >>>>> Departement Informatica Faculteit Bètawetenschappen -
> >>>>> Universiteit Utrecht
> >>>>>
> >>>>> On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette
> >>>>> <carette at mcmaster.ca<mailto:carette at mcmaster.ca>> wrote:
> >>>>>
> >>>>>> Does anyone have a proof in Agda that functions at type
> >>>>>> (Fin n -> Fin n) are extensional? Jacques
> >>>>>> _______________________________________________ Agda
> >>>>>> mailing list Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> >>>>>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>>>>
> >>>>>
> >>>>> _______________________________________________ Agda mailing
> >>>>> list Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> >>>>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>>>
> >>>>>
> >>>>>
> >>>>> _______________________________________________ Agda mailing
> >>>>> list Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> >>>>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>>>
> >>>>>
> >>>>
> >>>> _______________________________________________ Agda mailing
> >>>> list Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> >>>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>>
> >>>>
> >>>
> >>
> >>
> >>
> >> _______________________________________________ Agda mailing list
> >> Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> >> https://lists.chalmers.se/mailman/listinfo/agda
> >>
> > -----BEGIN PGP SIGNATURE-----
> > Version: GnuPG v2.0.14 (GNU/Linux)
> >
> > iQIbBAEBAgAGBQJU60laAAoJEFHmop5RZGmSfJcP91HMj9P8+iiF344OtyF+Pfv1
> > IUk+w4IndUMQcDPFys0GCX9VyMeg5W3ezwV1eYYLNlSghtR/rWAVtKRlDH/PQ8Hp
> > Q9RJhpEo3gNMW1cBSHWTM7HpmcI2z8ttualtE/1+yK4XPRC0vXw6V6mOHv4KmDES
> > xjhsKy4ut8Ah4pTXvb0+MkTvI46F7dpBlkpQmAFygpfOtNz7ahZ4+bQjlmdPMu6B
> > DG9jwtA9HuEBoxR84Fni0w9gA5da+Ew7cF0mcuG777RK3M6NnuB+jnyk18w7qUKv
> > bQ9s4Is0YZ4KHkDmNe6tVnTbDaivzQfN6rBTFPfrRPHCo0b4cU3Dpos7dQdOf56a
> > qvlmC8hoB60KGaLYx+SqjAHfEudHsTPzpDQUHZE0T+zlqLBI1g8y9my20rd5PN3t
> > S4sapKOVsVibd+XnNbGDhoRDA4Uy1KccO0O9Yt8w1/yTpJqik4DfB8g7tEIzsgc+
> > 137F+WnUfNiilpukOWrhzSRmxpmOgGZaA96o4tsq6eZjf8w9OSZeYFzEqn+pCtci
> > gClqrFGIdbBXHEcOMnJ5K+Y1y+1himsvfM8XavdE0tTfv2+aGknpwm9qRs6SG7+w
> > gNV18wNhkL6BqdDTnEIJ6y1PvK/IDmi6D9Ar9eL8nvcELzzsEbDFLFWkm/ElSzZ6
> > OC285Dst5uKeClsp238=
> > =qT5j
> > -----END PGP SIGNATURE-----
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150224/ea7ce0ed/attachment-0001.html