Çift yönlü tür denetimi bulmacası

• Grace içindeki çift yönlü tür denetimi uygulamasında, listedeki ilk öğenin türü tüm öğelerin türüymüş gibi kullanıldığı için port: 8080 alanı siliniyor ve yanlış değerlendirme sonucu üretiliyordu
• Sorunlu örnek, { domain: "google.com" } ve { domain: "localhost", port: 8080 } listesini dolaşıp varsayılan port olarak 443 kullanan bir koddu; beklenen değer [ "google.com:443", "localhost:8080" ] iken bunun yerine [ "google.com:443", "localhost:443" ] döndürülüyordu
• Eski liste çıkarımı, ilk öğeden List { domain: Text } türünü çıkarıp kalan öğeleri bu türe göre denetliyordu; ayrıntılandırma (elaboration) sürecinde üst türde bulunmayan port alanı siliniyordu
• Düzeltilen uygulama, önce tüm öğe türlerini çıkarıyor, ardından en özgül üst türü hesaplıyor ve her öğeyi bu türe göre yeniden denetleyerek eksik Optional değerleri null veya some ile dolduruyor
• Düzeltmeden sonra asıl liste List { domain: Text, port: Optional Natural } olarak çıkarılıyor; ilk kaydın port alanı null, ikinci kaydın port: 8080 değeri ise some 8080 olarak korunuyor ve beklenen sonuç döndürülüyor

---

Grace'in liste türü çıkarımı hatası

• Grace, Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism temelli bir çift yönlü tür denetimi sistemi kullanıyor; bu yaklaşımın sınırlarını aşmak için biriken uygulama ayrıntıları zamanla garip bir hataya yol açtı
• Sorunlu program, authorities listesini dolaşırken her kaydın domain ve port alanlarını bağlıyor, port yoksa varsayılan olarak 443 kullanan bir liste üreteci biçimindeydi

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

• Beklenen sonuç [ "google.com:443", "localhost:8080" ] idi, ancak hatalı sürüm [ "google.com:443", "localhost:443" ] döndürerek ikinci kaydın port: 8080 alanını tamamen yok sayıyordu
• Sorun değerlendiricide değil, tür denetleyicide ortaya çıkıyordu; liste türü çıkarımı ile tür denetimi sırasında yapılan ayrıntılandırma birlikte etkili oluyordu

Çift yönlü tür denetimi ve eski liste çıkarımı yaklaşımının sınırları

• Grace'in authorities listesi için beklediği tür şuydu

List { domain: Text, port: Optional Natural }

• Bu tür, her kaydın zorunlu domain: Text alanına sahip olduğunu ve port: Optional Natural alanının bulunabileceğini ya da bulunmayabileceğini ifade eder
• Gerçekte eski uygulama şu şekilde daha dar bir tür çıkarıyordu

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

• Çift yönlü tür denetimi temelde iki işe ayrılır
  • ifadenin türünü çıkarmak
  • ifadenin beklenen türe uyup uymadığını denetlemek
• Yalnızca bu iki işlemle, bir listedeki farklı öğe türlerini birleştirip tüm listenin öğe üst türünü üretmek kolay değildir
• Eski Grace uygulaması liste türünü şu şekilde çıkarıyordu
  • listenin ilk öğesinin türünü çıkarıyordu
  • kalan tüm öğelerin, ilk öğeden çıkarılan türe uyup uymadığını denetliyordu
• İlk öğe { domain: "google.com" } için tür { domain: Text } olduğundan, tüm liste öğelerinin türü de { domain: Text } oluyordu
• Farklı bir tür istenirse açık tür notasyonu eklemek gerekiyordu; ancak Grace'in işlemeyi hedeflediği gerçek dünyadaki JSON şemaları büyük ve karmaşık olabildiği için, tüm şemayı dev bir tür notasyonu olarak yazmaya zorlamak istenmiyordu

Ayrıntılandırma neden değerlendirme sonucunu da değiştirdi

• Grace'in tür denetleyicisi yalnızca tür hatalarını yakalamaz; tür denetimi sırasında ifadeyi ayarlayan ayrıntılandırma (elaboration) işlemini de yapar
• Bir alt tür, bir üst türe göre denetlenirken iki tür farklıysa tür denetleyici açık bir zorlama dönüşümü (coercion) ekler
• Grace değerlendiricisi dahili olarak tüm Optional değerleri null veya some x etiketi taşıyan değerler olarak temsil eder
• Optional beklenen bir konuma etiketsiz bir değer konursa, Grace otomatik olarak some etiketini ekler

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

• İlk öğenin türü Optional Natural olarak çıkarılıp ikinci öğe etiketsiz Natural ise, tür denetleyici tür uyuşmazlığı hatası vermek yerine some etiketini ekler
• Aynı şey kayıtlarda da olur; Grace kayıt alt türlerini destekler ve kayıtları üst türe uydurmak için zorlar

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

• Bir kayıt daha küçük bir kayıt türüyle notlandığında, tür denetleyici bunu kabul ederken üst türde bulunmayan alanları kaldırır
• Eski uygulamada yalnızca authorities listesini değerlendirmek bile port alanının aşağıdaki gibi silinmesine yol açıyordu

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

• Bu sonuç şu akışla ortaya çıkıyordu
  • ilk öğenin türü { domain: Text } olarak çıkarılıyordu
  • ikinci öğe bu beklenen türe göre denetleniyordu
  • ikinci öğe bu türle uyumluydu ama ek port alanına sahipti
  • tür denetleyici beklenen türe uydurmak için port alanını kaldırıyordu
• Kayıt zorlama dönüşümünün kendisi temel neden değildi; asıl neden, liste türü çıkarımında ilk öğenin türünü tüm listenin türüymüş gibi ele alan yaklaşımdı

Çözüm: en özgül üst türü hesaplamak

• Grace, listenin tamamının türünü doğru çıkarmak için yeni bir işlem ekledi
• Yeni işlem, iki türün en özgül üst türünü (most-specific supertype), yani en küçük üst sınırını (least upper bound) hesaplar
• C'nin A ve B için bir üst tür olması, C'nin hem Anın hem de Bnin üst türü olması demektir
• C'nin A ve B için en özgül üst tür olması ise, C'nin A ve Bnin diğer tüm üst türlerinin alt türü olması demektir
• Bu yeni işlemi kullanan liste türü çıkarımı artık şu sırayla çalışıyor
  • listedeki her öğenin türünü çıkarıyor
  • tüm öğe türlerinin en özgül üst türünü hesaplıyor
  • her öğenin bu en özgül üst türe uyup uymadığını denetliyor
  • bu en özgül üst türü tüm listenin öğe türü olarak döndürüyor
• Bu yöntemle aşağıdaki liste doğru türü çıkarıyor

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

• Dahili akış şu şekilde
  • { x: 1 } için { x: Natural } türü çıkarılıyor
  • { y: true } için { y: Bool } türü çıkarılıyor
  • bu iki türün en özgül üst türü { x: Optional Natural, y: Optional Bool } oluyor
  • her öğe bu üst türe göre denetleniyor
• Her öğenin yeniden üst türe göre denetlenmesinin nedeni, eksik some ve null değerlerini doldurmak gibi doğru ayrıntılandırmayı uygulayabilmektir

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

Düzeltmeden sonra authorities türü ve değerlendirme sonucu

• Tür denetleyicisindeki düzeltmeden sonra asıl authorities listesi beklenen türü çıkarıyor

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

• Ayrıntılandırılmış değerlendirme sonucu da port alanını isteğe bağlı alan olarak koruyor

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

• İlk kayıttaki eksik port alanı null ile dolduruluyor, ikinci kaydın port: 8080 değeri ise some 8080 olarak korunuyor
• Orijinal liste üreteci örneği de beklenen sonucu döndürüyor

[ "google.com:443", "localhost:8080" ]

JSON desteği ile uygulama karmaşıklığı arasındaki tercih

• Grace'in çift yönlü tür denetiminde ısrar etmesinin nedeni, bu yaklaşımın karmaşık olsa da gerçek dünyadaki JSON türlerini çıkarabilecek kadar güçlü bir tür denetimi çatısı sunduğuna inanılması
• Hindley-Milner çıkarımı ya da benzer daha basit tür denetimi çatıları, gerçek JSON verilerinde görülebilen biçimleri ele almakta zorlanır
• Grace yalnızca JSON işleri için ergonomik bir dil olarak tasarlanmadı, ama JSON desteğini de göz ardı etmedi
• Dhall deneyimi, kullanıcıların ergonomik JSON birlikte çalışabilirliğine duyarlı olduğunu gösterdi; bu nedenle Grace'in sözdizimi ve tür sistemi, uygulama karmaşıklığı artsa bile JSON uyumluluğunu gözeterek tasarlandı

Bakmaya değer ilgili kaynaklar

• Datatype unification using Monoids: Grace'te en özgül üst türü hesaplarken kullanılan algoritmayla özünde aynı olan, basit veri türü çıkarımı algoritmasını ele alır
• The appeal of bidirectional typechecking: Bir şekilde alt tür kullanan bir dili uygulamak isteyenlerin neden çift yönlü tür denetimini öğrenmeye değer bulabileceğini anlatır
• Local Type Inference: Çift yönlü tür denetiminin öncü makalelerinden biridir; en küçük üst sınır ve ifadelerin iç dile ayrıntılandırılması gibi tekniklerin kaynağı olarak anılır

Ek: kayıt zorlama dönüşümü neden gerekli

• Aşağıdaki Grace ifadesi, kayıt zorlama dönüşümünün neden gerekli olduğunu gösteren bir örnektir

let f (input: { }) = input.x

in  f { x: 1 }

• Bu ifade tür denetiminden geçerse, fnin dönüş türünün ne olması gerektiği bir sorun haline gelir
• Dönüş türü Natural olamaz

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

• f, boş kayıt türü { } olan bir input alır; bu yüzden o kayıttan bir Natural değeri çıkaramaz
• Çağrı sırasında tesadüfen x alanı olan bir kayıt verilse bile, f fonksiyonunun { } türündeki her girdi için çalışması gerekir
• Tür denetleyicinin, bildirilen girdi türünde bulunmayan alan erişimini reddetmesi de tutarlı bir seçim olurdu; ancak bu durumda gerçek JSON verisini işlemek için gereken yetenek kaybedilirdi
• Asıl authorities örneği, özünde aşağıdaki ifadenin sözdizimsel şekeriyle aynıdır

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

• Eksik alan erişimi reddedilirse, potansiyel olarak eksik olabilecek alanları bağlamak veya varsayılan değerle işlemek mümkün olmaz
• Gerçek JSON verisini iyi işlemek için yapılan tasarım tercihi şuydu
  • alan yoksa null döndürmek
  • erişim türünü forall (a: Type) . Optional a olarak belirlemek
• Bu tür, yalnızca null içerebilen bir türdür
• Bu yaklaşım seçildiğinde, üst türde bulunmayan alanların kayıttan mutlaka kaldırılması gerekir
• Ek alanlar kaldırılmazsa aşağıdaki örnek 1 : forall (a: Type) . Optional a döndürmüş olur

let f (input: { }) = input.x

in  f { x: 1 }

• Bu, yalnızca null içermesi gereken bir türe 1 yerleştiren yanlış türde bir ifade olur
• Böyle bir yanlış ifade değerlendiriciyi bile bozabilir

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

• Gerçek JSON verisini işleyen Grace için kayıtları üst türe göre açıkça zorlamak makul bir davranıştır; gerçek hata zorlama dönüşümünde değil, List türü çıkarımı için kullanılan eski geçici çözümdeydi

[GN⁺]

Lobste.rs görüşleri

• Complete And Easy makalesini gerçekten çalışan bir hale getirmiş olmaları kutlanacak bir şey. Bu aynı zamanda iki yönlü tip denetiminin açgözlü doğasının ince sorunlar yaratabildiğine dair iyi bir örnek
  Bu bir eleştiri değil; çıkarımda her zaman sorunlar vardır ve sonuçta hangi sorunları göze alacağını seçmeye daha yakındır. Bu yüzden kişisel olarak alt tipleme ve tip zorlamalarını çoğunlukla antipattern olarak görüyorum
  Veriyi tipin hakikat kaynağı yaparsanız verinin yanlış olup olmadığını denetlemek zorlaşır ve örnekteki gibi faydalı bir hata yerine yanlış bir tip elde edersiniz. Yine de Dhall'ı yapan kişi olduğundan, bu konuyu muhtemelen benden çok daha iyi biliyordur. Birden fazla veriyi alıp şema üretme fikrinin kendisi araştırmaya değer, ama tiplerin genelde betimleyici değil kural koyucu olarak görüldüğü düşünülürse buna “tip denetimi” demek gerekir mi emin değilim

• Neden f'in doğrudan reddedilmediğini pek anlayamıyorum. O alanı asla taşıyamayacak bir tipin kaydında bir alana erişiliyor; bu neredeyse kesinlikle bir program hatası ve tip denetleyicisinin bunu bildirmesi gereken bir durum gibi görünüyor
  authority örneğinden farkı, port tipinin eksik olması değil Optional olması. Eksik alanları reddetmek, isteğe bağlı alanları da reddetmek zorunda olduğunuz anlamına gelmez. Zaten tipe dayalı olarak değerleri zorluyorsanız, { domain: "google.com" } değerini de { domain: "google.com", port: null } değerine zorlayabilirsiniz

  • Kısaca söylemek gerekirse f'i illa reddetmeye gerek yok; bu gereksiz bir kısıtlama. Hatalı alan erişiminin null : forall (a : Type) . Optional a döndürmesi, hatalı alan erişimini reddetmekten kesin olarak daha iyi görünüyor
    Daha fazla geçerli programa izin veriyor ve yanlış tiplendirilmiş programlar yine başarısız oluyor. Örneğin erişilen değeri null işlemeden kullanmaya çalışan bir program hâlâ tip hatası verir

• Aklıma ilk gelen şey, satır tipleri (row types) bunun çözümü olduğu. Muhtemelen bunu zaten düşünmüşlerdir. Burada satır tipleri alt tiplemeyle etkileşime girince mi bozuluyor?

  • Grace'te satır tipleri ve satır çokbiçimliliği var. Grace'te satırlara “fields” deniyor ama onun dışında tamamen aynı
    Aslında en özgül üst tip algoritması da satır tiplerini hesaba katıyor
    Örneğin şöyle yazarsanız:

    \record0 record1 ->
    
    let _ = record0.x
    
    let _ = record1.y
    
    in  [ record0, record1 ]  
    

    Grace bu ifade için şu tipi çıkarıyor:

    forall (a : Type) .  
    forall (b : Type) .  
    forall (c : Fields) .  
      { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }  
    

• Bu, Bidirectional Typing makalesinin 5.1.1 bölümünde sözü edilen açgözlü örnekleme sorununa bir örnek değil mi?
  “Özgün kurulumda bu açgözlü yaklaşımın argüman sırasına duyarlı olması oldukça talihsizdi. Ancak başka alt tipleme biçimleri olmayan predikatif yüksek dereceli çokbiçimlilik ortamında iyi çalışabilir. ‘tabby-first problem’ ortaya çıkamaz, çünkü tipin kesin olarak küçülebileceği tek yol kesin olarak daha çokbiçimli hale gelmesidir ve ilk argüman çokbiçimliyse 𝛼'yı çokbiçimli bir tiple örneklemek gerekir; bu da predikatifliği ihlal eder”