[Agda] Fin n -> Fin n extensional?
Dan Doel
dan.doel at gmail.com
Tue Feb 24 01:30:10 CET 2015
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> 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> 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> 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> 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>
> > >>>> 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> 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> Promovendus -
> > >>>>> Departement Informatica Faculteit Bètawetenschappen -
> > >>>>> Universiteit Utrecht
> > >>>>>
> > >>>>> On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette
> > >>>>> <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
> > >>>>>> https://lists.chalmers.se/mailman/listinfo/agda
> > >>>>>>
> > >>>>>
> > >>>>> _______________________________________________ Agda mailing
> > >>>>> list Agda at lists.chalmers.se
> > >>>>> https://lists.chalmers.se/mailman/listinfo/agda
> > >>>>>
> > >>>>>
> > >>>>>
> > >>>>> _______________________________________________ Agda mailing
> > >>>>> list Agda at lists.chalmers.se
> > >>>>> https://lists.chalmers.se/mailman/listinfo/agda
> > >>>>>
> > >>>>>
> > >>>>
> > >>>> _______________________________________________ Agda mailing
> > >>>> list Agda at lists.chalmers.se
> > >>>> https://lists.chalmers.se/mailman/listinfo/agda
> > >>>>
> > >>>>
> > >>>
> > >>
> > >>
> > >>
> > >> _______________________________________________ Agda mailing list
> > >> 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
> > > https://lists.chalmers.se/mailman/listinfo/agda
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150223/b4ea62e4/attachment-0001.html
More information about the Agda
mailing list