I think one might reasonably expect that
f(x:Ring) : LinearAggregate(x) == List (x)
would work. And in almost does (at least in OpenAxiom):
(1) -> f(x:Ring) : LinearAggregate(x) == List (x)
x is not a valid type.
Unfortunately the interpreter in OpenAxiom does not treat categories
in quite the same way as the compiler. There is however the domain of
domains in OpenAxiom so we may write:
(1) -> f(x:Domain) : Domain == List (x)
Function declaration f : Domain -> Domain has been added to
workspace.
Type: Void
(2) -> f(Integer)
Compiling function f with type Domain -> Domain
(2) List Integer
Type: Domain
In FriCAS (1.1.2) we get:
(1) -> f(x:Ring) : LinearAggregate(x) == List (x)
Function declaration f : Ring -> LinearAggregate(NIL) has been added
to workspace.
Type: Void
(2) -> f(x:Domain) : Domain == List (x)
Function declaration f : NIL -> NIL has been added to workspace.
1 old definition(s) deleted for function or rule f
Type: Void
The closest equivalent of Domain in FriCAS is Type, but even this does not work:
(3) -> f(x:Type) : Type == List (x)
Function declaration f : Type -> Type has been added to workspace.
1 old definition(s) deleted for function or rule f
Type: Void
(4) -> f(Integer)
Compiling function f with type Type -> Type
>> System error:
The index 3 is too large.
On Fri, Aug 19, 2011 at 12:10 PM, Bill Page <bill.p...@newsynthesis.org> wrote:
> I think no. What would you expect this to mean? What is the notation
> 'x:Ring' in this context? What is the scope of 'x'?
>
> On Fri, Aug 19, 2011 at 10:16 AM, Yrogirg <yrog...@gmail.com> wrote:
>> And can a function return something like (x : Ring) as a result with
>> dependent types? For example
>>
>> f : Type == List (x : Ring)
>>
>> --
>
------------------------------------------------------------------------------
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
