Type inference

בOCaml אחד הפיצרים שהקומפיילר נותן הוא type inference. הפיצ׳ר הזה מאפשר למתכנת לא להצהיר על המשתנה ישירות אלא לתת לקומפיילר באמצעות כללי היסק לפרש את הטיפוס בעצמו. Type inference נותן לנו את היכולת להמיר תחשיב למדא ללא טיפוסים לתחשיב למדא עם טיפוסים וככה לקבל את הפיצ׳ר של type safety.

נבין את כיצד עובד המנגנון של הסקת טיפוסים על מקרה מצומצם של השפה. נגדיר אותו כ $\lambda \text{OCaml}$, שילוב של תחשיב למדא ואוקמל .בשפה זאת הביטויים מוגדרים כך

1. כל משתנה הוא ביטוי.
2. אם x משתנה ו t ביטוי אז $\text{fun x}\to \text{t}$ ביטוי.
3. אם $t_1,t_2$ ביטויים אז $t_1{t}_2$ ביטויים.

הגדרה:
נניח קבוצה אינסופית של משתני טיפוס.
- אם $\alpha$ משתנה טיפוס אז הוא טיפוס.
- אם T,S טיפוסים אז כך גם $T\to S$ .

הגדרה:
יחס ההטפסה של $\lambda OCaml$ $\mathrm{\Gamma }⊢t:T$ מוגדר כך -

בעיית הסקת הטיפוסים

נגדיר את בעיה זו כך:
קלט- ביטוי t
פלט- הקשר הטפסה $\mathrm{\Gamma }$ ומיפוי m מביטויים שמופיעים ב t לטיפוסים כך שלכל תת-ביטוי $t^{\prime }$ של t מתקיים $\mathrm{\Gamma }⊢t^{\prime }:m(t^{\prime })$ (כולל t עצמו).

פתרון:

1. יצירת מערכת משוואות בין ביטוי לטיפוס
2. פתרון המערכת
3. תרגום הפתרון ל $\mathrm{\Gamma }$ ו m המתאימים.

יצירת מערכת משוואות

נגדיר t ביטוי נורמלי אם לכל 2 ביטויים $t_1=\text{ fun x...}$ ו $t_2=\text{ fun y...}$ שמופיעים ב t , המשתנים x ו y שונים זה מזה.

נשים לב: לכל ביטוי יש ביטוי נורמלי השקול לו על ידי שימוש בכלל אלפה .

הגדרה עבור t ביטוי נגדיר $A_t$ קבוצת המשוואות. לכל מופע של כל ביטוי שמופיע ב t ניצור משתנה טיפוס משלו ואז

1. אם $\alpha ,\beta$ מתאימים למופעים שונים של אותו הטיפוס אז נוסיף את $\alpha =\beta$ ל $A_t$ .למשל עבור הפונקציה $funx\to x$ נסמן עבור ה x הראשון שהוא מטיפוס ${\alpha }_x^1$ והשני הוא מטיפוס ${\alpha }_x^2$ ונוסיף את ${\alpha }_x^1={\alpha }_x^2$ ל $A_t$ .
2. אם משתני הטיפוס $\alpha ,\beta ,\gamma$ מתאימים ל $t_1,t_2,t_1{t}_2$ בהתאמה אז נוסיף את $\alpha =\beta \to \gamma$ ל $A_t$.
3. לכל מופע $funx\to t^{\prime }$ אם $\alpha ,\beta ,\gamma$ מתאימים ל $x,t^{\prime },funx\to t^{\prime }$ בהתאמה אז נוסיף את $\gamma =\alpha \to \beta$ ל $A_t$.

דוגמה: עבור הביטוי $t=(\text{ fun x}\to x)y$

כעת נגדיר את $A_t$:

תרגום הפתרון

כיצד מתרגמים את הפתרון לכללי הטפסה ומיפוי?
באמצעות כללי substitution. החלפה היא פונקציה שמתאימה טיפוס לכל משתנה טיפוס.
החלפה $\sigma$ מורחבת לטיפוסים באופן הבא

הגדרה: החלפה $\sigma$ מאחדת שיוויון $T_1=T_2$ אם $\sigma (T_1)=\sigma (T_2)$ .
$\sigma$ מאחדת קבוצת שוויונות אם היא מאחדת את כל השיוויונות בקבוצה.

נסתכל על הדוגמה ממקודם-

וגם

הגדרה: יהי t ביטוי ו $\beta$ פונקציה שמתאימה לכל תת ביטוי $t^{\prime }$ של t את משתנה הטיפוס המתאים לאחד המופעים של $t^{\prime }$ ותהי $\alpha$ החלפה שמאחדת את $A_t$ אז

משפט: ${\mathrm{\Gamma }}_{\sigma }^{\beta }$ ו $\sigma \circ \beta$ הם הפתרון לבעיית ההטפסה של t. בצורה פורמלית: יהי $t$ ביטוי ו $\beta ,\sigma$ כמו לעיל אז ${\mathrm{\Gamma }}_{\sigma }^{\beta }⊢t^{\prime }:\sigma (\beta (t^{\prime }))$

אם אין $\sigma$ כנ״ל אז t לא מטופס היטב.

פתרון מערכת משוואות

הגדרה:
בעיית היוניפיקציה-
קלט- קבוצה של שוויונות בין ביטויים
פלט- החלפה $\sigma$ שמאחדת אותם

למשל אם x=y נרצה לבנות $\sigma$ כך ש $\sigma (x)=\sigma (y)$ נוכל להגדיר ש $\sigma (x)=\sigma (y)=x$ .

ומה אם המשוואה אומרת ש $x+y=x\cdot y$ ? כיוון שלא משנה מה יהיו כללי ההחלפה של המשתנים יתקיים $\sigma (x+y)=\sigma (x)+\sigma (y)$ וכנ״ל עבור $\cdot$ אז אין פתרון.

מקרה נוסף שיכול לעניין אותנו בניתוח האלגוריתם שנראה בהמשך הוא מהצורה

נוכל למצוא $\sigma$ שתאחד כל $t_i,s_i$ בנפרד כלומר סיגמה שתקיים $\sigma (t_i)=\sigma (s_i)$.

והמקרה האחרון שיכול לעניין הוא $x=f(y)$ נוכל להגדיר ש $\sigma (x)=f(y)$ ו $\sigma (y)=y$ .

כעת נסתכל על האלגוריתם בOCaml:

type id = string;;
type term = | Var of id | Term of id * term list
(*invariant for substitution*)
(*no id on a lhs occurs in any term earlier in the list*)

type substitution = (id * term) list

(*check if a variable occurs in a term*)
let rec occurs (x : id)(t : term) = match t with 
	| Var y -> x = y
	| Term (_ , s)-> List.exists ( occurs x )s

(*substitute term s for all accurrences of variable x in term t*)
let rec subst (s : term)(x : id)(t : term) = match t with
	| Var y -> if x = y then s else t
	| Term (f,u) -> Term ( f, List.map (subst s x) u)


(*apply a substitution right to left *)
let apply (s: substitution)(t:term) = 
	List.fold_right (fun (x,u)->subst u x)s t

(*unidy one pair*)
let rec unify_one (s:term)(t:term) = match (s,t) with
	| (Var x, Var y) -> if x = y then [] else [(x,t)]
	| (Term(f,sc), Term(g,tc))-> if 
		f = g && List.length sc = List.length tc
			then unify(List.combine sc tc)
			else failwith "not unifiable: head symbol conflict"

	| ((Var x, Term(_,_ as t)))
	| (( Term(_,_ as t), Var x))->
		if occurs x t 
			then failwith "not unifiable: circularity"
			else [(x,t)]

(*unify a list of pairs*)
and unify (s: (term * term)list) = match s with
	| []->[]
	| (x,y) :: t ->
		let t2 = unify t in 
			let t1 = unify_one (apply t2 x)(apply t2 y) in t1@t2;;

ובפסודו קוד זה האלגוריתם לקביעת הטיפוסים

נסתכל על דוגמה של ה ביטוי $\alpha \to \alpha$. לפי הקוד זה יהיה מהצורה Term("->", [Var ('a'), Var('a')].

• substitution הוא פונקצית ההחלפה $\sigma$ .
• occurs היא פונקציה שבודקת אם id כלשהו מופיע בביטוי t מסויים.
• subst - מחליפים את המופיעים החופשיים של x ב s בביטוי t
• apply - מפעילה את subst על כל איבר ב s מהסוף.
• unify_one and unify - נזכיר ש and זה keyword שמאפשר mutual recursion ב OCaml. זה נועד לפתור את המקרה של $f(t_1,t_2)=f(s_1,s_2)$ .
  • unify- מקבל רשימה של זוגות של term כאשר היחס בינהם הוא שיוויון. אם הרשימה ריקה אז המקרה ברור, אם יש איבר מהצורה (x,y) אז פותרים את יתר הרשימה t ואז מבצעים unify_one על התוצאה עם x ועל התוצאה עם y ומחזירים את שרשור התוצאה.
  • unify_one- מבצע unify על זוג של term יחיד שהיחס בינהם הוא שיוויון.
    • אם שניהם משתנים שונים אז מבצעים substitution לביטוי t.
    • אם המקרה יותר מורכב של פונקציות אז בודקים האם הם מכילים את אותו מספר ארגומנטים וגם שהם שווים ואז מבצעים unify לכל זוג בנפרד בצורה רקורסיבית
    • המקרה השלישי והאחרון בודק מצב שיש בצד אחד משתנה ובצד השני ביטוי ופשוט בודקים האם יש מצב שהמשתנה מופיע בביטוי ואם כן מחזירים שגיאה כי אחרת נקבל רקורסיה אין סופית של החלפות.

דוגמה
let f x = 2+x .

1. נשים טיפוסים גנריים לכל משתנה

• משתנה שמופיע מספר פעמים בעל אותו טיפוס
• יש להוסיף טיפוס עבור הפלט של התוכנית
• פונקציה תמיד תהיה מטיפוס $domain\to range$
• מבחינה פורמלית כדי למצוא את כל המשתנים והפונקציות משתמשים בעץ הגזירה של הביטוי (ניתן להחשיב את יצירת עץ הגזירה כשלב נוסף באלגוריתם)

2. קובעים את האילוצים

3. נפתור את האילוצים, מהמערכת הנ״ל אפשר לקבוע ש $t_4=int\to t_2\to t_5$ . אבל גם מאיך ש $t_4$ מוגדר אפשר להסיק כי $t_2=int$ וגם $t_5=int$ . סך הכל נקבל $f:int\to int$ .

4. קביעת הטיפוס של הפונקציה לפי מה שאמרנו למעלה $f:int\to int$ .

נחזור לפסודו קוד של של Hindley-milner type inference ממקודם

ננסה להבין איך האלגוריתם עובד על הדוגמה ממקודם בתצורת למדה כלומר $f=\lambda x.x+2$ :

ניתן לראות שמה AST חילצו את כל האילוצים. כעת עם האלגוריתם unify ניתן לפתור את האילוצים באופן הבא-

1. כל על טיפוס ועל המשוואה שלו
   1. חפש משוואה אחרת המכילה את הטיפוס
   2. אם מצאת החלף את הטיפוס במשוואה שהתקבלה.
      
      
      
      
      

ניתן לראות בסדרת הפעולות הנ״ל שכל ריצה חיפשנו את המקומות שבהם נמצא הטיפוס הזה וממש החלפנו אותו בהשמה. למשל עבור $T_3=T_4\to T_2$ מצאנו את $T_3$ ב $T_5$ וביצענו הצבה וכעת $T_5=T_1\to T_3=T_1\to T_4\to T_2$ . ככה המשכנו להציב שוב ושוב עד שהגענו לביטוי האחרון שבו כבר היה כלל החלפה. כיוון ש $T_1\to nat\to T_2=nat\to nat\to nat$ אז יכלנו להחליף את $T_1,T_2$ ב nat בהתאמה.

בצורה פורמלית:

נסתכל על דוגמה נוספת $\text{let f x = 5.+x}$ .
נבצע השמה של טיפוסים גנריים לכל התוכנית

נסתכל על האילוצים

כעת אם ננסה לפתור אותם נקבל ש $t_4=float\to t_2\to t_5$ וגם $t_4=\text{int}\to \text{int}\to \text{int}$ שזה conflict בין הטיפוסים ולכן type error.

דוגמה
$\text{let f x y = x y}$ .

1. השמת טיפוסים
   
2. אילוצים : $t_1=t_2\to t_3\to t_4$ וגם $t_2=t_3\to t_4$
3. פתרון לאילוצים: $t_1=(t_3\to t_4)\to t_3\to t_4$
4. סה״כ $f:(a\to b)\to a\to b$ , מצב כזה נקרא type variable כלומר פונקציה גנרית.

רקורסיה
נסתכל על הקוד הבא:

let rec length xs = 
	match xs with 
		| [] -> 0
		| (h:t) -> 1 + length t

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

1. הטיפוס של כל אחד מהקלטים (צד שמאל של החץ) צריכים להיות שווים
2. הטיפוס של כל אחד מהפלטים (צד ימין של החץ צריך להיות שווה)

נשים טיפוסים לקטע הקוד הנ״ל

נשים לב שאת הרשימה שמנו מראש בטיפוס עטוף ב $[]$ כי אנחנו יודעים שהטיפוס הוא רשימה מסוג של משהו.

נבנה את האילוצים

1. קל להבין למה $t_1$ הוא פונקציה שהקלט שלה $t_2$ והפלט הוא $t_3$
2. $t_2$ הוא טיפוס של רשימה מסוג $t_4$ בגלל ה case הראשון וגם מטיפוס $t_7$ בגלל ה case השני.
3. בגלל ערך החזרה של המקרה הראשון - 0 , ניתן להגיד ש $t_3$ הוא שקול ל int.
4. בנוסף $t_3=t_8$ בגלל אותו הסבר
5. בגלל פעולת ה apply אנחנו יודעים שמצד ימין יש רשימה ומצד שמאל יש אלמנט שהוא מהטיפוס של איבר ברשימה.
6. length היא פונקציה בגלל המקרה השני שהפלט שלה הוא int.

כך ניתן לפתור את האילוצים ולגלות ש $length:[a]\to int$ .