On Wed, Feb 29, 2012 at 06:03:12PM -0500, Bill Page wrote:
> On Wed, Feb 29, 2012 at 2:53 PM, Serge D. Mechveliani wrote:
> > ...
> > On Mon, Feb 27, 2012 at 10:38:05PM +0100, Ralf Hemmecke wrote:
> > >...
> >> In Aldor one would even have the "extend" keyword and so could add new
> >> properties/functions to already existing domains.
> >>
>
> Although "extend" is part of Aldor, my point of view is that this is
> rarely needed and maybe only rarely a good idea in Axiom.
>
> >
> > This is the most suspicious thing which I observe in Axiom.
> > So far, I hope that I have missed some point. But you are the
> > second why mention the feature.
> > It is difficult to imagine how can an user behave without adding
> > his category instances to the standard library domains.
> > For example, in DoCon, I introduce a category (class), say (contrived)
> >
> > class Sized a where size :: a -> Integer
> >
> > And usually the first instances for such a category are like this:
> >
> > instance Sized Integer where size = abs
> > instance Sized a => Sized [a] where size = sum . map size
> >
> > instance (Sized a, Sized b) => Sized (a, b)
> > where
> > where size (x, y)= (size x) + (size y)
> >
> > Here Integer, [] := List, and (,) := Pair
> > are type constructors from the standard library. And this helps a lot
> > the further usage of Sized.
>
> In Axiom categories are not classes. An Axiom category is a kind of
> predicate. It must be explicitly asserted by the programmer that a
> domain satisfies some category expression (formed from Join and with
> clauses). Domains satisfy only the named categories. In addition this
> category assertion requires that the domain implement a specific set
> of exported operations for which it is the programmers responsibility
> to ensure that the operations exported by the domain respect the
> axioms that are implicit in the category names which occur in the
> category expression. So categories are a kind of "interface contract".
> Axiom categories form a lattice of sub-categories based on domain
> satisfaction, i.e. Any domain which satisfies category C==Join(A,B)
> also satisfies both A and B.
The syntax is different, but I do not see any difference in the meaning.
For example, in Haskell there is not a standard Set, nor AdditiveMonoid,
the user must define them, if needs.
Imagine now that Spad is similar in this.
The user defines in Haskell
class Set a => AdditiveMonoid a where (+) :: a -> a -> a
0 :: a
-- Documentation: + must be associative, commutative,
-- it must hold forall x (x+0 == x).
And in Spad ( sorry, the syntax needs correction! ):
Category AdditiveMonoid(...) ... with Join(Set) ... ==
add
+ : (%, %) -> %
0 : %
+++ Documentation: + must be associative, commutative,
+++ it must hold forall x (x+0 = x).
In both cases the meaning _for the compiler_ is
the Universal Algebra defined by the signature
{(+) :: % -> % -> %, 0 :: %}.
intersected with the Universal Algebra of Set.
-- it does not include any additional laws.
In Haskell, `Set a' is placed before `=>',
and in Spad it is placed under Join(...).
And the meaning for the compiler in both cases is just the
_class of domains_
which signature include this signature and the signature of Set.
And in both cases the _intended meaning for a CA developer_
is denoted in the _commentary_
(and Haskell does not presume any CA developer, Haskell is for CA as well
as, for example, for designing a parser, or a compiler for Prolog).
Further, Spad says:
a domain belongs to a category only by explicit assertion placed in
the domain definition.
Haskell is similar: such an assertion is an instance declaration:
instance AdditiveMonoid Integer where (+) = +_Integer
0 = zero_Integer
instance (AdditiveMonoid a, AdditiveMonoid b) =>
AdditiveMonoid (a, b)
where
(x,y) + (x', y') = (x+x', y+y')
(the second declares the instance for the domain constructor of Pair
-- what is Product in Spad).
If the user defines for Integer x+y = x+1 instead of +_Integer,
the compiler will still consider Integer as a member of AdditiveMonoid.
But this (+) instance is not associative.
Hence the AdditiveMonoid class does not coincide _for the compiler_
with the _class of additive monoids_ known in algebra.
Similar is with Spad.
In this part, I do not see any difference between Haskell and Spad --
except that the standard library domains can be extended in Haskell
(like in the above example).
This feature follows the line of mathematical _textbooks_.
A mathematician writes in a textbook
"Consider Z := Integer as an Euclidean ring, and also as an instance
of the Sized category, where size(n) = ...
",
and furher one writes Z and uses size(n), one does not write "Z2".
But I think, if your below suggestion with a `package' works, then,
probably, this feature is not so a great disadvantage in Spad.
Return to the concept difference.
The first real point I see is that in Spad, a domain constructor is a
Spad function whose return value belongs to Type.
The compiler understands this.
And I even use this in Spad when programing a certain generic parser.
In Haskell a function cannot neither return a type (domain) nor take it:
types (domains) are totally static.
> In Axiom there is a way to introduce new operations related to Integer
> without redefining what you mean by Integer. This is done by defining
> a package. It is common to see in the Axiom library for example
> something like:
>
> )abbrev package INTHEORY IntegerNumberTheoryFunctions
> IntegerNumberTheoryFunctions(): with
> divisors : Integer -> List(Integer)
> ...
>
> In your example this would become something like this:
>
> )abbrev package SIZED Sized
> Sized(A:OrderedRing): with
> size: A -> Integer
> size: List A -> Integer
> size: DirectProduct(2,A) -> Integer
> == add
> size(a:A):Integer == abs(a)
> size(a:List A):Integer == reduce(+,map(size$SizedInt(A),a))
> size(a:DirectProduct(2,A)):Integer == size(first a)$SizedInt(A) +
> size(second a)$SizedInt(A)
>
> Note: This code is just of illustration. I haven't actually tried to
> compile it.
Thank you. I shall think of this.
Regards,
------
Sergei
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
