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.

Should also add:

      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  
 
 [ 3 post ] 

 Relevant Pages 

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

2. Dylan's type system

3. Dylan's type system

4. Difference between a type system and a type constraint system

5. (fwd) harlequin's dylan-corba mailing list switching to MIT's info-dylan

6. Difference between a type system and a type constraint system

7. first attempt at Harlequin-Dylan

8. Intermetric's Mitchell Gart's vain attempt to censor other's opinions

9. (upgraded-complex-part-type 'cons)?

10. Bizarre behaviour of 'qsort' call attempt

11. Miranda's Type System

12. Biff's-own-guide to type systems?

 

 
Powered by phpBB® Forum Software