[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Axiom domains and Aldor return types
From: |
William Sit |
Subject: |
Re: [Axiom-developer] Axiom domains and Aldor return types |
Date: |
Fri, 14 Jan 2005 11:50:51 -0500 |
Stephen Wilson wrote:
> Lifting everything to the package level is an example of how one will
> rapidly diverge from the math. For example, what if instead of a
> functor `PPF(n:PositiveInteger)==PrimeField(n) with ...' we want
> something more general, like, say, given any commutative ring R and a
> maximal ideal M in R we want the quotient field R/M. In a package
> like:
>
> RESCLASS(R: CommutativeRing, M: MaximalIdeal(R)): Field with ...
>
> RESCLASS is going to need to know about *every* commutative ring in
> the algebra. If R is the integers, and M a prime < 2^32, then it needs
> to know the field can be represented as machine integers, for example.
>
> But with dependent typing one can achieve this generality, since the
> required function is a categorical export, which each individual
> domain satisfies in its own way. It becomes possible to write
> extraordinarily generic algorithms given such a language facility.
I am not following your example. RESCLASS is already a domain constructor and
dependent types for domain constructor is not a problem in Axiom. Since RESCLASS
is a categorical construct, the implementation must NOT know anything about R or
M other than that R is a commutative ring and M is a maximal ideal of R. (By
the way, MaximalIdeal(R) is also a categorical domain construction and I wonder
how one can characterize algorithmically the set of maximal ideals of an
arbitrary commutative ring.) For a specific ring, such as the Integers, yes, we
know, and there you can implement an efficient R/M if you also know that M <
2^32. But I do not follow how this has to do with signature issues.
> If you cant
> write foo(n:INT):PrimeField(n), then programmers will define functions
> like mod_+(arg1:INT,arg2:INT,modulus:INT):INT and throw away the
> mathematical meaning of their types. Might as well be programming in
> C ( almost :).
The solution I proposed in package FOO:
> --%Foo
> )abbrev package FOO Foo
> Foo(n:PositiveInteger, k:PositiveInteger):T==C where
> T == with
> point:()->PrimeField(n)
> C == add
> point()==k::Integer::PrimeField(n)
>
> -- After compiling, we can use
> --
> -- point()$Foo(n,k)
>
> )abbrev package BARTEST Bartest
> Bartest: T==C where
> T == with
> barrun: () -> Void
> C == add
> import FOO
> barrun() ==
> for k in 4..5 repeat
> for n in [1,2,4,6]::List PositiveInteger repeat
> print(point()$Foo(n+1,k)::OutputForm)$PrintPackage
does not sacrifice the mathematical type structure of the original example that
Martin proposed:
g(n:PositiveInteger, k:PositiveInteger):PrimeField(n)
It reflects exactly the same structure with the exception that there is no
signature used and g(n,k) is replaced by the longer name
point()$Foo(n,k) as illustrated in the Bartest package. I do admit that Aldor is
nicer to allow that, so that such a wrapper is not necessary. But the wrapper is
straightforward and general and can even be automated.
If one MUST use the signature for g (other than it is convenient), then you need
Aldor. But can someone supply such an example from Aldor?
William
- [Axiom-developer] RE: Axiom domains and Aldor return types, Page, Bill, 2005/01/12
- [Axiom-developer] Re: [Aldor-l] RE: Axiom domains and Aldor return types, Ralf Hemmecke, 2005/01/12
- Re: [Axiom-developer] Re: [Aldor-l] RE: Axiom domains and Aldor returntypes, William Sit, 2005/01/12
- Re: [Axiom-developer] Re: [Aldor-l] RE: Axiom domains and Aldorreturntypes, William Sit, 2005/01/13
- Re: [Axiom-developer] Re: [Aldor-l] RE: Axiom domains andAldorreturntypes, William Sit, 2005/01/13
- Re: [Axiom-developer] Re: [Aldor-l] RE: Axiom domains and Aldorreturntypes, Martin Rubey, 2005/01/13
- RE: [Axiom-developer] Axiom domains and Aldor return types, Bill Page, 2005/01/13
- RE: [Axiom-developer] Axiom domains and Aldor return types, Martin Rubey, 2005/01/14
- Re: [Aldor-l] RE: [Axiom-developer] Axiom domains and Aldor return types, Gabriel Dos Reis, 2005/01/14
- Re: [Axiom-developer] Axiom domains and Aldor return types, Stephen Wilson, 2005/01/14
- Re: [Axiom-developer] Axiom domains and Aldor return types,
William Sit <=
- Re: [Axiom-developer] Axiom domains and Aldor return types, Stephen Wilson, 2005/01/14
- Re: [Axiom-developer] Axiom domains and Aldor return types, William Sit, 2005/01/15
- Re: [Axiom-developer] Axiom domains and Aldor return types, William Sit, 2005/01/15
- Re: [Axiom-developer] Axiom domains and Aldor return types, William Sit, 2005/01/15
- Re: [Axiom-developer] Axiom domains and Aldor return types, Stephen Wilson, 2005/01/16
- Re: [Axiom-developer] Axiom domains and Aldor return types, William Sit, 2005/01/17
- RE: [Axiom-developer] Axiom domains and Aldor return types, Bill Page, 2005/01/14
- Re: [Axiom-developer] Axiom domains and Aldor return types, William Sit, 2005/01/14
- RE: [Axiom-developer] Axiom domains and Aldor return types, Bill Page, 2005/01/16
- Re: [Axiom-developer] Axiom domains and Aldor return types, William Sit, 2005/01/14