Teka-teki pemeriksaan tipe bidirectional

 (haskellforall.com)
1 poin oleh GN⁺ 1 jam lalu | 1 komentar | Bagikan ke WhatsApp
  • Implementasi pemeriksaan tipe bidirectional di Grace menghasilkan evaluasi yang salah karena menggunakan tipe elemen pertama list seolah-olah sebagai tipe semua elemen, sehingga field port: 8080 terhapus
  • Contoh masalahnya adalah kode yang menelusuri list { domain: "google.com" } dan { domain: "localhost", port: 8080 } sambil memakai port bawaan 443, dan mengembalikan [ "google.com:443", "localhost:443" ] alih-alih nilai yang diharapkan [ "google.com:443", "localhost:8080" ]
  • Inferensi list lama menurunkan List { domain: Text } dari elemen pertama lalu memeriksa elemen-elemen berikutnya terhadap tipe itu, dan dalam proses elaboration field port yang tidak ada pada supertype tersebut dihapus
  • Implementasi yang diperbaiki kini menurunkan tipe semua elemen terlebih dahulu, lalu menghitung supertype paling spesifik, dan memeriksa ulang setiap elemen terhadap tipe itu untuk mengisi nilai Optional yang hilang dengan null atau some
  • Setelah perbaikan, list asli diturunkan sebagai List { domain: Text, port: Optional Natural }, dengan port pada record pertama menjadi null dan port: 8080 pada record kedua tetap dipertahankan sebagai some 8080, sehingga hasilnya kembali sesuai harapan

Bug inferensi tipe list di Grace

  • Grace menggunakan sistem pemeriksaan tipe bidirectional berbasis Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, dan akumulasi berbagai implementasi untuk mengakali keterbatasan pendekatan ini akhirnya memunculkan bug yang aneh
  • Program yang bermasalah berbentuk list comprehension yang menelusuri list authorities, lalu melakukan binding domain dan port dari tiap record, serta memakai 443 sebagai nilai bawaan jika port tidak ada
let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"
  • Hasil yang diharapkan adalah [ "google.com:443", "localhost:8080" ], tetapi versi yang memiliki bug mengembalikan [ "google.com:443", "localhost:443" ], sehingga sepenuhnya mengabaikan field port: 8080 pada record kedua
  • Masalahnya bukan terjadi di evaluator, melainkan di typechecker, dan dipengaruhi bersama oleh inferensi tipe list serta elaboration yang dilakukan selama pemeriksaan tipe

Pemeriksaan tipe bidirectional dan batasan pendekatan inferensi list lama

  • Tipe yang diharapkan Grace untuk list authorities adalah sebagai berikut
List { domain: Text, port: Optional Natural }
  • Tipe ini berarti tiap record memiliki field wajib domain: Text, dan field port: Optional Natural bisa ada atau tidak ada
  • Namun implementasi lama justru menurunkan tipe yang lebih sempit seperti berikut
>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }
  • Pemeriksaan tipe bidirectional pada dasarnya dibagi menjadi dua pekerjaan
    • Menurunkan tipe dari sebuah ekspresi
    • Memeriksa apakah sebuah ekspresi cocok dengan tipe yang diharapkan
  • Hanya dengan dua operasi ini, tidak mudah untuk menggabungkan tipe dari beberapa elemen di dalam list menjadi supertype elemen untuk keseluruhan list
  • Implementasi Grace sebelumnya menurunkan tipe list dengan cara berikut
    • Menurunkan tipe elemen pertama list
    • Memeriksa semua elemen sisanya apakah cocok dengan tipe yang diturunkan dari elemen pertama
  • Karena tipe elemen pertama { domain: "google.com" } adalah { domain: Text }, maka tipe elemen untuk seluruh list juga menjadi { domain: Text }
  • Jika ingin tipe lain, pengguna harus menambahkan anotasi tipe eksplisit, tetapi JSON dunia nyata yang ingin ditangani Grace bisa memiliki skema besar dan rumit, sehingga tidak diinginkan harus menulis seluruh skema sebagai anotasi tipe raksasa

Mengapa elaboration sampai mengubah hasil evaluasi

  • Typechecker Grace tidak hanya menangkap kesalahan tipe, tetapi juga melakukan elaboration yang menyesuaikan ekspresi selama proses pemeriksaan tipe
  • Saat memeriksa subtype terhadap supertype dan keduanya berbeda, typechecker menyisipkan coercion eksplisit
  • Secara internal, evaluator Grace merepresentasikan semua nilai Optional sebagai nilai bertanda null atau some x
  • Jika nilai tanpa tag dimasukkan ke posisi yang mengharapkan Optional, Grace otomatis menyisipkan tag some
>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]
  • Jika tipe elemen pertama diturunkan sebagai Optional Natural dan elemen kedua berupa Natural tanpa tag, typechecker akan menyisipkan tag some alih-alih menghasilkan error ketidakcocokan tipe
  • Hal yang sama juga terjadi pada record, dan Grace mendukung subtyping record serta melakukan coercion pada record agar sesuai dengan supertype
>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }
  • Jika sebuah record diberi anotasi dengan tipe record yang lebih kecil, typechecker mengizinkannya sambil menghapus field-field yang tidak ada pada supertype tersebut
  • Bahkan jika hanya mengevaluasi list authorities, implementasi lama akan menghapus field port seperti berikut
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]
  • Hasil ini terjadi melalui alur berikut
    • Tipe elemen pertama diturunkan sebagai { domain: Text }
    • Elemen kedua diperiksa terhadap tipe yang diharapkan itu
    • Elemen kedua memang cocok dengan tipe tersebut, tetapi memiliki field tambahan port
    • Typechecker menghapus field port agar sesuai dengan tipe yang diharapkan
  • Coercion pada record itu sendiri bukan akar masalahnya; penyebab sebenarnya adalah inferensi tipe list yang memperlakukan tipe elemen pertama sebagai tipe seluruh list

Solusi: menghitung supertype paling spesifik

  • Grace menambahkan operasi baru untuk menurunkan tipe list secara benar
  • Operasi baru ini menghitung supertype paling spesifik (most-specific supertype), yaitu least upper bound
  • C disebut supertype dari A dan B jika C adalah supertype dari A sekaligus supertype dari B
  • C disebut supertype paling spesifik dari A dan B jika C adalah subtype dari semua supertype lain milik A dan B
  • Dengan operasi baru ini, inferensi tipe list diubah menjadi urutan berikut
    • Menurunkan tipe tiap elemen list
    • Menghitung supertype paling spesifik dari semua tipe elemen
    • Memeriksa apakah tiap elemen cocok dengan supertype paling spesifik tersebut
    • Mengembalikan supertype paling spesifik itu sebagai tipe elemen untuk seluruh list
  • Dengan pendekatan ini, list berikut kini diturunkan dengan tipe yang benar
>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }
  • Alur internalnya adalah sebagai berikut
    • { x: 1 } diturunkan sebagai tipe { x: Natural }
    • { y: true } diturunkan sebagai tipe { y: Bool }
    • Supertype paling spesifik dari kedua tipe tersebut menjadi { x: Optional Natural, y: Optional Bool }
    • Tiap elemen kemudian diperiksa terhadap supertype tersebut
  • Tiap elemen perlu diperiksa ulang terhadap supertype itu agar elaboration yang benar bisa diterapkan, misalnya mengisi some dan null yang hilang
>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

Tipe dan hasil evaluasi authorities setelah perbaikan

  • Setelah perbaikan pada typechecker, list authorities asli kini diturunkan ke tipe yang diharapkan
>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }
  • Hasil evaluasi setelah elaboration juga mempertahankan port sebagai field opsional
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]
  • port yang tidak ada pada record pertama diisi dengan null, sedangkan port: 8080 pada record kedua dipertahankan sebagai some 8080
  • Contoh list comprehension semula juga kembali menghasilkan nilai yang diharapkan
[ "google.com:443", "localhost:8080" ]

Memilih antara dukungan JSON dan kompleksitas implementasi

  • Alasan Grace sangat menekankan pemeriksaan tipe bidirectional adalah karena pendekatan ini dianggap cukup kuat untuk menurunkan tipe JSON dunia nyata, meskipun kompleks
  • Inferensi Hindley-Milner atau kerangka typechecking yang lebih sederhana dan mirip dengannya sulit menangani bentuk data yang muncul pada data JSON nyata
  • Grace memang bukan bahasa yang dibuat semata-mata untuk ergonomi kerja dengan JSON, tetapi juga tidak mengabaikan dukungan JSON
  • Berdasarkan pengalaman dari Dhall, pembuat Grace melihat bahwa pengguna sangat peka terhadap ergonomi interoperabilitas JSON, sehingga sintaks dan sistem tipe Grace dirancang dengan mempertimbangkan kompatibilitas JSON meskipun kompleksitas implementasinya meningkat

Bacaan terkait yang layak dirujuk

  • Datatype unification using Monoids: membahas algoritme inferensi tipe data sederhana yang pada dasarnya sama dengan algoritme yang digunakan Grace untuk menghitung supertype paling spesifik
  • The appeal of bidirectional typechecking: membahas mengapa pemeriksaan tipe bidirectional layak dipelajari jika ingin mengimplementasikan bahasa yang memakai subtyping dalam bentuk apa pun
  • Local Type Inference: salah satu makalah perintis tentang pemeriksaan tipe bidirectional, dan disebut sebagai sumber teknik seperti least upper bound serta elaboration ekspresi ke bahasa internal

Lampiran: mengapa coercion record diperlukan

  • Ekspresi Grace berikut menunjukkan mengapa coercion record diperlukan
let f (input: { }) = input.x

in  f { x: 1 }
  • Jika ekspresi ini lolos pemeriksaan tipe, muncul pertanyaan: tipe hasil kembalian f seharusnya apa
  • Tipe kembalian itu tidak boleh berupa Natural
let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }
  • f menerima input bertipe record kosong { }, sehingga tidak mungkin mengekstrak nilai Natural dari record tersebut
  • Walaupun saat pemanggilan kebetulan diberikan record yang punya field x, fungsi f tetap harus dapat bekerja untuk input apa pun yang bertipe { }
  • Menolak akses field yang tidak ada pada tipe input yang dideklarasikan memang merupakan pilihan yang sound, tetapi itu akan menghilangkan kemampuan yang dibutuhkan untuk menangani data JSON nyata
  • Contoh authorities semula pada dasarnya setara dengan gula sintaks untuk ekspresi berikut
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)}"
  • Jika akses ke field yang tidak ada ditolak, maka field yang mungkin hilang tidak bisa di-bind atau diberi nilai bawaan
  • Pilihan desain untuk menangani data JSON dunia nyata dengan baik adalah sebagai berikut
    • Jika field tidak ada, kembalikan null
    • Beri tipe akses sebagai forall (a: Type) . Optional a
  • Tipe ini adalah tipe yang hanya bisa berisi null
  • Dengan pendekatan ini, field yang tidak ada pada supertype harus benar-benar dihapus dari record
  • Jika field tambahan tidak dihapus, contoh berikut akan mengembalikan 1 : forall (a: Type) . Optional a
let f (input: { }) = input.x

in  f { x: 1 }
  • Itu akan menjadi ekspresi dengan tipe salah, karena 1 masuk ke tipe yang seharusnya hanya bisa berisi null
  • Ekspresi salah seperti itu bahkan bisa merusak evaluator
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`
  • Dalam Grace yang menangani data JSON nyata, melakukan coercion record secara eksplisit agar sesuai dengan supertype adalah perilaku yang masuk akal, dan bug yang sebenarnya bukan terletak pada coercion itu, melainkan pada solusi sementara lama untuk inferensi tipe List

Bacaan terkait

1 komentar

 
GN⁺ 1 jam lalu
Komentar Lobste.rs

  • Patut diapresiasi karena berhasil membuat paper Complete And Easy menjadi sesuatu yang benar-benar berjalan. Ini juga contoh yang bagus tentang bagaimana sifat rakus dari bidirectional type checking bisa menimbulkan masalah yang halus
    Ini bukan kritik; inferensi memang selalu punya masalah, dan pada akhirnya lebih mirip memilih masalah mana yang mau ditanggung. Karena itu, secara pribadi saya menganggap subtyping dan type coercion umumnya mendekati anti-pattern
    Jika data dijadikan sumber kebenaran tipe, akan lebih sulit memeriksa apakah datanya salah, dan seperti pada contoh, kita malah mendapatkan tipe yang salah alih-alih error yang berguna. Tapi karena ini dibuat oleh orang yang membuat Dhall, sepertinya dia jauh lebih paham soal ini daripada saya. Gagasan menghasilkan skema dari beberapa data sendiri layak diteliti, tetapi karena tipe biasanya dianggap preskriptif, bukan deskriptif, saya tidak yakin apakah ini pantas disebut “type checking”

  • Saya kurang paham kenapa tidak langsung menolak f. Itu mengakses field dari record dengan tipe yang sama sekali tidak mungkin memiliki field tersebut, jadi hampir pasti ini bug program dan tampaknya memang situasi yang seharusnya diberitahukan oleh type checker
    Perbedaannya dengan contoh authority adalah tipe port bukan hilang, melainkan Optional. Menolak field yang hilang tidak berarti kita juga harus menolak field opsional. Jika Anda sudah melakukan type coercion berbasis tipe, maka { domain: "google.com" } juga bisa dikoersi menjadi nilai { domain: "google.com", port: null }

    • Singkatnya, f sebenarnya tidak perlu ditolak, dan itu adalah pembatasan yang tidak perlu. Saya menganggap pendekatan di mana akses field yang salah mengembalikan null : forall (a : Type) . Optional a secara ketat lebih baik daripada pendekatan yang menolak akses field yang salah
      Itu mengizinkan lebih banyak program yang valid, dan program yang salah tipe tetap gagal. Misalnya, program yang mencoba memakai nilai hasil akses itu tanpa menangani null akan tetap menghasilkan type error

  • Pikiran pertama saya adalah row types menyelesaikan ini. Sepertinya ini pasti sudah dipertimbangkan. Apakah di sini row types justru rusak karena berinteraksi dengan subtyping?

    • Grace memiliki row types dan row polymorphism. Di Grace, row disebut “fields”, tetapi selain itu persis sama
      Faktanya, algoritma least upper bound yang paling spesifik juga mempertimbangkan row types
      Misalnya jika ditulis seperti ini: 
      \\record0 record1 ->

let _ = record0.x

let _ = record1.y

in  [ record0, record1 ]
      Grace akan menginferensikan tipe berikut untuk ekspresi ini: 
      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 }

  • Bukankah ini contoh masalah greedy instantiation yang dibahas di bagian 5.1.1 paper Bidirectional Typing?
    “Dalam pengaturan awal, cukup disayangkan bahwa pendekatan rakus ini sensitif terhadap urutan argumen. Namun, ini bisa bekerja dengan baik dalam pengaturan polimorfisme rank tinggi predikatif tanpa bentuk subtyping lainnya. ‘tabby-first problem’ tidak bisa muncul, karena satu-satunya cara tipe bisa menjadi benar-benar lebih kecil adalah dengan menjadi benar-benar lebih polimorfik, dan jika argumen pertama bersifat polimorfik maka kita harus menginstansiasi 𝛼 dengan tipe polimorfik, yang melanggar predikativitas”