<p dir="ltr">Are you planning to compile such code?<br>
It doesn't really seem safe to me to compile all truncation-is-hprop to refl, especially when combined with univalence.<br>
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.</p>
<p dir="ltr">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)</p>
<div class="gmail_quote">On Jun 6, 2013 8:35 AM, "Martin Escardo" <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Dan,<br>
<br>
On 05/06/13 17:41, Dan Licata wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
As far as I understand it,<br>
primTrustMe is a way of asserting an equality, which is slightly better<br>
than a postulate because when it has type x = x , it reduces to refl.<br>
</blockquote>
> [...]<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I would guess that what you'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) -> Id p refl<br>
<br>
will be propositionally true, (∥ X ∥ is an hprop, and therefore an<br>
hset).<br>
</blockquote>
<br>
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?<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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't see why that would go wrong.<br>
</blockquote>
<br>
I agree. But it would be nice to hear from those who designed and implemented the feature.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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>
</blockquote>
<br>
I agree too.<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">
-Dan<br>
<br>
On Jun05, Martin Escardo wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
On 05/06/13 03:12, Guillaume Brunerie wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I’m not sure I understand what you are trying to do.<br>
</blockquote>
<br>
I am trying to use an unsound Agda feature to implement a sound<br>
construction (hpropositional reflection or truncation).<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I don’t really know what primTrustMe is,<br>
</blockquote>
<br>
Me neither, and this is why I asked the question here. The<br>
documentation <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>
says:<br>
<br>
"Note that the compiler replaces all uses of primTrustMe with the<br>
REFL builtin, without any check for definitional equality. Incorrect<br>
uses of primTrustMe can potentially lead to segfaults or similar<br>
problems."<br>
<br>
However, It Doesn't say what the correct uses are meant to be.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
but it seems to be some kind of postulate that every type is an<br>
hprop, which seems much worse than just postulating that a single<br>
type is an hprop.<br>
</blockquote>
<br>
Yes, but notice that I use it privately, hopefully in a sound way.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
What are you trying to achieve exactly?<br>
</blockquote>
<br>
I am trying to (soundly) implement hpropositional truncation that<br>
computes, without *any* postulate at all.<br>
<br>
Voevodsky's Coq implementation uses type-in-type (also unsound in<br>
general, but backed by sound resizing axioms in this case) and<br>
additionally postulates the axiom of function extensionality 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 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 ∥ → 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, 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 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't leak to modules that use this module but no<br>
unsound Agda features.<br>
<br>
The first part is Dan Licata's trick. We implement the hpropositional<br>
truncation of ∥ X ∥ as X itself, or rather its isomorphic copy ∥ X<br>
∥',<br>
which is kept private to the module:<br>
<br>
\begin{code}<br>
<br>
private<br>
data ∥_∥' (X : Set) : Set where<br>
∣_∣' : X → ∥ X ∥'<br>
<br>
∥_∥ : Set → Set<br>
∥_∥ = ∥_∥'<br>
<br>
∣_∣ : {X : Set} → X → ∥ X ∥<br>
∣_∣ = ∣_∣'<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 ∣' = 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 ∣' = 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 hproposition. We can<br>
achieve this with a postulate, but postulates don't compute. To try to<br>
get an implementation that fully computes, we privately use 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 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' : {X P : Set} → .(hprop P) → (X → P) → ∥ X ∥<br>
→ P<br>
Truncation-elim' _ f ∣ x ∣' = 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 ∣' = 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><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote>
<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>