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

שאלה ג (25 נקודות) להלן הצגה של מנונית תחכומה בשפה "יוטורג": $$\text{let } y = 9$$ $$\text{in}$$ $$\text{let } z = \text{zero?} (-(y,3))$$ $$\text{in}$$ $$\text{proc } (w)$$ $$\text{if } z \text{ then } (w \text{ } z) \text{ else } z$$ ברצונינו לקבוע מהו טיפוס תחכומה (אם קיימים), לשם כך, עיסקו להשתמש בהלוגוריתם בבחוניות שהוזכר בפרק 7 בסעיף טיפוס. **א (10 נקודות)** הקצו ליטורי תחכומים של טיפוס Type Variables של כל התחכומים בביטויים, וחברו משוואות משתנאות מהתחכומים לטיפוסים של קיימים שם.

רמז: יש לעבור על כל תת-ביטוי בתוכנית, להקצות לו משתנה טיפוס ייחודי, ולייצר משוואות אילוצים בהתאם לכללי הטיפוסיות של כל מבנה בשפה (קבוע, משתנה, let, if, proc, הפעלת פונקציה).

פתרון: אלגוריתם הסקת הטיפוסים פועל בשני שלבים עיקריים: ראשית, הקצאת משתני טיפוס לכל תת-ביטוי. שנית, יצירת מערכת משוואות (אילוצים) על משתנים אלו על פי כללי הטיפוסיות של השפה. פתרון מערכת המשוואות יניב את הטיפוס של הביטוי, אם קיים. **שלב 1: הקצאת משתני טיפוס (Type Variables)** נקצה משתנה טיפוס לכל תת-ביטוי ולכל משתנה בתוכנית. נסמן את הטיפוס של ביטוי $E$ ב-$T(E)$: * $T(y) = \tau_y$ * $T(9) = \tau_9$ * $T(z) = \tau_z$ * $T(3) = \tau_3$ * $T(-(y,3)) = \tau_{\text{minus_app}}$ * $T(\text{zero?}(-(y,3))) = \tau_{\text{zero_app}}$ * $T(w) = \tau_w$ * $T((w \text{ } z)) = \tau_{\text{wz_app}}$ * $T(\text{if } z \text{ then } (w \text{ } z) \text{ else } z) = \tau_{\text{if}}$ * $T(\text{proc } (w) \dots) = \tau_{\text{proc}}$ * $T(\text{let } z = \dots \text{ in } \dots) = \tau_{\text{let_z}}$ * $T(\text{let } y = \dots \text{ in } \dots) = \tau_{\text{let_y}}$ (זהו הטיפוס של הביטוי כולו) **שלב 2: יצירת משוואות טיפוסים** נגזור את מערכת המשוואות על סמך מבנה הביטוי וכללי הטיפוסיות: 1. **קבועים ופרימיטיבים:** * $\tau_9 = \text{Int}$ (הקבוע 9 הוא מספר שלם) * $\tau_3 = \text{Int}$ (הקבוע 3 הוא מספר שלם) * $T(-) = (\text{Int} \times \text{Int}) \to \text{Int}$ (הפעולה `-` מקבלת זוג שלמים ומחזירה שלם) * $T(\text{zero?}) = \text{Int} \to \text{Bool}$ (הפרדיקט `zero?` מקבל שלם ומחזיר בוליאני) 2. **ביטוי `let y = 9 in ...`:** * $\tau_y = \tau_9$ (המשתנה `y` מקבל את הטיפוס של הביטוי אליו הוא נקשר) * $\tau_{\text{let_y}} = \tau_{\text{let_z}}$ (הטיפוס של ביטוי `let` הוא הטיפוס של גוף הביטוי) 3. **ביטוי `let z = zero?(-(y,3)) in ...`:** * $\tau_z = \tau_{\text{zero_app}}$ (המשתנה `z` מקבל את הטיפוס של הביטוי אליו הוא נקשר) * $\tau_{\text{let_z}} = \tau_{\text{proc}}$ (הטיפוס של ביטוי `let` הוא הטיפוס של גוף הביטוי) 4. **הפעלת הפעולה `-` על `(y,3)`:** * $T(-) = (\tau_y \times \tau_3) \to \tau_{\text{minus_app}}$ (מכלל הטיפוסיות של הפעלת פונקציה) 5. **הפעלת הפרדיקט `zero?`:** * $T(\text{zero?}) = \tau_{\text{minus_app}} \to \tau_{\text{zero_app}}$ (מכלל הטיפוסיות של הפעלת פונקציה) 6. **הגדרת הפרוצדורה `proc (w) ...`:** * $\tau_{\text{proc}} = \tau_w \to \tau_{\text{if}}$ (הטיפוס של פרוצדורה הוא פונקציה מטיפוס הפרמטר לטיפוס הגוף) 7. **הפעלת המשתנה `w` על `z`:** * $\tau_w = \tau_z \to \tau_{\text{wz_app}}$ (הטיפוס של `w` חייב להיות פונקציה מהטיפוס של `z` לטיפוס התוצאה) 8. **ביטוי `if z then ... else ...`:** * $\tau_z = \text{Bool}$ (התנאי בביטוי `if` חייב להיות בוליאני) * $\tau_{\text{wz_app}} = \tau_z$ (ענף ה-`then` וענף ה-`else` חייבים להיות מאותו טיפוס) * $\tau_{\text{if}} = \tau_{\text{wz_app}}$ (הטיפוס של ביטוי `if` הוא הטיפוס המשותף של שני הענפים) $\blacksquare$