Type Unification — ikki yoki undan ortiq tur ifodasini teng qiladigan eng umumiy substitutionni topish jarayoni. U type inference, generic dasturlash va mantiqiy dasturlashda noma’lum type variable’larni konkret yoki boshqa o‘zgaruvchi turlar bilan bog‘laydi.
Constraintlarni yechish
Algoritm tenglamalar to‘plamini bosqichma-bosqich soddalashtiradi. List α = List Int tenglamasi α = Int ga ajraladi; α = β substitution yaratadi va qolgan tenglamalarga tatbiq etiladi. Constructor nomi yoki argument soni farq qilsa, masalan List α = Pair Int Bool, unification muvaffaqiyatsiz tugaydi.
Occurs check
Occurs check α = List α kabi cheksiz recursive turni rad etadi, chunki finite type tree ichida α o‘z tarkibida bo‘la olmaydi. Ayrim Prolog implementatsiyalari tezlik uchun occurs checkni cheklaydi va rational tree semantikasiga o‘tadi. Type systemda bu qadamni tashlash soundnessga ta’sir qilishi mumkin.
Umumiylik xossasi
Most general unifier ortiqcha aniqlik kiritmaydi. α → β va Int → γ uchun natija {α ↦ Int, β ↦ γ} bo‘ladi; β yoki γ ni asossiz String qilish kamroq umumiy yechimdir. Hindley–Milner inference constraint generationdan keyin shu unification mexanizmidan foydalanadi.
Implementatsiya
Effektiv implementatsiya substitution zanjirini doim nusxalash o‘rniga union–find, mutable type variable yoki path compression ishlatishi mumkin. Shunga qaramay, error diagnostics uchun qaysi source expression qaysi constraintni yaratgani saqlanadi. Aks holda type mismatch faqat ichki tur raqamlarini ko‘rsatib qoladi.
Verifikatsiya
Sinovlar constructor clash, occurs check, nested generic, polymorphic instantiation va bir nechta yechimga o‘xshash holatlarni qamraydi. Natijadagi substitution barcha boshlang‘ich tenglamalarni haqiqatan teng qilishi tekshiriladi. Keyin undan umumiyroq substitution mavjud emasligi nazariy invariantlar orqali nazorat qilinadi.
Type Unification bo‘yicha tahlil natijasi faqat yakuniy xulosa bilan emas, uni hosil qilgan IR versiyasi, target xususiyatlari va qo‘llangan taxminlar bilan birga saqlanadi. Compiler passlari ketma-ket o‘zgarganda oldingi natija avtomatik ravishda haqiqiy deb olinmaydi: tegishli dependencylar invalidatsiya qilinib, zarur qism qayta hisoblanadi. Debug rejimida asosiy invariant buzilgan nuqta va undan oldingi transformatsiya qayd etiladi; release rejimida esa tekshiruvlarning arzon qismi qoldiriladi. Shu yondashuv nazariy jihatdan qonuniy qoida implementatsiya xatosi yoki noto‘g‘ri cost model sabab zararli qarorga aylangan holatni ajratishga yordam beradi.
Kengaytirilgan jihatlar
Unificationni subtyping constraint solving bilan tenglashtirish noto‘g‘ri: klassik unification tenglik qidiradi, Int <: Number kabi yo‘nalishli munosabat esa boshqa solver talab qiladi. Higher-kinded type, row polymorphism yoki type class constraintlar oddiy first-order Robinson algoritmidan tashqariga chiqadi. Error reportingda solver muvaffaqiyatsiz bo‘lgan oxirgi tenglamani emas, minimal ziddiyatli constraintlar zanjirini ko‘rsatishi muhim. Persistent substitution yoki rollback mexanizmi overload candidate sinab ko‘rilganda foydali. Performance uchun type variable rank va level qiymatlari generalization chegarasini nazorat qiladi, aks holda local type tashqi polymorphic schemaga noto‘g‘ri chiqib ketishi mumkin.
Unifier substitutionni qo‘llaganda type variable nomlarini capture qilmasligi va scheme ichidagi quantified variable’larni ajratishi kerak. Fresh variable generator parallel compilationda takroriy identity bermaydi. Solver statistikasi constraint soni, union/find amallari, occurs-check tashriflari va maksimal type chuqurligini o‘lchaydi; noodatiy o‘sish pathological generic expressionni yoki regressiyani ko‘rsatadi.
Bog‘liq tushunchalar
type inference, substitution, most general unifier, occurs check, Hindley–Milner, constraint solving