login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

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).

Mathematical Terminology Related SPAD Terminology

Type

Types describe possible elements of a mathematical structure.

Types were introduced into mathematics in order to avoid certain paradoxes and to avoid statements or expressions which cannot be given a consistent interpretaton.

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.

Type Constructor

a type that depends on another type

more

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:

MyDomain(IntegerDomain)

If MyDomain is used on its own it is considered a function of type RingCategory -> E that returns a domain.

This is also known as a functor, since it maps each domain in one category to some domain in another category, and at least implicitly maps the operations exported by the first domain to operations exported by the second domain (via polymorphism, .e.g. + of Integer becomes + of Complex Integer). See Functor below

Dependent Type

a type that depends on a term

Dependent Type

MyDomain(t: Integer, x:SquareMatrix(t,Integer)) : E(t) == I(t) where ....

The types of other parameters, the type of the resulting domain E(t) and it's implementation I(t) can all depend on the actual parameters.

This can be used as a type when values are supplied for all arguments, for instance,

MyDomain(3,[[1,2,3],[4,5,6],[7,8,9]])

There is limited support for dependent types in SPAD. Details of limitations?

Term

a component of a mathematical expression

SPAD supports elements of a domain (constants or literals) and variables that stand for these elements.

Polymorphism

Terms depending on types. For instance a function could be defined that applies to many types.

Which types of polymorphism are supported?

Expression

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

Morphism

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

Domain

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.

Concrete 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:

• Sets
• Groups
• Rings
• ...

more

See notes below

Category

Generalisation of concrete category above. Properties can be expressed which are common to many concrete categories.

more

Category

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.

Object

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).

Functor

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),%) -> %

Functor

From the definition on the left we would expect a functor to have the signature:

myFunctor:Type->Type

Where each type is a particular category.

However in SPAD terminology functor is defined like this:

myFunctor(Type)

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:

myFunctor: G->H

where G and H are categories.

Again, we cannot generate H at runtime because categories are not first class.

BiFunctor?

A morphism from two categories to another category

(G1,G2) -> H

This must preserve structure:

bimap: (a->b)->(c->d)->F(a,c)->F(b,d)

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.

BiFunctor?

Similar to functor but defined like this:

myBiFunctor(Type,Type)

A Cartesian product could be defined like this:

Record(Type,Type)

and a sum like this:

Union(Type,Type)

Endofunctor

A functor from a category to itself

Type constructors can be nested, for instance lists (we can have lists of lists of lists)
again it would be interesting to manipulate in this form:
myEndofunctor: G-> G

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

Natural Transformation

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:
myNT: (G->H) -> (G->H)
in the case of an endofunctor we can compare to itself:
(G->G) -> (G->G)
but id is also G->G so we can have, for instance
id -> (G->G)
and if T is of type G->G
then T^n is also of type G->G

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?

MonadCat?(A : Type, M: Type -> Type): Category == with
unit: A -> M A
join: M M A -> M A
mult: (M A, M A) -> M A

endofunctor (M) has to be defined separately. and there is not much validation or type checking, for instance Type -> Type does not enforce endofunctor.

Algebra

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:

1. Applicative functor
2. Generative functor
3. Generative type

in this more general context? Would they be useful here? How would you define them?

Concrete Category (math) versus Domain (Axiom) --Bill Page, Thu, 17 Nov 2011 10:48:26 -0800 reply
Martin, I do not agree with the first entry in your table - (MJB - I've changed the entry this comment refers to).

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 or false (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.

re: Concrete Category (math) versus Domain (Axiom) --Martin Baker, Thu, 17 Nov 2011 11:04:14 -0800 reply
Bill, This is interesting stuff, feel free to modify the table, perhaps a summary should go in the table with a link to this detail?

BTW - I coded the table in HTML because I have HTML editors which make it much easier for me, but if you prefer other coding feel free to change it.

 Subject:   Be Bold !! ( 15 subscribers )