[Agda] Inspect on steroids

[Ulf Norell]

{-

Complete Agda module follows:

The with construct can be a bit tricky at times. There is the inspect idiom
that
you can use, but the problem with that is that you can choose to abstract
using
with a normal with, or you can use inspect to get the equation, but you
can't
have both.

Enter: Inspect on Steroids.

-}

module InspectOnSteroids where

-- Some preliminaries

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Unit : Set where
  unit : Unit

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

-- The key to steroid-infused inspect is being able to hide terms from the
evil with-abstraction monster.

-- The type of hidden terms.
Hidden : Set → Set
Hidden A = Unit → A

-- We can hide a function application
hide : {A : Set}{B : A → Set} (f : (x : A) → B x) (x : A) → Hidden (B x)
hide f x unit = f x

-- Revealing a hidden argument is easy.
reveal : {A : Set} → Hidden A → A
reveal f = f unit

-- Inspect on steroids relates hidden values and the corresponding
-- revealed values.
-- (I'm resisting the temptation to call it reveal_is_).

data Inspect {A : Set}(x : Hidden A)(y : A) : Set where
  it : reveal x ≡ y → Inspect x y

-- It's easy to show that revealing x gives you reveal x:
inspect : {A : Set}(x : Hidden A) → Inspect x (reveal x)
inspect f = it refl

-- Now to use it simply abstract over both the actual term and inspect of
the hidden term:

postulate
  T : Nat → Set

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

-- In the hole we have
-- Goal : T z
-- fx=z : f x ≡ z

-- / Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110910/1716f53d/attachment.html