[Agda] Fin n -> Fin n extensional?
Conor McBride
conor at strictlypositive.org
Tue Feb 24 11:37:11 CET 2015
Hi
Lurking briefly…resulting in delurking.
On 24 Feb 2015, at 09:45, Neelakantan Krishnaswami <n.krishnaswami at cs.bham.ac.uk> wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hello,
>
> This is a good point.
>
> However, you can retain a type preserving definitional equality
> validating K, even without eta-expanding identity proofs, simply
a ha ha ha...
> by equating all terms at identity type:
>
> Γ ⊢ q : Id[X](e,e')
> Γ ⊢ p : Id[X](e,e')
> ————————————————————————
> Γ ⊢ p ≡ q : Id[X](e,e')
>
> A type-directed equality algorithm will hit the Id case and then
> stop with success. You can do the same for units and empty types,
> even if you view them as positive types.
Proof irrelevance cannot “simply" be had for the asking. You need to make
sure that proofs are everywhere treated as irrelevant. For the empty type,
this is easy. For the unit type, this is nearly easy: if you happen to have a
dependent eliminator which computes by pattern matching
oneElim : forall {l}(x : One)(P : One -> Set l)(p: P void) -> P x
oneElim void P p = p
you have a little work to do. The trouble is that if void’ : One, then the type
oneElim void’ (\ _ -> Set) (Two -> Two)
is definitionally equal (because all Ones are equal) to Two -> Two, but mere
evaluation will not deliver that canonical form. Any process based on the
idea that evaluation is good enough to find a canonical form if there is one
is now busted. The fix is simple: exploit the eta law to make oneElim lazy:
oneElim _ _ p = p
is perfectly well typed. (i.e. just throw the damn eliminator away)
Let me expand a little on the following.
> On 23/02/15 22:29, Andrea Vezzosi wrote:
>> Jon,
>>
>> Yeah, I was going to add that eta expanding Id[X](e,e') to refl is
>> only type preserving when e and e' are judgementally equal, and in
>> an open context they might not be.
That’s a very “intensional” thing, of course. If you have the equality
reflection rule, then e and e’ are judgmentally equal and the eta-expansion
makes sense…with the usual dangerous consequences for open
computation in such systems.
>>
>> Best, Andrea
>>
>> On Mon, Feb 23, 2015 at 9: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
So, the fix for the Id type is trickier, as the pattern matching plays a
nontrivial role
idElim : {X : Set}(x y : X)(q : Id[X](x, y)(P : (x y : X) -> Id[X](x, y)) ->
P x x refl -> P x y q
idElim x .x refl P p = p
relies on the input p to have exactly the right type to be given as the output,
up to definitional equality; the identity proof being refl is a sound (and cheap)
but not complete test for that property. You cannot deploy the same fix as
with oneElim, because
idElim _ _ _ _ p = p
is ill typed and allows you to write non-normalizing terms, if you happen to
be in a (not atypical nonempty) context where Id[Two](tt, ff) is hypothetically
inhabited: take P _ tt _ = Nat; P _ ff _ = Nat -> Nat and write delta delta.
Two fixes which do work are the conditional behaviours (in evaluation)
idElim x y _ P p = p if x = y definitionally
or even more liberally
idElim x y _ P p = p if P x = P y definitionally
which at least keep the thing typesafe without needing to look at the proof.
Fortunately, the problem for whose solution the proof is a proxy is decidable,
namely the definitional equality of the input and output types. That is not
always so. In the case of observational equality, it looks like the problem
has become undecidable, because extensional equality is undecidable, but
the trick is to change the problem: in OTT we need to know only if coercion
can make *incremental* progress, and that is readily decidable by looking at
the heads of the types between which we coerce. But don’t get too hopeful...
> If you know the type is a subsingleton, then definitional equality can
> always succeed.
Termination propositions (e.g., Bove-Capretta domain predicates) tend to be
subsingletons, but the problem they solve is somewhat famously undecidable.
It is clear that pattern matching on termination proofs is a sound but not
complete test for whether the computation can take a step, but that would be
incompatible with making definitional equality trivial for termination proofs, for
the reason given above. To replace pattern matching on the proof by some
other test on the problem of whether to compute, without risking that some
liar will have us in a flat spin, does seem like asking too much.
Not all subsingletons can be made definitionally proof irrelevant and disposed
of from open computation. That’s why Coq’s Prop cannot be made proof
irrelevant. Subsingletons can, of course, be erased from the closed computation
we do at run time, whatever their sort.
The literature is full of work which erroneously conflates irrelevance in
typechecking with irrelevance in execution.
Blue in the face
Conor
> In the case of Id, this rule *makes* it into a
> subsingleton, of course! (Or rather, ensures that the syntax can only
> be interpreted by models in which equality is a subsingleton -- which
> rules out univalent models.)
>
> Best,
> Neel
>>>
>>>
>>> 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:
>> 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
>>>>>>>
>>>>> _______________________________________________ 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)
>
> iQIcBAEBAgAGBQJU7Eg5AAoJEFHmop5RZGmSND8QAIYdzpshHhbvJdCToFTHlysE
> Yqjeb7kgYk3kaYtQsrVSbe51srfSDrxUCT+WoQS3dpXsduXup+pa5XWDX6rQ5SY8
> T7Xd2pLOEDF/lkjDvGtZd1RHFa/tYA3IkyZkxPisQroEWEH8JWMz1B0uedwZx23y
> c3cCaSpSd8mNX2IemcH+FtGLngp/mez7V09YUR/J9ETRsmgyl1u7iJRNW018FB36
> qhtk4P0Sg/2C+13yLLJkkBy55X6iS3wQAJwLo3FXxJy2rBZJUcEt3R+da2LU3bBS
> 8q2EMTf5NOJBIFwOUWWgZMkyh4lyAaiiKPFwUKjQ2S0Nofkb/49YdSGw4vpuR1+u
> HxXDagO+8wZNn5PC/nDhbZFUhoc7raq3ADd3ft8HStedLVZvnVUun/EK+ZOzubGy
> YogUVoPZTmnl2PC/oSmrRvUsoPn4eLh9JYrrdbDUVtr4U8V8IPedoOmvJ7gDe0FI
> TXDA7PpSgoLFog+YhuNVow8QNyrBA00SSE7iqYwbi7UhQ+8flomOB3dhJncG1OzM
> EEfXCu6S2oe4ekYYDhM/2RHW7Q+No7HmKowqjLnlsoxKGJC5jjVrU7sGl/2qKVTQ
> V9r9MOdfzqZOv0TCGHApcpYttILiEtcel2OiUF3eFo6cVaDa/NK2SKeeil2RdHbT
> 9EvbHgX7FRCYtTqxlMeq
> =Csvc
> -----END PGP SIGNATURE-----
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list