Bagaimana Membaca Notasi Sistem Tipe?

 (langdev.stackexchange.com)
1 poin oleh GN⁺ 2023-08-17 | 1 komentar | Bagikan ke WhatsApp
  • Meski notasi sistem tipe berbeda-beda tergantung referensinya, jika memahami kerangka umum berupa tata bahasa, relasi pengetikan, dan aturan inferensi, kita bisa mengikuti sebagian besar variasinya
  • Sistem tipe bekerja di atas sintaks abstrak suatu bahasa, jadi pertama-tama perlu membedakan term yang memiliki tipe dan tipe itu sendiri dalam tata bahasa
  • ⊢ e: τ adalah judgment pengetikan yang berarti “ekspresi e memiliki tipe τ”, dan dibaca sebagai aturan inferensi di mana jika semua syarat di atas garis horizontal benar, maka kesimpulan di bawahnya juga benar
  • Ketika variabel dan fungsi diperkenalkan, konteks ditambahkan seperti pada Γ ⊢ e: τ untuk melacak nama variabel dan tipenya dalam scope saat ini
  • Banyak aturan pengetikan bisa dibaca seperti fungsi pemeriksa tipe rekursif, tetapi tidak semua judgment logis langsung menjadi algoritme pemeriksaan tipe yang dapat diputuskan

Notasi sistem tipe yang dimulai dari tata bahasa

  • Sistem tipe adalah sistem sintaktis dari bahasa pemrograman, yaitu sekumpulan aturan yang bekerja pada sintaks abstrak bahasa tersebut
  • Penjelasan sistem tipe yang komprehensif biasanya terlebih dahulu menyajikan struktur sintaks yang dibahas sebagai tata bahasa, lalu menuliskannya dengan notasi BNF
  • Bahkan dalam bahasa tipe yang paling sederhana, sintaks umumnya dibagi menjadi dua kategori besar
    • e: ekspresi (expression) yang memiliki tipe
    • τ: tipe (type) yang melekat pada ekspresi
  • Bahasa contoh memiliki literal boolean, literal integer, ekspresi kondisional, operasi aritmetika, dan operasi perbandingan sebagai ekspresi, serta menggunakan Bool dan Int sebagai tipe
  • Simbol tipe bisa ditulis sebagai t, T, σ, atau huruf Yunani kecil lain selain τ tergantung referensinya, tetapi struktur keseluruhannya tetap mirip
  • Bahasa yang lebih kompleks dapat mencakup lebih banyak kategori sintaks, seperti pernyataan atau pola untuk pattern matching

Membaca relasi dan judgment pengetikan

  • Setelah menentukan tata bahasanya, biasanya didefinisikan relasi pengetikan dalam bentuk e : τ
    • 1 + 2 : Int berarti “1 + 2 bertipe Int”
    • 1 + 2 : Bool berarti ekspresi yang sama bertipe Bool, sehingga tidak benar
    • true + 2 : Int berarti ekspresinya sendiri tidak valid, sehingga tidak memiliki tipe apa pun
  • ⊢ e : τ adalah judgment pengetikan, dan ⊢ bisa dibaca sebagai “pernyataan di sebelah kanan benar”
  • Aturan tanpa apa pun di atas garis horizontal adalah aksioma (axiom) yang selalu benar
    • ⊢ true : Bool
    • ⊢ false : Bool
    • aturan literal integer seperti ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • Aturan yang memiliki bagian atas dan bawah garis adalah aturan inferensi
    • jika semua syarat di atas benar, maka kesimpulan di bawahnya benar
    • jika e₁ dan e₂ sama-sama Int, maka e₁ + e₂ adalah Int
    • jika e₁ dan e₂ sama-sama Int, maka e₁ < e₂ adalah Bool

Ekspresi kondisional dan variabel tipe

  • Dua cabang dari if ... then ... else ... boleh bertipe apa pun, tetapi keduanya harus memiliki tipe yang sama
    • if true then 1 else 2 valid
    • if true then false else true valid
    • if true then 1 else true tidak valid
  • Untuk menyatakan hal ini, aturan menggunakan variabel τ untuk merepresentasikan tipe cabang
    • ekspresi kondisi e₁ harus bertipe Bool
    • cabang then e₂ dan cabang else e₃ harus memiliki tipe τ yang sama
    • tipe seluruh ekspresi kondisional juga menjadi τ
  • Saat menerapkan aturan, tipe apa pun boleh dipilih sebagai τ, tetapi pilihan itu harus dipertahankan secara konsisten dalam aturan yang sama

Membaca aturan inferensi seperti algoritme

  • Notasi ini berasal dari logika formal, dan cara spesifikasi sistem tipe sangat mirip dengan deduksi natural
  • Aturan-aturan seperti ini dipakai untuk menyusun bukti formal tentang sifat sistem, dan penting untuk membuktikan properti seperti type safety
  • Judgment logis tidak selalu langsung berkorespondensi dengan algoritme pemeriksaan tipe yang dapat diputuskan
  • Dalam banyak kasus, ⊢ e : τ dapat dibaca seperti fungsi yang menghasilkan tipe τ dari ekspresi e
    • biasanya ada satu aturan untuk setiap bentuk ekspresi dalam tata bahasa
    • setiap aturan pengetikan dapat dipandang sebagai satu cabang dari fungsi pemeriksa tipe rekursif
  • Fungsi infer pada contoh berkorespondensi dengan alur berikut
    • true atau false menghasilkan Bool
    • literal integer menghasilkan Int
    • e₁ + e₂ memeriksa apakah hasil inferensi kedua sisi sama-sama Int, lalu menghasilkan Int
    • e₁ < e₂ memeriksa apakah kedua sisi sama-sama Int, lalu menghasilkan Bool
    • if e₁ then e₂ else e₃ memeriksa apakah kondisinya Bool, lalu memeriksa apakah tipe dua cabangnya sama, dan mengembalikan tipe tersebut
  • Meski tidak selalu bisa langsung diterjemahkan menjadi algoritme, memahami judgment dengan e sebagai input dan τ sebagai output memudahkan kita mengikuti aliran informasinya

Variabel dan konteks

  • Untuk menangani bahasa pemrograman yang berguna, kita memerlukan variabel, dan contoh diperluas dengan menambahkan fungsi hingga berbentuk simply typed lambda calculus
  • Tata bahasa yang diperluas mencakup hal-hal berikut
    • variabel x
    • abstraksi fungsi λx:τ. e
    • penerapan fungsi e e
    • tipe fungsi τ → τ
  • λx:τ. e berkorespondensi dengan (x:τ) => e di TypeScript, dan f x berkorespondensi dengan f(x)
  • Karena tipe variabel bergantung pada konteks tempat variabel itu muncul, aturan tidak bisa ditulis hanya dalam bentuk sederhana ⊢ x : ???
  • Karena itu, judgment pengetikan diperluas menjadi Γ ⊢ e : τ
    • Γ adalah konteks atau lingkungan tipe
    • ⊢ memisahkan asumsi kontekstual di kiri dan pernyataan yang harus dibuktikan di kanan
    • dibaca sebagai “di bawah konteks Γ, ekspresi e memiliki tipe τ”
  • Secara algoritmis, Γ bisa dipandang sebagai input tambahan dalam bentuk Map<Variable, Type>
  • Secara formal, konteks juga dinyatakan sebagai struktur sintaks
    • ∅: konteks kosong
    • Γ, x:τ: konteks yang ditambah binding variabel
    • kadang • dipakai sebagai konteks kosong sebagai ganti ∅
  • Dalam representasi ini, konteks lebih dekat ke association list yang memetakan nama variabel ke tipe

Peran konteks di dalam aturan

  • Banyak aturan pengetikan tidak mengubah konteks dan hanya meneruskannya apa adanya
    • Γ ⊢ true : Bool
    • jika Γ ⊢ e₁ : Int dan Γ ⊢ e₂ : Int, maka Γ ⊢ e₁ + e₂ : Int
  • Dalam aturan penggunaan variabel dan ekspresi lambda, konteks memegang peran utama
    • jika x:τ ∈ Γ, maka Γ ⊢ x : τ
    • jika Γ, x:τ₁ ⊢ e : τ₂, maka Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Saat memeriksa tipe isi lambda e, konteks diperluas dengan binding baru x:τ₁
  • Aturan variabel menyimpulkan bahwa jika binding variabel ada dalam konteks saat ini, maka variabel itu memiliki tipe tersebut
  • Konteks dipakai sebagai mekanisme komunikasi yang menyampaikan informasi antara aturan lambda dan aturan variabel
  • Demi penyederhanaan, spesifikasi sistem tipe seperti ini biasanya mengasumsikan bahwa semua variabel sudah diresolusikan dan dibuat unik, sehingga variable shadowing tidak dibahas
  • Aturan penerapan fungsi memeriksa tipe ekspresi fungsi dan argumen sekaligus
    • e₁ harus bertipe τ₁ → τ₂
    • e₂ harus bertipe τ₁
    • tipe dari keseluruhan penerapan e₁ e₂ adalah τ₂

Notasi tambahan yang sering muncul

  • Aturan inferensi tidak selalu ditulis secara vertikal saja
    • beberapa syarat bisa diletakkan berdampingan secara horizontal
    • tata letak vertikal dan horizontal bisa dicampur dalam aturan yang sama
  • Syarat di atas garis biasanya berupa judgment lain, tetapi bisa juga berupa side condition berupa kondisi boolean sembarang
    • contohya adalah x:τ ∈ Γ pada aturan variabel
    • dalam sistem tipe algoritmis, α fresh bisa muncul, yang berarti α harus merupakan variabel tipe baru yang berbeda dari variabel tipe lain

Subtyping

  • Subtyping adalah relasi yang menangani kecocokan antar tipe dengan cara yang lebih longgar daripada kesetaraan ketat, dan harus didefinisikan secara eksplisit
  • Biasanya ditulis sebagai τ₁ <: τ₂ dan dibaca “τ₁ adalah subtype dari τ₂”
  • Relasi subtyping sederhana dapat memperkenalkan top type ⊤ dan bottom type ⊥
    • τ <: τ: setiap tipe adalah subtype dari dirinya sendiri
    • τ <: ⊤: setiap tipe adalah subtype dari ⊤
    • ⊥ <: τ: ⊥ adalah subtype dari setiap tipe
  • Aturan pertama adalah aturan refleksif, dan sering disingkat sebagai refl
  • Untuk mengizinkan subtyping, setiap aturan pengetikan yang mendukungnya harus secara eksplisit menggunakan relasi tersebut
    • pada aturan penerapan fungsi, penerapan bisa diizinkan jika tipe argumen τ₁ adalah subtype dari tipe parameter τ₂

Banyak konteks dan pemeriksaan tipe dua arah

  • Beberapa sistem tipe mendefinisikan judgment pengetikan yang melibatkan satu atau lebih konteks
    • konteks kedua biasanya disebut Δ
    • Γ;Δ ⊢ e : τ sering dipakai ketika kedua konteks berfungsi sebagai input
    • Γ ⊢ e : τ ⊣ Δ sering dipakai ketika Δ berfungsi sebagai output
  • Konteks kedua digunakan dengan cara yang berbeda-beda tergantung tujuannya
    • ia bisa dipakai untuk membatasi agar variabel tertentu hanya dapat dirujuk di dalam ekspresi tertentu
    • dalam bahasa pemrograman yang sadar sumber daya, ia bisa dipakai sebagai konteks keluaran untuk melacak variabel mana yang sudah dikonsumsi
  • Pemeriksaan tipe dua arah adalah pendekatan untuk melakukan inferensi tipe non-lokal yang terbatas tanpa constraint solver
  • Sistem dua arah membagi judgment umum Γ ⊢ e : τ menjadi dua judgment khusus
    • Γ ⊢ e ⇐ τ: judgment checking yang memeriksa apakah ekspresi e memiliki tipe yang diharapkan τ; secara algoritmis τ adalah input
    • Γ ⊢ e ⇒ τ: judgment inference yang dipakai ketika tidak ada informasi tipe yang diharapkan; secara algoritmis τ adalah output
  • Kedua judgment itu didefinisikan secara rekursif timbal balik untuk mengalirkan informasi tipe ke dua arah
  • Dalam pendekatan ini, beberapa anotasi tipe dapat dihilangkan, dan aturan pemeriksaan untuk abstraksi lambda bisa memperoleh tipe parameter dari tipe fungsi yang diharapkan, sehingga anotasi pada binder variabel dapat dihilangkan

Bacaan terkait

1 komentar

 
GN⁺ 2023-08-17
Komentar Hacker News

  • Guy Steele pernah memberikan presentasi tentang topik ini. Ia juga memberi nama yang bisa dicari untuk beberapa notasi, misalnya diagram aturan inferensi dua dimensi
    Ia menyebutnya metanotasi ilmu komputer, tetapi secara pribadi ini tampak lebih dekat ke teori bahasa pemrograman. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Notasi ini dapat ditelusuri sampai ke Frege. Sulit dicari kalau tidak tahu apa yang harus dicari, tetapi tulisan ini tampaknya rangkuman yang cukup bagus: https://plato.stanford.edu/entries/frege-logic
    Simbol turnstile |- sudah digunakan, dan garis horizontal yang di kelas disebut “Fregescher Schlussstrich”, yakni garis kesimpulan Frege, tampaknya awalnya merupakan bagian dari turnstile itu sendiri lalu menjadi elemen terpisah dalam notasi modern

    • “Schlussstrich” mungkin lebih tepat diterjemahkan sebagai garis deduksi atau garis inferensi

  • Types and Programming Languages karya Benjamin C. Pierce adalah buku teks yang bagus untuk membahas hal-hal seperti ini

    • Ironisnya, TAPL sendiri cukup tidak jelas dalam menjelaskan makna dasar sintaks yang dipakainya. Jawaban ini beberapa orde besaran lebih jelas daripada TAPL

  • Meski saya lulusan ilmu komputer, saya masih bingung dengan perbedaan makna |– dan |=, serta pada tingkat metasintaks mana masing-masing variabel yang dipakai berada
    Ironisnya, salah satu penyebabnya adalah notasi itu sendiri tidak memiliki tipe eksplisit

  • Untuk yang masih ragu membacanya: tulisan ini menjelaskan notasi sistem tipe yang muncul di makalah ilmu komputer, dan pada dasarnya merupakan pengantar ke notasi BNF, aturan inferensi, dan semacamnya untuk sistem tipe
    Tampaknya rangkuman yang bagus

    • Sejujurnya, yang saya butuhkan hanya cheatsheet yang memberi tahu bagaimana membaca simbol-simbol itu sebagai kata-kata bahasa Inggris
      Saya memahami konsep logis dari penerapan tipe, tetapi karena tidak sering membaca makalah ilmu komputer, pemetaan antara simbol dan maknanya tidak mudah melekat di kepala
    • Fakta bahwa hal seperti ini telah diabstraksikan secara menyeluruh selama bertahun-tahun menunjukkan sisi yang sangat khas ilmu komputer

  • Dalam salah satu contoh, 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 berarti “𝗍𝗋𝗎𝖾+2 bertipe 𝖨𝗇𝗍”, tetapi disebut makin aneh karena ekspresi 𝗍𝗋𝗎𝖾+2 itu sendiri tidak masuk akal dan tidak punya tipe
    Namun di Python, True + 2 benar-benar merupakan integer dan nilainya 3. Terlepas dari apakah memang seharusnya begitu, faktanya memang demikian

    • Jika Anda merasa True + 2 masuk akal, Anda bisa mendefinisikan sendiri aturan penilaian yang mengizinkannya
      Logika dan teori sistem tipe tidak peduli aksioma dan aturan inferensi apa yang Anda gunakan; keduanya hanya memungkinkan Anda menalar aturan-aturan itu dan interaksinya. Misalnya, Anda bisa menetapkan |- True : Bool, |- True : Int, atau jika ingin mengizinkannya hanya pada ekspresi tertentu, Anda bisa membuat aturan yang menarik |- True + x: Int dari |- x : Int
    • Bukankah ini berbeda-beda tergantung bahasanya? Misalnya di C, true dipetakan ke 1, jadi true+1=2
    • Meskipun True + 2 tidak menghasilkan error di Python atau C, itu tetap konyol karena demi memberi sedikit syntactic sugar kepada programmer, semantik bahasa dibuat lebih sulit untuk dinalar

  • Bagus. Selama beberapa tahun saya penasaran soal ini, tetapi tidak tahu harus memakai kata kunci apa untuk mencari tahu lebih lanjut

  • Kadang rasanya agak kesal ketika ada orang yang membagikan pengetahuan esoterik yang dulu susah payah dipelajari, secara gratis ;) Saya benar-benar berharap tulisan seperti ini sudah ada saat saya mempelajarinya. Semoga aksesibilitas yang lebih tinggi membuat bahasa yang berantakan jadi lebih sedikit

  • Saat membaca Ada Reference Manual, saya langsung mengenali jenis sintaks seperti ini. Saya tidak tahu namanya, tetapi menarik melihatnya dalam kasus penggunaan nyata, dan seluruh bahasa didefinisikan dengan notasi seperti itu
    Contoh: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Sepertinya ini tempat yang bagus untuk mengkhotbahkan satu pendirian yang akan saya pertahankan sampai akhir. Dalam format anotasi tipe yang memakai titik dua, spasi di kedua sisi titik dua harus sama
    Bagi saya, kebetulan ada dua simbol berbeda yang bentuknya sama, yaitu dua titik. Yang satu adalah titik dua label, seperti dalam bahasa Inggris, ketika bagian depan memperkenalkan bagian belakang atau sisi kiri menjadi label bagi sisi kanan; awal blok di Python, pasangan kunci-nilai, serta pasangan nama-nilai struct di C atau Rust termasuk di sini
    Yang satu lagi adalah anotasi tipe yang dipinjam dari matematika. Ini adalah relasi biner, dan relasi biner memberi spasi yang sama di kiri dan kanan. Sama seperti kita tidak menulis x= 1, x> y, atau x+ z, terasa lebih alami menulis x : X, bukan x: X
    Saat melihat a: b, saya langsung membacanya sebagai titik dua label, dan jika itu anotasi tipe, setiap kali diperlukan transformasi mental tambahan yang sangat kecil. Ini soal sintaks bahasa pemrograman, dan secara pribadi saya jauh lebih menyukai x : X daripada X x
    [1] “Evangelion” adalah kata keren yang berasal dari εὐαγγέλιον, yang berarti kabar baik. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Ada beberapa hal yang mungkin disalahpahami. Dalam penulisan matematika pun notasi seperti f: X->Y, dengan spasi lebih banyak di kanan titik dua, memang muncul; dari 3 buku yang saya periksa, 1 buku hanya memakai notasi itu
      Selain itu, itu juga masih dekat dengan pelabelan, yaitu melabeli suatu bentuk pemetaan tertentu. Kasus ketika titik dua benar-benar dipakai dengan makna berbeda dalam matematika adalah saat digunakan sebagai singkatan dari such that; misalnya dalam definisi himpunan seperti { x : x \in IN and x | 2} atau sering bersama kuantor
    • Sudut pandang yang menarik. Soal langkah mental tambahan itu sama seperti yang saya rasakan saat membaca notasi umum X x. x: X terasa jauh lebih alami bagi saya, dan juga terasa dekat dengan cara titik dua dipakai dalam bahasa alami
      Ada suatu proposisi, lalu bagian setelah titik dua menjelaskan proposisi itu lebih rinci; ini pas juga karena tipe adalah informasi tambahan tentang sesuatu yang ada di sebelah kiri
    • Dalam teori tipe, saya rasa praktik standarnya biasanya memberi spasi yang sama di kedua sisi titik dua, seperti t[spasi]:[spasi]T
      Teori tipe secara keseluruhan memang punya sisi yang berantakan dan tidak konsisten, tetapi untuk kasus ini justru termasuk contoh langka ketika semuanya cukup konsisten. Saya penasaran bagaimana saya menulisnya saat S1, lalu saya cek, dan ternyata saya juga menuliskannya secara simetris dengan rapi: https://dvt.name/logic/horse2.pdf
    • x: X cocok dengan penggunaan “penjelasan muncul setelah titik dua”
      Jadi bentuknya seperti variable x: It’s an X.
    • age: int dapat dengan mudah dibaca ulang dalam bahasa Inggris sebagai “person’s age: an integer”
      Karena itu, titik dua tidak pernah terlalu mengganggu saya