"Serge D. Mechveliani" <mech...@botik.ru> writes:

[...]

| > Spad allows much heavier overloading then is possible in Haskell.
| > [..]
| 
| Haskell has much of overloading. 

Haskell is more restrictive in its version overloading.  It wants your
overloaded functions/operators to have the same arity and be in a
generic instance relationship.  That is not the case in Spad.

   (1) -> )di op -

   There are 12 exposed functions called - :
      [1] (D,D) -> D from D if D has ABELGRP
      [2] D -> D from D if D has ABELGRP
      [....]

| I do not know of any example of what
| needs more overloading. May be, you give such?

Nothing is ever *needed*.  Well, we only need a binary editor :-/

In fact, overloading is not needed at all, as long as we can go along
with criptic names, and indeed that has been tried before again and again.

[...]

| > 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).
| 
| 
| Yes, this is a real point.
| I suspect that this (+ dependent types of Aldor)
| is the only principal feature in "(Spad+Aldor) minus Haskell".
| It weights a lot. Due to this DoCon has more complex architecture than 
| it could have.
| 
| 1) And what about ML or such languages? 

hmm, what do you mean?

| 2) Is this feature done by the Common Lisp object system (CLOS) ?
|    (I do not know what is CLOS).

No, Spad semantics in principle is independent from Lisp.
It is an unfortunate situation that the current implementation is done
with Lisp, therefore giving the mistaken impression that Lisp is needed.

There is an ongoing project in OpenAxiom to use Poly/ML as alternate
runtime for integration with proof assistants such as Isabelle.  See 
our paper at CICM/Calculemus 2011

   http://www.springerlink.com/content/d1t6326678385516/

In general, OpenAxiom tries hard to isolate Spad semantics from the
current implementation language.

-- Gaby

------------------------------------------------------------------------------
RSA(R) Conference 2012
Save $700 by Nov 18
Register now
http://p.sf.net/sfu/rsa-sfdev2dev1
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Reply via email to