An Attempt to Formalise Dylan's Type System (Part 2)

Part 2: Class Systems

28. A 'class system' or 'system' is a set of classes S such that for every

class C in S, every direct superclass of C is in S. Class systems

represent all the classes created at a given time during the running of a

Dylan program.

29. An object x is considered to be a 'potential object' of system S if

object-class(x) is in S.

30. For a class system S, 'pot(S)' is the set of all potential objects of S.

31. Two types A and B are considered 'disjoint in' system S if the

intersection of A, B and pot(S) is the empty set.

32. A class C is said to 'join' two types A and B in system S if S union

{C} is a system, A and B are disjoint in S, and A and B are not disjoint

in S union {C}.

33. Dylan allows the specification of certain types ('specified types').

These are:

a. Classes

b. 'Union types', each the union of any two specified types (known as

'component types').

c. 'Singletons', each a type containing exactly one object, for any object

(the singleton's 'object')

d. 'Limited types', each a certain kind of subset of a class (known as the

'base class' of the type). Dylan restricts limited types in such a way as

it can always calculate:

i. whether an object is a member of a limited type;

ii. whether a limited type is equivalent to a class;

iii. whether a limited type is equivalent to a singleton;

iv. whether one limited type is a subset of another limited type;

v. whether two limited types are disjoint in a class system.

34. Algorithm to determine whether a given class D is a subclass of a

given class C:

return D == C or any member of direct-superclasses(D) is a subclass of C.

35. Algorithm to determine whether a given object x is in a given class C:

return object-class(x) is a subclass of C.

36. Algorithm to determine whether a given object x is in a given

specified type T:

If T is a class: see (35);

if T is a union type: return x is in either of T's component types;

if T is a singleton: return x is the object of T;

if T is a limited type: see (33.d.i).

37. Algorithm to determine whether one given type A is a subset of another

given type B:

If B is a union type: return whether A is in either component of B;

if A is singleton type: return whether A's object is in B (36);

if A is a union type: return whether both components of A are subsets of B;

if A is a class:

if B is a singleton type: return no;

if B is a limited type: see (33.d.ii);

if B is a class: return whether A is a subclass of B (34);

if A is a limited type:

if B is a singleton type: return whether A and B are equivalent (33.d.ii);

if B is a limited type: see (33.d.iv);

if B is a class: return whether the base class of A is a subclass of B (34).

38. Algorithm for determining whether two types A, B are equivalent:

return whether A is a subset of B (37) and B is a subset of A (37).

39. Algorithm to determine whether two given types A, B are disjoint in

system S:

If either (wlog A) is a singleton type: return not whether A's object is

in B (36);

if either (wlog A) is a union type: return whether both components of A

are disjoint from B;

if both are classes: return not whether there exists a class in S that is

a subclass of both A and B;

if both are limited types: see (33.d.v);

if one (wlog A) is a class and the other (B) is a limited type: return

whether A is disjoint from the base class of B in S.

--

Ashley Yakeley, Seattle WA