I originally put this on AxiomWiki created by Bill Page but since that has disappeared I moved it here.
The aim of this page is to relate mathematical terms, such as those from category theory or type theory, to the way these terms are used in SPAD.
So a reader who has some acquaintance with a given term in a mathematical context can see how the term is used in SPAD and hopefully won't be confused by any differences in substance or approach.
The explanations in the table below are not intended to be precise mathematical definitions but only intended to highlight the relevant issues for this comparison purpose (I assume people will lookup the precise definition if they need to).
|Related SPAD Terminology
Types describe possible elements of a mathematical structure. So if an element is a member of a Concrete Category it has that type.
Generally the word 'type' could be used for something that is either a Domain, Category (or Package ?).
In SPAD type checking provides some level of code validation. Types also allow correct function/operation to be called when its name is overloaded (by pattern matching on both called and calling types). There is also some type inference.
In SPAD 'Type' also has a specific meaning as the name of a category which is top of the lattice of all categories. Therefore all categories and domains derive from it.
a type that depends on another type
Type Constructor or Functor
MyDomain(n: RingCategory) : E == I where ....
This can be used as a type when supplied with a domain which derives from the category used in the definition:
If MyDomain is used on its own then it is not a type because it cannot be constructed. However, it is a category in that it derives from the category 'Type'.
This is also known as a functor, in that it 'generates' one domain from another, see below.
a type that depends on a term
MyDomain(t: IntegerDomain) : E == I where ....
This can be used as a type when supplied with an element of IntegerDomain, for instance,
There is limited support for dependent types in SPAD. Details of limitations?
a component of a mathematical expression
|SPAD supports elements of a domain (constants or literals) and variables that stand for these elements.
Terms depending on types. For instance a function could be defined that applies to many types.
|Which types of polymorphism are supported?
Well-formed combination of symbols.
We could define an expression inductively like this:
Rep = Union(op:Symbol,first:%,second:%)
or we could use built-in domains Expression or Kernel
Allows us to compare certain concrete categories (preserve certain elements of structure)
If f is a structure-preserving mapping from G to H. If g1 and g2 are elements of G then the structure '*' is preserved if:
f(g1 * g2) = f(g1) * f(g2)
If '*' is the only structure in H then we might tend to think of f 'generating' H from G
Morphism and Mapping
Many domains in the SPAD library have a map function.
The SPAD library has MappingPackage1, MappingPackage2 and MappingPackage3 which allows functions to be created and manipulated in this way (although there are warnings this may have bugs).
However it is not possible to 'generate' one domain from another because domains are not first class objects and they cannot be created at runtime.
See notes below
An SPAD entity where we can construct elements.
So it must have at least one type signature, with implementation, of this form:
(....) -> %
In SPAD virtually all the library extends set. Its hard to see how a domain could be created that is not derived from something set-like.
SPAD does not provide a mechanism for enforcing axioms for instance (external properties of the category). Each implementation of a domain has to be implemented in such a way that it obeys the axioms. This makes it hard to use category theory principles.
Domains are objects in some (sub)-category.
A mathematical structure. Concrete Categories are either derived from set (by adding structure) or are isomorphic to such.
The category theoretic approach tends to concentrate on the external properties rather than this internal structure.
Example of concrete categories are:
See notes below
Generalisation of concrete category above. Properties can be expressed which are common to many concrete categories.
Allows a set of function signatures (function declarations) to be grouped together.
This can then be extended by domains and so provides a common 'interface' to those domains, that is allow the category to stand in for a domain under certain circumstances. Domains can inherit from multiple categories and so this allows a lattice structure of mathematical entities to be built.
Function definitions can also be included in SPAD categories.
Categories are not first class. (first class means an entity where the following operations can be done without restriction: constructed at run-time, passed as a parameter, returned from a function, or assigned into a variable) more.
An element of a category which we treat like a black-box in that we do not look inside it. It can have external properties though such as being initial or final.
SPAD is not object oriented in that instances do not have dynamic pointers to an object.
In the category theory sense SPAD does have some object-like properties in that domains allow some degree of encapsulation (not all functions are available externally).
A generalisation of morphism above to allow different categories to be compared.
They are represented as arrows G->H
A Functor preserves some structure so there must be some map:
map: (a->b) -> (F a -> F b)
where F is a functor
If defined in a type constructor this might have signature:
map : ((S -> S),%) -> %
From the definition on the left we would expect a functor to have the signature:
Where each type is a particular category.
However in SPAD terminology 'functor' is defined like this:
In other words 'functor' is used to refer to 'type constructor' see above. This is defined at compile-time. What is called a "functor" in Axiom might not be exactly what is called a functor in mathematics. In particular there is no specific requirement in Axiom that a functor actually be functorial, i.e. that it export a suitable 'map' operation.
When modeling category-theoretic functors it would be interesting to create and model them at runtime in this form:
where G and H are categories.
Again, we cannot generate H at runtime because categories are not first class.
A morphism from two categories to another category
(G1,G2) -> H
This must preserve structure:
where F is a bifunctor
If defined in a type constructor this might have signature:
map : (((S,S) -> S),%,%) -> %
Examples of bi-functor are Cartesian product and sum.
Similar to functor but defined like this:
A Cartesian product could be defined like this:
and a sum like this:
A functor from a category to itself
Type constructors can be nested, for instance lists (we can have lists of lists of lists)
If we want to model this in SPAD then I guess we need some inductively defined type:
Rep = Union(basetype,List %)
So an endofunctor is defined as a kind of mapping
T: X -> X
where B is in (i.e. satisfies) some category X. T applied to B is a domain, T applied to T applied to B is a domain - all in the same category X.
Similarly, T^2, i.e. T applied to T applied to _, is an endofunctor
T^2 : X -> X
A means of comparing two funtors with the same source and target which obey natuarlity law. (morphism of functors)
it would be interesting to manipulate in this form:
Endofunctor, together with two natural transformations which obey certain laws.
The category currently called monad is not a category theoretic monad (perhaps this comes from some older terminology?) Why not rename it?
Attempt at defining monad on this page:
MonadCat(A : Type, M: Type -> Type): Category == with
endofunctor (M) has to be defined separately. and there is not much validation or type checking, for instance Type -> Type does not enforce endofunctor.
In the context of monads then the associated algebra is a T-Algebra
The whole subject of SPAD is algebra rather than being an element of it.
However there may be value in modeling T-algebra as a subset in the hope that it could be defined in terms of its external properties rather than building up from set.
There is more terminology that might be useful here. When Googling this subject there is masses of stuff around monads and Haskell. I get the impression that Haskell monads are not derived from functors but people seem to think they should be (and in some libraries they are). Haskell also seems to have the concept of 'applicative functors' which are half way between functors and monads. I have only seen these terms defined in a Haskell context by giving examples. Has anyone come across the terms:
- Applicative functor
- Generative functor
- Generative type
in this more general context? Would they be useful here? How would you define them?
Martin, I do not agree with the first entry in your table.
An Axiom category corresponds to a particular type of mathematical concrete category. As in the discussion of Haskell and the Hask category, we can call the mathematical category that underlies Axiom Ax. Ax consists of all domains and all operations built-in to SPAD and defined in the Axiom library and all the other domains and function compositions that can be formed from these in SPAD code. The Axiom category Type corresponds to the mathematical category Ax. The Ax category is actually rather large and complex since it includes are products (Record) and co-products (Union) as well as exponential objects involving Mapping and function application. So it is at least a bi-cartesian closed category . Axiom only partially implements the notion of sub-object classified (sub-domain) but if this was complete it would make Ax a particular kind of topos . I think this is important since it strongly suggests how one could extend and generalize Axiom in a categorical manner.
An Axiom domain corresponds to an object in some category. In Axiom a domain is said to "satisfy" one or more Axiom categorys. Operators (functions) are morhphisms (arrows) in some category.
Axiom categories act like logical predicates. We can Join Axiom categories (as in lattice theory) to form more specific categories. (Aldor also implements an undocumented dual category lattice operation called Meet ). Axiom categories state some known facts about the morphisms (exported operators) in domains. For example, we can write:
Integer has SetCategory
Axiom returns either
true in this case). Mathematically we interpret this as representing the fact that the integers form a set and so are an object in the category SET. But Axiom categories are not just lists of exports. The actual name of an Axiom category is normally directly associated with some mathematical concept. It is unfortunate of course that Axiom has no direct way to enforce mathematical axioms. Instead a category is a kind of "contract" with other library developers and Axiom users.