Subtyping and Type Checking in Programming Language Design

CS 476 – Programming
Language Design
William Mansky
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!
1
Subtyping and Type Checking
2
Subtyping and Type Checking
Checking subtyping has the same problem:
3
Subtyping and Type Checking
But we can change it into a recursive algorithm:
4
Subtyping and Type Checking
 
But we can change it into a recursive algorithm:
 
 
 
 
 
 
How do we know this does the same thing?
5
Subtyping and Type Checking
6
Subtyping and Type Checking
7
Subtyping and Type Checking
8
Subtyping and Type Checking
9
Subtyping and Type Checking
10
Subtyping and Type Checking
11
Subtyping and Type Checking
12
Subtyping and Type Checking
13
Subtyping and Type Checking
14
Subtyping and Type Checking
15
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?
16
Syntax-Directed Rule Systems
 
17
Syntax-Directed Rule Systems
The Syntax-Directed Rule System Algorithm (“Rule Algorithm”):
Input: a judgment from the system
18
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
19
Syntax-Directed Rule Systems
 
Step 1: Find the rule that matches the syntax on the left-hand
side
20
Syntax-Directed Rule Systems
Step 2: Fill in the conclusion of the rule so that it 
exactly
matches what we’re trying to prove
21
Syntax-Directed Rule Systems
Step 2: Fill in the conclusion of the rule so that it 
exactly
matches what we’re trying to prove
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
23
Syntax-Directed Rule Systems
Step 3: Draw a line over the input, and write the filled-in
premises of the rule above it
24
Syntax-Directed Rule Systems
Step 3: Draw a line over the input, and write the filled-in
premises of the rule above it
25
Syntax-Directed Rule Systems
Step 3: Draw a line over the input, and write the filled-in
premises of the rule above it
26
Syntax-Directed Rule Systems
Step 4: For each premise, repeat from Step 1
27
Syntax-Directed Rule Systems
Step 4: For each premise, repeat from Step 1
28
Syntax-Directed Rule Systems
Step 4: For each premise, repeat from Step 1
29
Syntax-Directed Rule Systems
Step 4: For each premise, repeat from Step 1
30
Syntax-Directed Rule Systems
Step 4: For each premise, repeat from Step 1
31
Syntax-Directed Rule Systems
 
Step 4: For each premise, repeat from Step 1
When there are no judgments left in the premises, complete
32
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
33
Subtyping and Type Checking
With subtyping, we have:
When do we actually need to check subtyping?
And when can we get away with just using the most specific
type?
34
Subtyping and Type Checking
When do we actually need to check subtyping?
35
Subtyping and Type Checking
When do we actually need to check subtyping?
Only in arguments!
36
Subtyping and Type Checking
When do we actually need to check subtyping?
Only in arguments!
37
Subtyping and Type Checking
When do we actually need to check subtyping?
Only in arguments!
38
Subtyping and Type Checking
39
Slide Note
Embed
Share

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.


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.

E N D

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!

Related


More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#