CONTENTS - (Use <ENTER> g to access required sections)

 --  Question (A) - what is constrained to have a given type?
 --  Question(B) What grammar does a type-expression denote?
 --    (i) Do we separate type-names and variable-names?
 --    (ii) How do type-names relate to datakey, dataword and defstruct?
 --    (iii) Should type-name-space be flat?
 --  Should dynamic locals have a local type?

                       -------------------------
I am not quite sure  what sure what Steve means  by "Types must become  values
rather than names". A type  -is- in my scheme a  sequence of zero or more  POP
objects.  Since  in  general   there  is  no  way   of  enumerating  a   type,
representations of type have to be  in some sense symbolic, rather than  being
enumerations of all members of the type.  I use -type grammars- as the  actual
objects which represent a type. Clearly,  given the nature of POP (versus  say
Haskell or ML), these should be  first-class objects of POP-11, but of  course
should exist as an abstract data-type.

There are really two questions we have to address when we say

    declare x:Type;

(A) what is the entity -x- which is constrained to have the given -Type-?
(B) what is the grammar denoted by -Type-?

Question (A) - what is constrained to have a given type?
--------------------------------------------------------
  It is clear that the type should be attached to a -permanent identifier-
rather than to the word. Currently this is not done. If it were done, I think
that sections would be handled correctly. Relying on the standard section
mechanism, this would work with declarations separated from section bodies if
preferred (I think this is a good idea, as discussed later).

section mary;
  declare joe:Int->Int, annie:Word -> Number;
endsection

section mary => joe annie;

  define joe(x); lvars x;
    x+2
  enddefine;
  ....
endsection;

The current mechanism for lexicals, which maintains an association between
word and type, mirrors the mechanism the VM is described as using, and would
seem to be adequate. All that is needed is to extend the mechanism for
file-local lexicals.

However, as the system stands, there is no direct way of constraining the
types of lexicals. Experience with the system is indicating that, while much
can be done by type-inference, especially with a functional style of writing
POP-11, it is necessary to be able to put type-constraints on lexicals.
Because I am not enthusiastic about mandating in-line type constraints of the
style:

    define fred(x);
       lvars is_ok:Boolean = false;
    enddefine

I would advocate some kind of way of referring to specific lexicals, e.g.

    declare fred.is_ok:Boolean;

Question(B) What grammar does a type-expression denote?
-------------------------------------------------------
Strategically the questions here are:

(i) Do we separate type-name-space from variable-name-space?
(ii) How do type-names relate to the built-in dynamic type mechanisms of
    POP-11, i.e. key-cells and their associated datawords?
(iii) Does type-name-space have structure related to variable-name-space,
     is it flat, or does it have some other structure?

The decisions taken for the current type-checker are (i) YES, we do have
separated name-spaces and (ii) NO, type-name-space is flat.

  (i) Do we separate type-names and variable-names?
---------------------------------------------------
As far as (i) goes, let me say that I am in favour of keeping a separate
name-space for mapping type-names to type-grammars. If we consider precedents,
it is clear that mainstream LISP is -wrong- in having separate name-spaces for
functions and other object. That is because it prevents LISP being a proper
functional language. Taking the lambda-calculus as model it is quite clear
that LISP has it wrong. And this makes writing higher order functions rather
more difficult, since special operators have to be used to obtain
function-objects from function-names.

But in the same lambda-calculus model, types are distinct from values.
While I would aim to make type-grammars be user-manipulable objects of POP-11,
I nevertheless believe that the advantages of a separate namespace outweigh
the advantages of a uniform one, largely because, while users should be
-encouraged- to write higher order functions frequently, the manipulation of
type-grammars will be something of a specialist activity. Having separate
name-spaces facilitates the use of accepted and/or convenient notation (at
least in an ASCII world) of   T1*T2, T1+T2  for product and union of types,
whereas with a flat namespace T1*T2 would potentially mean ordinary
multiplication.

  (ii) How do type-names relate to datakey, dataword and defstruct?
--------------------------------------------------------------------
To discuss (ii): first let us observe that the built-in dynamic type system
based on key-cells has to be the foundation on which any type-checker is
constructed. The -dataword- is convenient, but secondary, since it is not
necessarily unique, and does not provide access to the attributes of the
class. Secondly, let us observe that the primitive type of objects having a
given key, is -inadequate- as a descriptive mechanism for many important POP
operations. A number can have any one of a variety of keys, some procedures
operate both on words and strings. Lists are best considered as an abstract
data-type, built out of objects which are either pairs or nil, but with
additional constraints.

Bearing this in mind, I have introduced capitalised type-names which are
(mostly) bound to grammars specifying which primitive types are to be unioned
to make up the capitalised type. Thus  Integer  denotes the type of all
monologs of objects that have -integer_key- and -biginteger_key- as their
datakey. This is a useful type because it is closed under +,- and *.

This does of course create problems in relating to defstruct, as well as to
the datakey names. defstruct focusses on a much narrower set of types than the
type-checker, since most of the types to which the latter refers are simply
"full" to defstruct. Moreover, most of the types referred to in defstruct have
very restricted closure properties, so that type-inference is of limited use.

Thus the clash between the conventions I have adopted and -defstruct- is
minimal, since defstruct is talking about different things. The near-clashes
are:
                                              PChar = integer or termin
      int = integer of natural wordsize       Int = POP-11 integer
            (say 32 bits)                           (say 30 bits)
      pint = POP-11 integer
      full = Any POPLOG item.                 Top = any POPLOG item except
                                                    a stack-mark

With the data-word/data-key naming conventions we have:

Clash?  Existing POP-11                    Current Type Checker

Y    integer = POP-11 integer               Int = POP-11 integer
Y    integer_key
Y    isinteger
N    biginteger = POP-11 long integer
N    isbiginteger
N    biginteger_key
Y    isintegral                           Integer = short and long integers

N   isnumber                               Number = anything with a numeric
                                                    dataword
                                                    (integer,....complex)

N   boolean_key                            Boolean = true or false
N   isboolean
N   false                                  False

  (iii) Should type-name-space be flat?
---------------------------------------
The arguments for having a structured name space are much the same as those
for having any name-space be structured, namely that stucture supports
modularity.

There is an argument however that types should be uniform across a large
program, in the same way, say, that uniform standards should apply across a
large engineering project. E.g. in an electronic system, there will be many
dispositions of individual integrated circuits, but only a limited number of
-types- of circuit. If a new type of circuit is needed for the project, quite
likely its designation will be standardised across the project.

For the moment, therefore, I propose to keep a flat name-space for types.

Should dynamic locals have a local type?
----------------------------------------
What should be done with dlocal variables is more problematic. I am inclined
to say that:

define fred(x);
  x+1
enddefine

define joe(x);
  subscrs(1,x)
enddefine

should -not- be type-correct, on the grounds that is -is- the same x in both
cases.

                       ---------------------------

        define revv( vector ); .... enddefine;

This is obviously useful for creating new languages. I am not sure that it
is so useful for the type-checker.

This is the approach to which I am inclining for the type-checker.

(2) Conventions for type variables
-----------------------------------

This is quite a complex issue, as I realise from talking to Haskellers.
I would like to defer discussion until I have hoisted aboard all they have to
say. Suffice it to say that it looks as though we should regard -List- as a
function on grammars in the same way as Hd and Tl are, and say e.g.  List(Int)

My "All" would seem to be related to capital Lambda in the second order
lambda-calculus. There is scope for getting the type-system right and
powerful, although one has to be careful not to require it to be too powerful
and so impossible to make efficient.

As a result of these discussions, I incline towards regarding List as a
function from types to types in the same way as Hd. With care one might arrive
at a precise characterisation of dynamic lists as:

  List = All a;  Pair(Hd(a),Tl(a)) +
                   Pair(^true, Unit->a)  + Nil

  Pair = All a,b; <pair_key>(a,b)

More Later. The a's and b's above would be monologs. One might have 3rd order
types, m and p for monolog and polylog:

         All a:m, b:p; ....

Robin.