[Agda] Inspect.

[flicky frans]

An example, taken from the original post about inspect on steroids
[1], works well:

    open import Level
    open import Relation.Binary.PropositionalEquality as P hiding (inspect)

    record Reveal_·_is_ {α β} {A : Set α} {B : A -> Set β}
      (f : (x : A) -> B x) (x : A) (y : B x) : Set (α ⊔ β) where
        constructor [_]
        field eq : f x ≡ y

    inspect : ∀ {α β} {A : Set α} {B : A -> Set β}
            -> (f : (x : A) -> B x) -> (x : A) -> Reveal f · x is f x
    inspect f x = [ refl ]

    postulate
      Nat : Set
      T : Nat → Set

    foo : (f : Nat → Nat)(x : Nat) → T (f x)
    foo f x with f x | inspect f x
    foo f x | z | [ fx=z ] = {!!}

``fx=z'' is of type ``f x ≡ z''. When I'm using the ``inspect'' from
the standard library

    foo : (f : Nat → Nat)(x : Nat) → T (f x)
    foo f x with f x | P.inspect f x
    foo f x | z | [ fx=z ] = {!!}

I get

    fx=z : .Data.Unit.Core.reveal (.Data.Unit.Core.hide f x) ≡ z

Or with opened Data.Unit.Core

    fx=z : reveal (hide f x) ≡ z

Which is beta-equal to ``f x ≡ z'', but looks somewhat confusing.

I didn't test this new ``inspect'' properly, because I don't actually
know, what other properties it must have besides hiding a function
application.

Am I right in thinking, that unification works as follows?

When you pattern-match like this:

    ... with f x | inspect f x
    ... | y | [ p ] = {!!}

Agda replaces all occurrences of ``f x'' with ``y'' in the context and
in the type of ``inspect f x'', which is ``Reveal f · x is f x'', so
the type becomes ``Reveal f · x is y''. Then you pattern-match on
``inspect f x'' and get ``p : f x ≡ y''.

[1] http://comments.gmane.org/gmane.comp.lang.agda/3125

2014-12-29 13:41 GMT+03:00, Andreas Abel <andreas.abel at ifi.lmu.de>:
> Frankly, I do not know.  We could replace the current definition by your
> simplification, provided that both work equally well wrt. unification.
> Did you do the experiments?
>
> Cheers,
> Andreas
>
> On 27.12.2014 17:52, flicky frans wrote:
>> Hello. I am probably missing something obvious, but why `inspect' is
>> not defined like this?
>>
>> record Reveal_·_is_ {α β} {A : Set α} {B : A -> Set β}
>>    (f : (x : A) -> B x) (x : A) (y : B x) : Set (α ⊔ β) where
>>      constructor [_]
>>      field eq : f x ≡ y
>>
>> inspect : ∀ {α β} {A : Set α} {B : A -> Set β}
>>          -> (f : (x : A) -> B x) -> (x : A) -> Reveal f · x is f x
>> inspect f x = [ refl ]
>>
>> This looks simpler and still allows you to pattern-match on (f x) and
>> to remember, that (f x ≡ y).
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>