Tip sistemi notasyonu nasıl okunmalı?

 (langdev.stackexchange.com)
1 puan yazan GN⁺ 2023-08-17 | 1 yorum | WhatsApp'ta paylaş
  • Tip sistemi notasyonu kaynaktan kaynağa değişse de sözdizimi, tipleme ilişkisi ve çıkarım kuralları gibi ortak çerçeveyi bilirseniz çoğu varyasyonu takip edebilirsiniz
  • Tip sistemleri dilin soyut sözdizimi üzerinde çalıştığı için, önce tipe sahip terimleri (term) ve tiplerin kendisini sözdizimsel olarak ayırmak gerekir
  • ⊢ e: τ, “e ifadesi τ tipine sahiptir” anlamına gelen bir tipleme yargısıdır; yatay çizginin üstündeki koşulların hepsi doğruysa alttaki sonucun da doğru olduğu bir çıkarım kuralı olarak okunur
  • Değişkenler ve fonksiyonlar devreye girdiğinde, geçerli kapsamdaki değişken adlarını ve tiplerini izlemek için Γ ⊢ e: τ biçiminde bir bağlam eklenir
  • Birçok tipleme kuralı özyinelemeli bir tip denetleme fonksiyonu gibi okunabilir, ancak her mantıksal yargı doğrudan karar verilebilir bir tip denetleme algoritmasına dönüşmez

Sözdiziminden başlayan tip sistemi notasyonu

  • Tip sistemi, programlama dilinin sözdizimsel bir sistemidir ve dilin soyut sözdizimi üzerinde çalışan bir kurallar kümesidir
  • Kapsamlı bir tip sistemi açıklaması genellikle ele aldığı sözdizimsel yapıyı önce gramer olarak sunar ve bunu BNF notasyonuyla gösterir
  • En basit tipli dilde bile sözdizimi kabaca iki kategoriye ayrılır
    • e: tipe sahip ifade (expression)
    • τ: ifadelere atanan tip (type)
  • Örnek dil; boolean literal’ları, tamsayı literal’larını, koşul ifadelerini, aritmetik işlemleri ve karşılaştırma işlemlerini ifade olarak içerir; tip olarak da Bool ve Int kullanır
  • Tip sembolü, kaynağa bağlı olarak τ yerine t, T, σ veya başka küçük Yunan harfleriyle de yazılabilir; genel yapı benzerdir
  • Daha karmaşık diller, deyimler veya pattern matching kalıpları gibi daha fazla sözdizimsel kategori içerebilir

Tipleme ilişkisini ve yargıları okumak

  • Sözdizimi belirlendikten sonra genellikle e : τ biçiminde bir tipleme ilişkisi tanımlanır
    • 1 + 2 : Int, “1 + 2, Int tipindedir” anlamına gelir
    • 1 + 2 : Bool, aynı ifadenin Bool tipinde olduğu anlamına geldiğinden doğru değildir
    • true + 2 : Int ise ifadenin kendisi anlamlı olmadığından hiçbir tipe sahip değildir
  • ⊢ e : τ bir tipleme yargısıdır; ⊢, “arkasındaki önerme doğrudur” diye okunabilir
  • Yatay çizginin üstünde hiçbir şey olmayan kurallar her zaman doğru olan aksiyomlardır (axiom)
    • ⊢ true : Bool
    • ⊢ false : Bool
    • ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int gibi tamsayı literal kuralları
  • Yatay çizginin hem üstü hem altı olan kurallar çıkarım kurallarıdır
    • Üstteki koşulların hepsi doğruysa alttaki sonuç doğrudur
    • e₁ ve e₂ ikisi de Int ise e₁ + e₂, Int tipindedir
    • e₁ ve e₂ ikisi de Int ise e₁ < e₂, Bool tipindedir

Koşul ifadeleri ve tip değişkenleri

  • if ... then ... else ... ifadesinin iki dalı herhangi bir tipte olabilir, ancak birbirleriyle aynı tipte olmalıdır
    • if true then 1 else 2 mümkündür
    • if true then false else true mümkündür
    • if true then 1 else true mümkün değildir
  • Bunu ifade etmek için kural, dal tipini temsil eden τ değişkenini kullanır
    • Koşul ifadesi e₁, Bool olmalıdır
    • then dalı e₂ ve else dalı e₃ aynı τ tipinde olmalıdır
    • Tüm koşul ifadesinin tipi de τ olur
  • Kural uygulanırken τ için herhangi bir tip seçilebilir, ancak aynı kural içinde bu seçim tutarlı biçimde korunmalıdır

Çıkarım kurallarını algoritma gibi okumak

  • Bu notasyon biçimsel mantıktan gelir ve tip sistemi belirtim tarzı özellikle doğal çıkarıma benzer
  • Bu tür kurallar sistem özelliklerine ilişkin biçimsel kanıtlar kurmak için kullanılır ve tip güvenliği gibi özellikleri kanıtlamada önemlidir
  • Mantıksal yargılar her zaman doğrudan karar verilebilir bir tip denetleme algoritmasına karşılık gelmez
  • Çoğu durumda ⊢ e : τ, e ifadesinden τ tipini elde eden bir fonksiyon gibi okunabilir
    • Sözdizimindeki her ifade biçimi için genellikle bir kural vardır
    • Her tipleme kuralı, özyinelemeli bir tip denetleme fonksiyonunun bir dalı gibi görülebilir
  • Örnekteki infer fonksiyonu aşağıdaki akışa karşılık gelir
    • true veya false, Bool tipindedir
    • Tamsayı literal’ları Int tipindedir
    • e₁ + e₂, iki tarafın çıkarım sonucunun da Int olduğunu doğruladıktan sonra Int olur
    • e₁ < e₂, iki tarafın da Int olduğunu doğruladıktan sonra Bool olur
    • if e₁ then e₂ else e₃, koşulun Bool olduğunu doğrular, iki dalın tipinin aynı olduğunu kontrol eder ve sonra o tipi döndürür
  • Doğrudan algoritmaya çevrilemese bile, yargıda eyi girdi, τyu çıktı gibi düşünmek bilgi akışını anlamayı kolaylaştırır

Değişkenler ve bağlam

  • Kullanışlı bir programlama dilini ele almak için değişkenler gerekir; örnek, fonksiyonlar eklenerek basit tipli lambda hesabı biçimine genişletilir
  • Genişletilmiş sözdizimi şunları içerir
    • Değişken x
    • Fonksiyon soyutlaması λx:τ. e
    • Fonksiyon uygulaması e e
    • Fonksiyon tipi τ → τ
  • λx:τ. e, TypeScript’teki (x:τ) => eye; f x ise f(x)e karşılık gelir
  • Bir değişkenin tipi, değişkenin geçtiği bağlama bağlı olduğundan basit bir ⊢ x : ??? biçimiyle kural yazılamaz
  • Bu yüzden tipleme yargısı Γ ⊢ e : τ biçimine genişletilir
    • Γ bağlam veya tip ortamıdır
    • ⊢, soldaki bağlamsal varsayımları sağdaki kanıtlanacak önermeden ayırır
    • “Bağlam Γ altında e ifadesi τ tipine sahiptir” diye okunur
  • Algoritmik olarak Γ, Map<Variable, Type> biçiminde ek bir girdi gibi görülebilir
  • Biçimsel olarak bağlam da sözdizimsel yapı olarak açıkça belirtilir
    • ∅: boş bağlam
    • Γ, x:τ: değişken bağlaması eklenmiş bağlam
    • Bazen ∅ yerine boş bağlam için • kullanılır
  • Bu gösterimde bağlam, değişken adlarını tiplere eşleyen bir association list’e yakındır

Bağlam kurallar içinde ne yapar?

  • Birçok tipleme kuralı bağlamı değiştirmeden olduğu gibi aktarır
    • Γ ⊢ true : Bool
    • Γ ⊢ e₁ : Int ve Γ ⊢ e₂ : Int ise Γ ⊢ e₁ + e₂ : Int
  • Değişken kullanımı ve lambda ifadesi kurallarında bağlam kilit rol oynar
    • x:τ ∈ Γ ise Γ ⊢ x : τ
    • Γ, x:τ₁ ⊢ e : τ₂ ise Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Lambda ifadesinin gövdesi e tip denetiminden geçirilirken bağlam yeni x:τ₁ bağlamasıyla genişletilir
  • Değişken kuralı, mevcut bağlamda değişken bağlaması varsa o değişkenin ilgili tipe sahip olduğuna hükmeder
  • Bağlam, lambda ifadesi kuralı ile değişken kuralı arasında bilgi taşıyan bir iletişim mekanizması olarak kullanılır
  • Basitleştirmek için, bu tür tip sistemi belirtimleri genellikle tüm değişkenlerin zaten çözümlendiğini ve benzersiz hale getirildiğini varsayar; değişken gölgeleme ele alınmaz
  • Fonksiyon uygulaması kuralı, fonksiyon ifadesinin ve argüman ifadesinin tiplerini birlikte kontrol eder
    • e₁, τ₁ → τ₂ tipinde olmalıdır
    • e₂, τ₁ tipinde olmalıdır
    • Tüm uygulama e₁ e₂nin tipi τ₂ olur

Sık görülen ek notasyonlar

  • Çıkarım kuralları her zaman yalnızca dikey yazılmaz
    • Birden fazla koşul yatay olarak yan yana yer alabilir
    • Dikey yerleşim ve yatay yerleşim aynı kural içinde karışık kullanılabilir
  • Yatay çizginin üstündeki koşullar genellikle başka yargılardır, ancak yan koşul (side condition) olan herhangi bir boolean koşul da gelebilir
    • Değişken kuralındaki x:τ ∈ Γ buna örnektir
    • Algoritmik tip sistemlerinde α fresh kullanılabilir; bu, αnın diğer tip değişkenlerinden ayırt edilen yeni bir tip değişkeni olması gerektiği anlamına gelir

Alt tipleme

  • Alt tipleme, tipler arasındaki uyumluluğu katı eşitlikten daha zayıf ele alan bir ilişkidir ve açıkça tanımlanmalıdır
  • Genellikle τ₁ <: τ₂ biçiminde yazılır ve “τ₁, τ₂nin alt tipidir” diye okunur
  • Basit bir alt tipleme ilişkisi en üst tip ⊤ ve en alt tip ⊥ kavramlarını getirebilir
    • τ <: τ: Her tip kendi kendisinin alt tipidir
    • τ <: ⊤: Her tip ⊤nin alt tipidir
    • ⊥ <: τ: ⊥, her tipin alt tipidir
  • İlk kural yansıma kuralıdır ve genellikle refl olarak kısaltılır
  • Alt tiplemeye izin vermek için, buna izin veren her tipleme kuralında ilişki açıkça kullanılmalıdır
    • Fonksiyon uygulaması kuralında argüman tipi τ₁, parametre tipi τ₂nin alt tipiyse uygulamaya izin verilebilir

Birden çok bağlam ve çift yönlü tip denetleme

  • Bazı tip sistemleri birden fazla bağlam içeren tipleme yargıları tanımlar
    • İkinci bağlam genellikle Δ olarak adlandırılır
    • Γ;Δ ⊢ e : τ, iki bağlam da girdi gibi kullanıldığında sıkça kullanılır
    • Γ ⊢ e : τ ⊣ Δ, Δ çıktı gibi kullanıldığında sıkça kullanılır
  • İkinci bağlam kullanım amacına göre farklı şekillerde değerlendirilir
    • Belirli değişkenlerin yalnızca belirli ifadeler içinde başvurulabilir olmasını sağlayabilir
    • Kaynak duyarlı programlama dillerinde hangi değişkenlerin tüketildiğini izleyen bir çıktı bağlamı olarak kullanılabilir
  • Çift yönlü tip denetleme, kısıt çözücü olmadan sınırlı yerel olmayan tip çıkarımı gerçekleştiren bir yaklaşımdır
  • Çift yönlü sistemler genel Γ ⊢ e : τ yargısını iki uzmanlaşmış yargıya ayırır
    • Γ ⊢ e ⇐ τ: e ifadesinin beklenen τ tipine sahip olup olmadığını doğrulayan denetleme (checking) yargısıdır; algoritmik olarak τ girdidir
    • Γ ⊢ e ⇒ τ: Beklenen tip bilgisi olmadığında kullanılan çıkarım (inference) yargısıdır; algoritmik olarak τ çıktıdır
  • İki yargı karşılıklı özyinelemeli olarak tanımlanır ve tip bilgisini iki yönde taşır
  • Bu yöntemle bazı tip açıklamaları atlanabilir; lambda soyutlamasının denetleme kuralı beklenen fonksiyon tipinden parametre tipini elde edebildiği için değişken bağlayıcısındaki açıklama atlanabilir

İlgili okumalar

1 yorum

 
GN⁺ 2023-08-17
Hacker News yorumları

  • Guy Steele geçmişte bu konuda bir sunum yapmıştı. Bazı gösterimlere aranabilir adlar da vermişti; örneğin iki boyutlu çıkarım kuralı diyagramları gibi
    Kendisi buna bilgisayar bilimi meta gösterimi diyor, ama kişisel olarak programlama dili teorisine daha yakın görünüyor. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Bu gösterimin kökeni Frege’ye kadar gider. Ne arayacağını bilmiyorsan bulması zor, ama bu yazı oldukça iyi bir özet gibi görünüyor: https://plato.stanford.edu/entries/frege-logic
    Turnstile sembolü |- zaten kullanılıyordu; derste “Fregescher Schlussstrich”, yani Frege’nin sonuç çizgisi denen yatay çizgi ise sanırım başlangıçta turnstile’ın bir parçasıyken modern gösterimde ayrı bir unsur hâline gelmiş

    • “Schlussstrich” muhtemelen tümdengelim çizgisi ya da çıkarım çizgisi diye daha iyi çevrilebilir

  • Benjamin C. Pierce’ın Types and Programming Languages kitabı bu konuları ele alan iyi bir ders kitabı

    • İronik biçimde TAPL, kendi kullandığı sözdizimin temel anlamını açıklamakta epey belirsiz. Bu yanıt TAPL’den birkaç mertebe daha açık

  • Bilgisayar bilimi mezunu olmama rağmen |– ile |= arasındaki anlam farkı ve kullanılan değişkenlerin her birinin hangi meta sözdizim düzeyinde olduğu hâlâ kafamı karıştırıyor
    İronik biçimde, gösterimin kendisinde açık tiplerin olmaması bunun nedenlerinden biri

  • Okuyup okumamakta tereddüt edenlere: Bu yazı, bilgisayar bilimi makalelerinde geçen tip sistemi gösterimini açıklıyor; fiilen tip sistemleri için BNF gösterimine, çıkarım kurallarına vb. giriş niteliğinde
    İyi bir özet gibi görünüyor

    • Açıkçası sembollerin İngilizce sözcüklerle nasıl okunduğunu anlatan bir cheat sheet yeterli olurdu
      Tip uygulamasının mantıksal kavramını anlıyorum, ama bilgisayar bilimi makalelerini sık okumadığım için sembollerle anlamları zihnimde pek oturmuyor
    • Bunun yıllar içinde böylesine titizlikle soyutlanmış olması, bilgisayar bilimine özgü yanı gösteriyor

  • Örneklerden birinde 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 ifadesinin “𝗍𝗋𝗎𝖾+2, 𝖨𝗇𝗍 tipindedir” anlamına geldiği, ancak 𝗍𝗋𝗎𝖾+2 ifadesinin kendisinin anlamsız olduğu ve bir tipi de olmadığı için daha da tuhaf olduğu söyleniyor
    Oysa Python’da True + 2 gerçekten bir tam sayıdır ve değeri de 3’tür. Böyle olması gerekir mi ayrı konu, ama fiilen durum bu

    • True + 2nin anlamlı olduğunu düşünüyorsan, buna izin veren yargı kuralını kendin tanımlayabilirsin
      Mantık ve tip sistemi teorisi hangi aksiyomları ve çıkarım kurallarını kullandığınla kendi başına ilgilenmez; yalnızca bu kurallar ve aralarındaki etkileşimler hakkında akıl yürütmeni sağlar. Örneğin |- True : Bool, |- True : Int gibi koyabilir ya da yalnızca belirli ifadelerde izin vermek istiyorsan |- x : Intten |- True + x: Int sonucunu çıkaracak şekilde kurabilirsin
    • Bu dilden dile değişen bir şey değil mi? Örneğin C’de true 1’e eşlendiği için true+1=2 olur
    • Python veya C’de True + 2 hata vermese bile, programcıya biraz sözdizimsel şeker vermek uğruna dilin semantiği üzerinde akıl yürütmeyi zorlaştırdığı için yine de aptalca

  • Güzel. Yıllardır merak ediyordum ama daha fazlasını öğrenmek için hangi arama terimlerini kullanacağımı bilmiyordum

  • Bazen zahmetle öğrendiğin ezoterik bilgiyi biri bedavaya ortaya dökünce boş yere rahatsız oluyorsun ;) Ben bunu öğrenirken böyle bir yazı olsaydı gerçekten harika olurdu. Erişilebilirlik arttıkça berbat dillerin azalmasını umuyorum

  • Ada Reference Manual’ı okurken bu tür sözdizimini hemen tanıdım. Adını bilmiyordum ama gerçek kullanım örneği olarak görmek ilginçti; dilin tamamı bu gösterimle tanımlanmış
    Örnek: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Burada sonuna kadar savunmaya karar verdiğim bir tezi yaymak için iyi bir yer gibi. İki nokta üst üste kullanan type annotation biçiminde, iki noktanın iki yanında boşluklar eşit olmalı
    Bana göre, tesadüfen aynı görünen, yani iki nokta olarak yazılan iki farklı işaret var. Biri İngilizcedeki gibi önceki kısmın sonraki kısmı tanıttığı ya da soldakinin sağdakinin etiketi olduğu etiket iki noktası; Python’daki blok başlangıcı, anahtar-değer çiftleri, C veya Rust’taki struct ad-değer çiftleri buna girer
    Diğeri ise matematikten ödünç alınmış type annotation’dır. Bu ikili bir ilişkidir ve ikili ilişkilerde sol ve sağ boşluk eşit bırakılır. x= 1, x> y, x+ z yazmadığımız gibi x: X değil, x : X yazmak doğal olur
    a: b gördüğümde onu hemen etiket iki noktası olarak okuyorum; type annotation olduğunda her seferinde çok küçük de olsa ek bir zihinsel dönüşüm gerekiyor. Bu, programlama dili sözdizimiyle ilgili bir mesele; kişisel olarak X x yerine x : X biçimini çok daha fazla tercih ediyorum
    [1] “Evangelion”, εὐαγγέλιον’dan, yani “iyi haber” anlamından gelen harika bir kelime. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Birkaç yanlış anlama olabilir. Matematik yazımında da f: X->Y gibi, iki noktanın sağında daha fazla boşluk bırakan gösterimler gerçekten görülür; kontrol ettiğim 3 kitaptan 1’i yalnızca bu gösterimi kullanıyordu
      Ayrıca bu da hâlâ etiketlemeye yakındır; belirli bir tür morfizmi etiketlemektir. Matematikte iki noktanın gerçekten farklı bir anlamda kullanıldığı durum, such that kısaltması olarak kullanıldığı zamandır; örneğin { x : x \in IN and x | 2} gibi küme tanımlarında veya niceleyicilerle birlikte sıkça kullanılır
    • İlginç bir bakış açısı. Ek zihinsel adım hakkındaki söz, yaygın X x gösterimini okurken hissettiğim şeyle aynı. x: X bana çok daha doğal geliyor ve doğal dilde iki nokta üst üsteyi kullanma biçimimize de daha yakın hissettiriyor
      Bir önerme var ve iki noktadan sonrası o önermeyi daha ayrıntılı açıklıyor gibi; type da soldaki şey hakkında ek bilgi olduğundan tam oturuyor
    • Type theory’de genellikle t[boşluk]:[boşluk]T gibi iki noktanın iki yanında eşit boşluk bırakmak standart uygulama sayılır
      Type theory genel olarak tutarsız bir karmaşa olabilen yanlara sahip, ama bu örnekte herkesin oldukça tutarlı olduğu nadir durumlardan biri. Lisans yıllarında nasıl yazdığımı merak edip baktım; ben de göze hoş gelecek şekilde simetrik yazmışım: https://dvt.name/logic/horse2.pdf
    • x: X, “iki noktadan sonra açıklama gelir” kullanımına karşılık gelir
      Yani variable x: It’s an X. gibi
    • age: int, İngilizcede “person’s age: an integer” gibi kolayca yeniden okunabilir
      Bu yüzden iki nokta üst üste beni pek rahatsız etmedi