Bill Page <[email protected]> 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
--
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.
