[Agda] Trust me regarding Dan Licata's trick
Guillaume Brunerie
guillaume.brunerie at gmail.com
Thu Jun 6 20:57:38 CEST 2013
But primTrustMe only computes when the endpoints are definitionally equal.
If they are not then the term is stuck just as any other postulate.
primTrustMe is not much better than a postulate when it comes to canonicity.
For instance consider T the hprop-truncation of bool, P the constant
fibration over T with fiber Nat, and consider the closed term:
transport P (truncation-is-hprop true false) 0
This is a natural number which should normalise to 0 if you have
canonicity, but it doesn't, even if you use primTrustMe.
(on the other hand if you *compile* it, then it will compute to 0, but
combining that with univalence you can easily get a segfault)
On Jun 6, 2013 3:20 PM, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:
>
>
> On 06/06/13 16:16, Guillaume Brunerie wrote:
>
>> Are you planning to compile such code?
>>
>
> Not necessarily, but I want to normalize closed terms of e.g. natural
> number type.
>
> When I say that I want a definition that computes, I mean that the
> addition of this construction should preserve canonicity (say for closed
> terms of natural number type).
>
> It doesn't really seem safe to me to compile all truncation-is-hprop to
>> refl, especially when combined with univalence.
>> As far as I understand, it only affects the compiler (not the
>> normalisation procedure in the type checker), so maybe it's safe if you
>> just want to type-check code.
>>
>
> If I wanted to just type check, then postulates would be enough.
>
> For the interval, given that the two endpoints are not definitionally
>> equal, I don't think there is any difference with the version using a
>> postulate (unless you compile the code, in which case strange things
>> might happen)
>>
>
> Well, I would be very surprised if it works, because the interval gives
> you functional extensionality, and it would be too easy to get that from
> data abstraction + primTrustMe in such a way that canonicity is preserved.
>
> Best,
> Martin
>
>
>
>> On Jun 6, 2013 8:35 AM, "Martin Escardo" <m.escardo at cs.bham.ac.uk
>> <mailto:m.escardo at cs.bham.ac.**uk <m.escardo at cs.bham.ac.uk>>> wrote:
>>
>> Hi Dan,
>>
>> On 05/06/13 17:41, Dan Licata wrote:
>>
>> As far as I understand it,
>> primTrustMe is a way of asserting an equality, which is slightly
>> better
>> than a postulate because when it has type x = x , it reduces to
>> refl.
>>
>> > [...]
>>
>> I would guess that what you're doing below is OK: For the usual
>> definition of ∥ X ∥ as a higher inductive type,
>>
>> (x : ∥ X ∥) (p : Id x x) -> Id p refl
>>
>> will be propositionally true, (∥ X ∥ is an hprop, and therefore an
>> hset).
>>
>>
>> Yes, that's precisely my intuition. But this intuition would work
>> for the interval too, because it is an hprop and hence an hset, but
>> I don't think this trick would work for the interval. Or would it?
>>
>> Using primTrustMe will strictify certain instances of this (the
>> ones where p is constructed by applying truncation-is-hprop to
>> definitionally equal arguments) to definitional equalities. Off
>> the
>> top of my head, I don't see why that would go wrong.
>>
>>
>> I agree. But it would be nice to hear from those who designed and
>> implemented the feature.
>>
>> On the other hand, using primTrustMe to implement the circle or
>> something like that would be bad: if loop : Id{S1} base base
>> is defined to be primTrustMe, it will reduce to refl.
>>
>>
>> I agree too.
>>
>> Best,
>> Martin
>>
>>
>> -Dan
>>
>> On Jun05, Martin Escardo wrote:
>>
>>
>> On 05/06/13 03:12, Guillaume Brunerie wrote:
>>
>> I’m not sure I understand what you are trying to do.
>>
>>
>> I am trying to use an unsound Agda feature to implement a
>> sound
>> construction (hpropositional reflection or truncation).
>>
>> I don’t really know what primTrustMe is,
>>
>>
>> Me neither, and this is why I asked the question here. The
>> documentation
>> http://code.haskell.org/Agda/_**_doc/release-notes/2-2-6.txt<http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt>
>> <http://code.haskell.org/Agda/**doc/release-notes/2-2-6.txt<http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt>
>> >
>> says:
>>
>> "Note that the compiler replaces all uses of primTrustMe
>> with the
>> REFL builtin, without any check for definitional
>> equality. Incorrect
>> uses of primTrustMe can potentially lead to segfaults or
>> similar
>> problems."
>>
>> However, It Doesn't say what the correct uses are meant to be.
>>
>> but it seems to be some kind of postulate that every
>> type is an
>> hprop, which seems much worse than just postulating that
>> a single
>> type is an hprop.
>>
>>
>> Yes, but notice that I use it privately, hopefully in a
>> sound way.
>>
>> What are you trying to achieve exactly?
>>
>>
>> I am trying to (soundly) implement hpropositional truncation
>> that
>> computes, without *any* postulate at all.
>>
>> Voevodsky's Coq implementation uses type-in-type (also
>> unsound in
>> general, but backed by sound resizing axioms in this case) and
>> additionally postulates the axiom of function extensionality
>> to show
>> that the truncation really is an hproposition.
>>
>> Here is an improved version of what I sent yesterday, with
>> more
>> explanations, and the main question repeated.
>>
>> Best,
>> Martin
>> ------------------------------**
>> __----------------------------**--__-------
>> Here is what we want to achieve:
>>
>> Given a type X, we want to construct a type ∥ X ∥:
>>
>> X type
>> ----------
>> ∥ X ∥ type
>>
>> We want any two elements of ∥ X ∥ to be propositionally
>> equal, written
>> hprop ∥ X ∥.
>>
>> We have the introduction rule:
>>
>> x : X
>> ---------------
>> ∣ x ∣ : ∥ X ∥
>>
>> The elimination rule or induction principle, for any P : ∥ X
>> ∥ → Set:
>>
>> g : (h : ∥ X ∥) → hprop(P h) f : ((x : X) → P ∣ x ∣)
>> ------------------------------**
>> __------------------------
>> elim g f : (h : ∥ X ∥) → P h
>>
>> The computation rule:
>>
>> elim g f ∣ x ∣ = f x
>>
>> Thus this is a bracket type that allows us to get out of it,
>> provided
>> the target has at most one element (is an hproposition).
>>
>> Here is the tentative implementation:
>>
>> \begin{code}
>>
>> module hpropositionalTruncationTentat**__ive where
>>
>> private
>> postulate Level : Set
>> postulate zero : Level
>> postulate suc : Level → Level
>>
>> {-# BUILTIN LEVEL Level #-}
>> {-# BUILTIN LEVELZERO zero #-}
>> {-# BUILTIN LEVELSUC suc #-}
>>
>> data _≡_ {ℓ} {X : Set ℓ} (x : X) : X → Set ℓ where
>> refl : x ≡ x
>>
>> {-# BUILTIN EQUALITY _≡_ #-}
>> {-# BUILTIN REFL refl #-}
>>
>> \end{code}
>>
>> This is unsound, but we try to use it to perform a sound
>> construction:
>>
>> \begin{code}
>>
>> private
>> primitive
>> primTrustMe : ∀{ℓ} {X : Set ℓ} {x y : X} → x ≡ y
>>
>> \end{code}
>>
>> Notice that we keep the above private to the module, so that
>> the
>> unsoundness doesn't leak to modules that use this module but
>> no
>> unsound Agda features.
>>
>> The first part is Dan Licata's trick. We implement the
>> hpropositional
>> truncation of ∥ X ∥ as X itself, or rather its isomorphic
>> copy ∥ X
>> ∥',
>> which is kept private to the module:
>>
>> \begin{code}
>>
>> private
>> data ∥_∥' (X : Set) : Set where
>> ∣_∣' : X → ∥ X ∥'
>>
>> ∥_∥ : Set → Set
>> ∥_∥ = ∥_∥'
>>
>> ∣_∣ : {X : Set} → X → ∥ X ∥
>> ∣_∣ = ∣_∣'
>>
>> hprop : Set → Set
>> hprop X = (x y : X) → x ≡ y
>>
>> truncation-rec : {X P : Set} → hprop P → (X → P) → ∥ X ∥ → P
>> truncation-rec _ f ∣ x ∣' = f x
>>
>> truncation-ind : {X : Set} {P : ∥ X ∥ → Set} → ((h : ∥ X ∥)
>> → hprop(P h)) → ((x : X) → P ∣ x ∣) → (h : ∥
>> X
>> ∥) → P h
>> truncation-ind _ f ∣ x ∣' = f x
>>
>> \end{code}
>>
>> The above -rec and -ind are the non-dependent and dependent
>> elimination rules respectively.
>>
>> The crucial requirement is that ∥ X ∥ is to be an
>> hproposition. We can
>> achieve this with a postulate, but postulates don't compute.
>> To try to
>> get an implementation that fully computes, we privately use
>> the above
>> generally unsound feature:
>>
>> \begin{code}
>>
>> truncation-is-hprop : {X : Set} → hprop ∥ X ∥
>> truncation-is-hprop _ _ = primTrustMe
>>
>> \end{code}
>>
>> Is that sound? The semantics of primTrustMe is not clearly
>> given in
>> the documentation.
>>
>> NB. Of course, we can make one parameter of the elimination
>> rule
>> computationally irrelevant:
>>
>> \begin{code}
>>
>> Truncation-elim' : {X P : Set} → .(hprop P) → (X → P) → ∥ X ∥
>> → P
>> Truncation-elim' _ f ∣ x ∣' = f x
>>
>> Truncation-elim : {X : Set} {P : ∥ X ∥ → Set} → .((h : ∥ X ∥)
>> → hprop(P h)) → ((x : X) → P ∣ x ∣) → (h : ∥ X ∥) → P h
>> Truncation-elim _ f ∣ x ∣' = f x
>>
>> \end{code}
>> ______________________________**___________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se**>
>> https://lists.chalmers.se/__**mailman/listinfo/agda<https://lists.chalmers.se/__mailman/listinfo/agda>
>> <https://lists.chalmers.se/**mailman/listinfo/agda<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<https://lists.chalmers.se/__mailman/listinfo/agda>
>> <https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>> >
>>
>> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130606/b3d06097/attachment-0001.html
More information about the Agda
mailing list