[Agda] Unexpected successful loading of silly program

[Ulf Norell]

On Tue, Mar 25, 2008 at 1:37 AM, Tristan Wibberley <tristan at wibberley.org>
wrote:

> Hi all,
>
> I changed the second clause of _-_ from:
>
> _-_ zero (succ n) {}
>
> to
>
> _-_ zero (succ n) = zero
>
> in this program:
>
>
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Patterns.PartialFunction
>
> however it then loaded successfully, furthermore, getting the canonical
> form for zero - (succ zero) gives zero but I would have expected it to
> fail. What does the {c : b ¿≤ℕ a} do exactly and why can I have an
> absurd case if the type of the function is total after all?
>

When you ask to evaluate an expression you're not told about any unsolved
metavariables in that expression (maybe you should be). In this case your
function reduces even though the proof argument is a metavariable (which can
never be solved). If you try to define

  test : N
  test = zero - succ zero

this becomes clear.

On a related note how do I add a proof to my program that a function is
> indeed partial to avoid errors which let it be total without noticing?
>

I'm not sure what you're after here. There is no distinction between partial
functions and total functions in Agda (in fact there are only total
functions). In this particular example I don't think there's a problem. The
only difference between the function with the extra right hand side and the
original one with an absurd pattern is that if you would happen to have a
proof of the appropriate false proposition then you can get the function to
reduce. For instance, you can prove that

lem : (p : succ zero =<N zero) -> _-_ zero (succ zero) {p} == zero
lem p = refl

This isn't terribly interesting because you can also prove

lem' : (p : succ zero =<N zero) -> {A : Set} -> A
lem' ()

BTW, how do you get unicode characters into the wiki in preformatted
> sections?


I think you have to type the character codes. The wiki is not very advanced.

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