Subtipe Semantik di Luau

Luau adalah bahasa pemrograman pertama yang memberikan kekuatan subtipe semantik ke tangan jutaan kreator.

Meminalkan hasil positif palsu

Salah satu masalah dalam pelaporan kesalahan tipe pada alat seperti widget Analisis Skrip di Roblox Studio adalah hasil positif palsu. Ini adalah peringatan yang merupakan artefak dari analisis, dan tidak sesuai dengan kesalahan yang dapat terjadi saat runtime. Misalnya, program

local x = CFrame.new()
local y
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z = x * y

melaporkan kesalahan tipe yang tidak mungkin terjadi saat runtime, karena CFrame mendukung perkalian dengan baik Vector3 maupun CFrame. (Tipe-nya adalah ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3).)

False positives sangat merugikan saat onboarding pengguna baru. Jika seorang pembuat yang ingin tahu tentang tipe mengaktifkan pengecekan tipe dan langsung dihadapkan pada dinding garis merah palsu, ada dorongan kuat untuk segera mematikannya kembali.

Ketidakakuratan dalam kesalahan tipe tidak dapat dihindari, karena tidak mungkin menentukan sebelumnya apakah kesalahan runtime akan terpicu. Desainer sistem tipe harus memilih antara menerima false positives atau false negatives. Di Luau, hal ini ditentukan oleh mode: mode strict cenderung menghasilkan false positives, sedangkan mode nonstrict cenderung menghasilkan false negatives.

Meskipun ketidakakuratan tidak dapat dihindari, kami berusaha menghilangkannya sebisa mungkin, karena hal ini menyebabkan kesalahan yang tidak relevan, serta ketidakakuratan dalam alat berbasis tipe seperti autocomplete atau dokumentasi API.

Subtyping sebagai sumber false positive

Salah satu sumber false positive di Luau (dan banyak bahasa serupa lainnya seperti TypeScript atau Flow) adalah subtyping. Subtyping digunakan setiap kali variabel diinisialisasi atau diberi nilai, dan setiap kali fungsi dipanggil: sistem tipe memeriksa apakah tipe ekspresi merupakan subtype dari tipe variabel. Misalnya, jika kita menambahkan tipe ke program di atas

local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z : Vector3 | CFrame = x * y

maka sistem tipe akan memeriksa apakah tipe dari CFrame multiplication merupakan subtipe dari (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame).

Subtyping adalah fitur yang sangat berguna, dan mendukung konstruksi tipe yang kaya seperti union tipe (T | U) dan intersection tipe (T & U). Misalnya, number? diimplementasikan sebagai tipe union (number | nil), yang dihuni oleh nilai-nilai yang berupa angka atau nil.

Sayangnya, interaksi antara subtyping dengan tipe persimpangan dan gabungan dapat menghasilkan hasil yang aneh. Sebuah kasus sederhana (namun agak artifisial) dalam versi Luau yang lebih lama adalah:

local x : (number?) & (string?) = nil
local y : nil = nil
y = x -- Type '(number?) & (string?)' could not be converted into 'nil'
x = y

Kesalahan ini disebabkan oleh kegagalan subtyping; algoritma subtyping lama melaporkan bahwa `(number?) & (string?)` bukan subtype dari `nil`. Ini adalah false positive, karena `number & string` tidak memiliki nilai, sehingga satu-satunya nilai yang mungkin untuk `(number?) & (string?)` adalah `nil`.

Ini adalah contoh buatan, tetapi ada masalah nyata yang diangkat oleh para pengembang akibat masalah ini, misalnya https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5. Saat ini, masalah ini sebagian besar memengaruhi pembuat yang memanfaatkan fitur sistem tipe yang canggih, tetapi seiring dengan semakin akuratnya inferensi tipe, tipe persatuan dan persimpangan akan menjadi lebih umum, bahkan dalam kode tanpa anotasi tipe.

Kelas false positive ini tidak lagi terjadi di Luau, karena kami telah beralih dari pendekatan lama kami tentang subtyping sintaksis ke alternatif yang disebut subtyping semantik.

Subtyping sintaksis

AKA “apa yang kami lakukan sebelumnya.”

Subtipe sintaksis adalah algoritma rekursif yang diarahkan oleh sintaksis. Kasus-kasus menarik yang perlu ditangani terkait tipe persimpangan dan persatuan adalah:

• Refleksivitas: T adalah subtipe dari T
• Persimpangan L: (T₁ & … & Tⱼ) adalah subtipe dari U setiap kali beberapa dari Tᵢ adalah subtipe dari U
• Gabungan L: (T₁ | … | Tⱼ) adalah subtipe dari U jika semua Tᵢ adalah subtipe dari U
• Persimpangan R: T adalah subtipe dari (U₁ & … & Uⱼ) jika T adalah subtipe dari semua Uᵢ
• Union R: T adalah subtipe dari (U₁ | … | Uⱼ) setiap kali T adalah subtipe dari beberapa Uᵢ.

Misalnya:

• Berdasarkan Reflexivity: nil adalah subtipe dari nil
• sehingga berdasarkan Union R: nil adalah subtipe dari number?
• dan: nil adalah subtipe dari string?
• jadi berdasarkan Intersection R: nil adalah subtipe dari (number?) & (string?).

Yay! Sayangnya, berdasarkan aturan-aturan ini:

• number bukanlah subtipe dari nil
• jadi berdasarkan Union L: (number?) bukan subjenis dari nil
• dan: string bukan subjenis dari nil
• jadi menurut Gabungan L: (string?) bukanlah subtipe dari nil
• jadi berdasarkan Intersection L: (number?) & (string?) bukanlah subtipe dari nil.

Ini adalah hal yang umum dalam subtipe sintaksis: ketika menghasilkan hasil “ya”, itu benar, tetapi ketika menghasilkan hasil “tidak”, itu mungkin salah. Algoritma ini merupakan perkiraan konservatif, dan karena hasil “tidak” dapat menyebabkan kesalahan tipe, ini menjadi sumber hasil positif palsu.

Subtipe semantik

AKA “apa yang kita lakukan sekarang.”

Daripada menganggap subtipe sebagai sesuatu yang diarahkan oleh sintaksis, kita pertama-tama mempertimbangkan semantiknya, dan kemudian kembali ke bagaimana semantik tersebut diimplementasikan. Untuk ini, kita mengadopsi subtipe semantik:

• Semantik dari suatu tipe adalah sekumpulan nilai.
• Tipe persimpangan dianggap sebagai persimpangan himpunan.
• Tipe gabungan dipandang sebagai gabungan himpunan.
• Subtyping dipandang sebagai inklusi himpunan.

Contoh:

dan karena subtipe diartikan sebagai inklusi himpunan:

Jadi, menurut subtipe semantik, (number?) & (string?) setara dengan nil, tetapi subtipe sintaksis hanya mendukung satu arah.

Semua ini baik-baik saja, tetapi jika kita ingin menggunakan subtipe semantik dalam alat, kita memerlukan algoritma, dan ternyata memeriksa subtipe semantik bukanlah hal yang mudah.

Subtyping semantik itu sulit

NP-sulit untuk lebih tepatnya.

Kita dapat mereduksi pewarnaan graf ke subtyping semantik dengan mengkodekan graf sebagai tipe Luau sedemikian rupa sehingga memeriksa subtyping pada tipe memiliki hasil yang sama dengan memeriksa ketidakmungkinan pewarnaan graf

Misalnya, mewarnai grafik tiga simpul dengan dua warna dapat dilakukan menggunakan tipe:

type Red = "red"
type Blue = "blue"
type Color = Red | Blue
type Coloring = (Color) -> (Color) -> (Color) -> boolean
type Uncolorable = (Color) -> (Color) -> (Color) -> false

Kemudian, sebuah graf dapat dikodekan sebagai tipe fungsi overload dengan subUncolorable dan superColoring sebagai fungsi overload yang mengembalikan false ketika suatu batasan dilanggar. Setiap overload mengkodekan satu batasan. Misalnya, sebuah garis memiliki batasan yang menyatakan bahwa simpul yang berdekatan tidak boleh memiliki warna yang sama:

type Line = Coloring
  & ((Red) -> (Red) -> (Color) -> false)
  & ((Blue) -> (Blue) -> (Color) -> false)
  & ((Color) -> (Red) -> (Red) -> false)
  & ((Color) -> (Blue) -> (Blue) -> false)

Segitiga serupa, tetapi titik ujungnya juga tidak boleh memiliki warna yang sama:

type Triangle = Line
  & ((Red) -> (Color) -> (Red) -> false)
  & ((Blue) -> (Color) -> (Blue) -> false)

Sekarang, `Triangle` adalah subtipe dari `Uncolorable`, tetapi `Line` bukan, karena garis dapat memiliki dua warna. Hal ini dapat digeneralisasikan ke grafik berhingga apa pun dengan jumlah warna berhingga, sehingga pengecekan subtipe adalah NP-hard.

Kami menangani hal ini dengan dua cara:

• kami menyimpan tipe dalam cache untuk mengurangi penggunaan memori, dan
• menyerah dengan kesalahan “Code Too Complex” jika cache tipe menjadi terlalu besar.

Semoga hal ini tidak sering terjadi dalam praktiknya. Ada bukti kuat bahwa masalah seperti ini tidak muncul dalam praktiknya berdasarkan pengalaman dengan sistem tipe seperti Standard ML, yang EXPTIME-complete, tetapi dalam praktiknya Anda harus berusaha keras untuk membuat kode pita Mesin Turing sebagai tipe.

Normalisasi tipe

Algoritma yang digunakan untuk menentukan subtipe semantik adalah normalisasi tipe. Alih-alih dipandu oleh sintaksis, kami terlebih dahulu menulis ulang tipe agar dinormalisasi, kemudian memeriksa subtipe pada tipe yang telah dinormalisasi.

Tipe yang dinormalisasi adalah gabungan dari:

• tipe nil yang dinormalisasi (never atau nil)
• tipe bilangan yang dinormalisasi (never atau number)
• tipe boolean yang dinormalisasi (baik never atau true atau false atau boolean)
• tipe fungsi yang dinormalisasi (baik never atau irisan dari tipe-tipe fungsi) dst

Setelah tipe dinormalisasi, memeriksa subtyping semantik menjadi mudah.

Setiap tipe dapat dinormalisasi (sayangnya, dengan beberapa batasan teknis seputar paket tipe generik). Langkah-langkah pentingnya adalah:

• menghapus persimpangan primitif yang tidak cocok, misalnya number & bool diganti dengan never, dan
• menghapus gabungan fungsi, misalnya ((number?) -> number) | ((string?) -> string) diganti dengan (nil) -> (number | string).

Misalnya, menormalisasi (number?) & (string?) akan menghapus number & string, sehingga yang tersisa hanyalah nil.

Upaya pertama kami dalam menerapkan normalisasi tipe menerapkannya secara bebas, tetapi hal ini mengakibatkan kinerja yang sangat buruk (kode kompleks berubah dari pemeriksaan tipe yang memakan waktu kurang dari satu menit menjadi harus dijalankan semalaman). Alasan di balik hal ini sangat sederhana: terdapat optimasi dalam algoritma subtyping Luau untuk menangani refleksivitas (T adalah subtipe dari T) yang melakukan pemeriksaan kesetaraan pointer yang murah. Normalisasi tipe dapat mengubah tipe yang identik secara pointer menjadi tipe yang setara secara semantik (tetapi tidak identik secara pointer), yang secara signifikan menurunkan kinerja.

Karena masalah kinerja ini, kami masih menggunakan subtipe sintaksis sebagai pemeriksaan pertama untuk subtipe, dan hanya melakukan normalisasi tipe jika algoritma sintaksis gagal. Hal ini tepat, karena subtipe sintaksis merupakan perkiraan konservatif terhadap subtipe semantik.

Subtyping semantik pragmatis

Subtyping semantik yang tersedia secara umum sedikit berbeda dari yang diimplementasikan di Luau, karena memerlukan model yang bersifat teori himpunan, yang mensyaratkan bahwa penghuni tipe fungsi “berperilaku seperti fungsi.” Ada dua alasan mengapa kami menghilangkan persyaratan ini.

Pertama, kami menormalisasi tipe fungsi menjadi irisan fungsi, misalnya kumpulan yang sangat berantakan dari gabungan dan irisan fungsi:

((number?) -> number?) | (((number) -> number) & ((string?) -> string?))

dinormalisasi menjadi fungsi yang di-overload:

((number) -> number?) & ((nil) -> (number | string)?)

Subtyping semantik teori himpunan tidak mendukung normalisasi ini, dan sebaliknya menormalisasi fungsi ke bentuk normal disjungtif (gabungan dari irisan fungsi). Kami tidak melakukan ini karena alasan ergonomis: fungsi yang di-overload adalah idiomatik di Luau, tetapi DNF tidak, dan kami tidak ingin menyajikan tipe yang tidak idiomatik kepada pengguna.

Normalisasi kami bergantung pada penulisan ulang gabungan tipe fungsi:

((A) -> B) | ((C) -> D)   →   (A & C) -> (B | D)

Normalisasi ini valid dalam model kami, tetapi tidak dalam model teori himpunan.

Kedua, di Luau, tipe dari aplikasi fungsi f(x) adalah B jika f memiliki tipe (A) -> B dan x memiliki tipe A. Secara tak terduga, hal ini tidak selalu benar dalam model teori himpunan, karena adanya tipe yang tidak terpakai. Dalam model teori himpunan, jika x memiliki tipe never, maka f(x) memiliki tipe never. Kami tidak ingin membebani pengguna dengan gagasan bahwa penerapan fungsi memiliki kasus khusus, terutama karena kasus khusus tersebut hanya dapat muncul dalam kode mati.

Dalam model teori himpunan, (never) -> A adalah subtipe dari (never) -> B, terlepas dari apa pun nilai A dan B. Hal ini tidak berlaku di Luau.

Karena dua alasan ini (yang lebih berkaitan dengan ergonomi daripada hal teknis), kami mengabaikan persyaratan teori himpunan dan menggunakan subtipe semantik pragmatis.

Tipe negasi

Perbedaan lain antara sistem tipe Luau dan subtipe semantik yang tersedia di pasaran adalah bahwa Luau tidak mendukung semua tipe negasi.

Kasus umum yang membutuhkan tipe negasi adalah dalam pemeriksaan tipe kondisional:

-- initially x has type T
if type(x) == "string" then
  --  in this branch x has type T & string
else
  -- in this branch x has type T & ~string
end

Ini menggunakan tipe negasi ~string yang dihuni oleh nilai-nilai yang bukan string.

Di Luau, kami hanya mengizinkan penyempurnaan pengetikan semacam ini pada tipe uji seperti string, function, Part, dan seterusnya, dan bukan pada tipe struktural seperti (A) -> B, yang menghindari kasus umum tipe negasi umum.

Prototipe dan verifikasi

Selama perancangan algoritma subtyping semantik Luau, terjadi perubahan (misalnya, awalnya kami mengira akan dapat menggunakan subtyping teori himpunan). Selama masa perubahan yang cepat ini, penting untuk dapat beriterasi dengan cepat, sehingga kami awalnya mengimplementasikan prototipe daripada langsung melompat ke implementasi produksi.

Memvalidasi prototipe sangat penting, karena algoritma subtyping dapat memiliki kasus tepi yang tidak terduga. Karena alasan ini, kami mengadopsi Agda sebagai bahasa prototipe. Selain mendukung pengujian unit, Agda juga mendukung verifikasi mekanis, sehingga kami yakin dengan desainnya.

Prototipe ini tidak mengimplementasikan seluruh Luau, hanya subset fungsionalnya, tetapi ini cukup untuk menemukan interaksi fitur yang halus yang kemungkinan besar akan muncul sebagai bug yang sulit diperbaiki di produksi.

Pembuatan prototipe tidaklah sempurna, misalnya masalah utama yang kami temui dalam produksi adalah tentang kinerja dan pustaka standar C++, yang tidak akan pernah terdeteksi oleh prototipe. Namun, implementasi produksi secara umum cukup mudah (atau setidaknya semudah yang bisa dilakukan oleh perubahan 3kLOC).

Langkah selanjutnya

Subtyping semantik telah menghilangkan satu sumber false positive, tetapi masih ada yang lain yang harus dilacak:

• Aplikasi fungsi dan operator yang di-overload
• Akses properti pada ekspresi tipe kompleks
• Properti read-only pada tabel
• Variabel yang berubah tipenya seiring waktu (alias typestates)

Upaya untuk menghilangkan garis merah yang tidak perlu terus berlanjut!

Ucapan Terima Kasih

Terima kasih kepada Giuseppe Castagna dan Ben Greenman atas komentar bermanfaat mereka pada draf posting ini.

Alan mengoordinasikan desain dan implementasi sistem tipe Luau, yang membantu mendorong banyak fitur pengembangan di Roblox Studio. Dr. Jeffrey memiliki pengalaman lebih dari 30 tahun dalam penelitian bahasa pemrograman, telah menjadi anggota aktif dari berbagai proyek perangkat lunak sumber terbuka, dan memegang gelar DPhil dari Universitas Oxford, Inggris.