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 <[email protected]> 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 <[email protected]> wrote:
>> And can a function return something like (x : Ring) as a result with
>> dependent types? For example
>>
>> f : Type == List (x : Ring)
>>
>> --
>
--
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.
