[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

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
>> 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 hpropositionalTruncationTentative 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
>> https://lists.chalmers.se/mailman/listinfo/agda
>