[Agda] Trust me regarding Dan Licata's trick

[Guillaume Brunerie]

Are you planning to compile such code?
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.

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)
On Jun 6, 2013 8:35 AM, "Martin Escardo" <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>
>>> 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
>>> 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/ea05310a/attachment-0001.html