Mengapa tidak menggunakan tipe dependen

• Tipe dependen (type theory) mencakup objek bukti, tetapi penulis menilainya sebagai struktur yang tidak perlu dan tidak efisien
• Penulis pernah meneliti langsung sistem berbasis tipe dependen lama seperti AUTOMATH dan sistem formal Martin-Löf, tetapi Isabelle berkembang sebagai kerangka logika generik
• Isabelle/HOL yang berbasis pada teori tipe sederhana (higher-order logic) memiliki keunggulan dalam otomatisasi, pustaka skala besar, dan keterbacaan
• Melalui proyek ALEXANDRIA, telah dibuktikan bahwa bahkan hanya dengan logika orde tinggi pun formalisasi teorema matematika tingkat lanjut dimungkinkan
• Meski sistem tipe dependen seperti Lean makin matang, penulis tetap lebih memilih kepraktisan pendekatan logika orde tinggi karena masalah performa dan kompleksitas

---

Tipe dependen dan objek bukti

• Dalam teori tipe dependen, objek bukti (proof objects) bersifat esensial, tetapi penulis menganggapnya sebagai pemborosan ruang
  • Dalam arsitektur LCF, hanya langkah pembuktian yang sah yang dapat dijalankan melalui pemeriksaan tipe di level bahasa implementasi, bukan di dalam logika itu sendiri
  • Berkat wawasan Robin Milner, konsep proof kernel diperkenalkan dan menjadi fondasi Isabelle
• Menanggapi pertanyaan “mengapa tidak menggunakan tipe dependen”, penulis menjawab bahwa ia sudah lama menggunakannya

Pengalaman dengan AUTOMATH

• Pada 1977 di Caltech, penulis menghadiri kuliah N. G. de Bruijn tentang AUTOMATH, tetapi tidak sempat menggunakan sistemnya secara langsung
  • Saat itu sistem universitas Eindhoven tidak terhubung ke ARPAnet, dan diperlukan komputer berbasis ALGOL 60
• AUTOMATH adalah sistem tipe dependen, tetapi tidak mengimplementasikan korespondensi Curry–Howard
  • Pengguna harus menambahkan sendiri simbol dan aturan inferensi dari logika yang diinginkan sebagai aksioma
  • de Bruijn mengibaratkannya sebagai “restoran besar yang menyediakan semua makanan”
• Isabelle mewarisi gagasan ini dan mengejar keumuman sebagai kerangka logika
  • Namun, de Bruijn membenci teori himpunan dan memandang matematika pada dasarnya sebagai sesuatu yang berbasis tipe
• Penulis sempat mempertanyakan verifikasi keabsahan AUTOMATH, dan de Bruijn mengirimkan buku teori bahasa (300 halaman), tetapi itu tidak memuaskan

Teori tipe formal Martin-Löf

• Saat meneliti teori tipe formal Martin-Löf di Universitas Chalmers, Göteborg, penulis terpesona oleh kemungkinan sintesis program
  • Ia menilai pendekatan ini jelas “benar” karena langsung mengimplementasikan prinsip logika intuisionistik Heyting
• Selama beberapa tahun penelitian, penulis mengimplementasikan versi awal Isabelle dengan teori Martin-Löf
  • Hingga kini, itu masih disertakan dalam distribusi sebagai Isabelle/CTT
• Namun kemudian penelitian itu runtuh akibat suasana dogmatis yang berpusat pada Per Martin-Löf dan peralihan yang dipaksakan ke intensional equality intrinsik
• Sistem-sistem berikutnya seperti Calculus of Constructions(CoC), Rocq, dan Lean pun meninggalkan pertanyaan yang sama
  • CoC telah melalui berbagai varian dan aksioma opsional selama puluhan tahun

Pilihan riset dan arah Isabelle

• Para peneliti harus memilih antara mengembangkan sistem formal baru dan memperluas serta memanfaatkan sistem yang sudah ada
  • Isabelle dirancang sebagai kerangka yang digeneralisasi agar dapat menampung berbagai logika
• Pada 1985, Mike Gordon melakukan verifikasi perangkat keras dengan teori tipe sederhana Church
  • Setelah itu John Harrison merancang pengodean dimensi vektor
• Isabelle/HOL menambahkan kelas tipe aksiomatik dan sistem modul locale ke teori Church
• Komunitas Lean, berbasis CoC, berhasil mencapai formalisasi matematika berskala besar (mathlib)

Proyek ALEXANDRIA dan uji batas logika orde tinggi

• Proyek ALEXANDRIA yang didukung ERC menekankan otomatisasi, pustaka, dan keterbacaan Isabelle
• Pada awalnya diperkirakan logika orde tinggi akan menemui batas, tetapi dalam praktiknya matematika tingkat lanjut seperti skema Grothendieck pun berhasil diformalkan
  • Paulo Emílio de Vilhena dan Martin Baillon membuktikan bahwa setiap medan memiliki ekstensi tertutup aljabar
• Proyek ini meluas hingga hasil tingkat lanjut seperti teorema Balog–Szemerédi–Gowers
  • Klaim bahwa “formalisasi matematika mustahil tanpa tipe dependen” menghilang, dan yang tersisa hanya klaim bahwa “tipe dependen lebih rapi”

Lean dan pandangan saat ini tentang tipe dependen

• Skala komunitas Lean dan alat Blueprint memang membuat iri, tetapi masalah performa dan kompleksitas tetap ada
  • Benturan dengan intensional equality dan sulitnya menentukan kapan harus memakai tipe dependen terus dilaporkan berulang kali
• Penulis mengibaratkan tipe dependen seperti Full Self-Driving milik Tesla, untuk menunjukkan ekspektasi berlebihan dan ketidaknyamanan dalam praktik

Lampiran: batas teoretis logika orde tinggi

• Sebagian orang berpendapat bahwa logika orde tinggi lemah secara teori bukti, tetapi itu hanya berarti lebih lemah dibanding teori himpunan ZF
• Menurut hasil ALEXANDRIA, logika orde tinggi pun dapat menangani struktur matematika kompleks seperti skema Grothendieck
  • Hanya dua bukti yang memerlukan penambahan aksioma ZF, dan keduanya adalah teorema yang secara langsung menyebut objek ZF

Catatan kaki

• Intuisionisme adalah filsafat yang memandang bahasa sebagai sarana pencatatan semata, dan berbeda dari matematika konstruktif (constructive mathematics) masa kini

[GN⁺]

Komentar Hacker News

• Tipe dependen (dependent types) sangat berguna dalam situasi tertentu
  Misalnya, akan bagus jika Python bisa mengekspresikan tipe seperti “matriks float32 berukuran 10×5” dan melakukan pemeriksaan tipe terhadapnya
  Namun, konsep yang menyamakan bukti dan tipe seperti korespondensi Curry–Howard terasa membingungkan dari sudut pandang manusia
  Kesalahan tipe terasa seperti kekeliruan sederhana yang bisa diperbaiki, sedangkan kesalahan bukti adalah masalah yang jauh lebih rumit dan membutuhkan pemikiran
  Karena itu, menurut saya kekuatan nyata Lean bukan pada sistem tipenya, melainkan pada komunitas dan struktur open source mathlib
  Sementara AFP milik Isabelle dikelola seperti jurnal akademik, Lean aktif berkolaborasi berbasis pull request
  Saat ini saya sedang mengembangkan pembukti teorema baru Acorn(acornprover.org) dan ingin menggabungkan kelebihan Lean dan Isabelle
  Ekspresivitas tipe dependen Lean yang sederhana itu bagus, tetapi jika digunakan terlalu dalam akan sulit di-debug

  • Di C++ atau Rust, ekspresi tipe seperti ini juga dimungkinkan jika yang dipakai adalah array berukuran konstan
    Hanya saja, rentang indeks yang baru diketahui saat runtime tidak bisa dijamin pada waktu kompilasi
    Bahasa dengan tipe dependen sejati dapat mencegah error runtime di level tipe
  • Dengan const generics di Rust atau non-type template parameter di C++, ini juga sudah cukup memungkinkan
    Faktanya, bahkan dalam bahasa bertipe dependen pun, tipe dependen jarang dipakai untuk mencegah error runtime,
    dan lebih sering digunakan untuk invarian struktur data atau verifikasi setelah definisi program
    Referensi terkait: division-by-zero in type theory FAQ, materi presentasi Xavier Leroy
  • Di TypeScript juga bisa dibuat sedikit tiruan tipe dependen
    Misalnya, seperti baris ke-38 pada kode ini, ukuran matriks bisa diekspresikan sebagai tipe
    Saya juga mengimplementasikan definisi tipe vektor dan
    tipe hasil perkalian matriks
    Namun ini masih eksperimen di tingkat proyek pribadi, dan mungkin tidak cocok untuk proyek data berskala besar
  • Ungkapan “bukti itu sama dengan tipe” terdengar menarik
    Ini terkait dengan konsep Propositions as Types
    Saya penasaran bagaimana tipe dependen bekerja saat runtime, dan apakah pemeriksaan tipe saat kompilasi maupun runtime sama-sama diperlukan
    Ada juga pertanyaan apakah implementasinya akan menimbulkan kompleksitas karena semakin banyak referensi tidak langsung
  • Pernyataan “ingin mengekspresikan tipe matriks 10×5 di Python” pada akhirnya berarti bukankah itu bisa langsung didefinisikan sendiri sebagai kelas?

• Argumen Dr. Paulson bukan bahwa tipe dependen itu buruk, melainkan bahwa tipe dependen tidak wajib
  Rasanya akan lebih baik jika ada pembahasan lebih lanjut tentang masalah performa Lean atau soal intensional equality
  Seperti HEq milik Isabelle(tautan), kasus yang bukan definitional equality bisa menimbulkan masalah
  Karena itu saya berpikir lebih baik menggunakan tipe dependen sesedikit mungkin
  Bahkan sistem tanpa tipe statis seperti ACL2 pun tetap bisa melakukan verifikasi dengan baik
  Pada akhirnya yang penting adalah keseimbangan antara kepraktisan dan kemampuan verifikasi

  • Dari sudut pandang verifikasi perangkat lunak, Isabelle (non-dependen) juga sudah cukup kuat
    Lean dan Agda masih lebih jarang dipakai untuk verifikasi skala industri
    Menarik juga membandingkan Concrete Semantics(tautan) dan Logical Verification 2025(tautan)
    Secara realistis, refinement types mungkin lebih praktis
    Contoh: Rust Creusot, Dafny, dan contoh pembuktian leftpad di LiquidHaskell
  • Dalam matematika, bukti tidak digunakan sebagai program sehingga tipe dependen bekerja dengan baik
    Namun dalam verifikasi program, sering dibutuhkan lemma bantu yang rumit seperti “dua bukti ini identik”, dan ini sering kali tidak dapat dibuktikan
  • Saya penasaran mengapa “tipe dependen sebaiknya dipakai sesedikit mungkin”
  • Klaim “tidak diperlukan” terdengar seperti penghindaran
    Yang penting adalah seberapa bergunanya suatu fitur, bukan apakah ia wajib ada atau tidak
    Pada akhirnya, pemilihan alat adalah soal selera pengembang dan efisiensi

• Menarik bahwa banyak perdebatan dalam logika modern pada akhirnya bermuara pada preferensi estetika
  Jika manfaat nyatanya benar-benar sangat dominan, mungkin tidak akan ada perdebatan
  Sebagai referensi, makalah Paulson dan Lamport tahun 1999 “Typing in Specification Languages” layak dibaca
  Setelah itu, berkembang juga formalisme informal seperti TLA+ dari Lamport

  • Saya melihat ini bukan sekadar masalah estetika, melainkan masalah trade-off
    Kita memperoleh keuntungan berupa jaminan saat kompilasi, tetapi harus membayar harganya dalam bentuk kompleksitas dan waktu build yang lebih lama
    Pada akhirnya, inti persoalannya adalah “apakah pertukaran itu sepadan”

• Masalah HOL (teori tipe sederhana) bukan pada dependensinya, melainkan pada kurangnya kekuatan logis
  Ini setara dengan versi terbatas teori himpunan Zermelo, sehingga terlalu lemah untuk memformalkan matematika modern secara penuh
  Khususnya, sulit menangani persoalan ukuran di bidang seperti teori kategori (category theory)

  • Ada contoh formalisasi skema Grothendieck dengan memanfaatkan fitur locales di Isabelle
    Saya penasaran seberapa berbeda hal ini dari gaya kerja matematikawan sungguhan
  • Untuk meningkatkan kekuatan logis, kita juga bisa menambahkan aksioma
    Misalnya, menambahkan ‘inaccessible cardinal’ akan menjadi mirip dengan konsep ‘universe’ dalam teori tipe

• Saya dulu mengambil spesialisasi formal methods dan menganggap tipe dependen itu keren, tetapi dalam praktiknya penggunaannya selalu seperti perjuangan berat
  Saat memakai F#, saya pernah mencoba memperkenalkan F*, tetapi rekan-rekan merasa kurva belajar matematisnya terlalu membebani
  Pada akhirnya saya sampai pada kesimpulan sinis bahwa alat yang mengandung unsur matematika tidak dipelajari dengan baik oleh para engineer

  • F* lebih berfokus pada verifikasi perangkat lunak daripada matematika, jadi karakternya berbeda dari Lean
    Ia memungkinkan penggunaan ringan tipe dependen dengan memanfaatkan penyelesaian kendala berbasis SMT
    Namun, ini tidak menjawab pertanyaan filosofis seperti “apakah ini benar-benar tepat”
    Dunia pembuktian matematika dan verifikasi perangkat lunak memang cukup berbeda
  • Orang bukan tidak mau belajar hal baru, melainkan hanya menilai manfaatnya tidak sebanding dengan investasinya
    Pada akhirnya waktu itu terbatas

• Di perusahaan kami, Phosphor, kami sedang bereksperimen menggabungkan tipe dependen dengan kueri database/graf
  Kami bisa menutupi keterbatasan RDF dan membangun sistem kueri berbasis logika
  Dalam praktiknya kami memakai TypeDB(typedb.com), yang lebih cepat daripada MongoDB dan berguna untuk pemodelan data yang kompleks
  Ini juga mirip dengan konsep ontology milik Palantir

  • Saya penasaran apakah frasa “membangun growth engine non-dilutif” bisa dijelaskan dengan lebih konkret
  • Saya ingin tahu alasan memilih TypeDB dan angka performa yang nyata

• Pada akhirnya, rahasia tipe dependen tampaknya adalah mengetahui kapan sebaiknya tidak menggunakannya
  Daripada mengkritik Lean atau Rocq, saya jadi berpikir apakah dalam situasi tertentu pendekatan gaya Isabelle bisa lebih tepat

• Proyek formalisasi Alexandria(tautan) dari tim riset Paulson sangat mengesankan
  Khususnya, riset formalisasi algoritma komputasi kuantum(tautan makalah) sangat menarik

• Dulu saya percaya tipe dependen adalah masa depan, tetapi dalam proyek nyata penurunan produktivitasnya terlalu besar
  Sekarang saya lebih menyukai solusi yang jelas dan mudah dirawat
  Jika sebuah alat bisa dipahami dan dikembangkan oleh tim, maka itulah alat yang bagus

• Saya lebih menyukai sistem tipe yang berada di batas menuju tipe dependen, bukan tipe dependen penuh
  Misalnya, Purescript menyediakan row-type yang lebih kuat daripada Haskell secara bawaan,
  dan juga mendukung list level tipe, string, hingga regex
  Ini bisa dimanfaatkan sebagai gaya pemrograman logika berbasis typeclass