Perhaps I should have included a more explicit example:
(2) -> y:f()$test(Integer) := [1,2,3]
(2) [1,2,3]
Type: List(Integer)
On Fri, Aug 19, 2011 at 3:53 PM, Bill Page <[email protected]> wrote:
> 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.
