[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## Re: Axiom musings ... runtime computation of first-class dependent types

**From**: |
Martin Baker |

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

**Date**: |
Mon, 30 May 2022 11:19:47 +0100 |

**User-agent**: |
Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.9.0 |

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