<p dir="ltr">But primTrustMe only computes when the endpoints are definitionally equal. If they are not then the term is stuck just as any other postulate.<br>
primTrustMe is not much better than a postulate when it comes to canonicity.</p>
<p dir="ltr">For instance consider T the hprop-truncation of bool, P the constant fibration over T with fiber Nat, and consider the closed term:<br>
transport P (truncation-is-hprop true false) 0</p>
<p dir="ltr">This is a natural number which should normalise to 0 if you have canonicity, but it doesn&#39;t, even if you use primTrustMe.<br>
(on the other hand if you *compile* it, then it will compute to 0, but combining that with univalence you can easily get a segfault)</p>
<div class="gmail_quote">On Jun 6, 2013 3:20 PM, &quot;Martin Escardo&quot; &lt;<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>&gt; wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
<br>
On 06/06/13 16:16, Guillaume Brunerie wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Are you planning to compile such code?<br>
</blockquote>
<br>
Not necessarily, but I want to normalize closed terms of e.g. natural number type.<br>
<br>
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).<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
It doesn&#39;t really seem safe to me to compile all truncation-is-hprop to<br>
refl, especially when combined with univalence.<br>
As far as I understand, it only affects the compiler (not the<br>
normalisation procedure in the type checker), so maybe it&#39;s safe if you<br>
just want to type-check code.<br>
</blockquote>
<br>
If I wanted to just type check, then postulates would be enough.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
For the interval, given that the two endpoints are not definitionally<br>
equal, I don&#39;t think there is any difference with the version using a<br>
postulate (unless you compile the code, in which case strange things<br>
might happen)<br>
</blockquote>
<br>
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.<br>

<br>
Best,<br>
Martin<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
On Jun 6, 2013 8:35 AM, &quot;Martin Escardo&quot; &lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a><br>
&lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;&gt; wrote:<br>
<br>
    Hi Dan,<br>
<br>
    On 05/06/13 17:41, Dan Licata wrote:<br>
<br>
        As far as I understand it,<br>
        primTrustMe is a way of asserting an equality, which is slightly<br>
        better<br>
        than a postulate because when it has type x = x , it reduces to<br>
        refl.<br>
<br>
     &gt; [...]<br>
<br>
        I would guess that what you&#39;re doing below is OK:  For the usual<br>
        definition of ∥ X ∥ as a higher inductive type,<br>
<br>
        (x : ∥ X ∥) (p : Id x x) -&gt; Id p refl<br>
<br>
        will be propositionally true, (∥ X ∥ is an hprop, and therefore an<br>
        hset).<br>
<br>
<br>
    Yes, that&#39;s precisely my intuition. But this intuition would work<br>
    for the interval too, because it is an hprop and hence an hset, but<br>
    I don&#39;t think this trick would work for the interval. Or would it?<br>
<br>
        Using primTrustMe will strictify certain instances of this (the<br>
        ones where p is constructed by applying truncation-is-hprop to<br>
        definitionally equal arguments) to definitional equalities.  Off the<br>
        top of my head, I don&#39;t see why that would go wrong.<br>
<br>
<br>
    I agree. But it would be nice to hear from those who designed and<br>
    implemented the feature.<br>
<br>
        On the other hand, using primTrustMe to implement the circle or<br>
        something like that would be bad: if loop : Id{S1} base base<br>
        is defined to be primTrustMe, it will reduce to refl.<br>
<br>
<br>
    I agree too.<br>
<br>
    Best,<br>
    Martin<br>
<br>
<br>
        -Dan<br>
<br>
        On Jun05, Martin Escardo wrote:<br>
<br>
<br>
            On 05/06/13 03:12, Guillaume Brunerie wrote:<br>
<br>
                I’m not sure I understand what you are trying to do.<br>
<br>
<br>
            I am trying to use an unsound Agda feature to implement a sound<br>
            construction (hpropositional reflection or truncation).<br>
<br>
                I don’t really know what primTrustMe is,<br>
<br>
<br>
            Me neither, and this is why I asked the question here. The<br>
            documentation<br>
            <a href="http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt" target="_blank">http://code.haskell.org/Agda/_<u></u>_doc/release-notes/2-2-6.txt</a><br>
            &lt;<a href="http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt" target="_blank">http://code.haskell.org/Agda/<u></u>doc/release-notes/2-2-6.txt</a>&gt;<br>
            says:<br>
<br>
                &quot;Note that the compiler replaces all uses of primTrustMe<br>
            with the<br>
                REFL builtin, without any check for definitional<br>
            equality. Incorrect<br>
                uses of primTrustMe can potentially lead to segfaults or<br>
            similar<br>
                problems.&quot;<br>
<br>
            However, It Doesn&#39;t say what the correct uses are meant to be.<br>
<br>
                but it seems to be some kind of postulate that every<br>
                type is an<br>
                hprop, which seems much worse than just postulating that<br>
                a single<br>
                type is an hprop.<br>
<br>
<br>
            Yes, but notice that I use it privately, hopefully in a<br>
            sound way.<br>
<br>
                What are you trying to achieve exactly?<br>
<br>
<br>
            I am trying to (soundly) implement hpropositional truncation<br>
            that<br>
            computes, without *any* postulate at all.<br>
<br>
            Voevodsky&#39;s Coq implementation uses type-in-type (also<br>
            unsound in<br>
            general, but backed by sound resizing axioms in this case) and<br>
            additionally postulates the axiom of function extensionality<br>
            to show<br>
            that the truncation really is an hproposition.<br>
<br>
            Here is an improved version of what I sent yesterday, with more<br>
            explanations, and the main question repeated.<br>
<br>
            Best,<br>
            Martin<br>
            ------------------------------<u></u>__----------------------------<u></u>--__-------<br>
            Here is what we want to achieve:<br>
<br>
            Given a type X, we want to construct a type ∥ X ∥:<br>
<br>
                         X type<br>
                       ----------<br>
                        ∥ X ∥ type<br>
<br>
            We want any two elements of ∥ X ∥ to be propositionally<br>
            equal, written<br>
            hprop ∥ X ∥.<br>
<br>
            We have the introduction rule:<br>
<br>
                             x : X<br>
                        ---------------<br>
                          ∣ x ∣ :  ∥ X ∥<br>
<br>
            The elimination rule or induction principle, for any P : ∥ X<br>
            ∥ → Set:<br>
<br>
                   g : (h : ∥ X ∥) → hprop(P h)  f : ((x : X) → P ∣ x ∣)<br>
                 ------------------------------<u></u>__------------------------<br>
                         elim g f : (h : ∥ X ∥) → P h<br>
<br>
            The computation rule:<br>
<br>
                   elim g f ∣ x ∣ = f x<br>
<br>
            Thus this is a bracket type that allows us to get out of it,<br>
            provided<br>
            the target has at most one element (is an hproposition).<br>
<br>
            Here is the tentative implementation:<br>
<br>
            \begin{code}<br>
<br>
            module hpropositionalTruncationTentat<u></u>__ive where<br>
<br>
            private<br>
               postulate Level : Set<br>
               postulate zero : Level<br>
               postulate suc  : Level → Level<br>
<br>
            {-# BUILTIN LEVEL     Level #-}<br>
            {-# BUILTIN LEVELZERO zero  #-}<br>
            {-# BUILTIN LEVELSUC  suc   #-}<br>
<br>
            data _≡_ {ℓ} {X : Set ℓ} (x : X) : X → Set ℓ where<br>
                refl : x ≡ x<br>
<br>
            {-# BUILTIN EQUALITY _≡_  #-}<br>
            {-# BUILTIN REFL     refl #-}<br>
<br>
            \end{code}<br>
<br>
            This is unsound, but we try to use it to perform a sound<br>
            construction:<br>
<br>
            \begin{code}<br>
<br>
            private<br>
               primitive<br>
                 primTrustMe : ∀{ℓ} {X : Set ℓ} {x y : X} → x ≡ y<br>
<br>
            \end{code}<br>
<br>
            Notice that we keep the above private to the module, so that the<br>
            unsoundness doesn&#39;t leak to modules that use this module but no<br>
            unsound Agda features.<br>
<br>
            The first part is Dan Licata&#39;s trick. We implement the<br>
            hpropositional<br>
            truncation of ∥ X ∥ as X itself, or rather its isomorphic<br>
            copy ∥ X<br>
            ∥&#39;,<br>
            which is kept private to the module:<br>
<br>
            \begin{code}<br>
<br>
            private<br>
                data ∥_∥&#39; (X : Set) : Set where<br>
                  ∣_∣&#39; : X → ∥ X ∥&#39;<br>
<br>
            ∥_∥ : Set → Set<br>
            ∥_∥ = ∥_∥&#39;<br>
<br>
            ∣_∣ : {X : Set} → X → ∥ X ∥<br>
            ∣_∣ = ∣_∣&#39;<br>
<br>
            hprop : Set → Set<br>
            hprop X = (x y : X) → x ≡ y<br>
<br>
            truncation-rec : {X P : Set} → hprop P → (X → P) → ∥ X ∥ → P<br>
            truncation-rec _ f ∣ x ∣&#39; = f x<br>
<br>
            truncation-ind : {X : Set} {P : ∥ X ∥ → Set} → ((h : ∥ X ∥)<br>
                             → hprop(P h)) → ((x : X) → P ∣ x ∣) → (h : ∥ X<br>
            ∥) → P h<br>
            truncation-ind _ f ∣ x ∣&#39; = f x<br>
<br>
            \end{code}<br>
<br>
            The above -rec and -ind are the non-dependent and dependent<br>
            elimination rules respectively.<br>
<br>
            The crucial requirement is that ∥ X ∥ is to be an<br>
            hproposition. We can<br>
            achieve this with a postulate, but postulates don&#39;t compute.<br>
            To try to<br>
            get an implementation that fully computes, we privately use<br>
            the above<br>
            generally unsound feature:<br>
<br>
            \begin{code}<br>
<br>
            truncation-is-hprop : {X : Set} → hprop ∥ X ∥<br>
            truncation-is-hprop _ _ = primTrustMe<br>
<br>
            \end{code}<br>
<br>
            Is that sound? The semantics of primTrustMe is not clearly<br>
            given in<br>
            the documentation.<br>
<br>
            NB. Of course, we can make one parameter of the elimination rule<br>
            computationally irrelevant:<br>
<br>
            \begin{code}<br>
<br>
            Truncation-elim&#39; : {X P : Set} → .(hprop P) → (X → P) → ∥ X ∥<br>
            → P<br>
            Truncation-elim&#39; _ f ∣ x ∣&#39; = f x<br>
<br>
            Truncation-elim : {X : Set} {P : ∥ X ∥ → Set} → .((h : ∥ X ∥)<br>
            → hprop(P h)) → ((x : X) → P ∣ x ∣) → (h : ∥ X ∥) → P h<br>
            Truncation-elim _ f ∣ x ∣&#39; = f x<br>
<br>
            \end{code}<br>
            ______________________________<u></u>___________________<br>
            Agda mailing list<br>
            <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
            <a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
            &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>&gt;<br>
<br>
<br>
    ______________________________<u></u>___________________<br>
    Agda mailing list<br>
    <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
    <a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
    &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>&gt;<br>
<br>
</blockquote>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div>