[Agda] Inspect.

[Andreas Abel]

Your analysis is correct.

The way to proceed here would be

* check the standard library with your simplified Reveal
* check your own projects and maybe some others you get hold of
* submit a pull request to agda/agda-stdlib on github.

Thanks,
Andreas


On 29.12.2014 13:55, flicky frans wrote:
> 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/
>>


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