[Agda] Dependent Types at Work

[Tristan Wibberley]

On Wed, 2008-03-12 at 11:27 +0100, Peter Dybjer wrote:
> Ana Bove and I have written a tutorial on dependently typed programming in
> Agda:
> 
> http://www.cs.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf
> 
> It is not self-contained and only deals with some of the features of Agda.
> But it may serve as a complement to other documentation, especially for
> people with little previous experience of dependent types.

I'm just studying agda2 now as I find the dependently typed language
idea very interesting.

I'm reading this document as it is the best material I've found on the
subject but there is one thing in particular lacking. One of the first
exercises is to write a subtraction function and refers to "cut-off"
which makes sense (it is only defined for first arguments greater in
value than or equal in value to the second argument). However, I can't
find any hints on how to achieve that effect.

I imagine that the subtraction function will require an implicit
argument first to introduce names of types and values that are deduced
based on the second argument and used in the first argument, but I can't
figure out how to define a small type that has all the values of Nat
that are greater than or equal to the value of the second argument (I
think that is the approach to take).

I think I have found a hint to this way down on page 17 on data _==_:

"This type tells us when two elements in a set A are equal. Not
surprisingly, it also tells us that we can only constructs proofs that
an element is equal to itself!"

But I can't fathom how to use that knowledge.


I think this example is right to be near the top since it really
showcases what dependently typed languages are good for, but it needs
this technique to be covered first.

If somebody can explain this technique, I can be a guinea pig for
whatever text needs to be added :)

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