[Agda] Dependent Types at Work

[Tristan Wibberley]

On Thu, 2008-03-20 at 18:29 -0400, Dan Licata wrote:

[snip]

> Instead of saying
> 
>   subtraction is only defined for first arguments greater in
>   value than or equal in value to the second argument
> say
> 
>   subtraction is only defined for second arguments less in
>   value than or equal in value to the first argument

Oh yeah! :) That would be easier.

[snip]

>   data NatLTE : Nat -> Set where
>     lzero : {n : Nat} -> NatLTE n
>     lsucc : {n : Nat} -> NatLTE n -> NatLTE (S n)
> 
> You may want to compare this type NatLTE with the type Fin n on page 15.

[snip]

> Does that help?


Yeah, I actually looked at that first, but I didn't think of deduction
of the Nat that makes a NatLTE so I was thinking callers would have to
conjecture that NatLTE held for the two arguments and I gave it up as a
bad job. BTW, is there a word like "callers" for "proofs that use a
proof" instead of the old "functions that use a function"?
"Conjecturers" is a little unwieldy :)

I think this method of "implicit conversion" based on the truth of a
proposition should be introduced explicitly before the subtraction
exercise.

After reading further, I can understand this when shown it - but for a
newbie to the language it would save a lot of pain to say "This is how
you define functions only where the values of its arguments meet certain
requirements".

Thanks for the help
-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.