Type System
টাইপ সিস্টেম
Program-এর expression গুলোকে type ভাগ করে compile/run-এর আগেই কিছু ভুল অসম্ভব করে দেওয়ার formal ব্যবস্থা।
Judgment form: Γ ⊢ e : τ — environment Γ-তে expression e-র type τ।
- Soundness = progress + preservation: well-typed program আটকায় না, step করলেও well-typed থাকে
- Static/dynamic শুধু check-এর সময় না — expressiveness-এর সীমাও ভিন্ন (dynamic-এ tag check runtime-এ)
- Strong/weak: implicit conversion কতদূর —
int + boolaccept হয় কি? - Type system-এর শক্তিই দাম: dependent type-এ আরো জিনিস প্রমাণ হয়, inference/inference-failure কঠিন
- Practical payoff:
Option<T>null-check enforce করে — billion-dollar mistake-এর type-level সমাধান