[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

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}