Bill Page <[email protected]> writes:
| On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <[email protected]> wrote:
| >
| > I thought you were after something more elaborate where an operation
| > from a domain has a dependent type...
| >
| > 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.
| >
|
| Here is a domain exporting an operation that returns a type. Although
| one might claim that the type that it returns is not explicitly
| dependent ...
|
| (1) -> )sys cat dep2.spad
|
| )abbrev domain TEST test
| test(x:Ring): with
| f : () -> LinearAggregate(x)
Note that the following will not work (because the compiler does not
allow syntax for it)
f: (n: Integer) -> SquareMatrix(n,x)
which has SquareMatrix in operation position.
-- 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.
