Tip Sistemleri
Tip sistemleri, program ifadelerini hesapladıkları değer türlerine göre sınıflandırarak, bir programın çalışmasından önce geniş hata sınıflarını önleyen resmi disiplinlerdir.
Tanım
Bir tip sistemi, ifadeleri hesapladıkları değer türlerine göre sınıflandırarak belirli program davranışlarının yokluğunu kanıtlamak için kullanılan, uygulanabilir bir sentaktik yöntem olarak tanımlanmaktadır.
Kapsam
Bu kapsam, tip sistemlerinin teorisini ve tasarımını ele almaktadır: statik ve dinamik tipleme, parametrik ve ad hoc polimorfizm, alt tipleme (subtyping), tip çıkarımı (type inference) ve bağımlı (dependent) ve alt yapısal (substructural) tipler gibi gelişmiş sistemler. Ayrıca, tip sağlamlığı (type soundness), Curry-Howard yazışması (correspondence) aracılığıyla tipler ve mantık arasındaki ilişki ve tipleme disiplinlerinin ifade gücünü güvenceler ve karar verilebilirlik (decidability) ile nasıl dengelediği konularını da incelemektedir.
Alt konular
Temel sorular
- Bir tip sistemi hangi güvenceleri sağlamaktadır ve tip sağlamlığı nedir?
- Polimorfizm ve alt tipleme (subtyping), güvenliği feda etmeden ifade gücünü nasıl artırmaktadır?
- Tipler otomatik olarak çıkarılabilir mi ve çıkarım ne zaman karar verilebilirdir (decidable)?
- Tipler, tam spesifikasyonlara kadar zengin program özelliklerini ne ölçüde kodlayabilir?
Temel kuramlar
- İlerleme ve koruma yoluyla tip sağlamlığı
- Wright ve Felleisen'ın sentaktik yaklaşımı, iyi tiplemeli programların takılıp kalmadığını (stuck) göstererek bir tip sisteminin sağlamlığını kanıtlamaktadır: tipler değerlendirme altında korunmakta ve iyi tiplemeli terimler her zaman ilerleme kaydedebilmektedir.
- Polimorfizm ve soyutlamanın tipolojisi
- Cardelli ve Wegner, tipleme kavramları alanını düzenleyerek, parametrik ve ad hoc polimorfizmi, dahil etmeyi (alt tipleme) ve veri soyutlamasını birleşik bir çerçeve içinde birbirinden ayırmaktadır.
- Programlama dili temeli olarak tip teorisi
- Harper, dil özelliklerinin tipleme ve değerlendirme kurallarıyla tanımlandığı, tip teorisini dil tasarımı için düzenleyici temel olarak ele alan tek tip bir statik-ve-dinamik metodoloji geliştirmektedir.
Klinik önem
Tip sistemleri, en yaygın kullanılan resmi yöntemler arasında yer almaktadır: derleme zamanında hataları yakalamakta, arayüzleri belgelemekte, güvenli yeniden düzenlemeyi (refactoring) mümkün kılmakta ve düzenleyici araçları (editor tooling) yönlendirmektedir. Jenerikler (generics), kademeli tipleme (gradual typing) ve sahiplik tipleri (ownership types) gibi ilerlemeler doğrudan ana akım endüstriyel dillere girmiştir.
Tarihçe
Tiplemeli diller, Algol ve basit tiplemeli lambda kalkülüsü gibi erken sistemlerle ortaya çıkmıştır. Milner'ın polimorfik tip çıkarımı (1978) ML'in temelini oluşturmuştur; Girard ve Reynolds, parametrik polimorfizm için bağımsız olarak System F'yi geliştirmişlerdir. Cardelli ve Wegner'ın 1985 tarihli araştırması alanı sistemleştirmiş ve ilerleme-ve-koruma yöntemi (1994), Pierce ve Harper'ın daha sonra ders kitaplarında standart sağlamlık tekniği olarak kabul ettiği yöntem haline gelmiştir.
Tartışmalar
- Statik ve dinamik tipleme
- Uzun süredir devam eden bir tartışma, statik tiplemenin erken hata tespiti ve belgelenmesini, dinamik tiplemenin esnekliği ve hızlı yinelemesiyle karşılaştırmakta, kademeli tipleme ise bir uzlaşma olarak sunulmaktadır.
Öne çıkan isimler
- Benjamin Pierce
- Robert Harper
- Luca Cardelli
- Robin Milner
- Matthias Felleisen
İlgili konular
Temel eserler
- pierce2002
- harper2016
- cardelli1985
- wright1994
Sıkça sorulan sorular
- Bir tip sisteminin sağlam olması ne anlama gelmektedir?
- Sağlamlık, iyi tiplemeli programların tip sisteminin önlemek üzere tasarlandığı hataları sergileyemeyeceği anlamına gelmektedir; bu durum genellikle tiplerin değerlendirme sırasında korunduğu ve iyi tiplemeli programların asla takılıp kalmadığı gösterilerek kanıtlanmaktadır.
- Dinamik tiplemeli dillerin tip sistemleri var mıdır?
- Bu dillerin tipleri vardır ve çalışma zamanı tip kontrolleri yaparlar, ancak yürütmeden önce hatalı tiplemeli programları reddeden statik bir tip sisteminden yoksundurlar; tip hataları bunun yerine çalışma zamanı arızaları olarak ortaya çıkmaktadır.