# [Agda] Trust me regarding Dan Licata's trick

Guillaume Brunerie guillaume.brunerie at gmail.com
Fri Jun 7 14:00:31 CEST 2013

On Jun 7, 2013 5:40 AM, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:
>
>
>
> On 06/06/13 19:57, Guillaume Brunerie wrote:
>>
>> This is a natural number which should normalise to 0 if you have
>> canonicity, but it doesn't, even if you use primTrustMe.
>> (on the other hand if you *compile* it, then it will compute to 0,
>
>
> It is a bit disturbing that the normalization for type checking is
different from the normalization given by compilation for running terms.

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.

>> but
>> combining that with univalence you can easily get a segfault)
>
>
> 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).

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.

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.

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.
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.
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.

> Anyway, if trustMe does work as a postulate as claimed earlier, why is it
needed/useful at all?

My impression is that it can be used to get some unsafe coercion between
arbitrary types, like Obj.magic in OCaml.

Guillaume

>> On Jun 6, 2013 3:20 PM, "Martin Escardo" <m.escardo at cs.bham.ac.uk
>> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>>
>>
>>
>>     On 06/06/13 16:16, Guillaume Brunerie wrote:
>>
>>         Are you planning to compile such code?
>>
>>
>>     Not necessarily, but I want to normalize closed terms of e.g.
>>     natural number type.
>>
>>     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).
>>
>>         It doesn't really seem safe to me to compile all
>>         truncation-is-hprop to
>>         refl, especially when combined with univalence.
>>         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.
>>
>>
>>     If I wanted to just type check, then postulates would be enough.
>>
>>         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)
>>
>>
>>     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.
>>
>>     Best,
>>     Martin
>>
>>
>>
>>         On Jun 6, 2013 8:35 AM, "Martin Escardo"
>>         <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>
>>         <mailto:m.escardo at cs.bham.ac.__uk
>>
>>         <mailto:m.escardo at cs.bham.ac.uk>>> wrote:
>>
>>              Hi Dan,
>>
>>              On 05/06/13 17:41, Dan Licata wrote:
>>
>>                  As far as I understand it,
>>                  primTrustMe is a way of asserting an equality, which is
>>         slightly
>>                  better
>>                  than a postulate because when it has type x = x , it
>>         reduces to
>>                  refl.
>>
>>               > [...]
>>
>>                  I would guess that what you're doing below is OK:  For
>>         the usual
>>                  definition of ∥ X ∥ as a higher inductive type,
>>
>>                  (x : ∥ X ∥) (p : Id x x) -> Id p refl
>>
>>                  will be propositionally true, (∥ X ∥ is an hprop, and
>>         therefore an
>>                  hset).
>>
>>
>>              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?
>>
>>                  Using primTrustMe will strictify certain instances of
>>         this (the
>>                  ones where p is constructed by applying
>>         truncation-is-hprop to
>>                  definitionally equal arguments) to definitional
>>         equalities.  Off the
>>                  top of my head, I don't see why that would go wrong.
>>
>>
>>              I agree. But it would be nice to hear from those who
>>         designed and
>>              implemented the feature.
>>
>>                  On the other hand, using primTrustMe to implement the
>>         circle or
>>                  something like that would be bad: if loop : Id{S1} base
>>         base
>>                  is defined to be primTrustMe, it will reduce to refl.
>>
>>
>>              I agree too.
>>
>>              Best,
>>              Martin
>>
>>
>>                  -Dan
>>
>>                  On Jun05, Martin Escardo wrote:
>>
>>
>>                      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
>>
>>
>>                      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 hpropositionalTruncationTentat____ive 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}
>>                      ___________________________________________________
>>
>>                      Agda mailing list
>>         Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>
>>         https://lists.chalmers.se/____mailman/listinfo/agda
>>         <https://lists.chalmers.se/__mailman/listinfo/agda>
>>                      <https://lists.chalmers.se/__mailman/listinfo/agda
>>         <https://lists.chalmers.se/mailman/listinfo/agda>>
>>
>>
>>              ___________________________________________________
>>
>>              Agda mailing list
>>         Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>
>>         https://lists.chalmers.se/____mailman/listinfo/agda
>>         <https://lists.chalmers.se/__mailman/listinfo/agda>
>>
>>              <https://lists.chalmers.se/__mailman/listinfo/agda
>>         <https://lists.chalmers.se/mailman/listinfo/agda>>
>>
>>     _________________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/__mailman/listinfo/agda
>>     <https://lists.chalmers.se/mailman/listinfo/agda>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130607/4010f138/attachment-0001.html