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

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

רמז: בשפת INFERRED גוף ה-proc הוא ביטוי יחיד. התחביר `proc (x : Type) Expression` מאפשר בדיוק ביטוי אחד כגוף. הקצו: `t0` לכל הביטוי, `tx` ל-`x`, `tbody` לגוף ה-proc. הכלל: `zero?(e)` דורש שטיפוס `e` יהיה `int` ומחזיר `bool`. פתרו עם unification.

פתרון: **הבהרה תחבירית:** בשפת INFERRED (פרק 7 ב-EOPL), תחביר `proc` הוא: ``` Expression ::= proc (Identifier : Type) Expression ``` הגוף הוא **ביטוי יחיד**. בשפה זו אין `begin`/sequence. לכן בתוכנית: ``` (proc (x : !) zero?(x) let z=7 in z) ``` הגוף של ה-proc הוא `zero?(x)` בלבד — זהו ביטוי שלם. הביטוי `let z=7 in z` מופיע אחרי סיום גוף ה-proc בתוך הסוגריים החיצוניים, אך מבחינה תחבירית ב-INFERRED גוף ה-proc אינו יכול לכלול שניים — הפרסר לוקח את הביטוי הראשון (`zero?(x)`) כגוף, ו-`let z=7 in z` הוא תוספת שאינה חלק מגוף ה-proc. מסקנה: הגוף הוא `zero?(x)`, טיפוס ה-proc הוא `int → bool`. --- **סעיף א — הקצאת משתני טיפוס ובניית משוואות:** נסמן: - $t_0$: טיפוס הביטוי הכולל `(proc (x : !) zero?(x))` - $t_x$: טיפוס הפרמטר `x` - $t_{body}$: טיפוס גוף ה-proc, כלומר `zero?(x)` משתני הטיפוס הנוספים הנובעים מתת-הביטויים: - הביטוי `zero?(x)`: `zero?` הוא פרימיטיב בעל טיפוס `int → bool`. הוא מוחל על `x`. - `!` (unknown type annotation) מקבל משתנה טיפוס חדש, נסמנו $t_x$. **משוואות:** 1. כלל `proc`: גוף ה-proc הוא $t_{body}$, הפרמטר הוא $t_x$: $$t_0 = (t_x \to t_{body})$$ 2. כלל `zero?`: `zero?(x)` דורש ש-`x` יהיה מטיפוס `int`, ומחזיר `bool`: $$t_x = \text{int}$$ $$t_{body} = \text{bool}$$ (הסימן `!` בהכרזת הפרמטר מציין טיפוס לא-ידוע שיוסק — הוא מקבל את משתנה הטיפוס $t_x$.) --- **סעיף ב — פתרון המשוואות (substitution ו-unification):** נתחיל עם substitution ריקה $\sigma = \{\}$. **שלב 1:** ממשוואה (2), נאחד $t_x$ עם $\text{int}$: $$\sigma = \{t_x \mapsto \text{int}\}$$ **שלב 2:** ממשוואה (2), נאחד $t_{body}$ עם $\text{bool}$: $$\sigma = \{t_x \mapsto \text{int},\ t_{body} \mapsto \text{bool}\}$$ **שלב 3:** ממשוואה (1), נציב את $\sigma$ ונקבל: $$t_0 = (\sigma(t_x) \to \sigma(t_{body})) = (\text{int} \to \text{bool})$$ **Substitution סופי:** $$\sigma = \{t_x \mapsto \text{int},\ t_{body} \mapsto \text{bool},\ t_0 \mapsto (\text{int} \to \text{bool})\}$$ **הטיפוס של התוכנית:** $(\text{int} \to \text{bool})$ כלומר, התוכנית היא פרוצדורה המקבלת ארגומנט מסוג `int` ומחזירה ערך מסוג `bool`. $\blacksquare$