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 <bill.p...@newsynthesis.org> wrote:
> On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <g...@cs.tamu.edu> 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.
>
------------------------------------------------------------------------------
Get a FREE DOWNLOAD! and learn more about uberSVN rich system,
user administration capabilities and model configuration. Take
the hassle out of deploying and managing Subversion and the
tools developers use with it. http://p.sf.net/sfu/wandisco-d2d-2
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
