ברוכים הבאים לשיעור בנושא אלגוריתם האיחוד (Unification), כלי יסודי ומרכזי בהיסק טיפוסים (Type Inference) בשפות תכנות. יחידה זו תעמיק בהבנה תיאורטית ויישומית של האלגוריתם, חשיבותו למערכות טיפוסים גמישות, והמושגים המרכזיים המרכיבים אותו.
אלגוריתם האיחוד: הליבה של היסק טיפוסים
אלגוריתם האיחוד הוא מנגנון חישובי המאפשר למצוא את ההצבה הכללית ביותר (Most General Unifier - MGU) שהופכת שני ביטויים לזהים. בהקשר של שפות תכנות, ביטויים אלו הם לרוב ביטויי טיפוסים, והמטרה היא לפתור סדרת משוואות טיפוסים הנוצרות מקוד המקור. יכולת זו קריטית לשפות עם היסק טיפוסים חזק, כמו ML, Haskell, וגם בשפות מודרניות רבות. האיחוד מאפשר למערכת הטיפוסים "ללמוד" על הקשרים בין טיפוסים שונים בתוכנית, על ידי פתרון אילוצי טיפוסים הנוצרים מקוד המקור.
מושגי יסוד באיחוד
כדי להבין את אלגוריתם האיחוד, עלינו להכיר מספר מושגי מפתח:
משתנה טיפוס (Type Variable):
מציין טיפוס לא ידוע או גנרי שיש לקבוע את ערכו. מסומן לרוב באותיות קטנות כמו
a, b, 'a, 'b. משתני טיפוס מאפשרים פולימורפיזם (Polymorphism) - היכולת של פונקציה או מבנה נתונים לפעול על טיפוסים שונים.משוואת טיפוס (Type Equation):
ביטוי מהצורה
T1 = T2, המייצג אילוץ ששני הטיפוסים T1 ו-T2 חייבים להיות זהים. מערכת האיחוד מקבלת קבוצה של משוואות טיפוסים ומנסה לפתור אותן.הצבה (Substitution):
פונקציה (או מיפוי) ממשתני טיפוס לטיפוסים. הצבה מייצגת פתרון חלקי או מלא למערכת משוואות טיפוסים. לדוגמה, הצבה
{a -> int, b -> list} מחליפה את משתנה הטיפוס a ב-int ואת b ב-list.מופעים (Substitutions):
בהקשר של אלגוריתם האיחוד, "מופעים" מתייחסים לרוב להצבות – מיפויים ממשתני טיפוס לטיפוסים. הצבות אלו הן הפתרונות שאנו מחפשים למשוואות הטיפוסים, וכאשר אנו מיישמים הצבה על ביטוי טיפוס, אנו מקבלים "מופע" ספציפי יותר של אותו טיפוס.
מאחד כללי ביותר (MGU - Most General Unifier):
הצבה שהיא פתרון למערכת משו
מצאתם טעות או שחסר משהו?