<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'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, "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">
<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'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'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'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, "Martin Escardo" <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a><br>
<mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>>> 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>
> [...]<br>
<br>
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>
<br>
<br>
Yes, that'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'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'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>
<<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<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."<br>
<br>
However, It Doesn'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'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'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<br>
hpropositional<br>
truncation of ∥ X ∥ as X itself, or rather its isomorphic<br>
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<br>
hproposition. We can<br>
achieve this with a postulate, but postulates don'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' : {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> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><br>
<br>
<br>
______________________________<u></u>___________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><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>