On Fri, Aug 19, 2011 at 2:59 PM, Gabriel Dos Reis <g...@cs.tamu.edu> wrote:
> Bill Page <bill.p...@newsynthesis.org> 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.
>
I guess it is fairly simple: I would like the semantics of the
interpreter to be closer to those of the compiler so "function"
definitions like
f(x:Ring) : LinearAggregate(x) == List (x)
should compile as type constructors just the way they do in the compiler.
> 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 so
> 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
> category as a type that prescribes representation, then their is a
> question of how do you express the notion that a value has several
> representation -- as opposed to one. How do you go from one
> representation to the next? How do you know which representation
> is going to be needed down the pipeline after several calls?
>
The original Axiom solution (Steven Watt) was to say that categories
are collections of domains. Membership of a domain in some category is
the "predicate" to which you refer. Membership is determined by
assertion - not just by their properties (exports). So categories are
"higher order" types in that sense. But maybe we do not want to assume
any more structure than necessary? We need to know when one category
is included in another (i.e. sub-categories) but Axiom does not fully
evaluate types, neither domains nor categories, so do we really need
to call them predicates?
> Interestingly the Haskell folks also ran into similar issue in the past.
> During a recent 4-day visit at TAMU [1], Simon Peyton Jones and I
> violently agreed that categories or C++ concepts or Haskell type classes
> (we were discussing similarities and dissimilatiries between C++
> concepts and Haskell type classes) are best treated as not types in the
> traditional sense of describing data -- or else, one might run into
> serious logical an implementation issues. They are
> non-representational predicates.
>
This sounds like a recourse to theorem proving and a step away from algebra.
> In OpenAxiom, we sidestep the issue by saying that there is a domain
> called Domain that represents all domains as *values*. Similarly, we
> have a domain named Category that represents all categories as
> *values* -- yes that `Category' that you put as a return type of a
> category constructor is a real domain (not a fake one) in OpenAxiom.
>
I like this! Perhaps it would also make sense even 'has' would be an
operation exported by the domain Category and to the extent possible
these domains would be defined or at least extended in the library.
It seems to me that this is mostly orthogonal to how to interpret
f(x:Ring) : LinearAggregate(x) == List (x)
This could define f as a type constructor, where as
f(x:Domain) : Domain == List (x)
is a function that returns a domain. So perhaps to return to an
earlier post by Yrogirg:
--
From: Yrogirg <yrog...@gmail.com>
Date: Sat, Aug 13, 2011 at 1:53 PM
Subject: [fricas-devel] Re: What can be done with types as first-class objects?
To: FriCAS - computer algebra system <fricas-de...@googlegroups.com>
> Types are "first class", because you can give types as input to
> functions. And "dependent types" are types that depend on the input.
I'm confused. So let us have a function, that takes a value as an
argument and returns a type, and this function is possible because
types are first-class objects. But this function is not the same as a
dependent type?
And hence SquareMatrix is not a dependent type?
(1) -> m : SquareMatrix(2, Integer) := matrix[[1,2],[9,8]]
┌1 2┐
(1) │ │
└9 8┘
Type: SquareMatrix(2,Integer)
--
Since OpenAxiom implements the notion of the Domain of domains, what
about a function that returns a domain constructor? E.g. Should we
expect this to work:
DoubleList(): Domain->Domain == x +-> List List x
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
