[Agda] Trust me regarding Dan Licata's trick

Martin Escardo m.escardo at cs.bham.ac.uk
Thu Jun 6 20:20:38 CEST 2013



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>> 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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>


More information about the Agda mailing list