[Agda] Trust me regarding Dan Licata's trick

[Dan Licata]

Hi Martin,

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've seen it used in conjunction with builtin types like strings.  For
example, there is a 

primitive
  primStringEquality : String -> String -> Sums.Bool

But now, say you want to give this a fancier type:

equal/id : (x y : String) -> Sums.Maybe (Id x y)
equal/id s1 s2 with (primStringEquality s1 s2)
... | Sums.True  = Sums.Some ?
... | Sums.False = Sums.None 

There's no primitive certification for primStringEquality, so you'd have
to fill the ? with a postulate (at least there wasn't when I stole this
code from Nisse's library a few years ago).  

But then you can get into trouble because, when you call equal/id on
two concrete strings, it reduces to a postulate, so transport/etc. get
stuck.  I think I ran into this when trying to do some reflective
theorem proving: you would like that
equal/id "HR" "HR" |-> Some refl  
but it reduces to Some <a postulate>, so despite everything being
closed, things don't compute.


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). 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. 

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.  

-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