Re: Axiom musings ... runtime computation of first-class dependent types

[Martin Baker]

Tim,

Thanks for your reply, lots to think about in this subject isn't there.
Like you I'm attempting the daunting (but interesting) path of trying to 
understand this subject better.

> Dependent types allow functions to exist in the type definition. The
> functions can be executed "at run time". Current languages that have
> support for dependent types such as Agda and Idris use very, very
> limited forms of this facility. They only extend the type in certain
> carefully defined ways that allow the compiler to type check the code.

Yes, as you say, natural numbers (and related structures such as lists) 
have very nice properties. Idris does a good job of seamlessly 
converting between the Peano form (for proofs) and the usual form (for 
efficient algebra).

I like this idea that the representation holds the full information 
about the domain so its fully defined for proofs as well as holding the 
data for algebra.

As a thought experiment, I am trying to work out what it would take for 
this to be done on all mathematical structures.

As a first step, could this be extended to integers?

We could say that Integer = Nat+Nat. In spad terms that would be:
Rep := Union(negative : NNI, positive NNI)

Or Integer = 2*Nat. In spad terms that would be:
Rep := Record(sign : Bool, value NNI)

This would provide a structure to store an integer so it would work for 
the algebra but it doesn't seem to fully define an integer for proofs in 
that it doesn't glue the negative and positive Nats together. For that 
we seem to need equations like:

S (-1) = 0
P 0 = -1
S P = P S = Id

where:
S is successor
P is predecessor

As soon as we add equations to the representation then we loose some of 
the nice properties - more complexity - no canonical form.

At each step we seem to loose nice properties, when we get to fraction:

Rep:= Record(num:IntegralDomain, den:IntegralDomain)

Then we seem to need to need a normalisation algorithm to put in normal 
form so we can test for equality.

I still think there is something very powerful about combining algebra 
and proofs in this way so I would be interested to know if you have 
found a path through all this?

Martin