From 1a2bf63b8b104d1b8a6b84cf5ec0febf43833dd7 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 27 Feb 2018 09:32:55 -0500
Subject: [PATCH] books/bookvol10.1 add new chapter
Goal: Axiom Literate Documentation
---
books/bookvol10.1.pamphlet | 1923 ++++++++++++++++++++++++++++++++++++++++
changelog | 2 +
patch | 4 +-
src/axiom-website/patches.html | 2 +
4 files changed, 1929 insertions(+), 2 deletions(-)
diff --git a/books/bookvol10.1.pamphlet b/books/bookvol10.1.pamphlet
index d4d5d16..d7848e2 100644
--- a/books/bookvol10.1.pamphlet
+++ b/books/bookvol10.1.pamphlet
@@ -2494,6 +2494,7 @@ Analysis or LSA. Although the domain is different, the concepts
are the same. We are trying to predict patterns of how words occur
in documents instead of trying to predict patterns of how players
score on holes.
+
\chapter{Quaternions}
from \cite{Altm05}:
\begin{quotation}
@@ -13982,6 +13983,1928 @@ obtained results are applicable to the type inference problem for a
user interface of a computer algebra system.
+\chapter[Type Systems 2]{A Type System for Computer Algebra}
+
+This is based on Santas \cite{Sant95}. Changes have been made to
+integrate it.
+
+Type systems for computer algebra systems like Axiom \cite{Jenk92}
+and theorem provers like
+Nuprl \cite{Cons85}, or
+functional programming languages like Standard ML (SML)
+\cite{Miln90} \cite{Miln91} \cite{Harp93a},
+Haskell \cite{Huda92}, etc. and
+object oriented languages \cite{Meye92} \cite{Gold83} \cite{Grog91}
+are usually stratified into levels or universes in a way similar to type
+theories like
+Damas and Milner's \cite{Dama82} type schemes,
+Martin-Lof's \cite{Mart73} constructive mathematics, etc.
+
+More specifically, Axiom's types are basically divided into
+{\tt domains} and {\tt categories}; Domains are both {\sl types} for
+run-time values like $Integer$, $Integer\rightarrow Boolean$ and
+$Fraction(Integer)$, and {\sl packages} which include definitions of
+other values. Categories are {\sl type} of domains, like $Ring$ and
+$Module(R)$. Categories and domains can be parameterized with other
+domains, allowing the definition of category and domain
+constructors. Categories specify the values defined in domains, and
+can form hierarchies of specifications.
+
+SML's types belong to two universes: $U_1$, which includes {\tt types}
+like $Integer$ and $String \rightarrow Boolean$, and the universe
+$U_2$ of types of {\tt modules}; this system as extended by Mitchell,
+Meldal, and Madhav \cite{Mitc91b} can include existential types
+($\exists$ types) in $U_1$ and dependent product and sum types
+($\Pi$ and $\Sigma$ types) in $U_2$. These two levels correspond
+essentially to the separation into {\tt monomorphic} and
+{\tt polymorphic} type expressions in the Damas and Milner
+\cite{Dama82} system. {\sl Monotypes} are arbitrary base types, an
+infinite number of {\tt type variables} and the types built from other
+monomorphic types through function space constructor $\rightarrow$.
+{\sl Polytypes} are the types which range over monotypes, through the
+universal quantifier $\forall$, like the type of the identity
+function: $\forall t.t\rightarrow t$. Since every monotype $\tau$ can
+be viewed as a polytype (like application of $\forall t.\tau$ to any
+monotype where $t$ is a type variable which does not exist in the type
+expression $\tau$), we assume that there is an injection from
+$U_1$ to $U_2$.
+
+On the other side of the camp, object oriented languages include the
+notions of {\tt class} and {\tt abstract class}, resulting in (a)
+implementation classes which can define {\tt objects}, and (b)
+abstract classes used explicitly for inheritance and specification of
+behaviour.
+
+The two-universe approach in Axiom has been designed and proved
+beneficial for the modeling of algebraic concepts, where
+{\sl categories} correspond to {\sl algebras} and {\sl domains} to
+sets of values which share common representation and functionality as
+described by Davenport, Trager \cite{Dave90} and Gianni
+\cite{Dave91}. Similar results have been accomplished in object
+oriented languages like C$++$ \cite{Stro95}, where abstract classes
+play the role of categories, while implementation classes model
+domains in Barton and Nackman \cite{Bart94}. On the other hand, the
+two universes and their corresponding elements in SML were design
+decisions for purely type-theoretic reasons. Although approaches vary,
+it is possible to define a mapping of the constructs defined in typed
+computer algebra systems to constructs of type theory similar to the
+ones used for the definition of programming languages like SML. This
+is important in two ways: it clarifies the semantics of computer
+algebra systems, and allows their further improvement by means of
+extensions, removal of inconsistencies, more expressiveness, and
+better performance. We try to accomplish these targets with the
+definition of a strong and static type system based on a powerful
+subset of the Axiom system, which we extend incrementally.
+
+We briefly examine some of the most recent concepts for object
+oriented programming and abstract datatypes for computer algebra
+systems. We observe that these concepts although quite powerful are
+not adequate for the properly typed modeling of the relations among
+simple algebraic constructs like the domains of integers and
+rationals.
+These concepts are simplified and integrated with the notions of
+domains and categories. We provide the formal definition of domain
+categories by means of existential types and the calculus for
+subtyping on categories. Our type system is enriched with transparent
+types which form the main construct of the sharing mechanism. Domains
+are extended to form packages while their corresponding types form
+dependent sums. Parameterized categories and functors are examined and
+their calculus is defined with subtyping rules. Sharing constraints
+are proved to handle many cases of parameterization resulting in
+flattening of parameterized categories with facilities for recursive
+definitions at the category level; there we establish the conditions for
+successful functor application. This reduces the load of the type
+system considerably, so as to afford the inference and manipulation of
+type classes.
+
+Since Axiom has the most references in the literature of typed
+computer algebra systems, the notation used here is based on an
+Axiom-like language which assumes:
+\begin{enumerate}
+\item values which consist of value variables, records, record
+components, (higher order) functions, term application, value
+components of packages and {\sl let} expressions
+\item type expressions with type variables, base types, record types,
+tagged unions, recursive types, function types, type components from
+packages, type constructors, and type application
+\item domain expressions with domain variables, self, domain
+constructors, parameterized domains and application
+\item expressions which can be used either as domains or types
+\item packages with package variables, package constructors, package
+components of other packages, parameterized packages and application
+\item categories with category variables, sharing, category
+constructors, parameterized categories and application
+\item sharing constraints
+\item facilities for accessing package components
+\end{enumerate}
+
+The abstract syntax of the language is given by the following grammar:
+\[\begin{array}{ll}
+{\rm values:} & e ::= x~|~\{x_i=e\}_{\forall i\in I}~|~e.x~|~
+(x:\delta)\mapsto e~|~e~e~|~x\$w~|~ let~x : \phi := e~in~e\\
+{\rm types:} & \tau ::= t~|~T~|~\{x_i:\tau\}_{\forall i\in I}~|
++[x_i:\tau]_{\forall i\in I}~|~\mu t.\tau~|~t\$\omega~|~
+\tau\rightarrow\tau~|~t\mapsto\tau~|~\tau~\tau\\
+{\rm domains:} & \delta ::= d~|~\%~|~add(\overline{\delta})~|~
+(d:\sigma)\mapsto\delta~|~\delta~\omega\\
+{\rm both:} & \phi ::= \delta~|~\tau\\
+{\rm packages:} & \pi ::= m~|~add(\overline{\pi})~|~m\$\omega~|~
+(m:\sigma)\mapsto\pi~|~\pi~\pi\\
+{\rm categories:} & \sigma ::= c~|~with(\overline{\sigma})~|~
+(m:\sigma)\mapsto\sigma~|~c~\omega\\
+\delta-{\rm comps:} & \overline{\delta} ::= \emptyset~|~
+Rep:=\phi;\overline{\delta}~|~x:=e;\overline{\delta}~|~
+\delta;\overline{\delta}\\
+\pi-{\rm comps:} & \overline{\pi} ::= \overline{\delta}~|~
+m:=\pi;~\overline{\pi}~|~t:=r;~\overline{\pi}~|~\pi;~\overline{\pi}\\
+\sigma-{\rm comps:} & \overline{\sigma} ::= \emptyset~|~
+m:\sigma ;~\overline{\sigma}~|~t:Type;~\overline{\sigma}~|~
+s;~\overline{\sigma}~|~x:\tau;~\overline{\sigma}~|~
+\sigma;~\overline{\sigma}\\
+{\rm sharings:} & s ::= t=\tau~|~t=d~|~t=d\$w~|~m=\omega\\
+{\rm access:} & \omega ::= m~|~\omega~\omega~|~m\$\omega\\
+\end{array}\]
+
+The components inside the {\sl with} and {\sl add} constructs are
+optional. {\sl let} expressions can be defined for types, domains,
+packages, and categories. Declarations in value expressions are
+optional, thus $let~x:=e~in~e$ is valid too. Wherever we have
+$t=thing$ or $t:Type$ we can assume also that $Rep=thing$ and
+$Rep:type$ is allowed, but not vice versa. Records with $n>0$
+components are represented as
+$\{x_i:\tau\}_{\forall i\in\{1,\ldots,n\}}$. Similarly for unions,
+replacing \{\} with $+[]$. Values can include $n$-tuples of the form
+$(e,\ldots,e)$ which are implicitly viewed as records indexed by
+integers from 1 to $n$; the expression $()$ is the empty tuple and is
+the same as \{\}; there are no 1-tuples. Tagged unions can model
+enumerated types or variations as in:
+
+$\quad bool:=true = false$
+
+$\quad tree(t:Type):=empty + node : (tree~t, tree~t) + leaf : t$
+
+The syntax of this language hardly distinguishes between domains and
+packages; this comes in accordance with the Axiom language where
+domains are packages. Since domains can be used in a context where
+types are expected, $\phi$ defines a dummy union of domains and
+types. Types can be lifted to domains, and the representation of
+domains can be viewed as type. The exact transformations are examined
+in what follows; this allows us to have domains in union and record
+types without complicating the language. Additionally packages assume
+the arrow types as special cases of $\Pi$ types where there are no
+dependencies between the domain and the range of the types.
+
+The calculus of the presented type system is given by a set of
+selected rules. Each rule has a number of antecedent judgments above a
+horizontal line (optional) and a conclusion judgment below the
+line. Each judgment has the form $E\vdash\mathcal{A}$, for an
+environment $E$ and an assertion $\mathcal{A}$, depending on the
+judgment. Environments contain typing assumptions for variables, type
+variable declarations and subtyping assumptions. Typical judgments are
+$E\vdash x$ asserting that $x$ is definable in $E$, $E\vdash x:\sigma$
+meaning that $x$ has type $\sigma$ under assumptions $E$ and
+$E\vdash \sigma^\prime\sqsubseteq\sigma$ asserting that
+$\sigma^\prime$ is a subtype of $\sigma$ (or equivalently,
+$\sigma$ is a supertype of $\sigma^\prime$) in $E$; we demand that all
+the environments be well formed. An environment can be extended
+with new assumptions as in $E;x:\sigma;E^\prime\vdash x:\sigma;$ this
+environment is well formed provided that there is no other assumption
+for $x$ in $E;E^\prime;$ variables can be renamed in case of
+conflicts.
+
+Some of the examples given have been influenced by the modeling of
+algebraic concepts in the Axiom library.
+
+Although demonstration of the simplicity of our type system is out of
+the scope of this chapter, we claim that it combines the concepts of
+{\tt domain} and {\tt package} and Haskell-like {\tt type classes}, it
+increases the expressiveness of the programs with the propagation of
+sharing constraints, it distinguishes compile time and run-time
+constructs allowing for static and strong type checking and more
+optimizations and reduces the need for {\tt coercions} and
+{\tt retractions} (described in Sutor and Jenks \cite{Suto87} and
+analyzed by Fortenbacher \cite{Fort90} in Axiom.
+
+\subsection{Object in Computer Algebra}
+
+Many computer algebra operations involve purely functional objects:
+functions or methods operate on objects and return a new object with a
+new internal state, instead of updating the state of an older
+object. If the objects are big (like lists, arrays, or polynomials)
+then in-place updating is more common. In object-oriented programming
+however there is always an updating of the internal state of an
+object: an {\tt object} must be a {\tt reference}. Due to the poor
+type-theoretic properties of references and side-effects, most type
+theoretic accounts of object-oriented programming by
+Cardelli and Wegner \cite{Card85},
+Cardelli \cite{Card86},
+Ghelli \cite{Ghel91},
+Pierce \cite{Pier91},
+etc. deal with purely functional objects and employ techniques used
+for purely functional closures, or define special constructors for
+dealing with the increased complexity of object subsumption and
+effects.
+
+Object oriented languages usually take one object (e.g. a rational
+number) with methods and functions for reading and updating its
+numerator and denominator or performing addition among rationals - to
+be an element of a recursively defined type (Bruce and Mitchell
+\cite{Bruc92}) like:
+\begin{verbatim}
+Rational : Category := with (
+ new: (Integer,Integer) -> Rep ;
+ numerator: Rep -> Integer ;
+ denominator: Rep -> Integer ;
+ SetNumDenom: Rep - (Integer,Integer) -> Rep ;
+ + : Rep -> Rep -> Rep ;
+ * : Rep -> Rep -> Rep ; etc. )
+\end{verbatim}
+where {\sl Rep} stands for the type under scope, here {\sl Rational},
+or any subtype of {\sl Rational}.
+
+This encoding hides the fact that Rationals may have an internal state
+that is shared by all its methods: the responsibility for building a
+new instance of Rational in response to a call to {\sl new} is placed
+within the function {\sl new} itself. Another notation identifies the
+representation of instances with the implementation of the
+representation, as in Pierce and Turner \cite{Pier93}
+\begin{verbatim}
+RationalFun := (Rep: Type) -> with (
+ new: (Integer,Integer) -> Rep ;
+ numerator: Rep -> Integer ;
+ denominator: Rep -> Integer ;
+ SetNumDenom: Rep -> (Integer,Integer) -> Rep ;
+ + : Rep -> Rep -> Rep ;
+ * : Rep -> Rep -> Rep, etc. )
+\end{verbatim}
+
+This method gives the caller of {\sl new} the responsibility for
+transforming the value returned by {\sl new} into a new Rational
+instance. Although this notation may seem strange, it offers much in
+terms of {\sl simplicity}: the entire development, including the
+notions of {\sl Rep}, can be carried out without the need of
+{\tt recursive types}, dealt by Amadio and Cardelli \cite{Amad93}
+or {\tt extensible records} (Cardelli \cite{Card88a}, Mitchell
+\cite{Mitc88a}, Wirth \cite{Wirt88}) which are implementation
+dependent; however, expressiveness is sacrificed. Using recursive
+types the above expressions can have any desirable formulation as in
+\begin{verbatim}
+RationalFun := (Rep < F(Rep)) -> with (
+ new: (Integer,Integer) -> Rep ;
+ etc. )
+\end{verbatim}
+where {\bf F} can be the functor {\sl RationalFun} itself. This
+formulation is closer to our intuition about object-oriented
+programming with subtypes. It can be further enriched with other
+second-order constructs, which lead to the definition of special
+{\tt object constructors} by Abadi and Cardelli (\cite{Abad94}
+\cite{Abad94a}).
+
+These scheme are based on {\tt existential types}
+(Mitchell and Plotkin \cite{Mitc88})
+which hide the implementation of the objects,
+allowing us to deal with first class {\tt abstract types}
+(Liskov \cite{Lisk79},
+Burstall and Lampson \cite{Lamp88},
+Milner and Tofte \cite{Miln91},
+Bruce and Mitchell \cite{Bruc92})
+independently of implementation details without
+any cost in type safety. In the next sections we present some examples
+of the advantages and the limitations of this approach: this leads us
+to the introduction of constructs which make the representations
+visible in order to add more flexibility to the type system keeping it
+consistent and sound while increasing the efficiency of the
+implementations.
+
+{\sl RationalFun} is actually the type of a {\tt functor}, i.e. a
+{\sl function from types to types} and specifies the visible behaviour
+of the functions on rationals, in terms of the
+{\sl abstract representation type}. An object satisfying this
+specification consists of a list of functions of type
+{\sl RationalFun(Rep)} for some concrete type {\sl Rep}, paired with a
+state of type {\sl Rep}: both are surrounded with an abstraction
+barrier that protects the {\tt internal structure} from access except
+through the above specified functions. By internal structure we mean
+either the internal state, or the hidden functions that operate on
+this state, or any other operation including the ones mentioned in the
+specification. This encapsulation is directly expressed by a (possibly
+recursively defined) existential type:
+\begin{verbatim}
+Rational:=((Rep: Type) +> with (Rep, RationalFun(Rep))) SomeRep
+\end{verbatim}
+Abstracting {\sl RationalFun} from {\sl Rational} yields a higher
+order type operator that, given a specification, forms the
+{\tt type} of objects that satisfy it.
+\begin{verbatim}
+DeclareDomain := (Fun: Type -> Category) +>
+ (((Rep: Type) +> with(Rep,Fun(Rep))) SomeRep)
+\end{verbatim}
+The type of {\sl Rational} objects can now be expressed by applying
+the {\sl DeclareDomain} constructor to the specification of
+{\sl RationalFun}:
+\begin{verbatim}
+Rational := DeclareDomain(RationalFun)
+\end{verbatim}
+or the shortcut:
+\begin{verbatim}
+Rational : RationalFun
+\end{verbatim}
+
+In order to give proper treatment to the interaction between
+representations and subtyping, it is necessary to separate
+{\sl Rational} into the specifications of its functions and the
+operators which capture the common structure of all object types. This
+separation is also important for the semantical construction of
+categories and the definition of the internal structures of the types.
+
+\subsection{Multiple Representations}
+
+Rationals are created using the function {\sl box}, which captures the
+semantics of dynamic objects in object oriented programming. A
+rational number with {\tt representation} (x:Integer,y:Integer),
+{\tt internal state} (5,2) and method implementations:
+\begin{verbatim}
+numerator := (r:{x:Integer, y:Integer}) +> r.x
+denominator := (r:{x:Integer, y:Integer}) +> r.y
+\end{verbatim}
+can be created as:
+\begin{verbatim}
+r: := box ( coerceTo ( ( Rep := {x:=5, y:=2},
+ (numerator := (r:{x:Integer,y:Integer}) +> r.x ;
+ + := (r:{x:Integer,y:Integer}) +> (arg: Rational) +>
+ new((r.x*denominator arg + r.y*numerator arg)/
+ (r.y * denominator arg)
+ etc. )),
+ Rational ))
+\end{verbatim}
+
+The {\sl coerce} function here is only a syntactic construct, which
+shows the compiler how to view the introduced list; in this example it
+is the identity function since we provide exactly what is necessary
+for building a rational.
+
+The {\sl box} function is helpful for the implementation of the
+{\sl new} function and the $+$ and $*$ operators which return new
+instances of Rational:
+\begin{verbatim}
+new:=(initX:Integer, initY:Integer) +>
+ box ( coerceTo ( (Rep:={x:=initX,y:=initY},...), Rational))
+\end{verbatim}
+
+Unlike Axiom, in object oriented systems based on {\tt delegation}
+(Ungar and Smith \cite{Unga91}) or on {\tt subtyping} the elements of an
+object type have different internal representations and different
+internal representations of their functions. For example, a rational
+with representation type $(x:Integer)$ might be implemented as
+follows:
+\begin{verbatim}
+r2 := box ( coerceTo ( (Rep := {x:=5},
+ (numerator := (r:{x:Integer}) +> r.x ;
+ denominator := (r:{x:Integer}) +> 1 ;
+ + := (r:{x:Integer}) +> (arg:Rational) +> new(r.x + numerator arg) ;
+ etc. )),
+ Rational ))
+\end{verbatim}
+and the definition of {\sl new} changes accordingly. The functions
+{\sl SetNumDenom, numerator, denominator} have compatible signatures
+as in the previous implementation since we abstract
+$s:\{x:Integer\}$ to $s:Rep$.
+
+Static type checking can be obtained even without having all the
+information about the internal structure of the objects. The constants
+0 and 1 can be implemented in any of the two ways, having $x$ assigned
+to 0 and 1 respectively, while the $y$ field can be 1. This
+variability will be helpful for defining type classes in a later
+section.
+
+Type checking however is complicated by the evaluation
+process. Suppose that we invoke the function {\sl SetNumDenom} passing
+to it the object $r_2$. We have to open $r_2$, and make sure that the
+only functions applicable to its {\sl Rep} are the ones declared in
+{\sl Rational}. Consequently we produce a new value of type {\sl Rep},
+which is {\sl reboxed} as a rational number which has access to the
+methods of $r_2$, and hides {\sl Rep}. The same process happens for
+functions like $+$ and $*$. The functions {\sl numerator} and
+{\sl denominator} do not return any new object, so no reboxing is
+necessary. The complications appear when {\tt binary operations} are
+introduced in this schema. Since the two arguments of the {\sl plus}
+operator may have different representations, it is {\sl necessary}
+that the objects are accessed through the functions that operate on
+their structure, if the compiler allows this at all. However, calling
+{\sl plus} from $r_1$ does not necessarily return the same results as
+{\sl plus} from $r_2$. The problem can be transferred one level
+deeper, namely at binary operations on integers, which might pose
+similar representation complications. This is a result of the pure
+object oriented scenario with message passing we have assumed so
+far. Although such asymmetries do not seem appealing for ordinary
+arithmetic operations, the above constructs are quite useful for the
+implementation of operations which depend on one argument or
+operations on elements of heterogeneous lists. In order to handle the
+above, some object oriented systems are extended with generic
+functions: this results in very complex calculi for modeling their
+behaviour, which do not scale up easily for applications in computer
+algebra.
+
+\subsection{Domains and Categories}
+
+It is useful to have all the operations defined in the previous
+section in the class {\sl Rational}. In such case we assume a hidden
+{\sl common representation} for all objects of class {\sl Rational},
+so we can assume that Rational is defined locally:
+\begin{verbatim}
+let Rep := {x:Integer, y:Integer}
+in RationalDomain := coerce (
+ (new := (m:Integer, n:Integer) +> box {x:=m, y:=n} ;
+ numerator := (s:Rep) +> s.x ;
+ + := (s1:Rep) +> (s2:Rep) +> box(...) ;
+ etc. ),
+ RationalFun Rep)
+\end{verbatim}
+
+Many simplifications can be performed. Since all the objects of
+{\sl RationalDomain} have the same representation, unboxing and
+reboxing is not needed for performing the operations
+{\sl SetNumDenom}, $+$, etc. These functions can operate directly on
+the representations of the objects. By doing this we reduce the
+computational cost of the boxing operations, be we restrict the
+application of the above functions to objects of the same domain. The
+function {\sl coerce} replaces syntactically all the annotations which
+include {\sl Rep} with annotations which include {\sl
+RationalDomain}. There are two main reasons for this: since {\sl Rep}
+has been defined locally, it should not escape this local scope;
+additionally, we may want {\sl Rep} to be opaque,
+so that other definitions do not depend on
+the implementation of this particular representation.
+
+The above construct is not unique in Axiom. It corresponds to
+{\tt abstype} declarations in SML, or {\tt clusters} introduced by
+Liskov, Snyder, Atkinson, and Schaffert \cite{Lisk77} \cite{Lisk79}
+in CLU and, as we saw before, classes with {\tt private members} in
+object oriented languages.
+
+\subsubsection{Categories}
+
+We have seen that the instances of a class may have various
+representations, while it is desirable to have an abstraction on the
+level of functions defined for the instances of a class.
+Mitchell and Plotkin \cite{Mitc88}
+proposed that the {\sl interface part of a data type be viewed as a
+type, while the implementation part as a value of that
+type}. According to this analysis a domain comprises:
+\begin{enumerate}
+\item the internal representation of its instances
+\item operations for analyzing and manipulating this representation
+\item an abstraction barrier that prevents any access to the
+representation except by means of the given operations
+\end{enumerate}
+
+Some of the functions defined in the example with rationals, like
+{\sl numerator}, {\sl denominator}, {\sl SetNumDenom}, and {\sl new}
+deal only with the representation of its instances. These functions
+form the {\sl type of the representation}. Other functions like
+$+$, $*$, $/$, and the constants 0 and 1 are expected to be declared
+in a transparent fashion to any form of implementation. The
+second set of operations can be included in the specification of many
+other types, independently of the operations which manipulate the
+representation. For instance ($+$) can be defined for Matrices and
+Booleans, without any need for them to include operations like
+{\sl numerator} or {\sl denominator}. At the same time, a
+($+$) defined to operate on rationals, should not accept matrix values
+as arguments.
+
+We can transliterate this, using {\tt categories}:
+\begin{verbatim}
+RationalMeta := (Rep:Type) +> (
+ + : Rep -> Rep -> Rep ;
+ - : Rep -> Rep ;
+ * : Rep -> Rep -> Rep ;
+ / : Rep -> Rep -> Rep ;
+ 0 : Rep ;
+ 1 : Rep ;
+\end{verbatim}
+
+This specification can be viewed as a coding for the
+{\tt algebraic structure} {\sl Field}: we write
+\begin{verbatim}
+Field:=RationalMeta
+\end{verbatim}
+
+{\sl Rep} refers to the implementation of the domains declared as
+instances of Field:
+\begin{verbatim}
+Rational : Field
+\end{verbatim}
+
+The programming language {\sl Haskell} defines similar constructs
+calling them {\tt typeclasses}. The analogous constructs for object
+oriented languages are {\tt abstract classes}, although they cannot
+express the constraint we have posed above.
+
+Axiom's categories and object oriented abstract classes can provide
+{\tt default definitions} in categories which can be overridden in
+other categories or in the domains instances of these categories. This
+construct has great expressive capabilities but we do not handle it in
+this paper, because its semantics are not well understood and may
+cause unsoundness in the type system. We will examine an alternative,
+which can be extended to support default definitions at category
+level.
+
+\subsubsection{Existential Types}
+
+Categories are the way {\tt existential types} are coded in the type
+system. The category {\sl Field} corresponds to the existential type
+\footnote{The fact that the name of the operators is lost in the
+translation is of minor importance. We can assume canonical
+representation of the components of {\sl Field} corresponding to the
+ordering in the resulting list}.
+\[\begin{array}{rl}
+\exists Rep & [(Rep,Rep)\rightarrow Rep, Rep \rightarrow Rep,\\
+&\quad (Rep,Rep)\rightarrow Rep,(Rep,Rep)\rightarrow Rep,Rep,Rep]
+\end{array}\]
+This means that there exists a type {\sl Rep}, which is used for the
+implementation of the operations {\sl plus}, {\sl minus}, etc. with
+the types $(Rep,Rep)\rightarrow Rep$, $Rep\rightarrow Rep$,
+etc. respectively.
+
+Existential types (\cite{Mitc88},\cite{Card85}) were introduced in
+constructive logic by Girard \cite{Gira72} and are related to
+{\tt infinite sums} in {\sl category theory}
+(Herrlich and Strecker \cite{Herr73}).
+If all the domains have a hidden representation, they are all
+described by types of the form: $\exists Rep.C$ where $Rep$ is free in
+$C$. In the domain declaration
+\[D : C := add(Rep := \tau, M)\]
+the type of the components of $M$ is the result of substituting $\tau$
+for $Rep$ in $M_i$ doing the appropriate $\alpha$-conversions if
+needed:
+\[M_i : [\tau/Rep]C_i\]
+allowing the type-checking of the definition of a domain. If a domain
+does not define any $Rep$, then a {\tt type variable} is assumed for
+the typing process; thus, $Rep$ can be instantiated to any other type
+in extensions of this domain.
+
+By declaring a variable as an instance of a domain $D$, the following
+constants are introduced:
+\[f_i : [D/Rep]C_i\]
+i.e. the name of the domain $D$ replaces all occurrences of $Rep$ in
+the above context. The only information provided to the global context
+about $D$ is its name and its exported operations. If its
+representation is visible the type system can infer the $D=\tau$.
+
+Since representations may involve recursive definitions as in the case
+of lists, we introduce the notion of {\tt recursive types}. A
+recursive type $\mu t.\tau$ satisfies the equation:
+\[\mu t.\tau = [\mu t.\tau/t]\tau\]
+In order to avoid the continuous replacement of $Rep$ in $D$ in a
+recursively defined domain, we can perform the substitution only once,
+and then bind the nested occurrence of $Rep$ to a fresh variable
+which can be equated to $D$ when needed during the inference
+process. In this way, we abstract recursive types away, by using one
+level of indirection provided by the existential types. The penalty we
+pay is that type equality for recursive types cannot be
+structural. The same type definition in two different contexts will
+introduce two different fresh variables and consequently two different
+types. Although the expressiveness is not the same as in the case of
+pure recursive types, since we cannot reason about type equality as in
+(Amadio and Cardelli \cite{Amad93}), this notation can model all the
+cases of recursive types. \cite{Mitc88}.
+
+\begin{figure}[t]
+\[\begin{array}{|ll|}
+\hline
+&\\
+\ [{\rm sub{\rm -}refl}] & E \vdash M \sqsubseteq M \\
+&\\
+\ [{\rm sub{\rm -}trans}] & \displaystyle
+\frac{E\vdash S\sqsubseteq T\quad E\vdash T\sqsubseteq U}
+{E\vdash S\sqsubseteq U}\\
+&\\
+\ [{\rm thinning}] & \displaystyle
+\frac{E\vdash M_a \sqsubseteq M_b}
+{E\vdash[\overline{M_a},M_{n+1}] \sqsubseteq [\overline{M_b}]} \quad
+\overline{\{M_1,\ldots,M_n\}}=M_1,\ldots,M_n\\
+&\\
+\ [\exists{\rm -opaque}] & \displaystyle
+\frac{E,Rep:Type \vdash M_a \sqsubseteq M_b}
+{E\vdash\exists Rep.M_a\sqsubseteq\exists Rep.M_b} \\
+&\\
+\ [\exists{\rm -transparent}] & \displaystyle
+\frac{E,Rep=\tau\vdash M_1\sqsubseteq M_2}
+{E\vdash\exists Rep=\tau .M_1\sqsubseteq\exists Rep=\tau.M_2}\\
+&\\
+\ [\exists{\rm -forget}] & \displaystyle
+\frac{E,Rep=\tau\vdash M_1\sqsubseteq M_2}
+{E\vdash\exists Rep=\tau .M_1\sqsubseteq\exists Rep .M_2}\\
+&\\
+\hline
+\end{array}\]
+\caption{\label{figure1}Subtyping rules for $\exists$-types}
+\end{figure}
+
+Domains have the {\tt transparent type}:
+\[\exists Rep = \tau.C\]
+where $Rep$ is free in $C$. This corresponds to a category where the
+representation of a domain is visible.
+
+The transparent type $\exists Rep = \tau.C$ can be reduced to the
+{\tt opaque type} $\exists Rep . C$ by {\sl forgetting or hiding} the
+constraint $Rep=\tau$. In such case all the information about the
+representation of $D$ is lost: $D$ is an {\tt abstract type}.
+
+\subsubsection{Subtyping among Categories}
+
+Categories build hierarchies analogous to the existing hierarchies in
+algebra as described by Davenport and Trager \cite{Dave90}. Although
+algebraic hierarchies are based on set theoretic terms concerning the
+properties of the algebraic structures, in a type system we can assume
+only type theoretic terms, which, in our case, correspond to algebraic
+constructs.
+
+Intuitively a category $B$ is a subtype of category $A$ (we write this
+as: $B\sqsubseteq A$), if each domain belonging to $B$ belongs to $A$,
+or satisfies the properties of $A$. The subtype relation is reflexive
+and transitive. The rules for subtyping are given in Figure \ref{figure1}.
+
+A Category $B$ extends category $A$ if its definition introduces new
+components. In such case, $B$ is a subtype of $A$ [thinning]. The
+subtype relation [$\exists$-opaque] between two opaque categories
+reduces to the previous rule. The [$\exists$-transparent] rule for
+transparent categories is slightly more complex: it requires that the
+representations of their instances are the same, and then reduces to
+the thinning rule. The rule [$\exists$-forget] involves forgetting the
+information about the domain representations. For a category with a
+constraint on the representation of its domains to be a subtype of a
+category without this constraint, we check if the former can form a
+subtype of the latter when the constraint is added. A category with
+fields labeled $with(x_1:\sigma_1,\ldots,x_m:\sigma_m)$ is a subtype
+of any category with a smaller collection of fields, where the type of
+each shared field in the {\sl less informative} type is a supertype of
+the one in the {\sl more informative} type.
+
+The above scheme is more general than Axiom's. Axiom allows subtyping
+among named categories only if this has been explicitly defined by the
+user. However the introduction of {\tt anonymous categories} in Axiom
+as described by Jenks and Sutor \cite{Jenk92}, should involve rules
+like the above modulo the transparent types (the current version
+forbids the declaration of transparent categories).
+
+Another advantage of the above scheme is that representation
+constraints can be specified directly in the categories: each domain
+whose type is $\exists Rep=\tau.M$ should define a representation
+equal to $\tau$. The reason we allow this is to make the system more
+flexible while maintaining consistency, so that {\tt domain
+extensions} do not lead to unsoundness.
+
+The last rule is a special case of the rule for subtyping defined in a
+new type calculus for SML by Harper and Lillibridge \cite{Harp94}: $\tau$
+expressions cannot include $\exists$-types in our scheme, separating
+the universe of categories from the universe of types. They can be
+shared with no anonymous domains though. Without this stratification,
+using the above general version would result in undecidability, since
+the substitution $[\tau/Rep]M_2$ can increase the size of type
+expressions as shown by Pierce \cite{Pier91a}. Additionally, sharing
+with domains from given paths gives a meaning to domain equality which
+would be otherwise very difficult to obtain. In this way we can always
+decide if two domains share by checking their paths: if two domains
+derive from the same path then they share, otherwise we have to
+examine the sharing constraints in which they participate.
+
+\subsection{Domain Sharing}
+
+In the previous section we mentioned the presence of
+{\tt transparent types}. The difference between opaque types, is that
+the information about the representation of a domain is visible in the
+case of transparency, and invisible otherwise. This means that in the
+declaration
+\[D : \exists Rep = Integer.[f : Rep\rightarrow Rep, x : Rep]\]
+the domain $D$ shares the same representation as the domain $Integer$,
+and the value components $x$ can be safely viewed as $Integer$. This
+allows a certain level of flexibility in the manipulation of domains
+and their components.
+
+Sharings introduces a form of equational reasoning in the system,
+similar to that presented by Martin-L\"of in his intuitionistic type
+theory \cite{Mart73}. The behaviour of sharings is summarized in the
+following rule for domains with transparent types:
+\[[\exists{\rm -sharing}]\quad\displaystyle
+\frac{E\vdash D:\exists Rep = \tau.M}{E\vdash D=\tau}\]
+This rule comes in accordance with Axiom's behaviour where the
+representation of a domain can be exchanged with the domain itself
+inside the scope of its definition.
+
+The first application of this construct is the extension of
+domains. In the above example, the domain $D$ extends the domain
+$Integer$ by introducing the function
+$F:Integer\rightarrow Integer$ and the integer value
+$x:Integer$. Every new domain which shares representation with $D$ and
+$Integer$ is again an extension of any of them.
+
+Opaque and transparent types can be combined to control domain
+extensions and ensure their safety. In the definitions
+\begin{verbatim}
+Semigroup := with (+ : Rep -> Rep -> Rep )
+Monoid := with ( Semigroup; 0:Rep )
+D1 : with (Semigroup; Rep=Integer) := add (
+ Rep := Integer ;
+ + := (+)$Integer )
+D2 : Monoid := add (
+ D1 ;
+ Rep := D1 ;
+ 0:Rep := 0$Integer )
+\end{verbatim}
+the domain $D_1$ shares with $Integer$. This allows a safe extension
+of $D_1$ in the body of $D_2$, which involves a value of type
+$Integer$. Since the type $Monoid$ of $D_2$ does not specify any
+sharing, $D_2$ is sharing with neither $Integer$ nor $D_1$. This does
+not mean that $D_2$ cannot be extended:
+\begin{verbatim}
+D3 : with ( Monoid; Rep=D2 ; double: Rep -> Rep) := add ( D2;
+ double(x:Rep):Rep := x+x )
+\end{verbatim}
+$D_3$ shares with $D_2$; instances of $D_2$ can be passed as arguments
+to the function $double$ defined in $D_3$.
+
+A side-effect of domain sharing is that if two domains $D_1$ and $D_2$
+share common representation and define functions with the same name
+$f$ such that
+\[f_{D_1} : t_1,\quad f_{D_2} : t_2,\quad t_1 = [D_1/D_2]t2\]
+then if both domains are imported in the same context, the system is
+unable to choose the right function; explicit selections (as we did
+above) are needed. This is part of a more general problem which
+suggests that name overloading in the same context is not recommended,
+although identifiers should be free to have different meanings in
+different contexts.
+
+\subsection{Packages and Categories}
+
+Type systems which provide domains and abstract types can be
+transformed into systems with {\tt module types}, by flattening
+domains into packages. Languages like
+{\sl Modula-2} \cite{Wirt83},
+{\sl Ada} \cite{Adax12}, and
+{\sl CAML} \cite{Lero17}
+which do not use domains or classes for the implementation of objects
+use the notion of {\tt package} or {\tt module} for encapsulating the
+appropriate behaviour: each domain $D$ with representation $t$ and
+operations $M_i$, where $t$ is free in $M$, can be viewed as a package
+with a type component $t$ and value components $M_i$ which depend on
+the type $t$.
+
+In such case it is useful to consider packages with type components as
+instances of categories. For example, a package which implements
+rationals, and its corresponding type are:
+\begin{verbatim}
+RationalPack := (
+ Rep := {x:Integer, y:Integer} ;
+ + : Rep -> Rep -> Rep := a +> b +>
+ {x := a.x*b.y + a.y*b.x, y:=a.x*b.x} ;
+ ... )
+\end{verbatim}
+\begin{verbatim}
+FieldPack := with (
+ Rep: Type ;
+ + : Rep -> Rep -> Rep ;
+ - : Rep -> Rep ;
+ * : Rep -> Rep -> Rep ;
+ ... )
+\end{verbatim}
+\begin{verbatim}
+RationalCatPack := with (FieldPack; Rep = {x:Integer, y:Integer})
+\end{verbatim}
+
+Categories which correspond to packages represent a type similar to an
+existential type, namely, a {\tt dependent sum type}
+(MacQueen \cite{Macq84},
+Harper, Mitchell, and Moggi \cite{Harp89},
+Constable et al \cite{Cons86}).
+Since all the type and value components of a package can be accessed,
+package categories are {\tt strong sums}
+(MacQueen \cite{Macq86}) of the form
+\[\Sigma t : Type . [(t,t)\rightarrow t,\quad t\rightarrow t;...]\]
+For reasons of symmetry, domain categories whose type component cannot
+be accessed form {\sl weak sums}
+(Harper and Lillibridge \cite{Harp94}).
+This approach has been influenced by
+Martin-L\"of's Constructive Mathematics \cite{Mart79}).
+
+Packages can be nested inside other packages. {\tt Nested packages}
+are accessed by accessing their parent package recursively. The
+components of a package can depend on the type components of other
+nested packages as in:
+\begin{verbatim}
+PolynomialCat := with (
+ R:Ring;
+ E:OrderedAbelianMonoid;
+ Rep:Type;
+ leadingCoefficient: Rep -> Rep$R;
+ degree: Rep -> Rep$E;
+ ... )
+\end{verbatim}
+
+In this way, {\sl extensions} on existing domains are easily
+implemented, by flattening domains to packages, and exposing their
+representations which are matched with the representation of the
+extensions. {\sl Sharing} among type components are introduced
+locally inside a package, allowing the definitions of constraints
+which are valid only inside a certain scope and are invisible outside
+of it. This information is not easily expressible with domains without
+equating the two domains as we saw in a previous section.
+
+Multiple type components are represented by
+{\tt nested $\Sigma$ types}, resulting in structures which contain two
+or more carrier sets (as in {\sl PolynomialCat}). This implies that
+many complex data structures can be defined in packages and make their
+representations visible to the world.
+
+The basic rules for subtyping on sum types are similar to the ones
+described for existential types but more general since multiple nested
+dependencies can occur in the body of a category. The rules are given
+in Figure \ref{figure2}. The rule $\Sigma$-instance needs special
+attention. We will see that types and values can be coerced to
+packages. Thus, type sharings are propagated together through the
+typing mechanism. In the absence of this mechanism, we would need to
+add additional rules such as
+\[[\Sigma{\rm-instance}-\tau] \quad\displaystyle
+\frac{E\vdash\tau\quad E;t=\tau\vdash\overline{\delta}:\overline{\sigma}}
+{E\vdash add(t=\tau,\overline{\delta}):with(t:Type,\overline{\sigma})}\]
+
+The correspondence between $\exists$-types and $\Sigma$-types is quite
+interesting and shows the set-theoretic distinction between the two
+constructs
+(Turner \cite[chapter 10]{Turn91},
+Mitchell and Plotkin \cite{Mitc88}):
+\[x\in\Sigma T : C.M \leftrightarrow \exists T : C.(x\in M)\]
+This relation is of practical interest too, since it denotes that
+abstract types hide their implementations and components, but packages
+expose it. For instance, when a package with an opaque type
+$\Sigma t.M$ is opened it introduces the constants
+$x_i : M_i$ and $t : Type$, which is similar to those of domains. On
+the other hand, if a transparent package of the form
+$\Sigma t=\tau.M$ is opened, the introduced components are:
+$x_i:[\tau/t]M_i$ and the type $t=\tau$ whose kind shows that it
+shares the same implementation as $\tau$, i.e. they are the same
+types. This however does not mean that the two packages are the same,
+allowing us to make a distinction between type and package sharings
+(something we could not do with domains alone).
+
+One could argue that packages with multiple type components correspond
+to multiple domain definitions. This is in general impossible when the
+distinction in the interface (category) for the two domains is not
+clear:
+\begin{verbatim}
+PackMultCat := with (
+ R: Type ;
+ S: Type ;
+ x: R -> S -> R )
+\end{verbatim}
+In order to implement the above package as a combination of two domain
+categories, each category needs to reference the representation of the
+domains of the other. This involves parameterization, which we discuss
+in the next section. In general $\Sigma$-types allow the typing of
+more expressions than $\exists$-types, since they introduce
+{\tt impredicative polymorphism} (Harper and Mitchell \cite{Harp93a}).
+
+\begin{figure}[h]
+\[\begin{array}{|ll|}
+\hline
+&\\
+\ [\Sigma{\rm -inherit}] & \displaystyle
+\frac{E\vdash\sigma\sqsubseteq \sigma^\prime}
+{E\vdash with(\sigma)\sqsubseteq with(\sigma^\prime)}\\
+&\\
+\ [\Sigma{\rm -thinning}] & \displaystyle
+\frac{\forall i\in I.\exists j\in J.\quad
+E;(;[\overline{\sigma_j}])_{\forall j\in J}\vdash \overline{\sigma_j}
+\sqsubseteq\overline{\sigma^\prime_i}}
+{E\vdash with(\overline{\sigma_j})_{\forall j\in J}\sqsubseteq
+with(\overline{\sigma^\prime_i})_{\forall i\in I}}\\
+&\\
+\ [\Sigma{\rm -sub}{\rm -val}] & \displaystyle
+\frac{E\vdash\tau^\prime\sqsubseteq \tau}
+{E\vdash x:\tau^\prime\sqsubseteq x:\tau}\\
+&\\
+\ [\Sigma{\rm -transparent}] & \displaystyle
+\frac{E\vdash\tau^\prime=\tau}
+{E\vdash t=\tau^\prime\sqsubseteq t=\tau}
+\quad\displaystyle
+\frac{E\vdash\omega_1=\omega_2}
+{E\vdash m=\omega_1\sqsubseteq m=\omega_2}\\
+&\\
+\ [\Sigma{\rm -forget}] & \displaystyle
+\frac{E\vdash\tau}{E\vdash t=\tau\sqsubseteq t}\\
+&\\
+\ [\Sigma{\rm -opaque}] & \displaystyle
+E\vdash t\sqsubseteq t\\
+&\\
+\ [\Sigma{\rm -decl}] & \displaystyle
+\frac{E\vdash\sigma^\prime\sqsubseteq\sigma}
+{E\vdash m:\sigma^\prime\sqsubseteq m:\sigma}\\
+&\\
+\ [\Sigma{\rm -nesting}] & \displaystyle
+\frac{E\vdash\sigma^\prime\sqsubseteq\sigma\quad
+E,m:\sigma^\prime\vdash\overline{\sigma^\prime}\sqsubseteq\overline{\sigma}}
+{E\vdash with(m:\sigma^\prime,\overline{\sigma^\prime})\sqsubseteq
+with(m:\sigma,\overline{\sigma})}\\
+&\\
+\ [\Sigma{\rm -sub}] & \displaystyle
+\frac{E\vdash m:\sigma^\prime\quad
+E\vdash\sigma^\prime\sqsubseteq\sigma}
+{E\vdash m:\sigma}\\
+&\\
+\ [\Sigma{\rm -instance}] & \displaystyle
+\frac{E\vdash\delta:\sigma\quad
+E,m:\sigma\vdash\overline{\delta}:\overline{\sigma}}
+{E\vdash add(m=\delta,\overline{\delta}):
+with(m:\sigma,\overline{\sigma})}\\
+&\\
+\hline
+\end{array}\]
+\caption{\label{figure2}Subtyping rules for $\exists$-types}
+\end{figure}
+
+\subsection{Parameterization}
+
+In the presentation of categories and domains in previous sections, we
+assumed that they are parameterized by the representation of their
+instances. This was merely a notational convenience in order to
+clarify the correspondence between domains and their existential
+types. Computer algebra systems like Axiom have chosen to use a
+special symbol such as \$ or \% for representing the unaccessible type
+component of the domain categories. We used a {\sl flattened} notation
+for packages in order to specify explicitly that type components can be
+accessible as if they were normal value components. Nevertheless, the
+code previously given for the creation of the objects $r_1$ and $r_2$,
+provides a concrete type for the representation as it is difficult to
+implement the functions without knowledge of the actual hidden type.
+
+\subsubsection{Parameterized Categories}
+
+What is hidden behind the notation we used is that it is possible to
+parameterize both domains and packages with other domains and
+packages. Given the relation between $\exists$-types and
+$\Sigma$-types and the conclusion that packages are more general than
+domains, we can assume that $\Sigma$-types and packages can be
+parameterized by other packages resulting in new $\Sigma$-types and
+packages respectively as in:
+\begin{verbatim}
+DictionaryCat (Keys: with
+ (T:Type;
+ eq:T->T->Boolean;
+ less:T->T->Boolean)
+ (Values: with (T:Type))
+ := with (
+ T:Type ;
+ empty: T ;
+ at: T -> T$Keys -> T$Values ;
+ update: T -> T$Keys -> T$Values -> T ;
+ ... )
+\end{verbatim}
+
+The parameterized category {\sl DictionaryCat} provides the interface
+of parameterized packages which receive two arguments: a package with
+ordering operations on its carrier set ({\sl Keys}) and a package
+which provides a carrier set ({\sl Values}). The type of the returned
+package depends on the carriers of the arguments as it can be seen by
+the signatures of the functions {\sl at} and {\sl update}. In this
+way, parameterized categories form {\tt dependent products} and their
+instances are mappings from packages to packages: we call them
+{\tt functors}.
+
+Ideally, a parameterized category is the type of a parameterized
+package. However, parameterized categories are used extensively in
+systems like Axiom to code the categories of Modules or Polynomials
+over a Ring, etc. \cite{Dave90} \cite{Dave91} which are actually
+simple $\Sigma$-types. Given the category of Polynomials as defined
+previously we can construct a parameterized package which returns
+implementations of polynomial types:
+\begin{verbatim}
+PolynomialRing(R:Ring,E:OrderedAbelianMonoid): PolynomialCat
+ := add (
+ R := R;
+ e := E;
+ Rep := List {k:Rep$E, c:Rep$R};
+ leadingCoefficient := r +> ... ;
+ degree := e +> ... ;
+ ...
+ )
+\end{verbatim}
+
+\begin{figure}[t]
+\[\begin{array}{|ll|}
+\hline
+&\\
+\ [\Pi F{\rm -apply}] & \displaystyle
+\frac{E\vdash m_1:\Pi\ m:c_1.c_2\quad E\vdash m_2:c_1}
+{E\vdash m_1(m_2):[m_2/m]c_2}\\
+&\\
+\ [\Pi{\rm -instance}] & \displaystyle
+\frac{E;m:c\vdash m^\prime:c^\prime}
+{E\vdash(m:c)\mapsto m^\prime:(m:c)\mapsto c^\prime}\\
+&\\
+\ [\Pi{\rm -apply}] & \displaystyle
+\frac{E:\vdash m_1:c_1\quad E\vdash add(M=m_1,m):\Sigma M=m_1.c_2}
+{E\vdash m:(\Pi M:c_1.c_2)m_1}\\
+&\\
+\ [\Pi{\rm -sub}] & \displaystyle
+\frac{E\vdash c^\prime_1\sqsubseteq c_1\quad
+E;m:c^\prime_1\vdash C_2\sqsubseteq c^\prime_2}
+{E\vdash\Pi(m:c_1).c_2\sqsubseteq\Pi(m:c^\prime_1).c^\prime_2}\\
+&\\
+\ [\Pi{\rm -subapply}] & \displaystyle
+\frac{E\vdash\Sigma m^\prime=m_1.c\sqsubseteq
+\Sigma m^\prime=m_1.[m^\prime/m]c_2}
+{E\vdash c\sqsubseteq (\Pi(m:c_1).c_2)m_1}\\
+&\\
+\hline
+\end{array}\]
+\caption{\label{figure3}Subtyping rules for $\Pi$-types}
+\end{figure}
+
+The advantage of this modeling is that the implementation of the
+coefficients and the terms of polynomials are accessible from the
+package which defined functionality on them. In this way, each
+polynomial package propagates all the information about its
+constituents: extensions of their functionality is possible by
+accessing not only the structure, but also the implementation of the
+types of their components.
+
+\subsubsection{Dependent Products}
+
+The category {\sl DictionaryCat} corresponds to the {\tt product type}
+\[\Pi(K:Ord).\Pi(T:Set).\Sigma(t:Type).
+[t,t\rightarrow K.t\rightarrow T.t,
+t\rightarrow K.t\rightarrow T.t\rightarrow t,...]\]
+
+The types of functors are {\tt dependent products}
+(Burstall and Lampson \cite{Lamp88},
+MacQueen \cite{Macq84} \cite{Macq86},
+Harper and Lillibridge \cite{Harp94}
+Leroy \cite{Lero94}): the type of the return package (domain) can depend on
+the functor arguments. In the declarations
+\[F(m:C^\prime):C=M\]
+\[M^{\prime\prime}=F(M^\prime)\]
+where $M$ is the instance of the category $C$,
+$M^\prime$ an instance of the category $C^\prime$ and the type of the
+components of $M^{\prime\prime}$ are equal to:
+\[M^{\prime\prime}_i:[M^\prime/m]C_i\]
+As it has been mentioned, the arguments of a functor (and of its
+dependent type) are always packages; a functor application results in
+a new package. The rules for typing and subtyping for dependent
+products are given in figure(\ref{figure3}).
+
+In order to pass a value $f$ as argument to a functor, a new anonymous
+package with a value component $f$ is generated implicitly, resulting
+in a functor with a package argument:
+\[\Pi(f:t_1\rightarrow t_2).M \Rightarrow
+\Pi(s:\Sigma().t_1\rightarrow
+t_2).[f\$s/f]M\]
+For example, consider the transformation:
+\[F(x:Integer):C:=M\Rightarrow F(X:with(x:Integer)):C:=[x\$X/x]M\]
+If we call $F$ with an integer argument $F(x:=3)$, then an anonymous
+package is generated: $F(add(x:Integer:=3))$ and $M$ is returned. If
+we pass two arguments, as in $F(x:=3,y:=4)$, then following the same
+procedure we have
+\[F(add(x:Integer:=3,y:Integer:=4))\]
+Given the rules $\Pi$F-apply and $\Sigma$-forget, the new argument
+matches the type $\Sigma()$.[$x:Integer$], and the functor application
+returns $M$.
+
+\subsubsection{Subtyping of Products}
+
+As we have seen, the arguments of parameterized categories have sum
+types, while the body is also an instance of a sum type. The case of
+categories (and domains) with $N$ arguments is viewed recursively: the
+body is parameterized by $N-1$ arguments, i.e. it has a product type,
+and after $N$ steps the final body is not parameterized (0 arguments),
+resulting in a sum type.
+
+The subtype relation among sum types can be extended to accommodate
+dependent products. The subtyping relation in this case involves
+{\sl contravariance} in the argument position and {\sl covariance} in
+the body type. The type $\Pi(m:C_1).C_2$ places a stronger constraint
+on the behaviour of its instances than $\Pi(m:C^\prime_1).C^\prime_2$
+if it demands that:
+\begin{enumerate}
+\item they behave properly on a larger set of inputs
+$(C^\prime_1)\sqsubseteq C_1)$ or
+\item their results fall within a smaller set of outputs
+$(C^\prime_2\sqsubseteq C^\prime_2)$, provided that the inputs range
+in $C^\prime_1$
+\end{enumerate}
+or possibly both ([$\Pi$-sub]).
+
+\subsubsection{Sharing (Take Two)}
+
+Sharing among type components is of special importance in the case of
+functors and product types. The rule $\Sigma$-transparent for sharing
+is powerful enough to allow the definition of functors which combine
+or compose domains and packages:
+\begin{verbatim}
+RingFun (P1:Monoid) (P2: with (Monoid; Rep=P1.Rep)):Category :=
+ with ( Monoid ;
+ * : Rep - Rep -> Rep ;
+ 1 : Rep )
+\end{verbatim}
+
+\begin{verbatim}
+BuildRing: RingFun := P1 +> P2 +>
+ add ( P1;
+ * := (+)$P2 ;
+ 1 := 0$P2 )
+\end{verbatim}
+In this example, two monoids with the same representation are combined
+in order to form a ring. Since the category {\sl Monoid} already
+exists in the system, the only additional action is to add a sharing
+constraint to it for $P2$.
+
+Without sharing the above construction is more complicated and less
+natural for modeling algebraic concepts. It would require the
+parameterization of algebraic categories with their representation:
+\begin{verbatim}
+RingFun(T:Type)(M1:Monoid(T))(M2:Monoid(T)):Category := ...
+\end{verbatim}
+
+Such constructs demand the implicit or explicit creation of new
+hierarchies for parameterized monoid categories. The former increases
+the load of a type system and its implementation dramatically while
+the latter demands that the user create parallel hierarchies for all
+possible cases of parameterization.
+
+Sharings reduce the need for instantiation of parameterized
+categories, as the above example shows. For instance, many cases which
+involve parameterized categories in the Axiom library can be reduced
+to simple categories with sharing constraints. The rest can be
+transformed to sum types with sharing constraints on their type
+components. This feature can be exploited for the implementation of
+higher order categories by means of first order possibly nested
+constructs and sharings, which reduce the complexity and the
+computational load of the compiler.
+
+\subsubsection{Flattening Dependent Products}
+
+The application of dependent products for the generation of new sum
+types complicates the elaboration of programs and adds considerable
+load in the typing process. In the presence of subtyping, new
+hierarchies have to be created since product types may extend other
+products. Sums do not have such complications and their hierarchies
+remain stable.
+
+One of the properties of $\Pi$-types is that their components cannot
+be accessed, thus sharing constraints cannot propagate to their
+environment. Therefor it is always desirable to involve $\Sigma$-types
+in the presence of static typing. On the other hand, sharing
+specifications can restrict a sum to certain implementations,
+emulating the results of product application to equivalent
+implementations.
+
+Another observation we made in the last sections is that it is not
+always convenient to implement categories as products if we want to
+access the implementations of the constituents of a package. For
+instance, the code of DictionaryCat was rather artificial. A more
+realistic implementation would demand the type of the keys and values
+to be accessible so as to perform computations other than the ones
+specified in this category, like transforming dictionaries to other
+structures. The category
+\begin{verbatim}
+DictionaryCat(Keys:=String; Values:=Integer)
+\end{verbatim}
+could be defined as
+\begin{verbatim}
+DictionaryCat := with (
+ Keys: with(Type;...);
+ Values: Type;
+ Rep: Type;
+ at: T -> Rep$Keys -> Rep$Values
+ ...
+ );
+ with (DictionaryCat; Keys=String; Values=Integer)
+\end{verbatim}
+allowing dictionaries to expose the implementation of Keys and Values
+and propagate evntual sharing constraints.
+
+However, in some cases, instantiation of dependent products can serve
+modeling purposes better than dependent sums. For instance, a
+{\sl Ring} is a {\sl LeftModule} over itself:
+\begin{verbatim}
+LeftModules(R: with(AbelianGroup; SemiGroup)) :=
+ (AbelianGroup;
+ * : (Rep,R) -> Rep )
+Ring := with (LeftModules(%):...)
+\end{verbatim}
+where the construct \% refers to the package which is an instance of
+the category we define (in this case {\sl Ring}). If $R$ were a nested
+package inside the definition of LeftModules then it should be defined
+forall the Rings too. This would cause great inconveniences in the
+coding of Rings since a Ring is a package which has an $R$ component
+assigned to itself, leading to recursions. The typing system should
+handle these cases automatically and in a transparent way.
+
+The application of dependent product types can be defined in terms of
+already defined constructs such as nested packages and sharings as the
+previous examples indicate. We distinguish two cases of interest:
+\begin{enumerate}
+\item Declarations of packages as instances of applications of
+$\Pi$-types of the form
+\[P_2:(\Pi(P:C_1).C_2)P_1:=P_3\]
+\item Inheritance of applications of $\Pi$-types of the form
+\[C_3:=\Sigma((\Pi P:C_1.C_2)P_1).C_x\]
+the right hand side of which is essentially the expression
+\[with((\Pi(P:C_1).C_2)P_1 ; C_x)\]
+\end{enumerate}
+The expression $(\Pi(P:C_1).C_2)P_1$ creates a sum type
+$\Sigma P:C_1=P_2.C_2$ with the sharing specification $P=P_2$.
+
+This transformation has another important consequence: it allows
+products to be transformed into sums, meaning that the arguments of a
+$\Pi$-type can have $\Pi$-types themselves without changing their
+inital semantics. This makes possible the definitions of
+{\tt higher order functors} similar to
+Cregut and MacQueen \cite{Macq94}.
+
+The RHS of the expression $P_2:(\Pi(P:C_1).C_2)P_1:=P_3$ is handles as
+above, but the typing mechanism should automatically add a $P$
+component to $P_3$ so that $P_3$ will match with the resulting sum
+type. Consequently, $P_2$ will have an implicit $P$ component. In case
+the declaration specifies the argument of a dependent product then
+$P_3$ plays the role of the argument passed during the application of
+the product as in
+$(\Pi(P:(\Pi(P:C_1).C_2)P_1).C_3)P_3$
+
+The expression
+\[\Sigma((\Pi P:C_1.C_2)P_1).C_x\]
+is transformed to
+\[((\Pi P^\prime : C_1.\Sigma[P^\prime/P]C_2.C_x)P_1)\quad
+{\rm where\ }P^\prime{\rm\ fresh}\]
+and then we proceed as above.
+
+These transformations assume that such directives to the typing
+mechanism should be coded directly in the $\Pi$-types and then
+elaborated during their applications, so that the appropriate
+components of the resulting $\Sigma$-types and their instances will be
+introduced when needed. This involves the following steps:
+\begin{enumerate}
+\item Add a directive for introducing component $p$ in the definition
+of the instances of the category resulting from applying
+$\Pi(P:C_1).C_2$ to a package $P_1$. In order to avoid name conflicts,
+a fresh variable $P^\prime$ can be introduced instead of $P$,
+performing the appropriate $\alpha$-conversions.
+\item Create a dummy package $P_{dummy}$ which satisfies $C_1$
+\item In the definition of the sum
+$\Sigma P^\prime:C_1.[P^\prime/P]C_2$
+propagate the directive of step 1 and do type-checking by sharing
+$P_{dummy}$ from step 2 with $P^\prime$. The directive from step 1
+should now affect the instances of the sum.
+\item If type checking succeeds, remove $P_{dummy}$. When a domain is
+matched against the introduced sum, the stored directives introduce
+the appropriate nested packages automatically, resulting in the
+generation of a new package. Add the appropriate sharings by
+generating a new category.\\
+In the above example,, if a package $M$ is to be matched against
+$Module(\%)$ (where \% refers to $M$), a new sum type $Module_{flat}$
+is generated through steps 1-3. Consequently a package $M_{new}$ is
+generated including all the components of $M$ plus a component
+$P^\prime$ resulting from the directives of step 3. A sharing
+specification $R^\prime=M$ is added to $Module_{flat}$. Type checking
+and propagation of sharings proceed.
+\item Any other operation involving sums should take into account the
+directives stored in them, or inherited by other sums. In this case,
+{\sl Ring} should include the directives given by
+{\sl LeftModule(\%)}.
+\end{enumerate}
+
+The above result in the rules $\Pi$-apply and $\Pi$-subapply in
+figure(\ref{figure3}).
+
+The typing process in this scheme is decidable, due to the generation
+of new sums and packages from existing components. However, the above
+steps avoid the generation of new type components since the old
+components are also members of the new packages. Thus propagation of
+type information is not affected.
+
+The rules for application of $\Pi$ types imply that a dependent
+product can be applied only when the dependencies of the body of the
+product to its arguments have been removed. This assumes an implicit
+coercion of the {\tt dependent product type} to an {\tt arrow type} as
+in
+\[(m:(\Pi M:C_1.C_2))m_1 \Rightarrow (m:C_1\rightarrow [m_1/M]C_2)m_1\]
+provided that $m_1$ can be shown to have the type $C_1$.
+
+\subsection{Subtyping of Domains}
+
+Descriptions of {\tt sets} of entities which belong to various
+domains can be arranged into useful classification hierarchies. For
+example, the set of integers can be seen as a subset of the rational
+numbers. This supports a useful kind of reasoning: if $X$ is an
+integer, then $X$ must also be a rational number, and every
+interpretation of a rational number should be true for $X$ if both
+domains are viewed as instances of the same category. For example, it
+should be valid to make the judgement
+\[\displaystyle
+\frac{E\vdash Integer\sqsubseteq Rational:Ring\quad E\vdash x:Integer}
+{E\vdash x:Rational}\]
+
+The semantics of $S\sqsubseteq T$ for domains and types can be derived
+by the corresponding relations in $\Sigma$ and $\Pi$-types; they are
+included in the following statement:
+
+If $S\sqsubseteq T:C$, then an instance of $S$ may safely be used in
+any operation specified in $C$ where an instance of $T$ is expected.
+
+For example the function
+\begin{verbatim}
+foo(x:Rational) := (x+1) * x**2
+\end{verbatim}
+can be safely applied to the integer argument 4 because it is possible
+to view any integer as a rational in the above operations. More
+important, since integers form a {\tt subring} of rationals, and the
+definition of {\sl foo} includes operations defined for rings, we can
+do this substitution under the assumption that both {\sl Integer} and
+{\sl Rational} form a ring. This leads to the more general subrule
+[sub-val] (figure \ref{figure4}).
+
+\subsubsection{Coercions}
+
+Two formal accounts can be given for the semantics of subtyping. In
+the simpler view, the syntactic subtype relation $S\sqsubseteq T$
+where $S,T$ are domains, is interpreted as asserting that the
+{\tt semantic domain} denoted by $S$ is included in that denoted by
+$T$. In the more general view $S\sqsubseteq T$ is interpreted as a
+{\tt canonical coercion function} from the domain denoted by $S$ to
+the one denoted by $T$:
+\[\displaystyle
+\frac{E\vdash S,T:C\quad E\vdash x:S\quad E\vdash {\bf coerce}:
+S\hookrightarrow T}{E\vdash {\bf coerce}(x):T}\]
+i.e.
+\[\displaystyle
+\frac{E\vdash x:S\quad E\vdash {}_C{\bf coerce}:S\hookrightarrow T}
+{E\vdash {}_C{\bf coerce}(x):T}\]
+where coercions keep information about the form of subtyping among
+domains in terms of algebraic relations: if $C$ involves {\sl Ring}
+structures, then the above rule describes a subring relation.
+
+Since coercions can be composed, the subtype information carried with
+them can be modified. In a type system, information cannot be
+generated from inside, therefore any composition of coercions reduces
+the information:
+\[\displaystyle
+\frac{E\vdash C_1\sqsubseteq C_2\quad
+E\vdash {}_{C_1}{\bf coerce}:R\hookrightarrow S\quad
+E\vdash {}_{C_2}{\bf coerce}:S\hookrightarrow T}
+{E\vdash {}_{C_1}{\bf coerce}:R\hookrightarrow T}\]
+\[\displaystyle
+\frac{E\vdash C_1\sqsubseteq C_2\quad
+E\vdash {}_{C_2}{\bf coerce}:R\hookrightarrow S\quad
+E\vdash {}_{C_1}{\bf coerce}:S\hookrightarrow T}
+{E\vdash {}_{C_1}{\bf coerce}:R\hookrightarrow T}\]
+
+In this way paths can be composed with different subtyping carried
+information. A useful theorem which can be proved by the above rules
+is that any direct coercion between two domains, carries more
+information than any other coercion path which uses an intermediate
+domain. This means that direct coercions are preferable in case of
+multiple paths. Assume the domains $A$, $B$, $C$, and $D$, and the
+coercions
+\[\begin{array}{c}
+A\hookrightarrow C\hookrightarrow B\\
+A\hookrightarrow D\hookrightarrow B\\
+\end{array}\]
+A type system cannot in general prove whether this graph commutes,
+since the former path may have different semantics than the
+latter. Since the path $A\hookrightarrow B$ keeps more information than the
+path $A\hookrightarrow C\hookrightarrow B$ any composition of the above paths leads to
+similar results, i.e. the path
+\[A\hookrightarrow B\hookrightarrow D\]
+is preferable for a transition from $A$ to $D$ than
+
+\begin{figure}[h]
+\[\begin{array}{|ll|}
+\hline
+&\\
+\ [{\rm sub-val}] & \displaystyle
+\frac{E\vdash x:S\quad E\vdash S\sqsubseteq T:C}
+{E\vdash x:T}\\
+&\\
+\ [\{\}{\rm -sub}] & \displaystyle
+\frac{\forall j\in\{1,\ldots,m\}\exists i\in\{1,\ldots,n\}~.~
+E\vdash x_i\equiv x_j~
+E\vdash \tau_i\sqsubseteq\tau_j,~m\le n}
+{\{x_i:\tau_i\}_{\forall i\in\{1,\ldots,n\}}\sqsubseteq
+\{x_j,\tau_j\}_{\forall j\in\{1,\ldots,m\}}}\\
+&\\
+\ [\rightarrow{\rm -sub}] & \displaystyle
+\frac{E\vdash T_1\sqsubseteq S_1\quad E\vdash S_2\sqsubseteq T_2}
+{E\vdash S_1\rightarrow S_2\sqsubseteq T_1\rightarrow T_2}\\
+&\\
+\ [\mu{\rm -sub}] & \displaystyle
+\frac{E;T_1:Type;S_1\sqsubseteq T_1\vdash S\sqsubseteq T}
+{E\vdash \mu S_1,S\sqsubseteq \mu T_1,T}\\
+&\\
+\ [{\rm +-sub}] & \displaystyle
+\frac{\forall i\in\{1,\ldots,m\}\exists j\in\{1,\ldots,n\}~.~
+E\vdash x_i\equiv x_j~E\vdash\tau_i\sqsubseteq\tau_j,~m\le n}
+{+[x_i:\tau_i]_{\forall i\in\{1,\ldots,m\}}\sqsubseteq
++[x_j:\tau_j]_{\forall j\in\{1,\ldots,n\}}}\\
+&\\
+\hline
+\end{array}\]
+\caption{\label{figure4}Subtyping rules for types}
+\end{figure}
+
+\[A\hookrightarrow C\hookrightarrow B\hookrightarrow E\hookrightarrow D\]
+It is important to mention that the length of the path is of no
+particular importance, although the preferable path is always shorter
+than any other path. For instance, if in the above paths the coercion
+$C\hookrightarrow D$ is added, then there is no way to choose any particular
+path.
+
+\subsubsection{Subtyping of Representations}
+
+In this section we restrict ourselves to natural subtyping between
+types of run-time objects. The subtyping rules for records, arrow
+types, and recursive types correspond to the subtyping rules for
+packages ($\Sigma$-thinning), dependent products ($\Pi$-sub), and
+domains ($\exists$-forget); a similar rule for {\tt disjoint unions}
+is added (figure \ref{figure4}).
+
+Records can be viewed as degenerated forms of packages where there are
+no type components, and no dependencies among the components and their
+types. The above rule for records supports the subtyping of tuples if
+we view tuples as records with integer fields.
+
+In a similar way, an arrow type is a $\Pi$-type where there is no
+dependency between the input type and the output:
+$\Pi(x:\tau_1).\tau_2$ reduces to $\tau_1\rightarrow\tau_2$ if $x$ is
+not in the expression $\tau_2$.
+
+The rule for function types interprets the rule for records in the
+following way: If we think of a record as a function from labels to
+values, a record $\tau$ represents a stronger constraints than
+$\tau^\prime$ on the behaviour of such function, if $\tau$ describes
+the function's behaviour on a larger set of labels or gives a stronger
+description of its behaviour on some of the labels also mentioned by
+$\tau^\prime$ (Pierce \cite{Pier91a}).
+
+By means of [+-sub] and [$\mu$-sub] our type system can assure that
+\[Tree(Integer)\sqsubseteq Tree(Rational)\].
+
+For continuing our analysis we introduce the category $Ring$ and
+repeat the definition of the category $Field$:
+\begin{verbatim}
+Ring := (Rep:Type) +> with (
+ + : Rep -> Rep -> Rep ;
+ - : Rep -> Rep ;
+ * : Rep -> Rep -> Rep ;
+ 0 : Rep ;
+ 1 : Rep )
+\end{verbatim}
+\begin{verbatim}
+Field := (Rep: Type) +> Ring(Rep) with (
+ / : Rep -> Rep -> Rep )
+\end{verbatim}
+and $Field\sqsubseteq Ring$ given the subtyping rules for existential
+types above. This means that {\sl every instance of the category Field
+can be viewed as an instance of Ring} or {\sl every instance of an
+instance of Field is also an instance of an instance of
+Ring}. Unfortunately the rules for subtyping among categories cannot
+be easily extended to rules for their instances.
+
+Given the definition of the type {\sl RationalFun} from above we can
+introduce in a similar way the type of integers which form a Ring. Our
+notation allows us to abstract the implementations away:
+\begin{verbatim}
+IntegerFun := (Rep:Type) +> (
+ new: Integer -> Rep ;
+ numerator: Rep -> Integer ;
+ denominator: Rep -> Integer ;
+ SetNumDenom: Rep -> Integer -> Rep ;
+ + : Rep -> Rep -> Rep ;
+ - : Rep -> Rep ;
+ * : Rep -> Rep -> Rep ;
+ 0 : Rep ;
+ 1 : Rep ; )
+\end{verbatim}
+It is not the case that $IntegerFun\sqsubseteq RationalFun$ since the
+specification of integers does not include the record field $/$,
+leaving $IntegerFun$ with one field less than $RationalFun$.
+
+The obvious solution to cope with the above problem is the use of
+coercions, as we saw in the previous section. The problem is that
+coercions are expensive in computational resources and in some cases
+they can introduce inconsistencies.
+
+\subsection{Type Classes}
+
+In this section, we are concerned with modeling subtyping without use
+of coercions. We introduce the concept of type classes, which has some
+similarities with the homonymous concept in Haskell
+(Nipkow and Prehofer \cite{Nipk95},
+Wadler and Blott \cite{Wadl88}). The semantics and the formal definitions
+for type classes are provided in the next section. Type classes are
+distinct from categories in the sense that they are not part of the
+user defined types. The main difference with Haskell's type classes is
+that our type classes are not syntactically defined in the language
+but are inferred by its type system, reducing the complexity of the
+former.
+
+It is clear now that we are not interested in a pure subtype
+relationship, but in an algebraic relationship based in terms of
+{\tt subrings}, {\tt subfields}, etc. We introduce type classes in
+order to provide the facility of viewing Integer as a {\tt subring} of
+Rational:
+\begin{verbatim}
+RationalRing := (Rep:Type) +> with (
+ + : Rep -> Rep -> Rep ;
+ - : Rep -> Rep ;
+ * : Rep -> Rep -> Rep ;
+ 0 : Rep ;
+ 1 : Rep )
+\end{verbatim}
+
+This declares that any eventual subtype of rational which happens to
+be an instance of {\sl Ring} implements the operations declared in the
+type class {\sl RationalRing}. Since {\sl Integer} forms a subring of
+{\sl Rational}, from the definition
+\begin{verbatim}
+IntegerRing := (Rep:Type) +> RationalRing(Rep)
+\end{verbatim}
+we may conclude:
+\[IntegerRing\sqsubseteq RationalRing\]
+The declaration of $Integer$ as instance of the type class
+$IntegerRing$ is straightforward:
+\begin{verbatim}
+Integer :: IntegerRing
+\end{verbatim}
+while for Rationals we need one additional type class:
+\begin{verbatim}
+RationalField := (Rep:Type) +> RationalRing(Rep) with (
+ / : Rep -> Rep -> Rep )
+
+Rational :: RationalField
+\end{verbatim}
+
+Given the function definition
+\begin{verbatim}
+dblSqrd(x::Rational) := (x+x)*(x+x)
+\end{verbatim}
+by means of type classes the system infers the most general signature
+for $dblSqrd$:
+\[\Gamma,\forall a::RationalRing \vdash dblSqrd :
+a\rightarrow a\rightarrow a\]
+$dblSqrd$ can receive as argument an instance of any the types of
+$RationalRing$, including $Integer$, without any need to coerce it to
+$Rational$: we have managed to define a natural subtype relationship
+between integers and rationals, which comes in accordance with the
+algebraic semantics of the terms.
+
+\subsubsection{Definition of Type Classes}
+
+For the definition of type classes we assume that operations do not
+belong to a type but to an algebra (that is, a particular collection
+of types). A class combines one or more types for the implementation
+of its instances. A class's instances do not need to have a common
+internal structure but they are elements of the types which a class
+assumes. Herewith we can define type classes.
+
+Formally a {\tt type class} has the following structure:
+$Class[T,B]$ in which $T$ is the set of types and $B$ is the behaviour
+of the class's instances. An instance of a type is by definition an
+instance of any of the classes in which this type belongs. The
+{\tt instanceOf relation} (denoted by ::) represents membership in a
+set of instances and as such it is {\sl irreflexive} and
+{\sl non-transitive}.
+
+The {\tt subclass relation} (denoted by $\sqsubseteq$) is a
+{\sl reflexive}, {\sl antisymmetric}, and {\sl transitive} binary
+ordering relation in the partial ordered set of classes.
+
+{\tt Subtyping} can be seen in two ways (which are consistent with the
+definitions given in the previous sections): subtyping by means of
+subclassing or coercions.
+
+\begin{figure}[h]
+\[\begin{array}{|ll|}
+\hline
+&\\
+\ [\bigcap{\rm -sub}] & \displaystyle
+\frac{\forall j\in\{1,\ldots,m\}\exists i\in\{1,\ldots,n\}~.~
+E\vdash\tau_i\sqsubseteq\tau_j,~m\le n}
+{\bigcap(\tau_i)_{\forall i\in\{1,\ldots,n\}}\sqsubseteq
+ \bigcap(\tau_j)_{\forall j\in\{1,\ldots,m\}}}\\
+&\\
+\hline
+\end{array}\]
+\caption{\label{figure5}Subtyping rules for intersection types}
+\end{figure}
+
+\[\begin{array}{cc}
+\displaystyle
+\frac{E\vdash x::C\quad E\vdash C\sqsubseteq C_i}{E\vdash x::C_i} &
+\displaystyle
+\frac{E\vdash x::C\quad E\vdash{\bf coerce}:C\hookrightarrow C_i}
+{E\vdash{\bf coerce}(x)::C_i}
+\end{array}\]
+The above rules handle the case of multiple subclassing for they
+are applied $\forall i\in[1,\ldots,n]$.
+
+Type classes $C_1$, $C_2$ are said to belong to the same
+{\tt inheritance path} when one can derive through $\sqsubseteq$ or
+$\hookrightarrow$ relationships that $C_1\sqsubseteq C_2$ or
+$C_1\hookrightarrow C_2$ respectively.
+
+The above inductive definitions can be seen as the definition of
+{\tt class}\\
+{\tt intersection} which differs from the classical definition
+of set intersection in the sense that equality for instances of
+different classes cannot be established. Such a relation is possible
+only between members of the same equality type. Identity is only
+possible between members of the same type. Class intersection
+corresponds to intersection of the sets of types implementing the
+classes. Classes define behaviour by means of a set of axioms and
+operations among each class's instances, therefore a class
+intersection produces behavioural {\sl union}. This definition has
+constructive power since an instance must be an element of a
+particular type. It corresponds to the subtyping rules for
+{\tt records} (union), and {\tt intersection types} (figure \ref{figure5}).
+
+{\tt Class Intersection:}
+\[x::(C_1\sqcap\ldots\sqcap C_n)\Leftrightarrow\forall_i x::C_i\]
+and
+\[[T_1,B_1]\sqcap\ldots\sqcap[T_n,B_n]=[\bigcap_iT_i\bigcup_iB_i]\]
+where we write [$T,B$] for the class implemented by each of the types
+$t\in T$ and supporting behaviours $b\in B$.
+
+In the case that $T_1\cap\ldots\cap T_n=\{\}$, the class intersection
+is $\bot$. Similarly, we can define the union of classes as their
+superclass:
+
+{\tt Class Union:}
+\[x::(C_1\sqcup\ldots\sqcup C_nn)\Leftrightarrow\exists_i x::C_i\]
+\[[T_1,B_1]\sqcup\ldots\sqcup[T_n,B_n]=[\bigcup_iT_i,\bigcap_iB_i]\]
+
+The rules we use for typing values with type-classes are similar to
+those of the Haskell system. We avoid repeating them here since they
+can be found in (Nipkow \cite{Nipk95}). Every new value declaration which
+involves instances of a domain which is a member of a type class is
+added to the value set of this type-class. Since a domain can be a
+member of many type classes the most general one which ensures the
+typing of the value is chosen. For every new value the same process is
+followed. This means that although the initial constructions of type
+classes depends on the category hierarchy, after the introduction of
+new values they can include more declarations.
+
+\subsubsection{Coercions vs. Typeclasses}
+
+Typeclasses allow a different kind of behaviour than coercions. If
+there is a coercion from $A$ to $B$, but we can perform the operations
+defined in $B$ directly in $A$ (assuming that instances of type $A$
+are passed as arguments) then we do not need to consider the
+possibility of multiple paths or computational effects, but we get the
+behaviour defined in $A$ (instead of that in $B$). The former is an
+advantage of typeclasses over coercions, the latter allows for more
+options in the design.
+
+It is worth noting that none of the forgoing would have been possible
+if the type variable $Rep$ was not introduced in the definition of
+domains and categories. Suppose that Rational and Integer had the
+definitions
+\begin{verbatim}
+Rational := ( ...
+ + : Rational -> Rational -> Rational
+ etc. )
+
+Integer := ( ...
+ + : Integer -> Integer -> Integer
+ etc. )
+\end{verbatim}
+
+This would influence the definitions of RationalFun and IntegerFun
+respectively, and finally the definitions of RationalRing and
+IntegerRing. There would have been no simple way to derive a subtype
+relationship among types which would include the terms
+\[Rational\rightarrow Rational\rightarrow Rational\]
+and
+\[Integer\rightarrow Integer\rightarrow Integer\]
+since these two cannot form a subtype relationship due to the
+introduction of the {\tt contravariance} rule for function types.
+
+For the same reason it is also difficult to use packages for defining
+the above form of subtyping. Domains have only one carrier set, making
+it simple to reason and infer type hierarchies. In the presence of
+more than one combined sets this task is more difficult since it can
+involve recursive domain definitions. Additionally, the form of
+subtyping proposed can be easily implemented with dictionaries
+specific to each type class. In the presence of multiple carriers this
+implementation requires multiple dictionaries, most of which may never
+be used. This approach would decrease the efficiency of the system
+without acutally bringing any substantial benefit.
+
+\subsection{Comparison with Related Work}
+
+The type system we have presented is an extension of Axiom's type
+system with the introduction of strong sums, higher order functors,
+transparent category types, structural type equivalence, sharing
+specifications and type classes. It can also be viewed as an extension
+of SML's module system by transforming abstract types (domains) to
+modules (packages), and introducing recursive higher order dependent
+products.
+
+Work of considerable value on type systems for computer algebra was
+done during the 90's with examples such as {\sl Newspeak}
+(Foderado \cite{Fode83}). A comparative review of systems of that generation
+is given by Fateman \cite{Fate90}. An implementation which increased our
+understanding about the relation between abstract types and
+existential types was the {\sl SOL} language by
+Mitchell and Plotkin \cite{Mitc88}
+and an extension of {\sl SML} with subtyping
+(Mitchell, Meldal, and Madhav \cite{}).
+Also the theorem prover {\sl Nuprl} based on predicative logic can
+elaborate many parts of our type system. $\Sigma$-types are part of
+the {\sl Nuprl} system and facts about abstract theoretical levels can
+be proved directly.
+
+Axiom's new language (Watt \cite{Watt94a}) includes the two first extensions
+but not the last three. Its full type system unifies the concept of
+domains and packages into the concept {\tt type}, allowing objects to
+be instances of packages. This introduces syntactic sugar for
+expressions of the form $Rep\$P$ we described above and is easily
+handled by a compiler. It views packages as records, something which
+needs delicate handling for avoiding unsoundness. Thus categories
+($\exists$ or $\Sigma$ types) are considered as types too, disallowing
+the use of the [forget] rule, since this would lead to undecidability.
+In fact, sharings are not supported.
+
+Various systems handle polymorphism in different ways. Axiom allows
+parameterization of domain definitions. In addition, its new language
+uses types as first class values (as in the language {\sl Pebble} by
+Burstall and Lampson \cite{Lamp88}) and adds run-time type tests, meaning
+that types can be passed as function parameters or returned by
+functions dynamically. This involves loss of static typing information
+as in (Mitchell, Meldal, and Madhav \cite{Mitc88})
+where $\Sigma$-types are coerced to $\exists$-types. In a language
+which does not allow overloaded identifiers for values in a given
+context, type variable can be inferred automatically as in the
+Hindley-Milner type system or by means of type classes as in
+{\sl Haskell's} typing mechanism, allowing for implicit type
+parameterization of functions. In {\sl XFun} by
+Dalmas \cite{Dalm92}
+everything can be a first class value as in the new Axiom, even
+categories (called {\tt signatures}). {\sl XFun} relies on run-time
+type checks. The same is valid about the {\sl Magma} system by
+Cannon and Playoust \cite{Cann01}, which, however, does not include many of
+the features we presented. {\sl Magma} does not allow user defined
+types.
+
+{\sl SML} supports functors with {\tt transparent signatures} and
+{\sl SML/NJ} extends their definition to higher order functors without
+mixing them with values. Recent extensions of the {\sl SML} module
+system with {\tt translucent sums} by
+Harper and Lillibridge \cite{Harp94} involve the definition of
+{\tt first class higher order modules} allowed to be defined as
+values. Type-checking restricts their flexibility in type contexts in
+order to maintain static and strong typing. Our system does not
+support the use of types as values but allows functors and products to
+be applied to them. The concept of type classes has been inspired by
+{\sl Haskell} in order to allow overloading of user defined functions
+on arbitrary types. The extension to support modules as values is
+possible since modules consist of a compile-type and run-time part as
+described in Harper, Mitchell, and Moggi \cite{Harp89}.
+All type information is resolved at compile time but implementations
+can be computed at run-time, thus type components cannot be used as
+values. For instance, if the body of a function $f$ with argument $x$
+involves code which applies a functor $F$ to a package $D$ the value
+components of which may depend on $x$, then the part of $F$ which
+involves type components (static part) can be applied to the type
+components of $D$ out of the body of the function $f$, and the value
+part of $F$ can be applied to the value components of $D$ inside the
+body of $f$, assuming type information derived from the static part. If
+the types depend on $x$ then only abstract types can be created,
+i.e. only minimal typing information can be propagated. Use of
+categories (or types) as values in a static type system is reasonable
+only under restrictions which allow for dynamic typing.
+
+An advanced concept which is part of the {\sl Nuprl} inferencer is the
+use of {\tt propositions as types}. Using propositions, properties
+like associativity can be expressed and proved at the category level
+but operations like equality demand special treatment. We have not
+addressed this issue in our presentation because we want first to
+establish basic type theoretic properties and examine the limits of
+the extensions analyzed. Additionally, the application of propositions
+is not so clear for modeling algebraic structures. Expressing category
+properties in a more limited form as in Axiom can be easily
+incorporated in our system by introducing additional (type or value)
+components into categories.
+
+The sharing construct we presented is an extension of {\sl SML}'s
+sharing constraints
+(MacQueen \cite{Macq88},
+Milner and Tofte \cite{Miln91}) and their extensions by
+Leroy \cite{Lero94},
+and Harper and Lillibridge \cite{Harp94},
+since we allow arbitrary type constructors to be shared, to the point
+this is allowed by the syntactic rules we defined in the
+introduction. Domains are implemented by the construct {\sl abstype}
+in the core {\sl SML} language, or by using packages (abstractions)
+with opaque types in the {\sl SML} module system. This is not possible
+for functors which always have transparent types.
+
+A difference between {\sl SML} and the system presented in this paper
+is that functors in {\sl SML} are {\tt generative}, i.e. two
+instantiations of a functor do not necessarily result in the same type
+or package. This implies that two occurrences of
+{\sl Polynomial(Integer,x)} in the same context may not have
+compatible carrier sets.
+
+\subsubsection{Conditional Categories}
+
+A feature of Axiom which we have not elaborated in this paper are
+{\tt conditional categories}, that is, parameterized categories whose
+body size and kind depends on their arguments. The introduction of
+dependent sums would allow conditional dependencies on the body of the
+category which carries them.
+
+Although the type theoretic properties of conditional categories are
+not well understood, it is easy to show that without certain
+restrictions imposed on them they result in undecidability quite
+easily, even if we assume that domains are not first class objects and
+the arguments of a category are not first class values (the
+undecidability in the case of value arguments is obvious and has been
+examined by Weber \cite{Webe93b}). This happens because the type of the
+argument of a conditional category (and thus its body) can increase in
+the presence of recursive definitions in a way similar to that
+encountered at the $F_{\le}$ type system which has been shown by
+Pierce \cite{Pier91a} to be undecidable. For example, given the definitions:
+\begin{verbatim}
+C():Category == with (if % has Ring then Ring)
+t: C() == add ...
+\end{verbatim}
+it is not clear whether $t$ is a $Ring$, and the system may loop. The
+above situation is handled in {\sl Gauss} (Monagan \cite{Mona93}) purely
+syntactially by viewing \% as the category in scope and checking if
+the defined category (here C) includes code for Rings up to the point
+where the conditional is found: this would add $Ring$ to $C$.
+
+Despite such inconveniences, conditional categories are a very useful
+and powerful construct, which is able to simulate examples supported
+by other higher order systems (like $F_{\le}$), and can implement in a
+unique way many applications from computer algebra where it can
+increase our understanding about the interaction of types.
+
+\subsection{Conclusions}
+
+We have presented selected parts of a type system for symbolic
+computation which is sound and consistent, and powerful enough for
+algebraic applications since it combines and extends commonly used
+systems. The issues of abstract representations, abstract and concrete
+implementations, subtyping without coercions and sharing of domains
+have been handled, solving many problems of existing approaches. For
+the purposes of our analysis we have extended the concept of
+categories to include strong sum types and sharings, and used
+existential types for defining subtyping among domains without need of
+coercions.
+
+A type inference mechanism transforms domains into packages and
+flattens parameterized categories with package instances into sum
+types with sharings. In this way we avoid the combinatorial explosion
+of subtyping hierarchies among categories. The information about
+domain structures is saved for later stages of the inference
+process. Another mechanism constructs type classes as a combination of
+categories and domains, in order to resolve the conflicts introduced by
+the different definitions of subclass and subtype in algebra and type
+theory accordingly. However, in cases in which a subdomain does not
+define operations of its supertype, coercions can be called.
+
+We tried to concentrate on typing issues with respect to computer
+algebra rather than presenting a complete language or system
+design. Therefore we left aside other important topics such as
+exception handling, pattern matching, etc. although these constructs
+are subject to typing in our scheme.
+
+Additional research is of interest in the following subjects:
+\begin{enumerate}
+\item Introduction of {\tt first class packages} in the system without
+sacrificing the nice properties of the presented stratification. This
+should split packages and functors into a static and dynamic part. In
+such case, records and functions can be removed as special cases of
+higher order constructs. The difficulties here involve recursive
+definitions and effects. We need a clear semantics for recursive
+package definitions.
+\item Examination of the appropriate constraints for the introduction
+of conditional categories in order to maintain soundness.
+\item An efficient implementation of type classes without sacrificing
+space
+\item A scheme for coercions which involes algebraic relations as in
+the case of the {\sl Weyl} system by Zippel \cite{Zipp93} instead of simple
+coercions from one type to another.
+\item A more remote target is the introduction of propositions at the
+category level and the integration of an environment for theorem
+proving at the top level.
+\end{enumerate}
+
+This introduced type system is currently implemented for the
+$\lambda{}A$ language designed and implemented by the author at ETH
+Zurich. The concepts presented have been tested in our implementation
+by translating them to SML constructs.
+
\chapter[Doye's Coercion Algorithm]{Doye's Coercion Algorithm by Nicolas Doye}
This chapter is based on a PhD thesis by Nicolas James Doye
diff --git a/changelog b/changelog
index e7f1f1a..da9904c 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20180227 tpd src/axiom-website/patches.html 20180227.03.tpd.patch
+20180227 tpd books/bookvol10.1 add new chapter
20180227 tpd src/axiom-website/patches.html 20180227.02.tpd.patch
20180227 tpd books/bookvolbug bug 7335: type resolution failure
20180227 tpd src/axiom-website/patches.html 20180227.01.tpd.patch
diff --git a/patch b/patch
index 28a1aed..c59bcb8 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,3 @@
-books/bookvolbug bug 7335: type resolution failure
+books/bookvol10.1 add new chapter
-Goal: Axiom Maintenance
\ No newline at end of file
+Goal: Axiom Literate Documentation
\ No newline at end of file
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 319b77f..32f6299 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5912,6 +5912,8 @@ books/bookvolbib add references

books/bookvolbib add references

20180227.02.tpd.patch
books/bookvolbug bug 7335: type resolution failure

+20180227.03.tpd.patch
+books/bookvol10.1 add new chapter

--
1.9.1