diff --git a/books/bookvol2.pamphlet b/books/bookvol2.pamphlet index 869c1e7..da71de9 100644 --- a/books/bookvol2.pamphlet +++ b/books/bookvol2.pamphlet @@ -299,6 +299,85 @@ November 10, 2003 ((iHy)) \eject \pagenumbering{arabic} \setcounter{chapter}{0} % Chapter 1 +\chapter{Axiom and Category Theory} +\section{Covariance and Contravariance} +Axiom has an order relation between types. The types can be in one of +five possible relationships. + +A type can be more general than another type. For example, Integer is +more general than PositiveInteger. + +A type can be more specific than another type. Conversely PositiveInteger +is more specific than Integer. + +A type can be equal to another type. + +A type can be converted or coerced to another type. For example, +Fraction(Polynomial(Integer)) can be coerced to Polynomial(Fraction(Integer)). + +A type can be unrelated to another type. String and Expression are not related. + +Covariance is converting from a wider type to a narrower type. +For instance, converting from Matrix(Float) to Matrix(Integer). + +Contravariance is converting from a narrower type to a wider type. +For instance, converting from Matrix(Integer) to Matrix(Float). + +Invariance means that one type cannot convert to another. +For instance, a Matrix(Float) which contains numbers which cannot +be represented as Integers cannot be converted to a Matrix(Integer). + +These facts form an order relation, which by definition is reflexive, +transitive and antisymmetric. + +Reflexive means that Integer = Integer. + +Transitive means that PositiveInteger $<$ Integer $<$ Float implies +that PositiveInteger $<$ Float. + +Antisymmetric means that PositiveInteger $<$ Float implies +not(Float $<$ PositiveInteger). + +\section{Axiom Type Lattice} + +The types in Axiom form a lattice based on the order relationship. +It is a lattice because Axiom supports multiple inheritance. + +References of interest include: + +Michael Barr and Charles Wells +``Category Theory for Computing Science'' 1998\\ +\verb|www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf| + +Saunders Mac Lane +``Catogories for the Working Mathematician''\\ +Springer-Verlag 2010 ISBN 978-1-4419-3123-8 + +Steve Awodey +``Category Theory''\\ +\verb|ftp://sumin.in.ua/Books/DVD-021/Awodey_S._Category_Theory(en)(305s).pdf| + +``Introduction to Category Theory''\\ +\verb|www.youtube.com/watch?v=eu0rj5C2Otg| + +Luca Cardelli and Peter Wegner +``On understanding types, data abstraction and polymorphism'' +Computing Surveys, Vol 17 no 4 pp471-522 Dec. 1985\\ +\verb|lucacardelli.name/Papers/OnUnderstanding.A4.pdf| + +A. J. H. Simons, +``Adding Axioms to Cardelli-Wegner Subtyping'' 1994\\ +\verb|staffwww.dcs.shef.ac.uk/people/A.Simons/research/reports/addaxiom.pdf| + +Dana Scott +``Data Types as Lattices''\\ +\verb|www.cs.ox.ac.uk/files/3287/PRG05.pdf| + +Roland Backhouse and Marcel Bijsterveld +``Category Theory as Coherently Constructive Lattice Theory'' +November 1994 + +\chapter{Implementation Details} \section{Makefile} This book is actually a literate program\cite{2} and can contain executable source code. In particular, the Makefile for this book diff --git a/changelog b/changelog index 9638126..fa951a8 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,5 @@ +20130314 tpd src/axiom-website/patches.html 20130314.11.tpd.patch +20130314 tpd books/bookvol2 Axiom and Category Theory chapter 20130314 tpd src/axiom-website/patches.html 20130314.10.tpd.patch 20130314 tpd buglist MLIFT fix 20001, add 20568 20130314 tpd books/bookvol10.3 MLIFT fix 20001, add 20568 diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 84c5dba..fcbba16 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -4049,5 +4049,7 @@ books/bookvol10.3 SINT fix 20057 pretend books/bookvol10.3 SMTS fix 20383, 50005, add 20567 20130314.10.tpd.patch books/bookvol10.3 MLIFT fix 20001, add 20568 +20130314.11.tpd.patch +books/bookvol2 Axiom and Category Theory chapter