[Agda] Fin n -> Fin n extensional?

[Gabriel Scherer]

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> 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>
> 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
>>
>
>
> _______________________________________________
> 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/20150224/3d5c6462/attachment.html