headers
Gabriel Dos Reis | 11 Aug 2011 01:37
Picon
Favicon

[open-axiom-devel] Integer and ConvertibleTo String


Hi,

The domain Integer, starting from OpenAxiom-1.4.2, will no longer satisfy
the category `ConvertibleTo String'.  That convertibility existed only to 
allow writing `convert(i) <at> String' for an integer `i'.  That looks at
best misguided.  Rather, please use the function

     string: Integer -> % from String

that has always existed.

-- Gaby

------------------------------------------------------------------------------
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-dev2dev
Permalink | Reply | 0 comments |
headers
Gabriel Dos Reis | 17 Aug 2011 17:52
Picon
Favicon

[open-axiom-devel] Spad categories and Haskell type classes

Martin Baker <ax87438@...> writes:

[...]

| I'll try to think of an example, say in Haskell one may write:
| 
| class Monad m where
|   fmap :: (a -> b) -> m a -> m b
|   id :: a -> m a
|   mult :: m (m a) -> m a
| 
| where 'm', 'a' and 'b' all stand for types, and we can loop these
| types back on themselves to give a whole sequence of types. If its not
| too confusing to give them SPAD type names a ListMonad may 'generate':
| 
| a = NNI
| m a = List NNI
| m m a = List List NNI
| m m m a = List List List NNI
| ...
| 
| This seems to me that a big essence of category theory, that is:
| external structure (arrows, functors, endofuntors) is generating
| internal structure (types) by a sort of closure operation.
| 
| I am struggling to understand if or how this could be transposed into
| SPAD.

It is often overlooked that the Spad language had an influence (and not so
small) on the design of Haskell type classes.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Bill Page | 19 Aug 2011 20:43
Gravatar

Re: [open-axiom-devel] Re: What can be done with types as first-class objects?

You might be curious how this works using Aldor in FriCAS:

(1) -> )sys cat dep1.as

#pile
#include "axiom.as"
f(x:Ring) : LinearAggregate(x) == List (x)

(1) -> )co dep1.as
   Compiling FriCAS source code from file /home/page/dep1.as using
      AXIOM-XL compiler and options
-O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y
$AXIOM/algebra -I $AXIOM/algebra
      Use the system command )set compiler args to change these
      options.
"/home/page/dep1.as", line 3:
f(x:Ring) : LinearAggregate(x) == List (x)
..^
[L3 C3] #1 (Warning) Function returns a domain that might not be
constant (which may cause problems if it is used in a dependent type).

   Compiling Lisp source code from file ./dep1.lsp
   Issuing )library command for dep1
   Reading /home/page/dep1.asy
   f is now explicitly exposed in frame frame1
   f will be automatically loaded when needed from /home/page/dep1
(1) -> x:f(Integer):=construct [1,2,3]

   (1)  [1,2,3]
                                                             Type: f(Integer)
(Continue reading)

Permalink | Reply | 9 comments |
headers
Gabriel Dos Reis | 19 Aug 2011 20:59
Picon
Favicon

[open-axiom-devel] Categories are predicates

Bill Page <bill.page@...> writes:

| I think one might reasonably expect that
| 
|   f(x:Ring) : LinearAggregate(x) == List (x)
| 
| would work. And in almost does (at least in OpenAxiom):
| 
| (1) -> f(x:Ring) : LinearAggregate(x) == List (x)
| 
|    x is not a valid type.
| 
| Unfortunately the interpreter in OpenAxiom does not treat categories
| in quite the same way as the compiler.

Hi Bill,

I would like to understand better what the real problem is, what you
would like to express  -- not a Spad code but rather the *idea* you
would like to express, then we could see how to express it or what it
would take to express it. 

Background:

Categories are predicates, not types in the traditional sense of
a prescription of data representation -- unlike domains.  A value
/belongs/ to a *unique* domain.  That is one of the reasons why it is some
simple to talk about "first class object": you know how to represent
their storage, how to pass them around, etc.  A domain /can satisfy/
several categories (e.g. predicates) at the same time.  If you treat a
(Continue reading)

Permalink | Reply | 1 comment |
headers
Bill Page | 19 Aug 2011 21:19
Gravatar

Re: [open-axiom-devel] Re: What can be done with types as first-class objects?

And just so I don't give the wrong impression I should not fail to
point out that this sort of dependent type does also work in SPAD:

(1) -> )sys cat dep1.spad

)abbrev domain F f
f(x:Ring) : LinearAggregate(x) == List (x)

(1) -> )co dep1.spad
   Compiling FriCAS source code from file /home/page/dep1.spad using
      old system compiler.
   F abbreviates domain f
------------------------------------------------------------------------
   initializing NRLIB F for f
   compiling into NRLIB F
****** Domain: $ already in scope
augmenting $: (finiteAggregate)
****** Domain: x already in scope
augmenting x: (Evalable x)
****** Domain: $ already in scope
augmenting $: (finiteAggregate)
****** Domain: $ already in scope
augmenting $: (shallowlyMutable)
****** Domain: x already in scope
augmenting x: (ConvertibleTo (InputForm))
(time taken in buildFunctor:  0)

;;;     ***       |f| REDEFINED

;;;     ***       |f| REDEFINED
(Continue reading)

Permalink | Reply | 8 comments |
headers
Bill Page | 19 Aug 2011 20:27
Gravatar

Re: [open-axiom-devel] Re: What can be done with types as first-class objects?

I think one might reasonably expect that

  f(x:Ring) : LinearAggregate(x) == List (x)

would work. And in almost does (at least in OpenAxiom):

(1) -> f(x:Ring) : LinearAggregate(x) == List (x)

   x is not a valid type.

Unfortunately the interpreter in OpenAxiom does not treat categories
in quite the same way as the compiler. There is however the domain of
domains in OpenAxiom so we may write:

(1) -> f(x:Domain) : Domain == List (x)
   Function declaration f : Domain -> Domain has been added to
      workspace.
                                                                   Type: Void
(2) -> f(Integer)
   Compiling function f with type Domain -> Domain

   (2)  List Integer
                                                                 Type: Domain

In FriCAS (1.1.2) we get:

(1) -> f(x:Ring) : LinearAggregate(x) == List (x)
   Function declaration f : Ring -> LinearAggregate(NIL) has been added
      to workspace.
                                                                   Type: Void
(Continue reading)

Permalink | Reply | 12 comments |
headers
Gabriel Dos Reis | 19 Aug 2011 21:34
Picon
Favicon

Re: [open-axiom-devel] What can be done with types as first-class objects?

Bill Page <bill.page@...> writes:

| And just so I don't give the wrong impression I should not fail to
| point out that this sort of dependent type does also work in SPAD:
| 
| (1) -> )sys cat dep1.spad
| 
| )abbrev domain F f
| f(x:Ring) : LinearAggregate(x) == List (x)

this the easy case and has been working in Spad as long as I have known
Spad for that is the way domain constructors work :-)

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. 

-- Gaby

------------------------------------------------------------------------------
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
(Continue reading)

Permalink | Reply | 7 comments |
headers
Bill Page | 19 Aug 2011 21:53
Gravatar

Re: [open-axiom-devel] What can be done with types as first-class objects?

On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <gdr@...> 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 .
(Continue reading)

Permalink | Reply | 6 comments |
headers
Gabriel Dos Reis | 19 Aug 2011 22:03
Picon
Favicon

Re: [open-axiom-devel] What can be done with types as first-class objects?

Bill Page <bill.page@...> writes:

| On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <gdr@...> 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 ...

I am not sure I understand the conclusion you wanted to draw from the example.
I thought I explicitly mentioned type families, which by definition
involve application of a non-contructor in operation position.  Again, I
might have missed the conclusion you wanted to draw.  Could you state it
in an unambiguous form?

-- Gaby

------------------------------------------------------------------------------
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
(Continue reading)

Permalink | Reply | 2 comments |
headers
Bill Page | 19 Aug 2011 22:07
Gravatar

Re: [open-axiom-devel] What can be done with types as first-class objects?

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.page@...> wrote:
> On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <gdr@...> 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
(Continue reading)

Permalink | Reply | 1 comment |

Gmane