Bağımlı ve Alt Yapısal Tipler
Bağımlı tipler, türlerin değerlere bağlı olmasını sağlayarak hassas spesifikasyonlara olanak tanırken, doğrusal (linear) ve afin (affine) tipler gibi alt yapısal tipler kaynakların nasıl kullanıldığını kontrol etmektedir.
Tanım
Bağımlı tipler, değerlere bağlı olan türlerdir ve tip seviyesinde hassas özelliklerin belirtilmesine ve kontrol edilmesine izin vermektedir; alt yapısal tip sistemleri, değişkenlerin (kaynakların) nasıl çoğaltılabileceğini veya atılabileceğini kısıtlamakta olup, doğrusal tipler her birinin tam olarak bir kez kullanılmasını gerektirmektedir.
Kapsam
Bu konu, geleneksel sistemlerin ötesine geçen ileri düzey tip disiplinlerini kapsamaktadır: türlerin program değerlerini belirtebildiği, tam spesifikasyonları ifade etmelerine ve kanıt olarak hizmet etmelerine olanak tanıyan bağımlı tipler; ve kaynak kullanımını, takma adlandırmayı (aliasing) ve yaşam sürelerini izlemek için daralma (contraction) ve zayıflatma (weakening) yapısal kurallarını kısıtlayan alt yapısal tipler (doğrusal, afin, sahiplik). Curry-Howard yazışması ve kanıt asistanları ile bağlantılıdır.
Temel sorular
- Tipler, tam program spesifikasyonlarını ifade etmek için değerlere nasıl bağımlı olabilir?
- Bağımlı tipler ile yapıcı kanıtlar (constructive proofs) arasındaki yazışma nedir?
- Doğrusal ve afin tipler kaynakları, sahipliği ve bellek güvenliğini nasıl modellemektedir?
- Bu zengin sistemlerin karar verilebilirlik (decidability) ve kullanılabilirlik açısından ne gibi ödünleşimleri (trade-off) bulunmaktadır?
Temel kuramlar
- Sezgisel (bağımlı) tip teorisi
- Martin-Löf'un tip teorisi, programlamayı ve yapıcı mantığı (constructive logic) birleştirerek tiplerin önermeler, programların ise kanıtlar olmasını sağlamakta ve bağımlı tipli diller ile kanıt asistanları için temel oluşturmaktadır.
- Doğrusal mantık (linear logic) ve doğrusal tipler
- Girard'ın doğrusal mantığı (linear logic), yapısal kuralları kontrol ederek klasik ve sezgisel mantığı iyileştirmekte olup, Wadler bunun üzerine inşa edilen doğrusal tiplerin yerinde güncellemeyi (in-place update) ve kaynak kullanımını güvenli bir şekilde nasıl yönetebileceğini göstermiştir.
- Alt yapısal sistemler için statikler
- Harper, alt yapısal ve diğer ileri tip sistemlerin metateorisini tek tip bir statik-ve-dinamik çerçeve içinde geliştirmekte, bunların sağlamlığını (soundness) ve kaynak yorumunu açıklığa kavuşturmaktadır.
Klinik önem
Bağımlı tipler, programların makine tarafından kontrol edilmiş doğruluk garantileriyle birlikte geldiği kanıt asistanlarını ve doğrulanmış yazılımları güçlendirmektedir. Alt yapısal ve sahiplik tipleri, bellek ve eşzamanlılık açısından güvenli sistem dillerinin temelini oluşturarak, çöp toplayıcı (garbage collector) olmadan güvenli manuel kaynak yönetimine olanak tanımaktadır.
Tarihçe
Martin-Löf'un sezgisel tip teorisi (1970'ler-1980'ler), bağımlı tipleri ve önermeler-olarak-tipler (propositions-as-types) görüşünü ortaya koyarak Coq, Agda ve Lean gibi kanıt asistanlarına yol açmıştır. Girard'ın 1987 tarihli doğrusal mantığı (linear logic), kaynağa duyarlı akıl yürütmeyi tanıtmıştır; Wadler'ın doğrusal tipleri bunu dil tasarımına taşımış, sahiplik ve ödünç alma kontrolü (borrow-checking) disiplinleri ise daha sonra alt yapısal fikirleri sistem programlamasında ana akım haline getirmiştir.
Tartışmalar
- İfade gücü (expressiveness) ile kullanılabilirlik ve karar verilebilirlik (decidability) arasındaki denge
- Bağımlı tipli ve alt yapısal sistemler çok güçlü garantiler ifade edebilmekle birlikte, programcılar üzerindeki yükü artırmakta ve tip kontrolünü karar verilemez (undecidable) veya zahmetli hale getirebilmektedir; bu durum, ne kadar gücün maliyete değeceği konusunda tartışmaları tetiklemektedir.
Öne çıkan isimler
- Per Martin-Löf
- Jean-Yves Girard
- Philip Wadler
- Robert Harper
İlgili konular
Temel eserler
- martinlof1984
- girard1987
- wadler1990
- harper2016
Sıkça sorulan sorular
- Bağımlı tip nedir?
- Bağımlı tip, tanımı bir değere bağlı olan bir türdür; örneğin belirli bir uzunluktaki vektörlerin tipi gibi, bu da tip sisteminin sıradan tiplerin ifade edemeyeceği zengin değişmezleri (invariants) uygulamasını sağlamaktadır.
- Doğrusal tipler neyi garanti etmektedir?
- Doğrusal tipler, her bir değerin tam olarak bir kez kullanılmasını gerektirmektedir; bu da bir derleyicinin çalışma zamanı çöp toplama (runtime garbage collection) olmadan yerinde güncellemeyi (in-place update) güvenli bir şekilde yapmasına, kaynakları yönetmesine ve takma adlandırma (aliasing) ile ilgili hataları önlemesine olanak tanımaktadır.