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

Part 1: Objects and Classes

Dylan deals in objects and classes. That classes are objects is not, for
the moment, relevant.

Anything not marked as a proposition is a definition or an axiom.

1. Let <object> be the set of all possible objects.

2. By 'type', I understand any subset of <object>.

3. An object x is said to be a 'general instance' of type T if x is a
member of T.

4. Let <class> be the set of all possible classes.

5. There is a map from <object> to <class> called 'object-class'.

6. Every class is a type.

7. For every object x, x is a member of object-class(x).

8. An object x is said to be a 'direct instance' of class C if
object-class(x) == C.

9. <object> is a class. By 'the root class', I understand <object>.

10. There is a map from <class> to the set of all subsets of <class>
called 'direct-superclasses'.

11. A class C is said to be a 'direct superclass' of class D if C is a
member of direct-superclasses(D).

12. A class D is said to be a 'direct subclass' of class C if C is a
member of direct-superclasses(D).

13. For every class C, direct-superclasses(C) = the empty set if and only
if C = <object>.

14. For every class D, every direct superclass of D is a strict superset of D.

15. For every object x, for every class H, if x is a member of H then
object-class(x) is a subset of H.

16. For every class C, for every class D, if C is a strict superset of D
then there exists a direct superclass H of D, such that C is a superset of
H.

17. Class C is said to be a 'superclass of depth 0' of class D if and only
if C = D.

18. For any given natural number n > 0, class C is said to be a
'superclass of depth n' of class D if and only if there exists a direct
superclass H of D such that C is a superclass of depth n-1 of H.

19. Class C is said to be a 'superclass' of class D if and only if there
exists some natural number n such that C is a superclass of depth n of
class D.

20. Class C is said to be a 'strict superclass' of class C if and only if
C is a superclass of D and C != D.

21. Class D is said to be a 'subclass' of class C if and only if C is a
superclass of D.

22. Class D is said to be a 'strict subclass' of class C if and only if C
is a strict superclass of D.

23. A class C is said to be 'of level 0' if and only if C = <object>.

24. For any given natural number n > 0, class C is said to be 'of level n'
if and only if every direct superclass of C is of level n-1.

25. Proposition: for any natural number n, if a class C is of level n,
then C is of level n+1.
Proof: Let P(n) be the proposition:
    If a class C is of level n, then C is of level n+1.

Suppose class C is of level 0. Then (23) C = <object>. Then (13) C has no
direct superclasses. Then every direct superclass of C is of level 0. Then
(24) C is of level 1. Therefore P(0) is true.

If for some n>0 P(n-1) is true:

    Suppose class C is of level n. Then (24) every direct superclass of C
is of level n-1. Because P(n-1) is true, every direct superclass of C is
of level n. Then (24) C is of level n+1. So P(n) is true.

P(0) is true, and for every n > 0, P(n-1) implies P(n). Therefore, by
induction, P(n) is true for all natural n.

For any natural number n, if a class C is of level n, then from P(n), C is
of level n+1. QED

26. For every class C, there exists a natural number n such that C is of
level n.

27. Proposition: for any two classes C and D, C is a superset of D if and
only if C is a superclass of D.
Proof:

i. Let P(n) be the proposition:
    For any two classes C and D, if C is a superclass of depth n of D,
then C is a superset of D.

If C is a superclass of depth 0 of D, then (17)  C = D and C is a superset
of D. Therefore P(0) is true. If for some n > 0 P(n-1) is true:

    Suppose C is a class that's a superclass of depth n of a class D. Then
(18) there exists a direct superclass H of D such that C is a superclass
of depth n-1 of H. We know (14) H is a superset of D. We know from P(n-1)
that C is a superset of H. Therefore C is a superset of D, and P(n) is
true.

P(0) is true, and for every n > 0, P(n-1) implies P(n). Therefore, by
induction, P(n) is true for all natural n.

Suppose class C is a superclass of class D. Then (19) there is some
natural n for which C is a superclass of depth n of D. Since P(n) is true,
C is a superset of D.

ii. Let Q(n) be the proposition:
    For any two classes C and D, if D is of level n, and C is a superset
of D, then C is a superclass of D.

If for some n > 0 Q(n-1) is true:

    Suppose D is a class of level n and C is a class that's a superset of
D. Then either:

        (a) C = D. Then (17) C is a superclass of depth 0 of D and (19) C
is a superclass of D.
        (b) C is a strict superset of D. Then (16) there exists a direct
superclass H of D, such that C is a superset of H. We know (24) H is of
level n-1, and C is a superset of H, so we know from Q(n-1) that C is a
superclass of H. We know (19) there exists some number i such that C is a
superclass of depth i of H. Since H is a direct superclass of D, then (18)
C is a superclass of depth i+1 of D. Therefore (19) C is a superclass of
D.

    Therefore C is a superclass of D. Therefore Q(n) is true.

Q(0) is true, and for every n > 0, Q(n-1) implies Q(n). Therefore, by
induction, Q(n) is true for all natural n.

Suppose class C is a superset of class D. Then (26) there is some natural
n such that D is of level n. Since Q(n) is true, C is a superclass of D.

iii. For any two classes C and D, if C is a superclass of D then (i) C is
a superset of D, and if C is a superset of D then (ii) C is a superclass
of D. Therefore C is a superset of D if and only if C is a superclass of
D. QED

--
Ashley Yakeley, Seattle WA



Sun, 20 May 2001 03:00:00 GMT  
 
 [ 1 post ] 

 Relevant Pages 

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

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