\section{Addresses}

Types, values and addresses are an important
part of Max's design.

\begin{description}
\item[Type] A set of unique values

\item[Value] A member of a type

\item[Address] An abstract, globally unique ID consisting of a type and a value

\end{description}

Max types are abstract entities that encapsulate the concept of
uniqueness.  A value in a type is different from all the other values
in the same type.  If you have some way to identify types uniquely,
then you can combine the type and a value from that type to get a
globally unique identifier.  An address is just such a globally unique
ID: Two addresses will be the same if and only if they are of the same
type and also have the same value in that type.

Since Max is meant to have no redundant abstractions, addresses must
be used anywhere uniqueness is needed.  Some examples of situations where 
you would use an address:
\label{addruses}

\begin{itemize}
\item A global constant
\item A reference to an object
\item The value of a typed variable, like a number or a string
\item The value of a pointer
\item The index into an array
\item A handle to a resource
\end{itemize}

@
You can probably think of many more applications of an address.
Addresses need to be quite versatile to support all these uses,
and their versatility depends on the expressiveness of the type system.
Since addresses and types are so closely tied together, we currently
define them in the same module, ``addr.''

<<type>>=
<<Set the current package>>
<<Addresses>>
<<Types>>
@

<<Addresses>>=
<<Define the representation of an address>>
<<Get the type of an address>>
<<Get the value of an address>>
<<Compare two addresses for equality>>
@
\subsection{Representing addresses}

An address consists of a type and a value.  We just use the
obvious approach and represent an address as a list of its type
and its value.

<<Define the representation of an address>>=
(defun make-address-form (typekey addrkey)
        (list typekey addrkey)
)
@
\subsection{Getting the type of an address}

Now that we have a representation of an address we need some 
functions to access its parts.

The only inherent operation on an address is to obtain its type.  The
type can be used to look up all the other operations dealing with the
address.

<<Get the type of an address>>=
; The first item in the list representating an address is the type.
(defun addr-type (addr)
        (car addr)
)
; Max function ADDR-TYPE
(add-init-hook #'(lambda () 
    (let ((addr-type 
                (make-function 'builtin-function *objects* *types*
                    #'current-type
                )
        ))
        (add-public-function addr-type)
        (add-name addr-type "type")
    )
))
@ 

\subsection{Getting the value of an address}

\emph{There is no operation to obtain the value of an address.}  That
is, inside Max, values are opaque.  We just said that we can look up
all the operations dealing with an address if we know its type.  So,
why would we ever need the value of the address?  We already have the
address itself, and we can get all the operations available, including
possibly converting to a string, retrieving an integer representing
the value, or getting some kind of hex number.  There is no reason to
expose the value of an address to the outside world.  In fact, it
would be bad style to allow access to the value except by going
through the published interface for the type.

Ok, so, inside Max you can't get directly at the value of an address.
Inside LISP, we have to get at it in the LISP functions for dealing
with addresses.

<<Get the value of an address>>=
; The second list item in an address is the "value":
; What this actually is depends on the type.
(defun addr-value (addr)
        (cadr addr)
)
@ 

\subsection{Comparing two addresses for equality}

Now, we already know addresses are globally unique IDs.  If we have
two, can we compare them?  Well, within Max, the answer is currently
``possibly not.''  That is, I can't think of a good reason to
\emph{require} that every type implement an equality operation,
so I won't.

Inside LISP, we often need to compare addresses, mostly in the unit
tests.  The function ADDR-EQUAL takes two addresses and returns the
LISP truth value (NIL or non-NIL) of their equality.  It will compare
the types first, then if they are equal, use a type-specific
comparison on the values.  However, the type-specific comparison
might trigger a runtime error (if the ADDR-VALUE-EQUAL method is not
defined on the target type).  Since ADDR-EQUAL is not a published
interface inside Max, that's OK.

<<Compare two addresses for equality>>=
; Two addresses are equal iff:
; their type field is the same symbol and
; their value is equal as defined by the class of the type of the addresses
; Uses addr-value-equal, a generic function which needs to be implemented
; by the class of every type (unless they want addr-equal to fail)
(defun addr-equal (a b)
        (and
                (type-equal (addr-type a) (addr-type b))
                (addr-value-equal 
                        (addr-type a)
                        (addr-value a) 
                        (addr-value b)
                )
        )
)
(add-init-hook #'(lambda ()
    (let ((addr-equal
        (make-function 'builtin-function
            (type-product *objects* *objects*)
            *boolean-type*
            #'(lambda (twoobjs)
                (let ((vals (product-values twoobjs)))
                    (boolean-cond #'(lambda ()
                        (addr-equal (first vals) (second vals))
                    ))
                )
            ))
        ))

        (add-public-function addr-equal)
        (add-name addr-equal "equal")

    )
))

@ 

\section{Types}

A type is an entity containing some number of unique values.  Max's
type system is designed to allow easy creation of types of all kinds
so that you can use the appropriate model for the problem you are
trying to solve.  There are enumerated types, union (sum) types, and
tuple (product) types.  We intend to add inductive types in a future
iteration.  Types themselves have the type ``types'', making them
first-class objects.  Most of the modules that follow are focused on
defining a new type and some behavior for it.

<<Types>>=
<<Definitions common to all types>>
<<Enumerated types>>
<<Sum types>>
<<Product types>>
<<The null type>>
@ 
<<Set the current package>>=    
(in-package :max)
@ 
The implementation of types contains the following elements,
which will be covered in the order shown.

<<Definitions common to all types>>=
<<Define the class of types>>
<<Base identity for type products>>
<<Base identity for type sums>>
<<Define the default comparison method for values in the same type>>
<<Create a class for the type of types>>
<<Create the one instance representing the type of types>>
<<Create the address of the type of types>>
<<Create a new type and return its address>>
<<Compare two types>>
<<Get the instance implementing a type given its address>>
@
\subsection{Representing types}

We use CLOS to represent types, since we have several different
kinds of types with different implementations.  Here's the base class.
All classes that implement types are derived from this class.
An instance of any type class implements an individual type.

<<Define the class of types>>=
(defclass max-type ()
        nil
)
@ 

Base case for type products.  Every type is a
1-tuple.  See \ref{products}.

<<Base identity for type products>>=
(defmethod factors ((atype max-type))
    (list (make-address-form (addr-value *types*) atype))
)

@ 
<<Base identity for type sums>>=
(defmethod members ((atype max-type))
    (list (make-address-form (addr-value *types*) atype))
)
@ 
\subsection{Comparing values in a type}

Most classes of types will have a method called ADDR-VALUE-EQUAL.  This
method compares two values that are already known to in the same type.
We'll define this method using EQ on the base class of types because many of 
the subclasses currently use EQ to compare values.  They won't have to
define their own method since they can just use this default one.

<<Define the default comparison method for values in the same type>>=
; Default comparison for two address values is EQ
; since most are now CLOS instances
(defmethod addr-value-equal ((s max-type) a b)
        (eq a b)
)
@ 

\subsection{The type of types}

We will want to refer to types explicitly as first-class objects in Max.
This means assigning an address to each type.  An address consists of
a type and a value, and if the value represents one type, we need to
create the type of types to complete the address.

@ 
Let's create a class for the type of types, since it's different
from other types.
<<Create a class for the type of types>>=
; the class for a type of types
(defclass types-type (max-type)
        nil
)
@ 
Let's create an instance of the class we just defined.
Since there's only one type of types, this seems silly, but
it's because CLOS is class-based instead of prototype-based.
CLOS dispatches on instances only.
<<Create the one instance representing the type of types>>=
; *types-instance* will be the CLOS instance of a type of types.
; There's normally just one such instance.
(defparameter *types-instance* (make-instance 'types-type))
@ 
Now we want to refer to the type of types in Max, so it should also
be a first-class object (address).  Since it's a type, it's only appropriate
that it be its own type.

We'll test that the type of types is its own type by checking its
type field is EQ to its value field.

@ 
<<Create the address of the type of types>>=

; *types* will be the Max address of the type of types.
(defparameter *types* (make-address-form *types-instance* *types-instance*))
(add-init-hook #'(lambda () (add-name *types* "types")))
@ 

\subsection{Creating types}

MAKE-TYPE creates a new type and returns its address.  It defaults to
creating an enumerated type (defined in section \ref{enum}), but you
can specify any class of type using the :class keyword argument.  The
:key keyword argument allows you to assign a symbolic name to this
type, but this option is currently ignored.

We'll store the instance implementing a type directly in the value
part of the address.  Recall that the value part can be anything;
it is totally up to the type being implemented.

<<Get the instance implementing a type given its address>>=
(defun typeaddr-instance (typeaddr)
        (addr-value typeaddr)
)
@
The type part of the address will contain the value of the 
type of types, which we take from the value field of *types*.

<<Create a new type and return its address>>=
; Ignore the key for now, maybe store in a slot for debugging later
(defun make-type (&key (class 'enumerated-type) key)
        (make-address-form (addr-value *types*) (make-instance class))
)
@

A and B are both instances.
Two types are equal if they have the same instance (EQ),
or, if they are different instances of the same class and 
their class considers them equal.

<<Compare two types>>=
(defun type-equal (a b)
    (or
        (eq a b)
        (and
            (eq (class-of a) (class-of b))
            (type-specific-equal (class-of a) a b)
        )
    )
)
(defun addr-type-equals (type addr)
    (type-equal (addr-value type) (addr-type addr))
)
@ 
By default, two types are equal if they have the same instance.
Types for which this is not true (such as product types) can 
override this method.
<<Compare two types>>=
(defmethod type-specific-equal ((ty max-type) a b)
    (eq a b)
)

@
\subsection{Enumerated types}
\label{enum}
The first class of types we want to create is a simple one: enumerated
types.  An enumerated type is defined by listing all the values.
<<Enumerated types>>=
<<Define the class of enumerated types>>
<<Get the hash table implementing an enumerated type>>
<<Create an identifier for a value>>
<<Add a value to an enumerated type>>
@
Currently we use a model where you create a new empty enumerated type
using MAKE-TYPE and then proceed to add values into it using
MAKE-ADDRESS.  This violates one of the principles of Max's design: to
only use one abstraction for dynamism (Pointers, section
\ref{ptr})
.  So this API should change someday to a better one
where you start with the empty enumerated type and repeatedly use a
function to return a new enumerated type based on the last one.
I have not thought about whether it is possible to make this change yet, but
it's not a high priority.

An enumerated type is implemented by a hash table stored in the instance.

<<Define the class of enumerated types>>=
; An enumerated type is created by adding elements one by one,
; explicitly.  It is necessarily finite, and is implemented by a
; hash table: each key corresponds to the address of one item in the 
; type.
; Current examples of enumerated types: *boolean-type*, *types*,
; *functions*
(defclass enumerated-type (max-type)
        ((hash :initform (make-hash-table)
                :accessor hash
                :documentation 
                "Keys are addresses; values are implementation data for each address"
        ))
)
@ 

TYPE-HASH is a function to retrieve the hash table that implements
an enumerated type.  It isn't meant to work with other classes of types,
but we can't make it a method because it takes an address, and addresses
are not CLOS instances.
<<Get the hash table implementing an enumerated type>>=
(defun type-hash (typeaddr)
        (hash (typeaddr-instance typeaddr))
)
@ 
The values in an enumerated type are represented by symbols used as the keys
in the hash table.  We allow the user (whoever is building an enumerated type)
to choose the symbols if they wish, otherwise we create one with a name
like ADDR1, ADDR2, etc.  

GET-ADDR-KEY takes a symbol or NULL; if NULL it creates a key named ADDRn
using its global variable that it increments when used (one counter
for all enumerated types).  If non-NULL it just returns the argument.
<<Create an identifier for a value>>=
(defparameter *n_keys* 0)
(defun get-addr-key (sym)
        ; Return key for address using "ADDRnn" if key not specified.
        ; Key names are only for implementation debugging and are not
        ; part of the system design.
        (if (null sym)
                (progn
                        (incf *n_keys*)
                        (nth-value 0
                                (read-from-string
                                        (format nil "~a~a" 'addr *n_keys*)
                                )
                        )
                )
                ; else str argument was provided
                sym
        )
)
@ 

MAKE-ADDRESS takes the address of an enumerated type and modifies it
to contain a new value.

The :key keyword argument specifies an optional symbolic name for the
new value.  If it is unspecified, GET-ADDR-KEY is called to generate
one.

The :value keyword argument allows enumerated types to store some
type-specific private information along with the value.
<<Add a value to an enumerated type>>=
#| 
Add a new value to an enumerated type and return the new address.

Required: typeaddr = the max address of the type that the address is
to live in

Optional: key = the symbol to put in the enumerated type's hash table
as this address' key rather than the default ADDRx

Optional: value = value to store in the type's hash table with the
new address as key (Use value only for things that are not Max
addresses and thus can't be returned in functions)
|#
(defun make-address (typeaddr &key key (value nil))
        (let ((type (typeaddr-instance typeaddr))
                (addr-key (get-addr-key key)))

                ; Hash value
                (setf (gethash addr-key (hash type)) value)

                ; Return the new address, including the type it is in
(make-address-form (addr-value typeaddr) addr-key) ) )
@ 
\subsection{Sum types}
\label{sums}
A sum type is a type created by taking the disjoint union of two or
more other types, here called member types.  Disjoint union means the
values in the two types never overlap, so the new type contains one
value for each value in either of the member types.  We need a
non-overlapping union because otherwise two addresses in different
types might be equal, and then addresses wouldn't be globally unique.

Contrast this kind of union to the union of mathematical sets.  See
SET-UNION in section \ref{sets})
.
@ 
Ok, here's the interface.
<<Sum types public interface>>=
<<Create the sum of N types>>
<<Get a sum constructor>>
<<Get all the sum constructors for a sum type>>
<<Get the current member type of a sum address>>
<<Sum destructor>>
@ 
And here's the layout of the implementation.
<<Sum types>>=
<<A class for sum types>>
<<Compare two values in the same sum type>>
<<Sum types public interface>>

@

Sum types definitely need their own class.  In the instance
implementing an individual sum type, we need to remember what
member types were summed to create it.  That's the only slot in this class.

<<A class for sum types>>=
; The class of types which are created by taking the sum of other types.
; Note that addresses in sum types are actually in a different type
; depending on which types are in the sum.
; Each sum type has its own instance of class sum-type.
; Two sum types made from the same members will have an identical-looking
;  instance- but won't be the same instance.
; When comparing the addresses of two such sum types, they will be unequal
; in the addr-value-equal sense.  Need a CLASS SUM-TYPE-ADDRESS or something
; if we want to be able to compare them and treated as addr-value-equal.
(defclass sum-type (max-type)
        ((members :reader members :type list
                :initarg :members
                :documentation "The list of types that were summed to make this one"))
)
@ 
TYPE-SUM creates a sum type.  It takes a LISP list of addresses of types, to be the
member types, and returns the address of the new type.

The new address is of the type ``types'', and has an instance of the class of
sum types as its value.

TODO: All types should be the sum of just 1 type

<<Create the sum of N types>>=
; Create a type containing the combined
; values from N other types
; (discriminated union?)
; The other types become known as the member types
(defun type-sum (&rest typeaddrs)
        (make-address-form 
                (addr-value *types*) 
                (make-instance 'sum-type :members typeaddrs)
        )
)
@

A sum constructor is a function taking an argument in one of the
member types of a sum, and returning a value in the sum type.
There are N sum constructors for the sum created from N types.
Max functions are defined in section \ref{function}
.

MAKE-SUM-CONSTRUCTOR takes the address of a sum type and the address of
one of its member types and returns the appropriate sum constructor.

The sum constructor is responsible for building an address into the
sum type (a sum address).  The type of a sum address indicates which
sum type it's in, and is an instance of the class of sum types.
The value in a sum address is simply the complete address from the
member type, including its type and value.

In Max we don't have type coercion, or subtyping.  All type conversion
has to be explicit in the first-order system, so that introspection
reveals a precise description of the system and proofs can be done
step by step.  Any automatic conversion can be done by searching for
conversion functions, building an expression containing them, and
evaluating the expression.

Since we don't have subtypes, we had to make the type of a sum address
simply be ``types.''  So functions operating on sum types must also
operate on any other type.  We'll treat non-sum types as if they were
the sum of a single type.

The ``if'' statement here creates a special case when both arguments
are the same type.  This allows any type to be a sum type of just
itself.  Also, if [[(make-sum-constructor *objects* *objects*)]] didn't
return identity, converting from objects to objects would make a value
that grows redundantly.

<<Get a sum constructor>>=
; Declare *objects* global that we refer to before it's initialized
(defparameter *objects* nil)
(defun make-sum-constructor (sumtype membertype)
    (if (eq (addr-value sumtype) (addr-value membertype))
        ;then
        (identity-function sumtype)
        ;else
        (make-function 'builtin-function membertype sumtype
                #'(lambda (membervalue)
                        (make-address-form (addr-value membertype) (addr-value membervalue))
                )
        )
    )
)

(add-init-hook #'(lambda ()
  (let ((make-sum-constructor 
            (make-function  'builtin-function 
                            (type-product *types* *types*)
                            *functions*
                #'(lambda (sum-and-member)
                     (apply #'make-sum-constructor (product-values sum-and-member)))
        )))
     (add-public-function make-sum-constructor)
     (add-name make-sum-constructor "constructor")
  )
))

@ 
Here's a helper function to get a set of max functions
that create values from each of the member types of a sum type.
Functions and sets are defined in later sections.% Add refs when complete
<<Get all the sum constructors for a sum type>>=
; Given the address of a sum type, return a Max set of
; function addresses, each one of which takes an argument
; in one of the member types and returns an address in the sum type.
(defun get-constructors (sumtype)
        (let    ((funcset (get-empty-set)))

                (map nil #'(lambda (membertype) 
                        (setf funcset (set-add funcset 
                                (make-sum-constructor sumtype membertype)
                        )))
                        (members (addr-value sumtype))
                )

                funcset
        )
)
(add-init-hook #'(lambda ()
    (let ((get-constructors (make-function 'builtin-function *types* *set-type*
            #'get-constructors)))

        (add-public-function get-constructors)
        (add-name get-constructors "constructors")
    )
))
    
@

Here we define equality of two values in the same sum type, specializing
our generic function for comparing two values in the same type.

Note that addr-value-equal's ``a'' and ``b'' arguments are
\emph{values} in the sum type, but \emph{addresses} in the member
types (as defined in the structure of a sum address above).  Therefore
we can compare ``a'' and ``b'' using the comparison for addresses,
ADDR-EQUAL.

<<Compare two values in the same sum type>>=
; Two addresses in the same sum type are equal iff their
; stored addresses are addr-equal.  ADDR-EQUAL compares
; their types and values.  It is assumed that their
; types are one of the member types of this sum type.
(defmethod addr-value-equal ((ss sum-type) a b)
        (addr-equal a b)
)
@

An address in a sum type must correspond to exactly one
of the member types.  CURRENT-TYPE does this lookup,
taking an address in a sum type and returning the
address of the member type.

<<Get the current member type of a sum address>>=
; Given an address in a sum type,
; return the address of the type of the current value
; (will be one of the sum type's members at all times)
(defun current-type (sumaddr)
        (make-address-form (addr-value *types*) (addr-type (addr-value sumaddr)))
)

@ 
Given a sum address return the sum value, which is an address
in the current sum type.
<<Sum destructor>>=
(defun sum-value (sumaddr)
    (addr-value sumaddr)
)


@ 
\subsection{Product types}
\label{products}

Product types, like sum types, are created from N other types.
However, while a sum type contains a value corresponding to exactly
one of the N types, a product type contains a value for \emph{each} of
the N types.

Product types create a multidimensional type.  An address is
constant, but given one in a product type you should be able to get a
new address by changing one of the component dimensions to refer to a
different address in its original type.
@
<<Product types interface>>=
<<Create a product type>>
<<Get the list of types used to create a product type>>
<<Product address constructor>>
<<Product address destructor>>
@ 
In order to completely implement product types, we'll need
a class and an internal method for comparing values, as well
as the functions implementing the interface.
<<Product types>>=
<<Create the class of product types>>
<<Compare two values in the same product type>>
<<Compare two product types>>
<<Product types interface>>
@
The only internal information an instance of a product type
needs to store is the factors: the list of types used to create it.
<<Create the class of product types>>=
; The class of types created by taking the product of other types.
(defclass product-type (max-type)
        ((factors :reader factors :type list
                :initarg :factors
                :documentation "The list of types that were multiplied to make this one"
        ))
)
@ 
TYPE-PRODUCT creates a product type.  The argument is a LISP list of
addresses of types... the result is the address of the product type.

Like TYPE-SUM, these implementations are imperfect.  They should
return the same type when given the same arguments, but they don't.  I
guess we need an ADDR-TYPE-EQUAL generic function in order to allow
different classes of types to compare their instances for equality,
instead of just using EQ which causes different instances to always be
different.

If only 1 type is specified, it is returned: The product of one type
is itself.

<<Create a product type>>=
; Create a type containing multiple dimensions:
; one for each of N other types
; Product types
; * Given a list of types, return a new type called a product type.  
;   The original types then become known as the factor types of the product type.
(defun type-product (&rest typeaddrs)
    (if (= 1 (length typeaddrs))
        (car typeaddrs)
        (make-address-form 
                (addr-value *types*) 
                (make-instance 'product-type :factors typeaddrs)
        )
    )
)
@ 
Here's a public interface to access the types used to create a product type.
<<Get the list of types used to create a product type>>=
; Given the address of a product type, return a list of addresses of its factor types
(defun product-types (prodtype)
        (factors (addr-value prodtype))
)
@ 

Return an address in a product type given the address of the type and
a LISP list of addresses in all of the component types.  The order of
addresses needs to be the same as the order of the addresses of their
types that was passed into TYPE-PRODUCT to create the product type.

Form of an address in a product type: Value field contains list of
addresses in the respective factor types.  This is kind of lazy; the
type field in these addresses is redundant, since it's stored in the
product type's instance. We'd have to use map to remove/add it back
in.

<<Product address constructor>>=
(defun make-product-addr (prodtype addrlist)
    (if (= 1 (length addrlist))
            (car addrlist)
            (make-address-form (addr-value prodtype) addrlist)
    )
)
@

Given an address in a product type, return a list of addresses in the
corresponding factor types

Inverse of MAKE-PRODUCT-ADDR.  A destructor is a function that
retrieves part of the structure of something.

<<Product address destructor>>=
(defun product-values (prodaddr)
        (addr-value prodaddr)
)

@
Compare two values in the same product type by comparing the respective values
corresponding to each component type.

<<Compare two values in the same product type>>=
; Compare values in the same type product
; Does not check if the factors match the types of the addresses in a or b,
; just if the addresses are equal
;
; Note: This method will only be called if the exact same
; type instance object is used for the type field of the address.
; If you make two set product types from the same factors,
; they will be DIFFERENT TYPES (this will change sometime)
(defmethod addr-value-equal ((ps product-type) a b)
        ; Create list of truth values for comparing each successive address in a and b
        ; then AND them all together (AND returns the list of truth values either way
        (eval (cons 'and (map 'list
                #'(lambda (x y) (addr-equal x y))
                (product-values a) (product-values b))
        ))
)
@ 

Compare two product types.  Two product types are equal
iff the corresponding component types are type-equal.

<<Compare two product types>>=
(defmethod type-specific-equal ((c product-type) a b)
    (eval (cons 'and (map 'list
        #'(lambda (x y) (type-equal x y))
        (factors a) (factors b))
    ))
)

@ 
\subsection{The null type}
\label{null-type}
@ 
<<The null type>>=
<<Define the null type>>
@
% Since we still haven't introduced max functions, maybe this should go into
% the function module. Or inside its own module.
<<Define the null type>>=
; Create the Null type, which never has any addresses.
; To be used for the domain of functions with no arguments,
; for example
(defclass null-type (max-type) nil)

(defparameter *null-type* (make-type :class 'null-type))
(add-init-hook #'(lambda () (add-name *null-type* "null")))
@  
Let's enable *print-circle*, in case we have some circular data
structures.  MOVE THIS to somewhere that actually creates circular
structures. (Hash table implemeneting *domains* inside function.lsp?)
<<Enable detection of circular data structures>>=
(setf *print-circle* t)