[Agda] Strange normalization

[Ulf Norell]

On Mon, Sep 29, 2008 at 11:35 AM, Sam Staton <ss368 at cam.ac.uk> wrote:

> Hello.
>
> Agda seems to normalize parameters to data types, to an excessive degree.
> See, for instance, the code below. I didn't expect this code to loop off
> forever, but it does.
>
> Is this a feature? I have found it annoying. (I'm just getting the hang of
> Agda, and I'm not a Haskell expert, so I apologize if the question is
> naive.) Best regards, Sam
>
>  bomb : Nat
>  bomb = ack (succ (succ (succ (succ zero)))) (succ (succ zero))
>
>  data D (f : Unit -> Nat) : Set where
>    d : D f
>
>  f : Unit -> Nat
>  f r = bomb
> --  f r = zero
>
>  T : Set
>  T = D f
>
> -- everything is fine if you comment out the following lines.
>  explode : T
>  explode = d


Checking type equality amounts to (a bit simplified) comparing the normal
forms of the two types. To check explode the type checker needs to check T =
D f, and the normal form of both sides is D (\r -> succ (...... (succ zero)
..... )), for a significant number of dots.

If you change the definition of f to match on its argument:

f : Unit -> Nat
f unit = bomb

the normal form of f will be \r -> f r (since there is no eta equality on
the Unit type) and checking explode will go through.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080929/293ea181/attachment.html