Tip Çıkarımı
Tip çıkarımı, ifadelerin tiplerini otomatik olarak yeniden yapılandırarak, programcıların açık tip belirtimlerini (annotations) atlamasına olanak tanır ve derleyici en genel tiplemeyi hesaplar.
Tanım
Tip çıkarımı (tip yeniden yapılandırması), programcının tüm tip belirtimlerini sağlamasını gerektirmeden, bir ifadenin yapısından ve kullanımından geçerli ve en genel bir tipi türetme sürecidir.
Kapsam
Bu konu, açık tip belirtimleri olmaksızın tipleri çıkarmaya yönelik algoritmaları ve kuramı kapsamakta olup, birleştirme (unification) ve let-polimorfizmi kullanımıyla Hindley-Milner sistemi ve Algoritma W üzerine odaklanmaktadır. Başat tipleri (principal types), karar verilebilirliği ve karmaşıklığı ile alt tipleme (subtyping), yüksek dereceli polimorfizm (higher-rank polymorphism) veya bağımlı tipler (dependent types) gibi daha zengin sistemlere çıkarımı genişletmenin zorluklarını ele almaktadır.
Temel sorular
- Hiçbir tip belirtilmediğinde bir derleyici tipleri nasıl yeniden yapılandırabilir?
- Başat tip nedir ve ne zaman her zaman var olur?
- Birleştirme (unification) Hindley-Milner çıkarımını nasıl yönlendirir?
- Daha zengin tip sistemlerinde çıkarım neden karar verilemez veya eksik hale gelir?
Temel kuramlar
- Hindley-Milner tip çıkarımı
- Milner'ın polimorfik tip disiplini, Algoritma W ile birlikte, birleştirme (unification) kullanarak let-bağlı polimorfizme sahip bir lambda kalkülüsü için tipleri çıkarır ve ML-ailesi dillerinde çıkarımın temelini oluşturur.
- Başat tip şemaları
- Damas ve Milner, her tiplendirilebilir ifadenin, tüm geçerli tiplerinin örnekleri olduğu en genel tip olan bir başat tip şemasına sahip olduğunu ve Algoritma W'nin bunu hesapladığını kanıtlamıştır.
- Kombinatoryal mantıkta başat tipler
- Hindley, tiplendirilebilir terimler için başat tiplerin varlığını ortaya koymuştur; bu, daha sonraki programlama dili tip çıkarımının temelini oluşturan öncül bir sonuçtur.
Klinik önem
Tip çıkarımı, güvenliği korurken açıklama yükünü ortadan kaldırarak statik olarak tiplendirilmiş dilleri çok daha kullanışlı hale getirmektedir ve tip ipuçları (type hints) ile otomatik tamamlama (autocompletion) gibi modern düzenleyici özelliklerini desteklemektedir. İfade gücü yüksek sistemlerdeki sınırları, programcıların hala açıklama sağlaması gereken noktaları şekillendirmektedir.
Tarihçe
Hindley'nin 1969'daki kombinatoryal mantıkta başat tipler üzerine yaptığı çalışma, pratik çıkarımı öngörmüştür. Milner'ın 1978 tarihli makalesi, ML için polimorfik tip sistemini ve Algoritma W'yi tanıtmış, Damas ve Milner'ın 1982 tarihli makalesi ise başatlığı (principality) kanıtlamıştır. Hindley-Milner sistemi, ML, Haskell ve daha sonraki birçok dil için standart haline gelmiş olup, çıkarımı daha zengin ortamlara genişletmeye yönelik araştırmalar devam etmektedir.
Tartışmalar
- Ne kadar çıkarım yapılmalı, ne kadar açıklama eklenmeli
- Tip sistemleri daha ifade gücü yüksek hale geldikçe, tam çıkarım karar verilemez hale gelmekte, bu da çıkarımı yönetilebilir ve öngörülebilir tutmak için otomatik olarak ne kadarının çıkarılması gerektiği ile açık belirtimler olarak ne kadarının gerekli olduğu konusunda bir tartışmayı tetiklemektedir.
Öne çıkan isimler
- Robin Milner
- Luis Damas
- Roger Hindley
- Benjamin Pierce
İlgili konular
Temel eserler
- milner1978
- damas1982
- hindley1969
- pierce2002
Sıkça sorulan sorular
- Başat tip nedir?
- Başat tip, bir ifadenin en genel tipidir; öyle ki o ifade için diğer her geçerli tip, onun bir yerine koyma (substitution) örneğidir. Hindley-Milner çıkarımı, bir başat tip mevcut olduğunda her zaman onu hesaplar.
- Neden tüm tip sistemleri tipleri otomatik olarak çıkaramaz?
- Çıkarım, çözülebilir kısıtlamalara dayanmaktadır; yüksek dereceli veya bağımlı tipler gibi ifade gücü yüksek sistemlerde, tam çıkarım karar verilemez hale gelmekte, bu nedenle bazı açıklamaların programcı tarafından sağlanması gerekmektedir.