

last edited 10 years ago by Bill Page 
11  
Editor: Bill Page
Time: 2011/12/24 05:56:41 GMT8 

Note: types 
changed:  <p>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.</p> <p>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.</p> <p>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).</p> <p><a href="http://axiomwiki.newsynthesis.org/CategoryTheoryAndAxiom">see also</a> </p> <table border="1"> <tr> <th bgcolor="#FFFF00" scope="col">Mathematical Terminology </th> <th bgcolor="#FFFF00" scope="col">Related SPAD Terminology </th> </tr> <tr> <td><h2>Type</h2> <p>Types describe possible elements of a mathematical structure.</p> <ul> <li><a href="http://en.wikipedia.org/wiki/Type_(model_theory)">in model theory</a></li> <li><a href="http://en.wikipedia.org/wiki/Type_theory">in type theory </a></li> </ul> <p>Types were introduced into mathematics in order to avoid certain paradoxes and to avoid statements or expressions which cannot be given a consistent interpretaton.</p></td> <td><h2>Type</h2> <p>Generally the word 'type' could be used for something that is either a Domain, Category (or Package ?).</p> <p>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. </p> <p>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. </p></td> </tr> <tr> <td><h2>Type Constructor</h2> <p>a type that depends on another type </p> <p><a href="http://en.wikipedia.org/wiki/Type_constructor">more</a></p></td> <td><h2>Type Constructor or Functor</h2> <pre>MyDomain(n: RingCategory) : E == I where .... </pre> <p>This can be used as a type when supplied with a domain which derives from the category used in the definition:</p> <pre>MyDomain(IntegerDomain)</pre> <p>If 'MyDomain' is used on its own it is considered a function of type 'RingCategory > E' that returns a domain.</p> <p>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":http:/SandBoxCategoryTerms#functor below </p></td> </tr> <tr> <td><h2>Dependent Type </h2> <p>a type that depends on a term</p></td> <td><h2>Dependent Type </h2> <pre>MyDomain(t: Integer, x:SquareMatrix(t,Integer)) : E(t) == I(t) where .... </pre> <p>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.</p> <p>This can be used as a type when values are supplied for all arguments, for instance,</p> <pre>MyDomain(3,[[1,2,3],[4,5,6],[7,8,9]])</pre> <p>There is limited support for dependent types in SPAD. Details of limitations? </p></td> </tr> <tr> <td><h2>Term</h2> <p>a component of a mathematical expression</p></td> <td>SPAD supports elements of a domain (constants or literals) and variables that stand for these elements.</td> </tr> <tr> <td><h2>Polymorphism</h2> <p>Terms depending on types. For instance a function could be defined that applies to many types. </p></td> <td>Which types of polymorphism are supported? </td> </tr> <tr> <td><h2>Expression</h2> <p>Wellformed combination of symbols.</p></td> <td><p>We could define an expression inductively like this: </p> <p>Rep = Union(op:Symbol,first:%,second:%) </p> <p>or we could use builtin domains Expression or Kernel </p></td> </tr> <tr> <td><h2>Morphism</h2> <p>Allows us to compare certain concrete categories (preserve certain elements of structure) </p> <p>If f is a structurepreserving mapping from G to H. If g1 and g2 are elements of G then the structure '*' is preserved if: </p> <p>f(g1 * g2) = f(g1) * f(g2)</p> <p>If '*' is the only structure in H then we might tend to think of f 'generating' H from G </p></td> <td><h2>Morphism and Mapping </h2> <p>Many domains in the SPAD library have a map function. </p> <p>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).</p> <p>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. </p></td> </tr> <tr> <td><p>"See notes below":http:#msg201111171048260800@axiomwiki.newsynthesis.org</p></td> <td><h2>Domain</h2> <p>An SPAD entity where we can construct elements.</p> <p>So it must have at least one type signature, with implementation, of this form: </p> <p>(....) > %</p> <p>In SPAD virtually all the library extends set. Its hard to see how a domain could be created that is not derived from something setlike.</p> <p>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.</p> <p>Domains are objects in some (sub)category. </p></td> </tr> <tr> <td><h2>Concrete Category </h2> <p>A mathematical structure. Concrete Categories are either derived from set (by adding structure) or are isomorphic to such.</p> <p>The category theoretic approach tends to concentrate on the external properties rather than this internal structure. </p> <p>Example of concrete categories are:</p> <ul> <li>Sets</li> <li>Groups</li> <li>Rings</li> <li>... </li> </ul> <p><a href="http://en.wikipedia.org/wiki/Concrete_category">more</a></p></td> <td><p>See notes below</p></td> </tr> <tr> <td><h2>Category</h2> <p>Generalisation of concrete category above. Properties can be expressed which are common to many concrete categories.</p> <p><a href="http://en.wikibooks.org/wiki/Haskell/Category_theory">more</a></p></td> <td><h2>Category</h2> <p>Allows a set of function signatures (function declarations) to be grouped together.</p> <p>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. </p> <p>Function definitions can also be included in SPAD categories. </p> <p>Categories are not first class. (first class means an entity where the following operations can be done without restriction: constructed at runtime, passed as a parameter, returned from a function, or assigned into a variable) <a href="http://en.wikipedia.org/wiki/Firstclass_object">more</a>.</p></td> </tr> <tr> <td><h2>Object</h2> <p>An element of a category which we treat like a blackbox in that we do not look inside it. It can have external properties though such as being initial or final. </p></td> <td><p>SPAD is not object oriented in that instances do not have dynamic pointers to an object.</p> <p>In the category theory sense SPAD does have some objectlike properties in that domains allow some degree of encapsulation (not all functions are available externally). </p></td> </tr> <tr> <td><a name="functor"><h2>Functor</h2></a> <p>A generalisation of morphism above to allow different categories to be compared.</p> <p>They are represented as arrows G>H</p> <p>A Functor preserves some structure so there must be some map:</p> <p>map: (a>b) > (F a > F b)</p> <p>where F is a functor</p> <p>If defined in a type constructor this might have signature: </p> <p>map : ((S > S),%) > % </p></td> <td><h2>Functor</h2> <p>From the definition on the left we would expect a functor to have the signature:</p> <p>myFunctor:Type>Type</p> <p>Where each type is a particular category. </p> <p>However in SPAD terminology 'functor' is defined like this: </p> <p>myFunctor(Type)</p> <p>In other words 'functor' is used to refer to 'type constructor' see above. This is defined at compiletime. 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.</p> <p> When modeling categorytheoretic functors it would be interesting to create and model them at runtime in this form:</p> <p>myFunctor: G>H</p> <p>where G and H are categories.</p> <p>Again, we cannot generate H at runtime because categories are not first class. </p></td> </tr> <tr> <td><h2>BiFunctor</h2> <p>A morphism from two categories to another category</p> <p>(G1,G2) > H</p> <p>This must preserve structure:</p> <p>bimap: (a>b)>(c>d)>F(a,c)>F(b,d)</p> <p>where F is a bifunctor</p> <p>If defined in a type constructor this might have signature: </p> <p>map : (((S,S) > S),%,%) > %</p> <p>Examples of bifunctor are Cartesian product and sum.</p></td> <td><h2>BiFunctor</h2> <p>Similar to functor but defined like this: </p> <p>myBiFunctor(Type,Type)</p> <p>A Cartesian product could be defined like this:</p> <p>Record(Type,Type)</p> <p>and a sum like this:</p> <p>Union(Type,Type)</p></td> </tr> <tr> <td><h2>Endofunctor</h2> <p>A functor from a category to itself </p></td> <td><p>Type constructors can be nested, for instance lists (we can have lists of lists of lists) <br /> again it would be interesting to manipulate in this form: <br /> myEndofunctor: G> G</p> <p>If we want to model this in SPAD then I guess we need some inductively defined type: </p> <p>Rep = Union(basetype,List %) </p> <p>So an endofunctor is defined as a kind of mapping</p> <p> T: X > X</p> <p>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.</p> <p>Similarly, T^2, i.e. T applied to T applied to _, is an endofunctor</p> <p> T^2 : X > X</p></td> </tr> <tr> <td><h2>Natural Transformation </h2> <p>A means of comparing two funtors with the same source and target which obey natuarlity law. (morphism of functors) </p></td> <td><p>it would be interesting to manipulate in this form: <br /> myNT: (G>H) > (G>H) <br /> in the case of an endofunctor we can compare to itself:<br /> (G>G) > (G>G)<br /> but id is also G>G so we can have, for instance <br /> id > (G>G) <br /> and if T is of type G>G<br /> then T^n is also of type G>G</p> </td> </tr> <tr> <td><h2>Monad</h2> <p>Endofunctor, together with two natural transformations which obey certain laws.</p></td> <td><p>The category currently called monad is not a category theoretic monad (perhaps this comes from some older terminology?) Why not rename it? </p> <p>Attempt at defining monad on <a href="http://axiomwiki.newsynthesis.org/SandBoxMonads#msg201111150725260800@axiomwiki.newsynthesis.org">this page</a>: </p> <p>MonadCat(A : Type, M: Type > Type): Category == with<br /> unit: A > M A<br /> join: M M A > M A<br /> mult: (M A, M A) > M A</p> <p>endofunctor (M) has to be defined separately. and there is not much validation or type checking, for instance Type > Type does not enforce endofunctor. </p></td> </tr> <tr> <td><h2>Algebra</h2> <p>In the context of monads then the associated algebra is a TAlgebra </p></td> <td><p>The whole subject of SPAD is algebra rather than being an element of it.</p> <p>However there may be value in modeling Talgebra as a subset in the hope that it could be defined in terms of its external properties rather than building up from set. </p></td> </tr> </table> <p>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:</p> <ol> <li> Applicative functor</li> <li> Generative functor</li> <li> Generative type</li> </ol> <p> in this more general context? Would they be useful here? How would you define them?</p> From BillPage Thu Nov 17 10:48:26 0800 2011 From: Bill Page Date: Thu, 17 Nov 2011 10:48:26 0800 Subject: Concrete Category (math) versus Domain (Axiom) MessageID: <201111171048260800@axiomwiki.newsynthesis.org> 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 builtin 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 coproducts (Union) as well as exponential objects involving Mapping and function application. So it is at least a "bicartesian closed category":http://en.wikipedia.org/wiki/Cartesian_closed_category . Axiom only partially implements the notion of subobject classified (subdomain) but if this was complete it would make **Ax** a particular kind of "topos":http://en.wikipedia.org/wiki/Topos#Formal_definition . 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":http://axiomwiki.newsynthesis.org/SandBoxAldorJoinAndMeet ). 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. From MartinBaker Thu Nov 17 11:04:14 0800 2011 From: Martin Baker Date: Thu, 17 Nov 2011 11:04:14 0800 Subject: re: Concrete Category (math) versus Domain (Axiom) MessageID: <201111171104140800@axiomwiki.newsynthesis.org> 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.
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 

TypeTypes 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. 
TypeGenerally the word 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 Constructora type that depends on another type 
Type Constructor or FunctorMyDomain(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 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. 
Dependent Typea type that depends on a term 
Dependent TypeMyDomain(t: Integer, x:SquareMatrix(t,Integer)) : E(t) == I(t) where .... The types of other parameters, the type of the resulting domain 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? 
Terma component of a mathematical expression 
SPAD supports elements of a domain (constants or literals) and variables that stand for these elements. 
PolymorphismTerms depending on types. For instance a function could be defined that applies to many types. 
Which types of polymorphism are supported? 
ExpressionWellformed combination of symbols. 
We could define an expression inductively like this: Rep = Union(op:Symbol,first:%,second:%) or we could use builtin domains Expression or Kernel 
MorphismAllows us to compare certain concrete categories (preserve certain elements of structure) If f is a structurepreserving mapping from G to H. If g1 and g2 are elements of G then the structure f(g1 g2) = f(g1) f(g2) If 
Morphism and MappingMany 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 
DomainAn 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 setlike. 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 CategoryA 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 
CategoryGeneralisation of concrete category above. Properties can be expressed which are common to many concrete categories. 
CategoryAllows a set of function signatures (function declarations) to be grouped together. This can then be extended by domains and so provides a common 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 runtime, passed as a parameter, returned from a function, or assigned into a variable) more. 
ObjectAn element of a category which we treat like a blackbox 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 objectlike properties in that domains allow some degree of encapsulation (not all functions are available externally). 
FunctorA 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),%) > % 
FunctorFrom 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 myFunctor(Type) In other words When modeling categorytheoretic 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 bifunctor 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) 
EndofunctorA 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 
Natural TransformationA 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: 
MonadEndofunctor, 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. 
AlgebraIn the context of monads then the associated algebra is a TAlgebra 
The whole subject of SPAD is algebra rather than being an element of it. However there may be value in modeling Talgebra 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:
in this more general context? Would they be useful here? How would you define them?
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 builtin 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 coproducts (Union) as well as exponential objects involving Mapping and function application. So it is at least a bicartesian closed category . Axiom only partially implements the notion of subobject classified (subdomain) 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.
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.