Type

Types describe possible elements of a mathematical structure.

• in model theory
• in type theory

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

Polymorphism

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

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

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

Monad

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