Serge D. Mechveliani wrote:
>
> People,
>
> I have the following notes and questions on Axiom and on the book
> "Axiom. The 30 year Horizon",
> which I have downloaded together with the FriCAS-1.1.4 source.
>
> The three languages
> -------------------
> The book mentiones the languages Spad (=?= Scratchpad ), Axiom, Aldor.
> What is the difference? Which one in described in the book?
> Which one is implemented in FriCAS-1.1.4 ?
>
As othere wrote FriCAS contains compier for Spad language and
almost all mathematical capabilities of FriCAS are written in
Spad.
> Spad \ ML = ? Spad \ Haskell = ?
> ---------------------------------
> What principal language constructs Spad (Axiom, Aldor) has that cannot
> be replaced with the ML language constructs
> (classes, structures, functors ...).
> I am experienced in Haskell and know very few of ML, so the question is
> mainly on Spad vs Haskell
> (and apart from Haskell's "laziness" and functionality).
Spad allows much heavier overloading then is possible in Haskell.
>From abstract point of view this may sound trivial (in principle
one can rename functions so that names are unique), but traditional
math notations is also overloaded, and overloading in Spad allows
staying closer to established notations.
Categories in FriCAS are analogus to Haskell type classes, but
they behave differently enough that you may be forced to substantially
restructure program. I do not know enough of Haskell to tell if
this restructuring is mechanical or require some inteligence.
And "cannot be replaced" is fuzzy -- if you allow only simple
local rewrite rules then very quickly you will find things which
cannot be handled, if you are determind to do complete rewrite then
nothing will stop you.
Anyway, FriCAS categories have parameters which may be types or
normal values -- my impression is that Haskell type classes
only allow types as parameters. In FriCAS parameters to
categories itself have types. Both interface part (exported
signatures) and implementation part may be conditioned on
types of parameters. Parameters to types may be computed
at runtime and effect of conditionals depends on actual
type. In absence of conditionals type checking uses
static information (given by categories), but for
example in:
f(a : A) : A ==
if A has Field then 1/a
else a
when typechecking '1/a' typechecker knows that A is a Field
(because we checked this in 'if'), so division is available.
This type of conditional is used a lot in FriCAS algebra.
BTW: Typically the above is written as:
if A has Field then
f(a : A) : A == 1/a
else
f(a : A) : A == a
In the first form test 'A has Field' is done each time f is
executed, in the second test is done when domain or package
containing f is initialized (there is separate instance for
each A).
> Language or Library?
> --------------------
>
> In many places it is written in this book "Axiom",
> "Axiom has this and this" -- without making it clear:
> the Axiom language or the Axiom library?
> Really, this ambiguity is great.
The Axiom book, and in particular first chapters, is intended
to introduce readers to Axiom. Fine distinctions between
language and library would probably overwhelm the readers.
> Then, it follows `Record' in the book. And it is, probably, a construct of
> the Language (in Haskelll records are in the language).
Well, Record can not be written in Spad: normal Spad constructors
take fixed number of arguments but record takes variable number of
arguments. In a sense Record is in library, but in part which must
be written in lower level language.
It is a philosophical question what is part of language and what
not. Spad types are runtime object and as such normally must be
present in the library (there are strange types, for example "failed"
which currently only exist inside compiler, but most Spad users have
no idea that they exist at all). At the top is Category, which have
only fake runtime representation and all its interesting behahviour is
hardcoded into Spad compiler. Record, Union, Enumeration
and Mapping are written in Boot -- lower level language in
which compiler and runtime support is currently written. Other
types are written in Spad. Compiler has special knowledge about
some types. For example compiler will automatically coerce
branches to Union if context requires this. Conditions are
assumed to give Boolean result and if you omit Boolean from
the library the compiler will fail in weird way.
Core Spad language is rather small, it contains powerful
mechanism for defining types (domains and categories),
allow defining functions (named or anonymous), contains
conditionals, iteration constructs, assignment and
finction call. 'is' tests if one type is the same as other type,
'has' test if types belong to a category, 'case' checks which
variant of union is valid -- they are treated in special
way by the compiler. '+' is recognized as operator by the
parser, so expressions have usual syntax, but after parsing
'+' is treated the same as any other functions. Iteration
constructs can produce lists or vectors and needed knowledge
about List and Vector is hardcoded in the compiler. The '..'
operator produces ranges and again knowledge about ranges
and integers is hardcoded in the compiler.
> Comparison to some Haskell features
> -----------------------------------
> a) Union of types is good.
> b) `case x <type>' is good.
> c) Using Subdomain, `pretend' looks good.
> d) Rules are good,
> because rule sin(2*x) == 2*sin(x)*cos(x)
> cannot be written as sin(2*x) = 2*sin(x)*cos(x) in Haskell.
> The Haskell programs often compute by pattern matching, but not of
> the LHS part of such kind.
Syntax for rules is build into interpreter, but this syntax is not
in Spad. The real work of rules is done by library code.
>
> e) Clarity of the code.
> For example, consider the lexicographic list comparison:
>
> lexListComp :: Ord a => [a] -> [a] -> ComparisonValue
> lexListComp xs ys = case (xs, ys)
> of
> ([], [] ) -> EQ
> ([], _ ) -> LT
> (_, [] ) -> GT
> (x: xs', y: ys') -> case compare x y
> of
> EQ -> lexListComp xs' ys'
> v -> v
>
> (no `val', no `defun', few parentheses,
> the long word `lexListComp' is not repeated).
>
> What is the nicest code for this in Spad ?
> Another question is about nested local values introduced by let-in and
> "where". For example,
> f x = let (p: (y, z): _) = g x x
> h ys = let h' = (\ x -> [x]) in ...
> in
> h [p, y, z]
>
> Dependent types
> ---------------
> Also there exists a particular question of dependent types and
> dependent instances (domains). In Haskell they are not possible.
> Due to this, DoCon has a more complicated architecture than it might have.
> And I do not know whether they really work in Aldor or in the current Spad.
They work, but dependence can be only on parameters of domain/package.
This means that if you want to heavy use of it you may be forced to
create a lot of packages so that you can express dependency (in
worst case you may be forced to put each function in a separate package).
--
Waldek Hebisch
[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.
