[Types-sig] List of FOO

[skaller]

Martin wrote, in reponse to Paul:

>>1. This system is supposed to be extensible, right? So I could, for
>> instance, define a binary tree module and have "binary trees of ints"
>> and "binary trees of strings." How do I define the binary tree class and
>> state that it is parameterizable?
>
>Good question; so far I only thought about making built in types (such
>as list) parameterizable. One could however do something similar with
>classes, though:

Let me turn that around. In Viper, there are NO fixed names
for any types: types are just any objects. This leads to
the question Martin asked immediately. Before I proceed, another
observation: in Viper, there is a class

	class PyListType: ....

for lists, but it is planned to allow

	class PyListOf: ...

The idea is that this is a parameterized type, and the
instance is specified by constructing an object:

	PyListOfInt = PyListOf(PyIntType)

The class PyListOf contains methods like 'append' which
take THREE arguments, instead of two: the first argument
is the type.

When an object of kind 'PyListOfInt' is the type object of
some object x, then a call like

	x.append(1)

ends up calling 

	PyListOf.append(PyIntType, x, 1)

which means it can check that 1 is of type PyIntType.
In other words, PyListOf is a meta-type, which happens
to be a class, and the instance type, PyListOfInt
is an _instance_ of it.

In this system, there is no provision for types like

	[Int]

meaning a list of integers, instead, any object
which has the type 'list of integers' actually
has a type object 'ListOfInt' physically available.

One of the points of this type system is that 
builtin types and user defined types are all the same:
they all have type objects which provide methods.
[That is, the type system is unified, although it
is not the case classes are types, but instead that
any object can be a type, and all types are objects]

In this system, the client must CONSTRUCT a type
as that type. Therefore

	[1,2,3]

has type list, NOT type list of integer.

I'm not saying this is good, but I am saying that
two problems raised in this list disappear automatically:

	1) complicated syntax, aluded to by Paul, cannot occur.
	   Indeed, NO new syntax is required at all (to name types)

There is ONLY one way to name a type: by refering to an object.
Hence 'function taking list of X of Y returning .....' simply
cannot occur: no new syntax for typing is used. Example:

	decl X: ListOfListOfTupleOfInt

is possible, if the client defined that horrible name.
You can't say:

	decl X: ListOf(IntType)

because that is a different object to the type object of

	decl Y:ListOfInt(IntType)

since class instance objects are compared by address.

	2) Extension objects are not different to builtin ones.

BOTH use the same idea, of having type objects associated with them,

[In fact, there is a hack in Viper: builtin types' type object
is found by an extra indirection, since the objects don't
exist when the interpreter is first started]

If I can summarise: there is considerable advantage using
arbitrary objects as type objects: they can be specified
using EXISTING python syntax, using the power of the EXISTING
python interpreter, without needing a special, second class
language, to complicate python, and pose an additional
implementation overhead.

In particular, the idea is that the type inference mechanism
can _compile_ the type objects like any other, and therefore
NO special handling is required for extension types.
The ONLY types the inference engine needs to 'know' about
are the builtin ones. 

I'm not sure if this will work :-)

BTW: In Viper, extension 'modules' do NOT build any vtables
or objects, they're just a table of named functions.
No types! The 'types' are constructed in Python,
usually with a class:

	class XType:
		mymethod = Xmymethod

[at present, all 'extensions' have their functions loaded
directly into _builtins_, which is something I will soon
have to fix]

--
One thing I think we DO need though, is a categorical sum.
In ML notation:

	IntOrNone = Int | None

Python does not support sum objects, so it isn't obvious
how to represent type sums using objects. I'm working on this.
In ML, this is done by:

	type Sum = X | Y of int | Z of float
	let sum = Y 1 in ...

Python, like other languages, needs this construction,
it is as fundamental as tuples (in fact, it is
precisely the categorical dual of a tuple or struct)
Dictionaries can be used for this, as can pairs
(kind, value), so it can be represented, just not
nicely. [I'm still thinking on how to do this 'pythonically' <g>]

--
John Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia
homepage: http://www.maxtal.com.au/~skaller
voice: 61-2-9660-0850