[Agda] Abstract blocks

[karim kanso]

Hi all,

Ive recently been playing about with abstract blocks and have identified
a behaviour that I did not expect.

Firstly, my understanding of definitions inside an abstract blocks is that
when used inside an abstract block they normalise/unfold, and outside of
abstract blocks they behave as postulates.

If a non-trivial type is defined as abstract, such as:

abstract
  F : ℕ → Set
  F 0 = ⊤
  F (suc n) = ⊤ × F n

and then used outside the block in function a definition:

Y : {n : ℕ} → (x : F n) → Set
Y _ = ⊤

or, concretely:

Z : F 1000 → Set
Z _ = ⊤

lemY : Y {n = 1000} ?
lemY = tt

lemZ : Z ?
lemZ = tt

These two final goals should have the type F 1000, and should not unfold F.
But they appear to see through abstract blocks when computing the their
types, and judging by the time taken to type-check these definitions
suggests that F is being normalised, although only one step reduction is
presented in the status window. I.e. after the file has type-checked it
will display the goals as (⊤ × F 999).

Notably, should I define:

abstract
  n1000 = 1000

postulate A : F n1000

The term: "Z A" is not accepted when manually checked by C-c,C-d; but is
accepted for the goals above.
e.g.
lemZ : Z A
lemZ = tt

Anyone know if this is this the intended behaviour, or confirm as a bug?

This occurs in the latest darcs version of Agda.


Thanks,
Karim Kanso
Swansea University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120107/d6bbc563/attachment-0001.html