למה צריך מערכות טיפוסים (Type Systems)?
עד עכשיו, השפות שבנינו (LET, PROC, IMPLICIT-REFS) היו שפות שבדקו טיפוסים בזמן ריצה (Run-time / Dynamic Typing). מה זה אומר? אם המתכנת עשה טעות וכתב -(5, true), המפרש שלנו התחיל לעבוד, ניסה לעשות expval->num לבוליאני, ואז קרס עם שגיאה באמצע הריצה.
הבעיה עם גילוי שגיאות מאוחר
דמיינו מערכת להטסת חללית. הפונקציה deployParachute() נקראת רק כאשר גובה החללית יורד מתחת ל-1000 מטר. אם בפונקציה הזו יש שגיאת טיפוס (למשל, מנסים להכפיל פונקציה במספר), אנחנו נגלה את זה רק בזמן שהחללית נופלת! זה מאוחר מדי.
המטרה של פרק 7 היא ליצור שפות שתופסות את השגיאות האלו לפני שהתוכנית בכלל מתחילה לרוץ (Compile-time / Static Typing).
מה זה "טיפוס" (Type)?
טיפוס הוא תווית שמודבקת לכל ביטוי בשפה, שאומרת "איזה סוג של מידע יצא מכאן בסוף?". בשפות שלנו יש שלושה טיפוסים מרכזיים:
- int - עבור כל המספרים.
- bool - עבור אמת ושקר.
- T1 -> T2 - עבור פונקציות. פונקציה שמקבלת טיפוס T1 ומחזירה טיפוס T2 (למשל: פונקציה שמקבלת int ומחזירה bool תיכתב כ-
int -> bool).
איך בודקים קוד בלי להריץ אותו?
הטריק הוא לבנות מפרש מקביל. אם למדנו שהפונקציה value-of רצה על ה-AST ומחשבת ערכים, אנחנו נבנה פונקציה חדשה שנקראת type-of. היא תרוץ על אותו ה-AST, אבל במקום לחשב מספרים, היא תחשב טיפוסים.
במקום סביבה רגילה (Environment) ששומרת [x=5], היא תשתמש בסביבת טיפוסים (Type Environment) ששומרת [x=int].
הדמיה השוואתית: בדיקת טיפוסים סטטית מול מפרש ריצה הדמיה אינטראקטיבית
ראו כיצד מערכת בדיקה סטטית (Type Checker) תופסת שגיאות טיפוס לפני ההרצה, לעומת מפרש רגיל (Interpreter) המגלה שגיאות רק בזמן ריצה וקורס.
בקרה:
צינור העיבוד ומצב הסביבה:
קבצי המקור של שפת CHECKED
שפת CHECKED היא שפה בעלת מערכת טיפוסים סטטית המוכרזת במפורש. בואו נראה אילו קבצים מגדירים אותה וכיצד הם משתלבים בארכיטקטורה של השפה.
checker.scm (חדש!)
לב מערכת הטיפוסים. מכיל את הפונקציה type-of ואת ייצוג סביבת הטיפוסים (Tenv).
lang.scm
מגדיר את הדקדוק המעודכן, הכולל ביטויי טיפוסים (Types) והערות טיפוס על משתנים.
interp.scm & data-structures.scm
המפרש וערכי הריצה. שים לב: הם אינם כוללים בדיקות טיפוסים בזמן ריצה! אנו מסתמכים ב-100% על ה-Type Checker.
top.scm
הקובץ המקשר שמנהל את ה-Pipeline הדו-שלבי: בדיקה סטטית (Type Check) ולאחר מכן ריצה (Evaluation).
צינור העיבוד הדו-שלבי (EOPL Pipeline)
בשפות הקודמות, הקוד עבר ישירות לפענוח (Parsing) ולאחר מכן לריצה. בשפת CHECKED אנו מוסיפים שלב ביניים קריטי:
🚀 Zero-Cost Abstraction
בגלל שהוכחנו סטטית שאין שגיאות טיפוס, מפרש הריצה ב-interp.scm רץ מהר יותר ופשוט יותר. אין צורך לבדוק ב-if-exp האם התנאי הוא בוליאני, או ב-diff-exp האם האיברים הם מספרים. הבטיחות מובטחת מראש!
שפת CHECKED (בדיקה סטטית)
שפת CHECKED היא השפה הראשונה שמוסיפה Type Checking (בדיקת טיפוסים). היא דורשת מהמתכנת להכריז במפורש (Explicit Annotations) על הטיפוס של כל פרמטר בפונקציה. זה מזכיר מאוד את שפת C או Java.
הדקדוק החדש (lang.scm)
נוסף לנו מבנה תחבירי חדש שנקרא Type, ושינינו את הגדרת הפונקציה (proc) כך שתדרוש את הטיפוס של הפרמטר שלה:
% הגדרות הטיפוסים בשפה:
Type ::= int
Type ::= bool
Type ::= (Type -> Type)
% השינוי בפונקציות ורקורסיה:
Expression ::= proc (Identifier : Type) Expression
Expression ::= letrec Type Identifier (Identifier : Type) = Expression in Expression
איך הקוד נראה?
כדי להגדיר פונקציה שמקבלת x ומחסרת ממנו 1, המתכנת חייב להצהיר ש-x הוא מסוג int.
let f = proc (x : int) -(x, 1)
in (f 10)בלולאת letrec ההכרזה ארוכה אפילו יותר, כי צריך להצהיר גם על טיפוס החזרה של הפונקציה עצמה:
letrec int fact (n : int) =
if zero?(n) then 1 else *(n, (fact -(n,1)))
in (fact 5)השוואה לשפות קודמות
בשפת PROC הישנה, פונקציות היו "דינמיות" לחלוטין. ב-CHECKED אנו מעבירים חלק מהאחריות למערכת הטיפוסים הסטטית. נשים לב להבדל התחבירי והסמנטי המרכזי:
| נושא | שפת PROC (דינמית) | שפת CHECKED (סטטית) |
|---|---|---|
| הגדרת פונקציה | proc (x) ... |
proc (x : int) ... |
| שגיאת טיפוסים | מתגלה רק בזמן ריצה כשמנסים לחשב את הביטוי. | מתגלה בשלב ה-Compilation (בדיקת הטיפוסים הסטטית) ללא הרצת קוד. |
| הגדרת רקורסיה | letrec f(x) = ... |
letrec bool f(x : int) = ... |
מנוע הבדיקה: type-of
הפונקציה type-of היא המקבילה המושלמת ל-value-of, אבל במקום לעבוד בעולם של טיפוסים (Types). היא רצה לאורך עץ ה-AST ומוודאת שכל פעולה היא חוקית.
מימוש type-of ב-checker.scm
(define type-of
(lambda (exp tenv) ; tenv = Type Environment!
(cases expression exp
; 1. מספר: הטיפוס שלו הוא תמיד int
(const-exp (num) (int-type))
; 2. שליפת משתנה מסביבת הטיפוסים (Tenv)
(var-exp (var) (apply-tenv tenv var))
; 3. חיסור מתמטי:
(diff-exp (exp1 exp2)
(let ((ty1 (type-of exp1 tenv))
(ty2 (type-of exp2 tenv)))
(check-equal-type! ty1 (int-type) exp1)
(check-equal-type! ty2 (int-type) exp2)
(int-type)))
; 4. בדיקת אפס (zero?):
(zero?-exp (exp1)
(let ((ty1 (type-of exp1 tenv)))
(check-equal-type! ty1 (int-type) exp1)
(bool-type)))
; 5. פקודת תנאי (if):
(if-exp (exp1 exp2 exp3)
(let ((ty1 (type-of exp1 tenv))
(ty2 (type-of exp2 tenv))
(ty3 (type-of exp3 tenv)))
(check-equal-type! ty1 (bool-type) exp1)
(check-equal-type! ty2 ty3 exp)
ty2))
; 6. ביטוי Let:
(let-exp (var exp1 body)
(let ((exp1-type (type-of exp1 tenv)))
(type-of body (extend-tenv var exp1-type tenv))))
; 7. יצירת פונקציה (proc):
(proc-exp (var var-type body)
(let ((result-type (type-of body (extend-tenv var var-type tenv))))
(proc-type var-type result-type)))
; 8. הפעלת פונקציה (call):
(call-exp (rator rand)
(let ((rator-type (type-of rator tenv))
(rand-type (type-of rand tenv)))
(cases type rator-type
(proc-type (arg-type result-type)
(begin
(check-equal-type! arg-type rand-type rand)
result-type))
(else (eopl:error 'type-of "Rator not a proc type!")))))
; 9. רקורסיה (letrec):
(letrec-exp (p-result-type p-name b-var b-var-type p-body letrec-body)
(let ((tenv-for-letrec-body
(extend-tenv p-name (proc-type b-var-type p-result-type) tenv)))
(let ((p-body-type
(type-of p-body (extend-tenv b-var b-var-type tenv-for-letrec-body))))
(check-equal-type! p-body-type p-result-type p-body)
(type-of letrec-body tenv-for-letrec-body))))
)))🧠 סביבת טיפוסים (Tenv) מול סביבת ריצה (Env)
חשוב להבין את ההפרדה המוחלטת בין שני סוגי הסביבות:
- סביבת ריצה (Environment): מופעלת ב-
value-of, שומרת שמות של משתנים ומקשרת אותם לערכי ריצה אמיתיים כמו מספרים או קלוז'רים (למשל:x = num-val(5)). - סביבת טיפוסים (Type Environment - Tenv): מופעלת ב-
type-of, שומרת שמות של משתנים ומקשרת אותם לטיפוסים הסטטיים שלהם (למשל:x = int-type). סביבה זו קיימת רק בזמן הקומפילציה!
מחולל טיפוסים מסדר גבוה (High-Order Type Builder) הדמיה אינטראקטיבית
בנו טיפוסים של פונקציות מסדר גבוה (פונקציות שמקבלות או מחזירות פונקציות) וראו כיצד מיוצגים הטיפוסים במפרש checker.scm של EOPL ומה משמעותם התחרותית.
התוצאה המיוצרת:
פונקציה המקבלת מספר שלם ומחזירה מספר שלם.
קבצי המקור של שפת INFERRED
שפת INFERRED מאפשרת להשמיט את הגדרות הטיפוסים באמצעות שימוש בסימן שאלה ?. כדי לבצע את פלא הסקת הטיפוסים, המפרש משתמש במערכת קבצים מתוחכמת יותר.
מבנה הקבצים החדש
-
inferrer.scm (מחליף את checker.scm)
מבצע את בדיקת הטיפוסים הסטטית. בניגוד ל-
type-ofהקודם שהחזיר טיפוס, כאן הוא מחזירan-answer- מבנה הכולל את הטיפוס המוסק ואת טבלת ההצבות (Substitutions) המעודכנת. -
substitutions.scm (חדש!)
מנהל מילון שממפה משתני טיפוס זמניים (Type Variables כמו $t_1, t_2$) לטיפוסים אמיתיים שהתגלו במהלך הריצה (למשל $int, bool$). מספק פונקציות חיוניות כמו
extend-subst(הוספת אילוץ) ו-apply-subst-to-type(שליפת המידע המעודכן). -
unifier.scm (חדש!)
מנוע האיחוד. הפונקציה
unifierמקבלת שני טיפוסים וסביבת הצבות. היא מנסה לאלץ את שני הטיפוסים להיות זהים. אם היא מצליחה, היא מחזירה סביבת הצבות חדשה הכוללת את המסקנות החדשות. אם יש התנגשות בלתי אפשרית (למשל $int$ מול $bool$), היא קורסת עם Type Error. -
equal-up-to-gensyms.scm (חדש!)
מודול עזר לבדיקות המשווה בין שני טיפוסים שנוצרו אוטומטית, ומוודא שהמבנה שלהם זהה ללא תלות במספר הסידורי הייחודי שהמפרש נתן להם במהלך יצירת משתנים זמניים.
הארכיטקטורה של הסקת טיפוסים
כאשר המפרש נתקל בסימן ? (המיוצג תחבירית כ-no-type בדקדוק), הוא מייצר עבורו משתנה טיפוס טרי (Fresh Type Variable). בקוד הוא נראה כ-%tvar-type עם מספר סידורי רץ (למשל tvar1, tvar2, tvar3).
בזמן ריצת ה-Inferrer על עץ התוכנית, אנו אוספים משוואות ומעבירים אותן ל-Unifier. ה-Unifier מעדכן את מאגר ה-Substitutions שמייצג את כל ה"ידע הקיים" שיש לנו על המשתנים הזמניים. כל משוואה שנפתרת מעשירה את הידע הזה.
בסיום ריצת אלגוריתם ההסקה, אנו מפעילים apply-subst-to-type על משתנה הטיפוס הראשי של התוכנית. פונקציה זו מחליפה את כל משתני הטיפוס הזמניים בטיפוסים האמיתיים שהסקנו בעזרת המילון.
הסקה אוטומטית: שפת INFERRED
שפת CHECKED היא בטוחה, אבל הופכת את הקוד למסורבל. מתכנתים לא רוצים לכתוב (x : int) בכל מקום. שפות מתקדמות כמו TypeScript או Haskell מאפשרות הסקת טיפוסים (Type Inference). המהדר חכם מספיק להסתכל על הקוד ולנחש לבד מה צריך להיות הטיפוס!
הדקדוק: סימן השאלה (?)
בשפת INFERRED, המתכנת יכול לכתוב סימן שאלה ? במקום לכתוב את הטיפוס. הוא אומר למפרש: "תגלה לבד".
; הטיפוס הוסתר בעזרת ?
let f = proc (x : ?) -(x, 1)
in (f 10)המטרה של האלגוריתם היא לפענח מה מסתתר מאחורי כל סימן שאלה בתוכנית, על ידי איסוף רמזים ופתרון משוואות.
שלושת השלבים להסקה
איך אלגוריתם כזה עובד? ממש כמו פתרון מערכת משוואות במתמטיקה (נעלמים $x, y$):
- מיפוי משתנים זמניים: מעניקים משתנה זמני (Type Variable המסומן באות $t$) לכל סימן שאלה ולכל ביטוי משמעותי בקוד.
- איסוף אילוצים (Constraints): עוברים על ה-AST ומייצרים משוואות לפי החוקים (למשל, חיסור דורש $int$).
- הצבה (Unification): פותרים את המשוואות בשיטת האלימינציה. ככל שפותרים יותר משוואות, ערך הנעלמים נחשף, עד שכל ה- $t$-ים הופכים לטיפוסים אמיתיים!
שלב 1: יצירת המשוואות (Constraints)
השלב הראשון בהפעלה הוא לקחת את התוכנית, להעניק שמות (Type Variables) לכל ביטוי, ולהוציא מהקוד את החוקים (המשוואות) שהוא מחייב. כל פעולה מתמטית או לוגית מפיקה משוואה.
חוקי הגזירה (The Rules)
בואו נכיר את התבניות. נניח שסימנו ביטוי $E$ במשתנה טיפוס $t_E$. אילו רמזים נוכל לדלות?
zero? בודקת האם מספר הוא 0. לכן: הקלט $t_{E1} = int$. התוצאה של הפעולה כולה היא תמיד $bool$.Rator על הארגומנט Rand, והפעולה כולה מחזירה תוצאה שנסמן ב-$t_{Res}$, אזי הפונקציה עצמה חייבת להיות מהמבנה: $t_{Rator} = t_{Rand} \r\rightarrow t_{Res}$.שלב 2: פתרון המשוואות (Unification)
לאחר שיצרנו את כל המשוואות (רשימת ה-Equations), אנחנו מתחילים "לנקות" אותן בעזרת טבלה של שתי עמודות: עמודת המשוואות (Equations) שעוד צריך לפתור, ועמודת ההצבות (Substitutions) שבה אנו שומרים עובדות מוגמרות שמצאנו.
איך פותרים (אלגוריתם ההצבה)?
אנו עוברים על עמודת המשוואות אחת-אחת (מלמעלה למטה) ומפעילים את החוקים הבאים:
- זהות: אם הגענו למשוואה כמו $int = int$ או $t_1 = t_1$, פשוט מוחקים אותה. אין לה משמעות.
- גילוי משתנה (Substitution): אם הגענו למשוואה מהצורה $t_1 = int$ (או $t_1 = t_2 \r\rightarrow bool$). מצאנו עובדה! מעבירים אותה לעמודת ההצבות. אבל, החלק החשוב ביותר: עוברים על כל שאר המשוואות שנותרו, ובכל מקום שכתוב $t_1$, מוחקים וכותבים במקומו את הערך החדש!
- פירוק פונקציות: אם הגענו למשוואה המורכבת משני חצים, למשל $t_1 \r\rightarrow int = bool \r\rightarrow t_2$. כדי שזה יהיה שווה, צד שמאל של החץ חייב להיות שווה לשמאל, והימני לימני. לכן, מוחקים את המשוואה הזו ומפצלים אותה לשתי משוואות חדשות בתחתית הרשימה: $t_1 = bool$ ו-$int = t_2$.
- שגיאת טיפוס (Failure): אם הגענו למצב של התנגשות מהותית, למשל $int = bool$, או $int = t_1 \r\rightarrow t_2$, האלגוריתם קורס. המשמעות: יש שגיאת טיפוס בקוד! המפרש פולט Type Error.
פתרון משוואות טיפוסים אינטראקטיבי (Unification Solver) הדמיה אינטראקטיבית
עקבו אחר אלגוריתם ה-Unification הפותר את משוואות הטיפוסים עבור הקוד הבא:
letrec f(x) = -(x, 1) in f(5)
בקרה:
רשימת משוואות (Equations):
טבלת הצבות (Substitutions):
דוגמאות הפעלה צעד-אחר-צעד
נראה כיצד האלגוריתם פועל בצורה שיטתית - החל משלב גזירת המשוואות (מבפנים החוצה) ועד לפתרונן והסקת הטיפוס הסופי.
דוגמה 1: היכרות עם let ומתמטיקה
מעקב אילוצים:
- נסמן את $x$ ב-$t_x$.
- נסמן את הביטוי
5ב-$t_1$. מאחר ו-5 הוא מספר, נוצרת משוואה: $t_1 = int$. - חוק ה-let קובע ש-$t_x = t_1$. לכן מסקנה ראשונה: $t_x = int$.
- הביטוי הפנימי
-(x, 3)מסומן כ-$t_2$. חיסור דורש שמאל=int וימין=int. הערך הימני 3 הוא אכן int. הערך השמאלי הוא $x$, ולכן דרוש $t_x = int$. זה תואם לחלוטין למסקנה שלנו ולכן הכל תקין. - תוצאת החיסור היא int. ולכן $t_2 = int$.
- התוכנית כולה מחזירה את תוצאת גוף ה-let. לכן $t_{prog} = int$.
דוגמה 2: זיהוי טיפוס פרמטר בעזרת תנאי (if)
שלבי הפתרון:
- נסמן את $x$ כ-$t_x$. הפונקציה עצמה מסומנת ב-$t_{proc} = t_x \r\rightarrow t_{body}$.
- נסתכל על התנאי:
zero?(x). הפעולה zero? דורשת שהקלט שלה יהיה מספר. מכאן נוצר האילוץ החשוב: $t_x = int$. (בלי שהצהרנו במפורש, המהדר מסיק ש-x הוא מספר!). - נסתכל על ה-then: הפלט הוא 1, לכן $t_{then} = int$.
- נסתכל על ה-else: הפלט הוא x, לכן $t_{else} = t_x$.
- חוק ה-if דורש ששני הענפים יהיו זהים: $t_{then} = t_{else}$. נציב את מה שגילינו: $int = t_x$. זה תואם בדיוק לסעיף 2.
- גוף הפונקציה ($t_{body}$) שווה לטיפוס ה-if שהוא $int$.
- הטיפוס הסופי של הפונקציה: $t_{proc} = t_x \r\rightarrow t_{body} = int \r\rightarrow int$.
דוגמה 3: פונקציות מסדר גבוה (Higher Order)
בדוגמה זו אין שום רמז "חיצוני" (כמו חיסור או מספר). איך עובדים נטו עם משוואות ההפעלה?
- נסמן את הפרמטרים: $f$ כ-$t_f$, ו-$x$ כ-$t_x$.
- הביטוי המרכזי הפנימי הוא
(f x). נסמן את תוצאת ההפעלה הזו כ-$t_{res}$. - נפעיל את חוק ה-Call-Exp: אנו מפעילים את f על x והתוצאה היא $t_{res}$. לכן $t_f$ חייב להיות פונקציה מ-$t_x$ ל-$t_{res}$. נוצרת המשוואה: $t_f = t_x \r\rightarrow t_{res}$.
- כעת נבנה את התוכנית בחזרה החוצה. הפונקציה הפנימית `proc(x:?)` מחזירה את ההפעלה. לכן הטיפוס שלה: $t_{inner} = t_x \r\rightarrow t_{res}$.
- הפונקציה החיצונית `proc(f:?)` מחזירה את הפונקציה הפנימית. לכן הטיפוס שלה: $t_{outer} = t_f \r\rightarrow t_{inner}$.
- נציב את הכל פנימה:
$t_{outer} = (t_x \r\rightarrow t_{res}) \r\rightarrow (t_x \r\rightarrow t_{res})$ - מכיוון שלא מצאנו שום קשר ל-int או bool, המשתנים $t_x$ ו-$t_{res}$ נשארים נעלמים עד סוף התוכנית. זה מצב חוקי ונקרא פולימורפיזם (Polymorphism) - הפונקציה הזו יכולה לקבל כל פונקציה וכל משתנה שמתאימים לה.
מקרי קצה ושגיאות טיפוס
אלגוריתם ה-Inference נתקל לעיתים בתוכניות מורכבות הכוללות קריאות רקורסיביות, או בתוכניות המכילות שגיאת טיפוס אמיתית שאינה ניתנת לפתרון.
דוגמה 4: רקורסיה עמוקה (letrec)
נשתמש בשיטת חילוץ המשוואות:
- הפרמטר וגוף ה-letrec: נסמן את הטיפוס של פונקציית ה-letrec כ-$t_{res}$ ואת הפרמטר ב-$t_x$. הטיפוס של הפונקציה f הוא במפורש $t_f = t_x \r\rightarrow t_{res}$.
- התנאי:
zero?(x)מסיק ש-$t_x = int$. - בלוק ה-then: מחזיר 0, לכן הטיפוס של then הוא $int$. מכיוון שתוצאת גוף הפונקציה חייבת להתאים, נסיק כי $t_{res} = int$. אז עד כה אנו יודעים ש-$f: int \r\rightarrow int$.
- בלוק ה-else: יש פה חיסור גדול, לכן תוצאתו $int$. (התאמה מושלמת ל-then).
- הקריאה הרקורסיבית: מבצעים
(f -(x,1)). אנו קוראים ל-f עם פרמטר שהוא חיסור (ולכן הוא int). הטיפוס של f מצפה ל-int. התוצאה של f חוזרת כ-$t_{res}$ שהוא int. הערך הזה הולך לפעולת החיסור החיצונית שמצפה ל-int. הכל מסתדר בצורה מושלמת! - התוצאה: התוכנית כולה מחזירה את הפונקציה
f, שטיפוסה הוא $int \r\rightarrow int$.
דוגמה 5: מניעת רקורסיה אינסופית בטיפוסים (Occurs Check)
מתי האלגוריתם נשבר? ננסה להסיק את הטיפוס של הפונקציה המבלבלת הבאה שמפעילה ארגומנט על עצמו (Self-Application):
מעקב אחר אלגוריתם ה-Unification:
- 1. נסמן את $x$ במשתנה טיפוס זמני: $t_x$.
- 2. הביטוי המרכזי הוא הפעלה:
(Rator Rand)=(x x). נסמן את תוצאת ההפעלה (הטיפוס שחוזר ממנה) ב-$t_{res}$. - 3. נפעיל את חוק ההפעלה (Call-Exp Constraint Rule):
ה-Rator הוא $x$ (מסוג $t_x$).
ה-Rand הוא $x$ (מסוג $t_x$).
משוואת הפעלת פונקציה דורשת: הטיפוס של ה-Rator שווה לחץ בין טיפוס ה-Rand לטיפוס התוצאה. נציב ונקבל:$$t_x = t_x \r\rightarrow t_{res}$$ - 4. ה-Unifier מקבל את המשוואה הזו ומנסה לבצע אלימינציה. הוא בודק במילון (Substitutions) ואז מבצע בדיקת שייכות (Occurs Check):
האם משתנה הטיפוס $t_x$ מופיע בתוך הביטוי $t_x \r\rightarrow t_{res}$? - 5. התשובה היא **כן** ($t_x$ מופיע ממש בצד שמאל של החץ).
- 6. התרסקות! ה-Unifier זורק שגיאת Occurs Check Violation. הפונקציה אינה ניתנת לטיפוס (Not Typeable) בשפת INFERRED!
אם האלגוריתם לא היה בודק זאת, היינו נכנסים ללולאה אינסופית בנסיון לפתור את הטיפוס. לא ניתן לכתוב ב-INFERRED פונקציה שמקבלת את עצמה ללא מערכת טיפוסים מורכבת יותר (כמו Recursive Types).
דוגמה מסכמת: הסקה בפונקציות מקוננות
נבצע כעת מעקב מלא אחר ה-Inferrer וה-Unifier עבור תוכנית מורכבת. דוגמה זו מסכמת את כל השלבים - משלב חלוקת המשתנים, דרך בניית 13 המשוואות, ועד לפתרונן בשיטת האלימינציה וההצבות.
in let p = proc(x: ?) if (x 5) then (q 10) else (q 20)
in (p q)
שלב א': איסוף ויצירת משוואות
ה-Inferrer סורק את ה-AST ומעניק משתנה $t$ לכל ביטוי:
| הביטוי (Expression) | משתנה הטיפוס | המשוואות שנוצרות (Constraints) / הסבר |
|---|---|---|
| y | $t_y$ | פרמטר של הפונקציה q |
| -(y, 10) | $t_1$ | 1. $t_y = int$ 2. $t_1 = int$ (חיסור דורש ומחזיר int) |
| zero?(-(y, 10)) | $t_2$ | 3. $t_1 = int$ (קלט חייב להיות int) 4. $t_2 = bool$ (תוצאת zero? היא בוליאנית) |
| proc(y:?)... | $t_q$ | 5. $t_q = t_y \r\rightarrow t_2$ (פונקציה מהפרמטר לגוף) |
| --- עוברים לחלק השני של הקוד --- | ||
| x | $t_x$ | פרמטר של הפונקציה p |
| (x 5) | $t_3$ | 6. $t_x = int \r\rightarrow t_3$ (x מופעל כפונקציה על המספר 5, ומחזיר את t_3) |
| (q 10) | $t_4$ | 7. $t_q = int \r\rightarrow t_4$ (q מופעל כפונקציה על 10, ומחזיר את t_4) |
| (q 20) | $t_5$ | 8. $t_q = int \r\rightarrow t_5$ (q מופעל על 20, ומחזיר את t_5) |
| if (x 5) then... | $t_{if}$ | 9. $t_3 = bool$ (תנאי ה-if חייב להיות בוליאני) 10. $t_4 = t_5$ (שני ענפי ה-if זהים) 11. $t_{if} = t_4$ (תוצאת ה-if) |
| proc(x:?)... | $t_p$ | 12. $t_p = t_x \r\rightarrow t_{if}$ (הפונקציה p) |
| (p q) | $t_{prog}$ | 13. $t_p = t_q \r\rightarrow t_{prog}$ (התוכנית כולה - p מופעלת על q) |
שלב ב': אלגוריתם ההצבות (Unification)
ה-Unifier מקבל את 13 המשוואות שמצאנו, ומפעיל אלימינציה שלב אחר שלב. הערכים מחלחלים (Substitute) במורד המשוואות ומעשירים את טבלת ההצבות.
המשוואות שעוד נותרו:
- 1. $t_y = int$
- 2. $t_1 = int$
- 3. $t_1 = int$
- 4. $t_2 = bool$
- 5. $t_q = t_y \r\rightarrow t_2$
- 6. $t_x = int \r\rightarrow t_3$
- 7. $t_q = int \r\rightarrow t_4$
- 8. $t_q = int \r\rightarrow t_5$
- 9. $t_3 = bool$
- 10. $t_4 = t_5$
- 11. $t_{if} = t_4$
- 12. $t_p = t_x \r\rightarrow t_{if}$
- 13. $t_p = t_q \r\rightarrow t_{prog}$
מילון ההצבות (Substitutions) שמתגבש:
- $\r\rightarrow t_y = int$ (ממשוואה 1)
- $\r\rightarrow t_1 = int$ (משוואות 2,3 - נמחקות)
- $\r\rightarrow t_2 = bool$ (ממשוואה 4)
- נציב את ty ו-t2 בתוך משוואה 5: $\r\rightarrow t_q = int \r\rightarrow bool$
- נציב את tq החדש בתוך 7 ו-8:
$int \r\rightarrow bool = int \r\rightarrow t_4 \implies t_4 = bool$
$int \r\rightarrow bool = int \r\rightarrow t_5 \implies t_5 = bool$
$\r\rightarrow t_4 = bool, \ t_5 = bool$ - ממשוואות 9, 11 נובע:
$\r\rightarrow t_3 = bool$
$\r\rightarrow t_{if} = bool$ (כי t4 הוא bool) - נציב את t3 במשוואה 6: $\r\rightarrow t_x = int \r\rightarrow bool$
- נבנה את משוואה 12 (הפונקציה p) עם tx ו-tif: $\r\rightarrow t_p = (int \r\rightarrow bool) \r\rightarrow bool$
- השלב הסופי! נציב את tp ואת tq במשוואה 13:
$(int \r\rightarrow bool) \r\rightarrow bool = (int \r\rightarrow bool) \r\rightarrow t_{prog}$
$\implies t_{prog} = bool$ 🎯
סיכום האלגוריתם
בסיום המעקב, ה-Inferrer מחזיר שהאלגוריתם סיים בהצלחה ללא סתירות, וטיפוס התוכנית הסופי ($t_{prog}$) הוא bool. אם הוא היה נתקל בסתירה - למשל אם $t_3$ היה אמור להיות גם $int$ וגם $bool$, האלגוריתם היה עוצר וזורק Type Error.
פתרון מטלת סיכום: הסקה עם פונקציות מסדר גבוה
במחלקה זו ננתח ונפתור צעד-אחר-צעד את שאלת ההסקה המרכזית עבור ביטוי המשלב let, פונקציות מסדר גבוה, והעברה של פונקציות כפרמטרים בשפת INFERRED.
in (p proc (b: int) zero? (b))
שלב א': הקצאת משתני טיפוס ויצירת משוואות
כדי להסיק את טיפוס הביטוי, ה-Inferrer סורק את ה-AST ומקצה משתנה טיפוס זמני לכל תת-ביטוי ולכל מזהה (Identifier) ללא טיפוס מוצהר:
| תת-הביטוי / משתנה (Expression) | משתנה הטיפוס | המשוואות שנוצרות (Constraints) / הסבר פדגוגי |
|---|---|---|
| E_0 (התוכנית כולה) | \(t_{prog}\) | הטיפוס הסופי של ביטוי ה-let כולו. לפי חוק ה-let, מתקיים: \(t_{prog} = t_{body}\) (טיפוס הגוף). |
| a | \(t_a\) | פרמטר ללא טיפוס מוצהר של הפונקציה p. מקבל משתנה טיפוס חופשי. |
| 6 | \(t_1\) | 1. \(t_1 = int\) (קבוע מספרי הוא תמיד מספר שלם) |
| (a 6) | \(t_2\) | 2. \(t_a = t_1 \rightarrow t_2\) (הפעלת פונקציה: a מופעלת על 6 ומחזירה את תוצאת הגוף t_2) |
| proc (a: ?) (a 6) | \(t_{rhs}\) | 3. \(t_{rhs} = t_a \rightarrow t_2\) (טיפוס הפונקציה הוא מטיפוס הפרמטר לטיפוס הגוף) |
| p | \(t_p\) | 4. \(t_p = t_{rhs}\) (קשירת המשתנה p לערך הימני ב-let) |
| --- גוף ה-let: (p proc (b: int) zero? (b)) --- | ||
| b | \(t_b\) | 5. \(t_b = int\) (פרמטר בעל הצהרת טיפוס מפורשת b: int) |
| zero? (b) | \(t_3\) | 6. \(t_b = int\) (קלט של zero? חייב להיות מספר) 7. \(t_3 = bool\) (פלט של zero? הוא תמיד בוליאני) |
| proc (b: int) zero? (b) | \(t_{arg}\) | 8. \(t_{arg} = t_b \rightarrow t_3\) (טיפוס פונקציית הארגומנט) |
| (p proc...) (גוף ה-let) | \(t_{body}\) | 9. \(t_p = t_{arg} \rightarrow t_{body}\) (הפעלת הפונקציה p על הארגומנט; התוצאה היא t_body) |
שלב ב': פתרון המשוואות (Unification & Substitution)
כעת, ה-Unifier מתחיל לפתור את מערכת המשוואות שהגדרנו באמצעות מעברים, הפשטות והצבות דו-כיווניות:
המשוואות שנאספו:
- (1) \(t_1 = int\)
- (2) \(t_a = t_1 \rightarrow t_2\)
- (3) \(t_{rhs} = t_a \rightarrow t_2\)
- (4) \(t_p = t_{rhs}\)
- (5) \(t_b = int\)
- (6) \(t_b = int\)
- (7) \(t_3 = bool\)
- (8) \(t_{arg} = t_b \rightarrow t_3\)
- (9) \(t_p = t_{arg} \rightarrow t_{body}\)
- (10) \(t_{prog} = t_{body}\)
שלבי צמצום והצבה:
-
קביעת טיפוסים ישירים:
ממשוואה (1): \(t_1 \mapsto int\)
ממשוואה (5) ו-(6): \(t_b \mapsto int\)
ממשוואה (7): \(t_3 \mapsto bool\) -
הצבה ב-\(t_a\):
נציב את \(t_1 = int\) במשוואה (2):
\(t_a \mapsto int \rightarrow t_2\) -
בניית טיפוס הפונקציה \(t_{rhs}\) וקשירת \(t_p\):
נציב את \(t_a\) במשוואה (3):
\(t_{rhs} = (int \rightarrow t_2) \rightarrow t_2\)
מכיוון ש-\(t_p = t_{rhs}\) (משוואה 4), נקבל:
\(t_p \mapsto (int \rightarrow t_2) \rightarrow t_2\) -
בניית טיפוס הארגומנט \(t_{arg}\):
נציב את \(t_b = int\) ו-\(t_3 = bool\) במשוואה (8):
\(t_{arg} \mapsto int \rightarrow bool\) -
איחוד (Unification) של טיפוסי \(t_p\):
נציב את \(t_p\) ואת \(t_{arg}\) במשוואה (9):
\( (int \rightarrow t_2) \rightarrow t_2 = (int \rightarrow bool) \rightarrow t_{body} \)
נפרק את השוויון בין שתי פונקציות (שמאל לשמאל, ימין לימין):- צד שמאל: \( int \rightarrow t_2 = int \rightarrow bool \)
מפירוק נוסף מקבלים: \(int = int\) (זהות) וכן \(t_2 \mapsto bool\). - צד ימין: \(t_2 = t_{body}\).
- צד שמאל: \( int \rightarrow t_2 = int \rightarrow bool \)
-
מציאת טיפוס הגוף \(t_{body}\):
מכיוון ש-\(t_2 = bool\) וכן \(t_{body} = t_2\), נובע ישירות ש:
\(t_{body} \mapsto bool\) -
הסקה סופית של טיפוס התוכנית:
ממשוואה (10): \(t_{prog} = t_{body}\). לכן:
\(t_{prog} \mapsto bool\) 🎯
💡 תובנה פדגוגית מהפתרון
בתוכנית זו, הפונקציה p היא פונקציה מסדר גבוה. היא מקבלת פונקציה כלשהי a ומפעילה אותה על המספר 6.
מאחר ו-p מפעילה את a על קלט מסוג int, המהדר מסיק באופן אוטומטי ש-a חייב להיות מטיפוס המקבל int (כלומר int -> t_2).
כאשר אנו מפעילים את p בגוף התוכנית על הארגומנט proc (b: int) zero? (b), שטיפוסו הוא int -> bool, מתבצעת התאמה מלאה!
משתנה הטיפוס \(t_2\) מתאחד עם bool, ולכן תוצאת הפונקציה כולה (וגם תוצאת התוכנית כולה) היא bool.