[Agda] Trust me regarding Dan Licata's trick
Martin Escardo
m.escardo at cs.bham.ac.uk
Fri Jun 7 10:42:44 CEST 2013
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.
> 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).
Anyway, if trustMe does work as a postulate as claimed earlier, why is
it needed/useful at all?
Martin
>
> 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
> http://code.haskell.org/Agda/____doc/release-notes/2-2-6.txt
> <http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt>
>
> <http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt
> <http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt>>
> 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>
>
More information about the Agda
mailing list