<p dir="ltr"><br>
On Jun 7, 2013 5:40 AM, "Martin Escardo" <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br>
><br>
><br>
><br>
> On 06/06/13 19:57, Guillaume Brunerie wrote:<br>
>><br>
>> This is a natural number which should normalise to 0 if you have<br>
>> 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,<br>
><br>
><br>
> It is a bit disturbing that the normalization for type checking is different from the normalization given by compilation for running terms.</p>
<p dir="ltr">One difference between normalization and compilation is that when you run a program you are guaranteed to be in the empty context whereas normalization also happens in non empty contexts.</p>
<p dir="ltr">>> but<br>
>> combining that with univalence you can easily get a segfault)<br>
><br>
><br>
> I want to understand this more precisely, because univalence is compatible with hpropositional truncation. Perhaps you are just saying that we cannot have all points of the truncation to be definitionally equal under univalence: the type checking is right (because it doesn't believe me when I ask to be trusted), but the compilation is wrong (for univalent foundations).</p>
<p dir="ltr">Univalence is compatible with truncation but not with primTrustMe. PrimTrustMe is based on the fact that in the empty context the only proof of equality should be refl, which is not compatible with univalence.</p>
<p dir="ltr">Here is how I think you can get a segfault using the interval (I haven't managed to actually get the segfault because I don't understand how to compile an Agda program yet). You can probably adapt it to truncations if you want.</p>
<p dir="ltr">Assuming univalence, the types Unit and Unit -> Unit are equivalent. Hence there is a dependent type over I whose fiber over 0 is Unit and whose fiber over 1 is Unit -> Unit.<br>
Then you can take the canonical element tt of Unit, transport it along the path of the interval (so that you get a function of type Unit -> Unit) and apply it to tt.<br>
What I think will happen if you try to compile it is that the path of the interval will be compiled to refl, hence the transport is just the identity so the program will try to apply the "function" tt to the argument tt, which is obviously problematic.</p>
<p dir="ltr">> Anyway, if trustMe does work as a postulate as claimed earlier, why is it needed/useful at all?</p>
<p dir="ltr">My impression is that it can be used to get some unsafe coercion between arbitrary types, like Obj.magic in OCaml.</p>
<p dir="ltr">Guillaume</p>
<p dir="ltr">>> 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><br>
>> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>>> wrote:<br>
>><br>
>><br>
>><br>
>> On 06/06/13 16:16, Guillaume Brunerie wrote:<br>
>><br>
>> Are you planning to compile such code?<br>
>><br>
>><br>
>> Not necessarily, but I want to normalize closed terms of e.g.<br>
>> natural number type.<br>
>><br>
>> When I say that I want a definition that computes, I mean that the<br>
>> addition of this construction should preserve canonicity (say for<br>
>> closed terms of natural number type).<br>
>><br>
>> It doesn't really seem safe to me to compile all<br>
>> 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<br>
>> if you<br>
>> just want to type-check code.<br>
>><br>
>><br>
>> If I wanted to just type check, then postulates would be enough.<br>
>><br>
>> For the interval, given that the two endpoints are not<br>
>> definitionally<br>
>> equal, I don't think there is any difference with the version<br>
>> using a<br>
>> postulate (unless you compile the code, in which case strange things<br>
>> might happen)<br>
>><br>
>><br>
>> Well, I would be very surprised if it works, because the interval<br>
>> gives you functional extensionality, and it would be too easy to get<br>
>> that from data abstraction + primTrustMe in such a way that<br>
>> canonicity is preserved.<br>
>><br>
>> Best,<br>
>> Martin<br>
>><br>
>><br>
>><br>
>> On Jun 6, 2013 8:35 AM, "Martin Escardo"<br>
>> <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>><br>
>> <mailto:<a href="mailto:m.escardo@cs.bham.ac.">m.escardo@cs.bham.ac.</a>__uk<br>
>><br>
>> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.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<br>
>> slightly<br>
>> better<br>
>> than a postulate because when it has type x = x , it<br>
>> reduces to<br>
>> refl.<br>
>><br>
>> > [...]<br>
>><br>
>> I would guess that what you're doing below is OK: For<br>
>> 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<br>
>> therefore an<br>
>> hset).<br>
>><br>
>><br>
>> Yes, that's precisely my intuition. But this intuition<br>
>> would work<br>
>> for the interval too, because it is an hprop and hence an<br>
>> hset, but<br>
>> I don't think this trick would work for the interval. Or<br>
>> would it?<br>
>><br>
>> Using primTrustMe will strictify certain instances of<br>
>> this (the<br>
>> ones where p is constructed by applying<br>
>> truncation-is-hprop to<br>
>> definitionally equal arguments) to definitional<br>
>> 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<br>
>> designed and<br>
>> implemented the feature.<br>
>><br>
>> On the other hand, using primTrustMe to implement the<br>
>> circle or<br>
>> something like that would be bad: if loop : Id{S1} base<br>
>> 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<br>
>> to do.<br>
>><br>
>><br>
>> I am trying to use an unsound Agda feature to<br>
>> 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<br>
>> here. The<br>
>> documentation<br>
>> <a href="http://code.haskell.org/Agda/____doc/release-notes/2-2-6.txt">http://code.haskell.org/Agda/____doc/release-notes/2-2-6.txt</a><br>
>> <<a href="http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt">http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt</a>><br>
>><br>
>><br>
>> <<a href="http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt">http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt</a><br>
>> <<a href="http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt">http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt</a>>><br>
>> says:<br>
>><br>
>> "Note that the compiler replaces all uses of<br>
>> primTrustMe<br>
>> with the<br>
>> REFL builtin, without any check for definitional<br>
>> equality. Incorrect<br>
>> uses of primTrustMe can potentially lead to<br>
>> segfaults or<br>
>> similar<br>
>> problems."<br>
>><br>
>> However, It Doesn't say what the correct uses are<br>
>> meant to be.<br>
>><br>
>> but it seems to be some kind of postulate that<br>
>> every<br>
>> type is an<br>
>> hprop, which seems much worse than just<br>
>> 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<br>
>> 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<br>
>> this case) and<br>
>> additionally postulates the axiom of function<br>
>> extensionality<br>
>> to show<br>
>> that the truncation really is an hproposition.<br>
>><br>
>> Here is an improved version of what I sent<br>
>> yesterday, with more<br>
>> explanations, and the main question repeated.<br>
>><br>
>> Best,<br>
>> Martin<br>
>><br>
>> ------------------------------____----------------------------__--__-------<br>
>><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<br>
>> any P : ∥ X<br>
>> ∥ → Set:<br>
>><br>
>> g : (h : ∥ X ∥) → hprop(P h) f : ((x : X) →<br>
>> P ∣ x ∣)<br>
>><br>
>> ------------------------------____------------------------<br>
>><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<br>
>> out of it,<br>
>> provided<br>
>> the target has at most one element (is an<br>
>> hproposition).<br>
>><br>
>> Here is the tentative implementation:<br>
>><br>
>> \begin{code}<br>
>><br>
>> module hpropositionalTruncationTentat____ive where<br>
>><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<br>
>> 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<br>
>> module, so that the<br>
>> unsoundness doesn't leak to modules that use this<br>
>> 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<br>
>> 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) →<br>
>> ∥ X ∥ → P<br>
>> truncation-rec _ f ∣ x ∣' = f x<br>
>><br>
>> truncation-ind : {X : Set} {P : ∥ X ∥ → Set} → ((h<br>
>> : ∥ X ∥)<br>
>> → hprop(P h)) → ((x : X) → P ∣ x<br>
>> ∣) → (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<br>
>> 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<br>
>> compute.<br>
>> To try to<br>
>> get an implementation that fully computes, we<br>
>> 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<br>
>> clearly<br>
>> given in<br>
>> the documentation.<br>
>><br>
>> NB. Of course, we can make one parameter of the<br>
>> elimination rule<br>
>> computationally irrelevant:<br>
>><br>
>> \begin{code}<br>
>><br>
>> Truncation-elim' : {X P : Set} → .(hprop P) → (X →<br>
>> P) → ∥ X ∥<br>
>> → P<br>
>> Truncation-elim' _ f ∣ x ∣' = f x<br>
>><br>
>> Truncation-elim : {X : Set} {P : ∥ X ∥ → Set} →<br>
>> .((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>
>> ___________________________________________________<br>
>><br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>><br>
>> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>>__><br>
>> <a href="https://lists.chalmers.se/____mailman/listinfo/agda">https://lists.chalmers.se/____mailman/listinfo/agda</a><br>
>> <<a href="https://lists.chalmers.se/__mailman/listinfo/agda">https://lists.chalmers.se/__mailman/listinfo/agda</a>><br>
>> <<a href="https://lists.chalmers.se/__mailman/listinfo/agda">https://lists.chalmers.se/__mailman/listinfo/agda</a><br>
>> <<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>>><br>
>><br>
>><br>
>> ___________________________________________________<br>
>><br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>><br>
>> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>>__><br>
>> <a href="https://lists.chalmers.se/____mailman/listinfo/agda">https://lists.chalmers.se/____mailman/listinfo/agda</a><br>
>> <<a href="https://lists.chalmers.se/__mailman/listinfo/agda">https://lists.chalmers.se/__mailman/listinfo/agda</a>><br>
>><br>
>> <<a href="https://lists.chalmers.se/__mailman/listinfo/agda">https://lists.chalmers.se/__mailman/listinfo/agda</a><br>
>> <<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>>><br>
>><br>
>> _________________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>><br>
>> <a href="https://lists.chalmers.se/__mailman/listinfo/agda">https://lists.chalmers.se/__mailman/listinfo/agda</a><br>
>> <<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>><br>
>><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</p>