Subtyping and Type Checking in Programming Language Design

In the realm of programming language design, subtyping and type checking play crucial roles. This content delves into how syntax-directed rule systems evolve when dealing with subtyping, presenting the challenges and the solutions through a recursive algorithm approach. The discussion includes the theorem stating the relationship between subtyping and the subtype relation, along with the proof by rule induction in each direction.

• Programming Language Design
• Subtyping
• Type Checking
• Recursive Algorithm
• Theorem

leno Follow

Uploaded on Oct 11, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. CS 476 Programming Language Design William Mansky

2. Subtyping and Type Checking Up until now, our rule systems have been syntax-directed: the syntax of a term tells us which rule to apply A syntax-directed rule system is also an algorithm!

3. Subtyping and Type Checking Up until now, our rule systems have been syntax-directed: the syntax of a term tells us which rule to apply But with subtyping, we have: ? ?1 ?1<:?2 ? ?2 This could apply to any term And we don t know what ?1 to try

4. Subtyping and Type Checking Checking subtyping has the same problem: ? <:? CT ? = class ? extends ? { } ? <:? ? <:? ? <:? ? <:?

5. Subtyping and Type Checking But we can change it into a recursive algorithm: ? <:? CT ? = class ? extends ? ? <:? ? <:?

6. Subtyping and Type Checking But we can change it into a recursive algorithm: subtype(?,?) CT ? = class ? extends ? subtype(?,?) subtype(?,?) How do we know this does the same thing?

7. Subtyping and Type Checking Theorem: ? <:? if and only if subtype(?,?). Proof: by rule induction in each direction. First: if subtype(?,?) then ? <:?. Base case: subtype(?,?) . Then ? <:?

8. Subtyping and Type Checking Inductive case: CT ? = class ? extends ? subtype(?,?) subtype(?,?) and by the inductive hypothesis, ? <:?. Then ? ? <:?

9. Subtyping and Type Checking Inductive case: CT ? = class ? extends ? subtype(?,?) subtype(?,?) and by the inductive hypothesis, ? <:?. Then ? <:? ? <:? ? <:?

10. Subtyping and Type Checking Inductive case: CT ? = class ? extends ? subtype(?,?) subtype(?,?) and by the inductive hypothesis, ? <:?. Then CT ? = class ? extends ? { } ? <:? ? <:? ? <:?

11. Subtyping and Type Checking Second: if ? <:? then subtype(?,?). Base case: . Then ? <:? subtype(?,?)

12. Subtyping and Type Checking Second: if ? <:? then subtype(?,?). Inductive case 1: CT ? = class ? extends ? { } ? <:? and no inductive hypothesis. Then ? subtype(?,?)

13. Subtyping and Type Checking Second: if ? <:? then subtype(?,?). Inductive case 1: CT ? = class ? extends ? { } ? <:? and no inductive hypothesis. Then CT ? = class ? extends ? subtype(?,?) subtype(?,?)

14. Subtyping and Type Checking Inductive case 2: ? <:? ? <:? ? <:? and by the inductive hypothesis, subtype(?,?) and subtype(?,?). Then ? subtype(?,?)

15. Subtyping and Type Checking Inductive case 2: ? <:? ? <:? ? <:? and by the inductive hypothesis, subtype(?,?) and subtype(?,?). Lemma: subtype is transitive. Proof: by rule induction. (Intuition: subtype just climbs up the class hierarchy, and if A is below B and B is below C, then A is below C.)

16. Subtyping and Type Checking Theorem: ? <:? if and only if subtype(?,?). Proof: by rule induction in each direction. We can conclude that the subtype algorithm correctly implements the subtyping relation <:. So we can use subtype in type checking.

17. Syntax-Directed Rule Systems The type systems we ve worked with have been syntax-directed A syntax-directed type system leads directly to an algorithm for applying that system What is that algorithm?

18. Syntax-Directed Rule Systems (? is a number) (?,?) ? (? ? = ?) (?,?) ? (?1,?) ?1 (?2,?) ?2 (? = ?1+ ?2) (?1+ ?2,?) ? ?,? ? ? ?,? (skip,? ? ? )

19. Syntax-Directed Rule Systems The Syntax-Directed Rule System Algorithm ( Rule Algorithm ): Input: a judgment from the system (?,?) ? ?,? (? ,? ) (3 + 4,{}) 7 x 3,{} (skip,{x = 3}) y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1 (x + y,{x = 3,y = 5}) 8

20. Syntax-Directed Rule Systems The Syntax-Directed Rule System Algorithm ( Rule Algorithm ): Input: a judgment from the system (?,?) ? ?,? (? ,? ) Output: a proof tree for that judgment, or an error if no proof exists

21. Syntax-Directed Rule Systems Step 1: Find the rule that matches the syntax on the left-hand side ?,? ? ? ?,? (skip,? ? ? ) Assign (y,Add (y,1)) y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

22. Syntax-Directed Rule Systems Step 2: Fill in the conclusion of the rule so that it exactly matches what we re trying to prove ?,? ? ? ?,? (skip,? ? ? ) y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

23. Syntax-Directed Rule Systems Step 2: Fill in the conclusion of the rule so that it exactly matches what we re trying to prove ? y ? y + 1 ? ?1 ?,? ? ? ?,? (skip,? ? ? ) y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

24. Syntax-Directed Rule Systems Step 2: Fill in the conclusion of the rule so that it exactly matches what we re trying to prove ? y ? y + 1 ? ?1 ? 1 ?,? ? ? ?,? (skip,? ? ? ) y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

25. Syntax-Directed Rule Systems Step 3: Draw a line over the input, and write the filled-in premises of the rule above it ?,? ? ? y ? y + 1 ? ?1 ? 1 ? ?,? (skip,? ? ? ) y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

26. Syntax-Directed Rule Systems Step 3: Draw a line over the input, and write the filled-in premises of the rule above it ?,? ? ? y ? y + 1 ? ?1 ? 1 ? ?,? (skip,? ? ? ) ?,? ? y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

27. Syntax-Directed Rule Systems Step 3: Draw a line over the input, and write the filled-in premises of the rule above it ?,? ? ? y ? y + 1 ? ?1 ? 1 ? ?,? (skip,? ? ? ) y + 1,?1 1 y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

28. Syntax-Directed Rule Systems Step 4: For each premise, repeat from Step 1 ?,? ? ? y ? y + 1 ? ?1 ? 1 ? ?,? (skip,? ? ? ) y + 1,?1 1 y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

29. Syntax-Directed Rule Systems Step 4: For each premise, repeat from Step 1 (?1,?) ?1 (?2,?) ?2 (? = ?1+ ?2) (?1+ ?2,?) ? y + 1,?1 1 y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

30. Syntax-Directed Rule Systems Step 4: For each premise, repeat from Step 1 (?1,?) ?1 (?2,?) ?2 (? = ?1+ ?2) (?1+ ?2,?) ? ?1 y ?2 1 ? ?1 ? 1 y + 1,?1 1 y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

31. Syntax-Directed Rule Systems Step 4: For each premise, repeat from Step 1 (?1,?) ?1 (?2,?) ?2 (? = ?1+ ?2) (?1+ ?2,?) ? ?1 y ?2 1 ? ?1 ? 1 y,?1 ? y + 1,?1 1 y y + 1,?1 (skip,?2) 1,?1 ? where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

32. Syntax-Directed Rule Systems Step 4: For each premise, repeat from Step 1 (?1(y) = 0) y,?1 0 y + 1,?1 1 y y + 1,?1 (skip,?2) 1,?1 ? where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

33. Syntax-Directed Rule Systems Step 4: For each premise, repeat from Step 1 When there are no judgments left in the premises, complete (?1(y) = 0) y,?1 0 (1 is a number) 1,?1 1 y + 1,?1 1 y y + 1,?1 (skip,?2) where ?1= x = 3,y = 0 and ?2= x = 3,y = 1

34. Syntax-Directed Rule Systems The Syntax-Directed Rule System Algorithm ( Rule Algorithm ): Step 1: Find the rule that matches the syntax on the left-hand side of the input Step 2: Fill in the conclusion of the rule so that it exactly matches what we re trying to prove Step 3: Draw a line over the input, and write the filled-in premises of the rule above it Step 4: For each premise, repeat from Step 1

35. Subtyping and Type Checking With subtyping, we have: ? ?1 ?1<:?2 ? ?2 When do we actually need to check subtyping? And when can we get away with just using the most specific type?

36. Subtyping and Type Checking When do we actually need to check subtyping? ? ? fields ? = ,? ? ?.? ? ?1 int ?2 int ?1+ ?2 int fields C = ?1 ?1, ,?? ?? ?1 ?1 ?? ?? new ? ?1, ?? ? ? C methods ? = ,? ? ?1 ?1, ,?? ?? ?1 ?1 ?? ?? ? = ?.? ?1, ??; ok

37. Subtyping and Type Checking When do we actually need to check subtyping? Only in arguments! fields C = ?1 ?1, ,?? ?? ?1 ?1 ?? ?? new ? ?1, ?? ? ? C methods ? = ,? ? ?1 ?1, ,?? ?? ?1 ?1 ?? ?? ? = ?.? ?1, ??; ok

38. Subtyping and Type Checking When do we actually need to check subtyping? Only in arguments! fields C = ?1 ?1, ,?? ?? 2?1 ?1 2?? ?? ?1<:?1 ??<:?? 2new ? ?1, ?? ? ? C methods ? = ,? ? ?1 ?1, ,?? ?? ?1 ?1 ?? ?? ? = ?.? ?1, ??; ok

39. Subtyping and Type Checking When do we actually need to check subtyping? Only in arguments! fields C = ?1 ?1, ,?? ?? 2?1 ?1 2?? ?? ?1<:?1 ??<:?? 2new ? ?1, ?? ? 2? C methods ? = ,? ? ?1 ?1, ,?? ?? 2?1 ?1 2?? ?? ?1<:?1 ??<:?? 2? = ?.? ?1, ??; ok

40. Subtyping and Type Checking Theorem: if 2? ?, then ? ?. Theorem: if ? ?, then there is some ? <:? such that 2? ?. (the most specific type for ?) We can conclude that 2? ok if and only if ? ok. So we can use system 2 as a typechecking algorithm for the original type system!