[Agda] Strange normalization

[Conor McBride]

Hi all

Sam wrote:

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

Ulf wrote:

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

I guess there are two issues here. One is how to make a
delay that actually delays. This example is a good reminder
of why one might want a unit type without an eta-law. We do
need to manage the intensional properties of our programs,
and more computation is not always better.

The other issue is the pragmatic one of how much cleverness
to spend on spotting the equality of non-normal forms. This
also splits into at least two questions.
   Design: should the static semantics ever depend on distinctions
     between definitionally equal terms?
   Implementation: should the implementation exploit distinctions
     between definitionally equal terms?

As far as the design question is concerned, I think not. Why
should terms which mean the same be treated differently?
But the more tactic-based systems, and Coq in particular,
seem to take another view. Massaging the definitional form of
a goal is often crucial to the applicability of tactics.

 From an implementation perpective, I've never felt embarrassed
about taking a long time to check that refl : ack 4 2 == ack 4 2
but I'm a bit bothered by refl : bomb == bomb. Definition is at
least one way the user can help us by pointing out sharing, and
it seems a shame to ignore it. On the other hand, one could
argue that /abstraction/ is really the right tool here, if it
only matters that bomb is bomb, and never that bomb is ack 4 2
in particular. We should not complain if the computer does as it
is told, but we should complain if we do not have language to
tell it better.

In that sense, examples like bomb are not the ones which convince
me that non-canonical sensitivity should be top priority. I get
more concerned by the issues like whether types should be
compared nominally or structurally. Even in a structural system
(perhaps one where types are given as codes in a universe), it
would be nice to have a cheap nominal comparison, sound but not
complete for the structural one.

If you implement in a lazy language, it's really convenient to
keep types in normal form, so you can just pattern match on them
directly, eg, to check for being (x : S) -> T. That's not to say
it's a bad idea to keep other labels as annotations on normal
forms, or to keep normal forms glued to other non-normal
representations of the same object (eg, definitions which have
been expanded on the way).

So this is a tricky issue. It would be really useful to collect
and analyse examples where equality works too hard despite our
best efforts to point out a coincidence. Premature optimization
considered harmful. But it's worth thinking about. Thanks, Sam.

All the best

Conor