שאלת מבחן בשפות תכנות - האוניברסיטה הפתוחה 2023 - מערכות טיפוסים

להלן נתונה תוכנית בשפת "ויקיש" (INFERRED): ``` let p=proc(x: ?) -(x,5) in (p -((p 5),5)) ``` ברצוננו לקבוע מהו טיפוס התוכנית (אם קיים). לשם כך, עליכם להשתמש באלגוריתם שנלמד בפרק 7 להקשת הטיפוס. א. (15 נקודות) הקצו לביטוי הנתון בשאלה ולתתי הביטויים שלו משתני-טיפוס (Type Variables) מתאימים, וחברו משוואות מתאימות לביטוי הנתון ולתתי הביטויים שלו. ב. (15 נקודות) פתרו את המשוואות שהרכבתם בסעיף א' תוך שימוש ב-substitution ו-unification בדומה למתואר בספר בעמודים 252-258. בסיום פתרון המשוואות רשמו מהו הטיפוס שאותו הקשתם עבור התוכנית הנתונה.

רמז: הקצו משתנה-טיפוס לכל תת-ביטוי: `t_p` לפרוצדורה, `t_x` לפרמטר `x`, ו-`t_body` לגוף. בנו משוואות מהגדרת `proc`, מביטוי החיסור, ומיישום הפרוצדורה, ואז פתרו בעזרת unification.

פתרון: **פתרון — הסקת טיפוסים לתוכנית INFERRED** **סעיף א — הקצאת משתני-טיפוס ובניית משוואות** נסמן: - $t_0$ — טיפוס התוכנית כולה (הביטוי `let ... in ...`) - $t_p$ — טיפוס המשתנה `p` (ופרוצדורת `proc(x: ?) -(x,5)`) - $t_x$ — טיפוס הפרמטר `x` - $t_1$ — טיפוס הביטוי `-(x,5)` (גוף הפרוצדורה) - $t_2$ — טיפוס הביטוי `(p 5)` (היישום הפנימי) - $t_3$ — טיפוס הביטוי `(p 5)-5)` כלומר `-((p 5),5)` - $t_4$ — טיפוס הביטוי `(p -((p 5),5))` (היישום החיצוני = גוף ה-`in`) **משוואות:** 1. מגדרת `proc(x: ?) -(x,5)`: הביטוי הוא פרוצדורה מ-$t_x$ ל-$t_1$: $$t_p = (t_x \to t_1)$$ 2. מביטוי החיסור `-(x,5)`: חיסור דורש ארגומנטים מסוג `int` ומחזיר `int`: $$t_x = \text{int}, \quad t_1 = \text{int}$$ 3. מיישום `(p 5)`: `p` מופעלת על `5` (מסוג `int`), טיפוס התוצאה הוא $t_2$: $$t_p = (\text{int} \to t_2)$$ 4. מביטוי `-((p 5),5)`: חיסור דורש `int`: $$t_2 = \text{int}, \quad t_3 = \text{int}$$ 5. מיישום `(p -((p 5),5))`: `p` מופעלת על ביטוי מסוג $t_3$, התוצאה מסוג $t_4$: $$t_p = (t_3 \to t_4)$$ 6. טיפוס ה-`let` שווה לטיפוס הגוף: $$t_0 = t_4$$ **סעיף ב — פתרון המשוואות בעזרת Substitution ו-Unification** מהמשוואה (2): $t_x = \text{int}$, $t_1 = \text{int}$. מהמשוואה (4): $t_2 = \text{int}$, $t_3 = \text{int}$. מהמשוואה (1): $t_p = (\text{int} \to \text{int})$. נאחד עם משוואה (3): $t_p = (\text{int} \to t_2)$ $$\text{unify}((\text{int} \to \text{int}),\ (\text{int} \to t_2)) \Rightarrow t_2 = \text{int} \checkmark$$ נאחד עם משוואה (5): $t_p = (t_3 \to t_4)$, כלומר $(\text{int} \to \text{int}) = (t_3 \to t_4)$ $$\Rightarrow t_3 = \text{int} \checkmark, \quad t_4 = \text{int}$$ ממשוואה (6): $t_0 = t_4 = \text{int}$. **טיפוס התוכנית: `int`** $\blacksquare$