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)
== add
f() : LinearAggregate(x) == List (x)
(1) -> )co dep2.spad
Compiling FriCAS source code from file /home/page/dep2.spad using
old system compiler.
Illegal NRLIB
TEST.NRLIB claims that its constructor name is the domain test but
test is already known to be the for package TEST .
TEST abbreviates domain test
------------------------------------------------------------------------
initializing NRLIB TEST for test
compiling into NRLIB TEST
compiling exported f : () -> LinearAggregate x
Time: 0.01 SEC.
(time taken in buildFunctor: 0)
;;; *** |test| REDEFINED
;;; *** |test| REDEFINED
Time: 0 SEC.
Cumulative Statistics for Constructor test
Time: 0.01 seconds
finalizing NRLIB TEST
Processing test for Browser database:
--->/home/page/dep2.spad-->test((f ((LinearAggregate x)))): Not documented!!!!
--->/home/page/dep2.spad-->test(constructor): Not documented!!!!
--->/home/page/dep2.spad-->test(): Missing Description
; compiling file "/home/page/TEST.NRLIB/TEST.lsp" (written 19 AUG 2011
03:46:38 PM):
; file: /home/page/TEST.NRLIB/TEST.lsp
; in: DEFUN |test;|
; (BOOT::|haddProp| BOOT::|$ConstructorCache| 'BOOT::|test| (LIST
BOOT::DV$1)
; (CONS 1 BOOT::$))
;
; caught WARNING:
; undefined variable: |$ConstructorCache|
; in: DEFUN |test|
; (VMLISP:HGET BOOT::|$ConstructorCache| 'BOOT::|test|)
; --> GETHASH
; ==>
; (SB-IMPL::GETHASH3 'BOOT::|test| BOOT::|$ConstructorCache| NIL)
;
; caught WARNING:
; undefined variable: |$ConstructorCache|
;
; compilation unit finished
; Undefined variable:
; |$ConstructorCache|
; caught 2 WARNING conditions
; /home/page/TEST.NRLIB/TEST.fasl written
; compilation finished in 0:00:00.022
------------------------------------------------------------------------
test is now explicitly exposed in frame frame1
test will be automatically loaded when needed from
/home/page/TEST.NRLIB/TEST
(1) -> x:f := [1,2,3]
(1) [1,2,3]
Type: List(PositiveInteger)
(2) ->
---
I could imagine that there would be cases where this does not work
properly, whether by design flaw or bugs. Can you give a simple
example?
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.
