Thanks, Gaby.

On Fri, Aug 19, 2011 at 4:26 PM, Gabriel Dos Reis <[email protected]> wrote:
>
> | >> 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 constructor.
>
> )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.)
>

If the associated type is "defined on case by case basis by each
domain" we can make the dependency more explicit. Presumably we still
want types to be static. Is there any situation where the following
would not be adequate?

)abbrev category MYAGG MyAggegate
MyAggegate(ElementType: Ring): Category == Type with
   elementType: Ring        -- to be defined by each domain
   toList: % -> List ElementType  -- idem
   sumAll: % -> ElementType       -- this one has a default implementation
 add
   import ElmentType
   --  sumAll x == reduce(_+,toList x,0$elementType)
   sumAll(x:%):ElementType ==
     r := 0
     for i in toList(x) repeat
       r:=r+i
     return r

--

Note: I had some problems using reduce in this context.

Regards,
Bill Page

-- 
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.


Reply via email to