Bill Page <bill.p...@newsynthesis.org> writes:
| Perhaps I should have included a more explicit example:
Yes, that does not tell me the conclusion you wanted to draw.
Mathematicians used to stated theorems so that everybody knows what the
proof is about :-)
I could not decide whether you wanted to prove a universal by that
example or you just wanted to prove an existential, and which one.
[...]
| >> Note also that Spad does not work properly with operations returning
| >> types -- for very deep implementation reasons, one that the Haskell
| >> people also faced when they added type families (i.e. type-level
| >> functions, still not accepting values at that level) leading to redesign
| >> of Haskell type rules and extension of its theoretical foundation.
As an example of my statement: consider a situation where an entity has an
associated type (say the element type of a container) that is defined on
case by case basis by each domain. That associated type, in general,
will be given by a type-level function which, because of the very nature
of its purpose, should not be a contructor.
)abbrev category MYAGG MyAggegate
MyAggegate(): Category == Type with
elementType: Ring -- to be defined by each domain
toList: % -> List elementType -- idem
sumAll: % -> elementType -- this one has a default implementation
add
sumAll x == reduce(_+,toList x,0$elementType)
This is just one simple example of (indirect) dependency.
Type dependency requires an advanced decision procedure of type equality
that goes beyond syntactic equally (which is the theoretical
underpinning of most of current Spad, ML, and Haskell98 type system.)
-- Gaby
------------------------------------------------------------------------------
Get a FREE DOWNLOAD! and learn more about uberSVN rich system,
user administration capabilities and model configuration. Take
the hassle out of deploying and managing Subversion and the
tools developers use with it. http://p.sf.net/sfu/wandisco-d2d-2
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
