An Attempt to Formalise Dylan's Type System (Part 2)
Author Message 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

Sun, 20 May 2001 03:00:00 GMT  An Attempt to Formalise Dylan's Type System (Part 2)

Quote:

> 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.

vi. whether a limited type is null (i.e. the empty set).

Change (37), (39) to:

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 A is null (33.d.vi): return yes;
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).

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:
if B is null (33.d.vi): return yes;
return whether A is disjoint from the base class of B in S.

--
Ashley Yakeley, Seattle WA

Mon, 21 May 2001 03:00:00 GMT  An Attempt to Formalise Dylan's Type System (Part 2)

Quote:

> 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 A is null (33.d.vi): return yes;
>     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).

An error has been pointed out to me:

# Don't forget the case where both A and B are union types and
# each component of A is in some component of B.

This should fix it:

37. Algorithm to determine whether one given type A is a subset of another
given type 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 B is a union type: return whether A is in either component 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 A is null (33.d.vi): return yes;
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).

--
Ashley Yakeley, Seattle WA

Tue, 22 May 2001 03:00:00 GMT

 Page 1 of 1 [ 3 post ]

Relevant Pages