No, SquareMatrix is not a dependent type. It is a type constructor.
Yes, in most cases you should consider it to be a function with two
arguments that returns a type. But FriCAS/Axiom places significant
limitations on what you can do with such functions.
SquareMatrix(2,Integer) is a type constant. It is not dependent on anything.
The type expression SquareMatrix(n,R) could be a dependent type, say
in the context
const(n:NNI,R:Ring,p:R):SquareMatrix(n,R) == p*1$SquareMatrix(n,R)
Unfortunately FriCAS (like the original Axiom system) does not fully
support dependent types.
The Aldor compiler does support such dependent types.
The FriCAS/Axiom interpreter however does allow for something similar:
(1) -> const(n,R,p)==p*1$SQMATRIX(n,R)
Type: Void
(2) -> const(3,POLY INT,2)
Cannot compile a $-expression involving a local variable.
FriCAS will attempt to step through and interpret the code.
+2 0 0+
(2) |0 2 0|
+0 0 2+
Type: SquareMatrix(3,Polynomial(Integer))
Note that you cannot write the type of the function const in to form
const: (A,B,C) -> D
Regards,
Bill Page.
On Sat, Aug 13, 2011 at 1:53 PM, Yrogirg <[email protected]> wrote:
>
>> Types are "first class", because you can give types as input to
>> functions. And "dependent types" are types that depend on the input.
>
> I'm confused. So let us have a function, that takes a value as an
> argument and returns a type, and this function is possible because
> types are first-class objects. But this function is not the same as a
> dependent type?
>
> And hence SquareMatrix is not a dependent type?
>
> (1) -> m : SquareMatrix(2, Integer) := matrix[[1,2],[9,8]]
>
> ┌1 2┐
> (1) │ │
> └9 8┘
> Type: SquareMatrix(2,Integer)
>
> --
> 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.
>
>
--
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.
