[Agda] Trust me regarding Dan Licata's trick
Martin Escardo
m.escardo at cs.bham.ac.uk
Fri Jun 7 22:19:00 CEST 2013
What is disturbing about hpropositional truncation is this:
We want the type (p q : || X ||) -> p == q to be inhabited, where "=="
is propositional equality.
But, if we take ||-|| as primitive, we don't want to have a constant for
that equality: how would we compute with it? What would J do to it?
So the easiest way out seems to add a rule to the theory extended with a
constructor ||-|| stipulating that all elements of ||X|| are
definitionally equal. You are saying that this way out is too
optimistic, as you would get, under univalence,
Unit = (Unit -> Unit)
definitionally, which doesn't sound right, and I agree.
So it seems that adding ||-|| as primitive poses the same problems as
adding functional extensionality or more generally univalence.
(Hence I take back my triviality hope of my previous message.)
You posit equalities that don't come from refl, and at the same time you
want to have J determined by its action on refl.
If not all points of ||X|| are definitionally equal, we are forced to
write equations for the postulated inhabitant of (p q : || X ||) -> p ==
q. I have no clue what they ought to be.
Best,
Martin
On 07/06/13 20:56, Guillaume Brunerie wrote:
> Do you also want the same elimination and computation rules as before?
> Again, that may be problematic when combined with univalence.
> Assuming univalence, the type Contr of small contractible types is a
> proposition.
> Hence you can define a map f from the truncation of Bool to
> Contr sending true to Unit and false to Unit -> Unit.
>
> Then, by the usual computation rule for truncation, you get f | true | =
> Unit.
> But | true | = | false |, hence
>
> Unit = f | true | = f | false | = Unit -> Unit
>
> (all equalities are definitional here).
>
> It's not a contradiction yet, but having Unit and Unit -> Unit
> definitionally equal is already quite strange.
> Guillaume
>
> On Jun 7, 2013 4:13 PM, "Martin Escardo" <m.escardo at cs.bham.ac.uk
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>
> Summary of discussion:
> ---------------------
>
> * primTrustMe doesn't do what I wanted.
>
> I wanted to identify all elements of any given type, definitionally,
> so as to get an Agda implementation of hpropositional truncation
> that fully computes, by replacing a postulate in Dan's trick with
> primTrustMe.
>
> For my purposes, I will use Dan's trick, as originally stated by
> him, with a postulate for identifying all points of || X ||.
>
> * Advantage (Dan's original point in
> http://homotopytypetheory.org/__2011/04/23/running-circles-__around-in-your-proof-__assistant/
> <http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/>):
>
>
> The elimination-rule equation for hpropositional truncation holds
> definitionally rather than just propositionally.
>
> This is precisely what I need to get my proofs accepted. (And what
> he and other people needed to get their proofs accepted in the
> presence of higher-inductive types (HIT's) for lines, circles,
> spheres etc.)
>
> * Disadvantage (again in Dan's original post):
>
> We lose canonicity if we use || - ||, because there is a
> postulate. (And we may gain SegFault if we attempt to fix this by
> using primTrustMe).
>
> I can live with that, using a postulate as Dan originally did,
> rather than my failed attempt with primTrustMe, waiting for the
> computational open problems in univalent foundations to be sorted
> out. primTrustMe can't solve them in this particular case, it seems.
>
> But I have the feeling that it should be trivial to extend Agda with
> a type constructor for hpropositional truncation so that canonicity
> is preserved (but primTrustMe doesn't seem to be the answer).
>
> Best,
> Martin
>
>
> On 07/06/13 13:00, Guillaume Brunerie wrote:
>
>
> On Jun 7, 2013 5:40 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:
> >
> >
> >
> > 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>
> <mailto: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>
> <mailto: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>>
> <mailto: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>>>
> >> <mailto:m.escardo at cs.bham.ac
> <mailto:m.escardo at cs.bham.ac>. <mailto:m.escardo at cs.bham.ac
> <mailto: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
> <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>>
> >>
> >>
> >>
> <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>__>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>>
> >> <mailto:Agda at lists.chalmers.se
> <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se
> <mailto:Agda at lists.chalmers.se>__>
> <mailto: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>>
> >>
> <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>__>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>>
> >> <mailto:Agda at lists.chalmers.se
> <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se
> <mailto:Agda at lists.chalmers.se>__>
> <mailto: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>>
> >>
> >>
> <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>__>
> <mailto: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>
>
> _________________________________________________
> 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