מבוא לפרק 7

למה צריך מערכות טיפוסים (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

שפת 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 אנו מוסיפים שלב ביניים קריטי:

Source Code (String)
⬇️ (scan&parse)
AST
⬇️ (type-of-program)
Safe! (returns Type)
Error! (Halt)
⬇️ (value-of-program)
ExpVal
🚀 Zero-Cost Abstraction

בגלל שהוכחנו סטטית שאין שגיאות טיפוס, מפרש הריצה ב-interp.scm רץ מהר יותר ופשוט יותר. אין צורך לבדוק ב-if-exp האם התנאי הוא בוליאני, או ב-diff-exp האם האיברים הם מספרים. הבטיחות מובטחת מראש!

משימה: בנה את הארכיטקטורה (Drag & Drop Architecture Builder) פעילות אינטראקטיבית

שפת CHECKED מפרידה לחלוטין בין שלב בדיקת הטיפוסים הסטטית לבין שלב הריצה. גררו את קטעי הקוד הבאים לקופסה (קובץ) המתאימה להם, או לחצו על קטע קוד ואז על קופסת היעד:

checker.scm (שלב סטטי) 0
interp.scm (שלב הריצה) 0
lang.scm (הגדרת השפה) 0
חלקי קוד לשיוך:

📂 חלוקת הקבצים ותוספת ה-Checker בשפת CHECKED

שם הקובץ מה התווסף / השתנה בשפת CHECKED? תפקיד בשלב הסטטי (Type Check)
checker.scm (קובץ חדש!) מימוש פונקציית type-of הבודקת ומאמתת טיפוסים של ביטויים בצורה רקורסיבית. מנוע אימות הטיפוסים הסטטי (לפני ריצה).
data-structures.scm הוספת הגדרות לטיפוסי שפה (int, bool, proc) והגדרת type-environment (Tenv). ייצוג טיפוסים וסביבת טיפוסים בזיכרון.
lang.scm הוספת הגדרות טיפוסים לתחביר (כמו proc(x : int) ...). הלקסר והפארסר מכריחים הגדרת טיפוסים מפורשת.
שפת CHECKED

שפת 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)

משחק פאזל: הזרקת טיפוסים (Type Annotation Puzzle) פעילות אינטראקטיבית

בשפת PROC הדינמית יכולנו לכתוב פונקציות ללא ציון טיפוסי הפרמטרים. בשפת CHECKED הסטטית, המהדר דורש להכריז על הטיפוסים מראש. השלימו את החורים בקוד הבא כדי להפוך אותו לקוד CHECKED חוקי שיעבור קומפילציה:

let f = proc (x : [ ? ])
if x then 1 else 0
in (f [ ? ])

השוואה לשפות קודמות

בשפת PROC הישנה, פונקציות היו "דינמיות" לחלוטין. ב-CHECKED אנו מעבירים חלק מהאחריות למערכת הטיפוסים הסטטית. נשים לב להבדל התחבירי והסמנטי המרכזי:

נושא שפת PROC (דינמית) שפת CHECKED (סטטית)
הגדרת פונקציה proc (x) ... proc (x : int) ...
שגיאת טיפוסים מתגלה רק בזמן ריצה כשמנסים לחשב את הביטוי. מתגלה בשלב ה-Compilation (בדיקת הטיפוסים הסטטית) ללא הרצת קוד.
הגדרת רקורסיה letrec f(x) = ... letrec bool f(x : int) = ...
שפת CHECKED

מנוע הבדיקה: 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 exp2)
          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))))
    )))

🔍 תפקידו של הפרמטר exp ב-check-equal-type!

הפונקציה check-equal-type! מקבלת את הטיפוס המצופה, הטיפוס בפועל, ואת ה-AST (הביטוי המקורי) שעובר בדיקה. מדוע אנו מעבירים את ה-AST של הביטוי? אם תתרחש שגיאת טיפוס (אי-התאמה), מפרש הבדיקה יוכל להשתמש בביטוי זה כדי להדפיס הודעת שגיאה מדויקת ומפורטת שמצביעה על השורה והביטוי המדויק שכשלו בקוד המקור. זה מסביר כיצד פועלות הודעות שגיאה בקומפיילרים אמיתיים ומקל על המתכנת לאתר את מקור הבעיה.

🧠 סביבת טיפוסים (Tenv) מול סביבת ריצה (Env)

חשוב להבין את ההפרדה המוחלטת בין שני סוגי הסביבות:

  • סביבת ריצה (Environment): מופעלת ב-value-of, שומרת שמות של משתנים ומקשרת אותם לערכי ריצה אמיתיים כמו מספרים או קלוז'רים (למשל: x = num-val(5)).
  • סביבת טיפוסים (Type Environment - Tenv): מופעלת ב-type-of, שומרת שמות של משתנים ומקשרת אותם לטיפוסים הסטטיים שלהם (למשל: x = int-type). סביבה זו קיימת רק בזמן הקומפילציה!

מחולל טיפוסים מסדר גבוה (High-Order Type Builder) הדמיה אינטראקטיבית

בנו טיפוסים של פונקציות מסדר גבוה (פונקציות שמקבלות או מחזירות פונקציות) וראו כיצד מיוצגים הטיפוסים במפרש checker.scm של EOPL ומה משמעותם התחרותית.

התוצאה המיוצרת:
הטיפוס לקריאה ידידותית: int -> int
ייצוג ה-AST במפרש EOPL: (proc-type (int-type) (int-type))
הסבר סמנטי (בעברית):

פונקציה המקבלת מספר שלם ומחזירה מספר שלם.

שפת INFERRED

קבצי המקור של שפת INFERRED

שפת INFERRED מאפשרת להשמיט את הגדרות הטיפוסים באמצעות שימוש בסימן שאלה ?. כדי לבצע את פלא הסקת הטיפוסים, המפרש משתמש במערכת קבצים מתוחכמת יותר.

מבנה הקבצים החדש

  • inferrer.scm (מחליף את checker.scm)

    מבצע את בדיקת הטיפוסים הסטטית. בניגוד ל-type-of הקודם שהחזיר טיפוס, כאן הוא מחזיר an-answer - מבנה הכולל את הטיפוס המוסק ואת טבלת ההצבות (Substitutions) המעודכנת.

    💡 מנגנון "השחלת המצב" (State Threading): סטודנטים רבים מתקשים להבין כיצד פתרון המשוואות נצבר בפועל תוך כדי הסריקה של העץ. המנגנון מתבסס על כך ש-an-answer אורז בתוכו לא רק את הטיפוס המוסק לביטוי הנוכחי, אלא גם את סביבת ההצבות (Substitutions) המעודכנת ביותר. כשבודקים ביטוי מורכב (למשל חיסור -(E1, E2)), המפרש תחילה בודק את E1 ומקבל an-answer עם סביבת הצבות חדשה. לאחר מכן, הוא מעביר את אותה סביבה חדשה ישירות לבדיקה של E2. הידע נצבר ומועבר מביטוי לביטוי בצורה טורית לאורך כל שלבי הסקת הטיפוסים.

  • 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 על משתנה הטיפוס הראשי של התוכנית. פונקציה זו מחליפה את כל משתני הטיפוס הזמניים בטיפוסים האמיתיים שהסקנו בעזרת המילון.

הדמיה: מנגנון השחלת המצב (The State-Threading Visualizer) הדמיה דינמית

בגלל ש-Scheme היא שפה פונקציונלית ללא משתנים גלובליים, הדרך היחידה להעביר את טבלת ההצבות (Substitutions) היא "להשחיל" אותה כקלט וכפלט בין שלבי סריקת העץ. ראו כיצד an-answer משורשר לאורך AST של הביטוי -(E1, E2):

בקרה:
לחצו על "צעד הבא" כדי להתחיל את הדמיית מעבר המצב בעץ.
מעבר ה-Subst בעץ:
diff-exp
E1
E2
an-answer subst: []

📂 חלוקת הקבצים בשפת הסקת טיפוסים INFERRED

שם הקובץ מה השתנה מ-CHECKED? תפקיד בשלב ההסקה (Inference)
checker.scm יצירת משתני טיפוס (Type Variables), ייצור מערכת משוואות וקריאה ל-unify. הסקה ופתרון משוואות הטיפוסים.
data-structures.scm הוספת משתנה טיפוס tvar-type והצבעות אליו (References) במבנה הטיפוסים. ייצוג הטיפוסים הדינמיים ומשוואותיהם בזיכרון.
lang.scm חזרה לתחביר PROC נקי (ללא הצהרות טיפוסים מפורשות מצד המתכנת!). קריאת קוד נקי ללא צורך בהצהרות טיפוס מפורשות.
שפת INFERRED

הסקה אוטומטית: שפת INFERRED

שפת CHECKED היא בטוחה, אבל הופכת את הקוד למסורבל. מתכנתים לא רוצים לכתוב (x : int) בכל מקום. שפות מתקדמות כמו TypeScript או Haskell מאפשרות הסקת טיפוסים (Type Inference). המהדר חכם מספיק להסתכל על הקוד ולנחש לבד מה צריך להיות הטיפוס!

הדקדוק: סימן השאלה (?)

בשפת INFERRED, המתכנת יכול לכתוב סימן שאלה ? במקום לכתוב את הטיפוס. הוא אומר למפרש: "תגלה לבד".

; הטיפוס הוסתר בעזרת ?
let f = proc (x : ?) -(x, 1)
in (f 10)

המטרה של האלגוריתם היא לפענח מה מסתתר מאחורי כל סימן שאלה בתוכנית, על ידי איסוף רמזים ופתרון משוואות.

שלושת השלבים להסקה

איך אלגוריתם כזה עובד? ממש כמו פתרון מערכת משוואות במתמטיקה (נעלמים $x, y$):

  1. מיפוי משתנים זמניים: מעניקים משתנה זמני (Type Variable המסומן באות $t$) לכל סימן שאלה ולכל ביטוי משמעותי בקוד.
  2. איסוף אילוצים (Constraints): עוברים על ה-AST ומייצרים משוואות לפי החוקים (למשל, חיסור דורש $int$).
  3. הצבה (Unification): פותרים את המשוואות בשיטת האלימינציה. ככל שפותרים יותר משוואות, ערך הנעלמים נחשף, עד שכל ה- $t$-ים הופכים לטיפוסים אמיתיים!

סורק ה-X-Ray: מה קורה מאחורי סימני השאלה? (The "Gensym" X-Ray Scanner) פעילות אינטראקטיבית

בשפת INFERRED המתכנת רושם סימני שאלה ? כדי לומר למפרש להסיק את הטיפוסים. בפועל, ה-Parser מתרגם כל ? למשתנה טיפוס ייחודי וטרי (Fresh Type Variable) שמיוצר על ידי מנגנון ה-gensym. העבירו את העכבר (או לחצו) על סימני השאלה וחלקי הקוד כדי לסרוק אותם ב-"X-ray" ולראות את המשתנים והאילוצים הפנימיים:

let f = proc (x : ?)
proc (y : ?)
-(x, y)
in (f 5)
🔍
תוצאת הסריקה:

העבירו את העכבר על אחד הרכיבים המסומנים בקו מקווקו מעל עורך הקוד.

⚖️ השוואת קוד: כתיבה בשפת CHECKED מול שפת INFERRED

תכונה שפת CHECKED (טיפוסים מפורשים) שפת INFERRED (טיפוסים מוסקים)
הצהרה על פרמטר פונקציה proc(x : int) -(x, 1) proc(x) -(x, 1)
הגדרת פונקציית פרינט proc(f : (int -> bool)) ... proc(f) ...
מתי נבדקים הטיפוסים? לפני זמן הריצה (Static type check) לפני זמן הריצה (Static type inference & check)
האם נדרש מאמץ מצד המתכנת? כן, מחייב כתיבת טיפוסים לכל פרמטר לא! המחשב מסיק את הטיפוסים בעצמו.
אלגוריתם הסקת טיפוסים

שלב 1: יצירת משוואות

ננתח צעד-אחר-צעד את יצירת המשוואות (כפי שנדרש בחלק א' של שאלות Q3). נשתמש בחלוקה המלמטה-למעלה (Bottom-Up) תוך החלת החוקים מקרה אחר מקרה (Case-by-Case).

💡 הכנה לבחינה: אלגוריתם המשוואות, ממן 16 ושאלה 3 במבחן

שימו לב: כל נושא אלגוריתם המשוואות (יצירה ופתרון) וממן 16 מקבילים לחלוטין לשאלה 3 במבחן. מומלץ מאוד לנסות לפתור אותם בעצמכם כדי לתרגל. תוכלו להיעזר ולהבין את הנושא טוב יותר על ידי התבוננות בשאלה 3 במבחן, ביחידת ה"הכנה לבחינה".

חוקי הגזירה (The Rules)

בואו נכיר את התבניות המרכזיות בגזירת משוואות. נניח שסימנו ביטוי $E$ במשתנה טיפוס $T_{E}$. אילו רמזים נוכל לדלות ממנו?

-(E1, E2)
פעולת חיסור דורשת מספרים. לכן נוצרות משוואות אילוץ: $T_{E1} = int$, וגם $T_{E2} = int$. בנוסף, התוצאה של הפעולה כולה היא $int$. זה נכון לכל פעולות המתמטיקה (+, *, /).
zero?(E1)
הפעולה zero? בודקת האם מספר הוא 0. לכן: הקלט $T_{E1} = int$. התוצאה של הפעולה כולה היא תמיד $bool$.
if E1 then E2 else E3
התנאי חייב להיות בוליאני: $T_{E1} = bool$. שני הבלוקים חייבים להחזיר אותו דבר בדיוק: $T_{E2} = T_{E3}$. התוצאה של ה-if כולו שווה לאחד מהם: $T_{if} = T_{E2}$.
proc (x) Body
יצירת פונקציה. הפונקציה יוצרת מבנה של חץ. הטיפוס של הפונקציה כולה שווה ל: $T_{proc} = T_x \rightarrow T_{Body}$ (פונקציה שמקבלת את טיפוס x ומחזירה את טיפוס הגוף).
(Rator Rand)
הפעלת פונקציה! זה החוק המרכזי ביותר להבנה. אם מפעילים את הפונקציה Rator על הארגומנט Rand, והפעולה כולה מחזירה תוצאה שנסמן ב-$T_{Res}$, אזי הפונקציה עצמה חייבת להיות מהמבנה: $T_{Rator} = T_{Rand} \rightarrow T_{Res}$.
let x = E1 in E2
חוק ה-let: הטיפוס של המשתנה x נקבע על ידי הביטוי $E_1$, כלומר $T_{x} = T_{E1}$. תוצאת ה-let כולו היא פשוט התוצאה של גוף ה-let: $T_{let} = T_{E2}$.
let x = 5 in -(x, 3)

הדגמת השלבים (Case by Case)

  • ⬇️
    שלב 1 (Top-Down): הקצאת משתנים.

    אנו סורקים את הביטוי מבחוץ פנימה ונותנים לכל תת-ביטוי משתנה ייעודי לפי הסדר: לביטוי כולו ניתן T0, לגוף ה-let ניתן T1, לפרמטרים הפנימיים T2 ו-T3, ולמזהה ניתן Tx.

  • ⬆️
    שלב 2 (Bottom-Up): איסוף משוואות למקרים ספציפיים.
    • מקרה קבוע (Const) - המספר 3: על פי חוק הקבועים הטיפוס שלו הוא int. לכן נרשום: T2 = int.
    • מקרה קבוע (Const) - המספר 5: אותו דבר, טיפוסו int: T3 = int.
    • מקרה חיסור (Diff) - הביטוי -(x,3): חוק החיסור דורש ששני הקלטים וגם הפלט יהיו מספרים. לכן נדרוש: Tx = int, T2 = int, T1 = int.
    • מקרה השמה (Let) - הביטוי השלם: המשתנה שמוגדר שווה לערכו (Tx = T3), והטיפוס השלם שווה לטיפוס הגוף (T0 = T1).

טבלת משוואות מסכמת - חלק א'

Expression Type Variable Equations (AQ)
let x = 5 in -(x, 3) T0 T0 = T1
-(x, 3) T1 Tx = int
T2 = int
T1 = int
x Tx
3 T2 T2 = int
5 T3 Tx = T3
T3 = int
x Tx
אלגוריתם הסקת טיפוסים

שלב 2: פתרון המשוואות (Unification)

כעת נדגים צעד-אחר-צעד את אלגוריתם ה-Unification, כפי שנדרש בחלק ב' של השאלות. תהליך זה מעביר משוואות פשוטות לצד ההצבות, ומפרק משוואות מורכבות בעזרת הפשטות.

הדגמת תהליך ההצבות (Case by Case)

  • 1️⃣
    שלב 1: הצבות בסיסיות (עוגנים ישירים)

    אנו מזהים את כל המשוואות החד-משמעיות ומעבירים אותן ישירות לעמודת ההצבות (Substitutions). למשל: Tx = int, T1 = int, T2 = int. אלה העוגנים שלנו להמשך הפתרון.

  • 2️⃣
    שלב 2: הצבת משתנים וטיפול בקונפליקטים עקיפים

    ניקח את המשוואה שנותרה Tx = T3 (בטבלה 2). נציב בה את הידע שכבר צברנו מטבלה 1: מכיוון ש-Tx = int, אנו "דורסים" את Tx ומקבלים int = T3, או בעצם T3 = int. לאחר שסיימנו את כל ההצבות, נגלה ש-T0 = int גם כן.

פריסת ה-Unification המלאה - חלק ב'

טבלה 1
Equations Substitutions
T0 = T1
Tx = int
T2 = int
T1 = int
Tx = T3
T3 = int
טבלה 2
Equations Substitutions
Tx = T3 T1 = int
T2 = int
Tx = int
T3 = int
T0 = int
טבלה 3 (סופית)
Equations Substitutions
T1 = int
T2 = int
Tx = int
T3 = int
T0 = int
מסקנה : T0 = int
✓
אלגוריתם הסקת טיפוסים

דוגמה מורכבת: If ופונקציות

ננתח ביטוי מסובך יותר הכולל תנאים ופונקציות, במדויק לפי פורמט Q3 המלא. כאן נראה כיצד טיפוסים זורמים מהפונקציה, אל ה-if, ואל התוצאה.

proc(x:?) if zero?(x) then 1 else x

חלק א': טבלת משוואות

Expression Type Variable Equations (AQ)
proc(x:?) if zero?(x) then 1 else x T0 T0 = Tx -> T1
if zero?(x) then 1 else x T1 T2 = bool
T3 = T4
T1 = T3
zero?(x) T2 Tx = int
T2 = bool
x Tx
1 T3 T3 = int
x T4 T4 = Tx

חלק ב': טבלאות ה-Unification

טבלה 1
Equations Substitutions
T0 = Tx -> T1
T2 = bool
T3 = T4
T1 = T3
Tx = int
T3 = int
T4 = Tx
טבלה 2
Equations Substitutions
T0 = Tx -> T1 T2 = bool
T3 = T4 T1 = T3
Tx = int
T3 = int
T4 = int
טבלה 3 (סופית)
Equations Substitutions
T2 = bool
T1 = int
Tx = int
T3 = int
T4 = int
T0 = int -> int
מסקנה : T0 = int -> int
✓
אלגוריתם הסקת טיפוסים

מקרי קצה ושגיאות טיפוס

אלגוריתם ה-Inference נתקל לעיתים בתוכניות מורכבות הכוללות קריאות רקורסיביות, או בתוכניות המכילות שגיאת טיפוס אמיתית שאינה ניתנת לפתרון.

דוגמה 4: רקורסיה עמוקה (letrec)

letrec ? f(x:?) = if zero?(x) then 0 else -((f -(x,1)), -1) in f

חלוקת משתנים (Top-Down):

  1. letrec ? f(x:?) = ... in f ➔ $t_0$
  2. f (גוף ה-letrec) ➔ $t_1$
  3. if zero?(x)... (גוף הפונקציה f) ➔ $t_2$
  4. zero?(x) ➔ $t_3$
  5. 0 ➔ $t_4$
  6. -((f -(x,1)), -1) ➔ $t_5$
  7. הפרמטר המוגדר x ➔ $t_x$
  8. שם הפונקציה המוגדרת f ➔ $t_f$

חילוץ משוואות ופתרון (Bottom-Up):

  1. קבועים: ברור לנו ש-$t_4 = int$ וכך גם שאר המספרים בביטוי.
  2. התנאי ($t_3$): הפעולה zero?(x) דורשת ש-$t_x = int$.
  3. בלוק ה-then: מחזיר 0, לכן ענף זה הוא $int$. מכיוון שתוצאת התנאי ($t_2$) חייבת להתאים לשני הענפים, נקבל כי $t_2 = int$.
  4. טיפוס הפונקציה ($t_f$): פונקציה תמיד ממפה את הפרמטר לגוף שלה, כלומר $t_f = t_x \r\rightarrow t_2$. נציב את הנתונים ונקבל $t_f = int \r\rightarrow int$.
  5. בלוק ה-else ($t_5$): זהו חיסור ולכן תוצאתו היא $int$. זה תואם בדיוק לענף ה-then! בנוסף, הקריאה הרקורסיבית מתבצעת על חיסור (שהוא int), והפונקציה f אכן מצפה ל-int.
  6. התוצאה (letrec): התוכנית כולה ($t_0$) מחזירה את גוף ה-letrec שהוא $t_1$. במקרה זה, $t_1$ הוא הפונקציה f. לכן: $t_0 = t_f = int \r\rightarrow int$.

דוגמה 5: מניעת רקורסיה אינסופית בטיפוסים (Occurs Check)

מתי האלגוריתם נשבר? ננסה להסיק את הטיפוס של הפונקציה המבלבלת הבאה שמפעילה ארגומנט על עצמו (Self-Application):

proc (x:?) (x x)

מעקב באמצעות Top-Down / Bottom-Up:

  • 1. חלוקה למשתנים: הפונקציה היא $t_0$, ההפעלה היא $t_1$. משתני ה-Rator וה-Rand הם שניהם $t_x$.
  • 2. ההפעלה ($t_1$): הפעלת פונקציה מחייבת שטיפוס ה-Rator יהיה חץ בין טיפוס ה-Rand לטיפוס התוצאה. נציב ונקבל:
    $$t_x = t_x \r\rightarrow t_1$$
  • 3. ה-Unifier מקבל את המשוואה הזו ומנסה לבצע אלימינציה. הוא בודק במילון (Substitutions) ואז מבצע בדיקת שייכות (Occurs Check):
    האם משתנה הטיפוס $t_x$ מופיע בתוך הביטוי $t_x \r\rightarrow t_1$?
  • 4. התשובה היא **כן** ($t_x$ מופיע ממש בצד שמאל של החץ).
  • 5. התרסקות! ה-Unifier זורק שגיאת Occurs Check Violation. הפונקציה אינה ניתנת לטיפוס (Not Typeable) בשפת INFERRED!

מה קורה בזיכרון של המפרש ללא Occurs Check?

ללא מנגנון ה-Occurs Check, המפרש ינסה לבצע את ההצבה בלולאה אינסופית. נראה כיצד ההצבה קורית שוב ושוב בזיכרון עבור השוויון $t_x = t_x \rightarrow t_1$:

1. נציב את t_x בתוך t_x → t_1 ונקבל:
(t_x → t_1) → t_1
2. נציב שוב את t_x לתוך התוצאה:
((t_x → t_1) → t_1) → t_1
3. נציב פעם נוספת:
(((t_x → t_1) → t_1) → t_1) → t_1

העץ בזיכרון של המפרש ילך ויגדל לאינסוף, עד שהמפרש יתרסק מ-Stack Overflow. לכן, ה-Occurs Check קריטי כדי לעצור את התהליך ולמנוע את קריסת המפרש.

אם האלגוריתם לא היה בודק זאת, היינו נכנסים ללולאה אינסופית. בשל כך, לא ניתן לכתוב ב-INFERRED פונקציה שמקבלת את עצמה ללא מערכת טיפוסים מורכבת יותר (כמו Recursive Types).

סימולציה: מדמה קריסת זיכרון (The Occurs-Check Memory Exploder) הדמיה אינטראקטיבית

בסעיף זה ראינו כיצד המשוואה t_x = t_x ➔ t_res עלולה להכניס את ה-Unifier ללולאה אינסופית. הדליקו/כבו את ה-Occurs Check ונסו לבצע הצבה חוזרת של t_x כדי להבין את חשיבות מנגנון ההגנה:

הגדרות סריקה:
הפעל Occurs Check:

מוכן להרצה. המשוואה: t_x = t_x ➔ t_res

מצב הזיכרון (Memory Layout):
t_x

⚠️ טבלת סיווג שגיאות טיפוס: זיהוי ואבחון

סוג שגיאה דוגמה משוואה סותרת הסבר
No Occurrence proc(x) (x x) t = t → t₂ משתנה מופיע בצד ימין של ההחלפה שלו עצמו — טיפוס אינסופי
Unification Failure zero?(proc(x) x) int = t₁→t₂ סתירה: ביטוי צריך להיות int אבל הוא פונקציה
Circular Type letrec f(x) = (f f) t = t → ... הטיפוס מפנה לעצמו באופן מעגלי
אלגוריתם הסקת טיפוסים

הרצה מלאה: Letrec מורכב

נבצע מעקב מלא ומושלם (Trace) עבור ביטוי Letrec מורכב בפורמט השלם, משלב הטבלה עד מסקנות היוניפיקציה בעזרת הפשטה ופירוק משוואות הפונקציה.

letrec f(x:?) = -(x,1) in f(5)

חלק א': טבלת בניית המשוואות ל-Letrec

Expression Type Variable Equations (AQ)
letrec f(x:?) = -(x,1) in f(5) T0 T0 = T4
f(x:?) = -(x,1) T1 Tf = Tx -> T2
-(x,1) T2 Tx = int
T3 = int
T2 = int
x Tx
1 T3 T3 = int
f(5) T4 Tf = T5 -> T4
f Tf
5 T5 T5 = int

חלק ב': תהליך ה-Unification

טבלה 1
Equations Substitutions
T0 = T4
Tf = Tx -> T2
Tx = int
T3 = int
T2 = int
Tf = T5 -> T4
T5 = int
טבלה 2
Equations Substitutions
Tf = Tx -> T2 T0 = T4
Tf = T5 -> T4 Tx = int
T3 = int
T2 = int
T5 = int
טבלה 3
Equations Substitutions
int -> int = int -> T4 T0 = T4
Tx = int
T3 = int
T2 = int
T5 = int
Tf = int -> int
טבלה 4 (סופית)
Equations Substitutions
Tx = int
T3 = int
T2 = int
T5 = int
Tf = int -> int
T4 = int
T0 = int
מסקנה : T0 = int
✓
אלגוריתם הסקת טיפוסים - ממ"ן

פתרון ממ"ן 16: פונקציות מסדר גבוה

זהו פתרון מלא, מדויק וזהה לזה שמוצג בסימולטור השאלות. הוא מדגים את העבודה השלמה על פתרון הפונקציות המסובכות.

let p = proc(a:?) (a 6) in (p proc(b:int) zero?(b))

חלק א': פירוק תת-הביטויים למשוואות

Expression Type Variable Equations (AQ)
let p = proc(a:?) (a 6) in (p proc(b:int) zero?(b)) T0 Tp = T2
T0 = T1
(p proc(b:int) zero?(b)) T1 Tp = T4 -> T1
proc(a:?) (a 6) T2 T2 = Ta -> T3
(a 6) T3 Ta = int -> T3
proc(b:int) zero?(b) T4 Tb = int
T4 = Tb -> T5
zero?(b) T5 Tb = int
T5 = bool
a Ta
b Tb
p Tp

חלק ב': הצבות אלגוריתם ה-Unification

טבלה 1
Equations Substitutions
Tp = T2
T0 = T1
T2 = Ta -> T3
Ta = int -> T3
Tp = T4 -> T1
Tb = int
T4 = Tb -> T5
T5 = bool
טבלה 2
Equations Substitutions
T2 = Ta -> T3 Tb = int
Ta = int -> T3 T5 = bool
Tp = T4 -> T1 Tp = T2
T4 = Tb -> T5 T0 = T1
טבלה 3
Equations Substitutions
T2 = Ta -> T3 Tb = int
T2 = T4 -> T1 T5 = bool
T0 = T1
Tp = T2
T4 = int -> bool
Ta = int -> T3
טבלה 4 (סופית)
Equations Substitutions
Tb = int
T5 = bool
T4 = int -> bool
Ta = int -> bool
T3 = bool
T1 = bool
Tp = (int -> bool) -> bool
T2 = (int -> bool) -> bool
T0 = bool
מסקנה : T0 = bool
✓