Tập 87: Pattern completeness — Khi match biết vét cạn mọi góc tối

Trạng thái sự thật: Chưa xảy ra — Roadmap của Sprint 148.

Chúng tôi sẽ phải quay lại và nâng cấp mệnh đề match ở một cấp độ cao hơn. Ở V0, thuật toán kiểm tra tính vét cạn (exhaustiveness checking) chỉ hoạt động tốt với các hằng số phẳng và enum đơn giản. Đối với các cấu trúc phức tạp, như enum lồng nhau hoặc match kết hợp với các guard điều kiện (match val { Variant(x) if x > 0 => ... }), checker hiện tại vẫn phải defer một phần phân tích do độ phức tạp lũy thừa của không gian tìm kiếm.

Mục tiêu của Sprint 148 là hiện thực hóa một thuật toán phân tích ma trận pattern hoàn chỉnh dựa trên nghiên cứu của Luc Maranget. Compiler sẽ xây dựng một cây quyết định tĩnh để chứng minh không có bất kỳ tổ hợp dữ liệu nào bị bỏ sót.

Nếu người dùng viết một guard điều kiện, compiler buộc phải yêu cầu có một nhánh fallback không điều kiện đi kèm, bởi vì tính đúng đắn của guard không thể được chứng minh hoàn toàn ở compile-time. Lỗi cảnh báo hoặc từ chối biên dịch phải đi kèm với source-span chính xác của nhánh bị thiếu, giúp người lập trình sửa lỗi trong vài giây thay vì phải chạy chương trình để đợi crash bất ngờ lúc runtime. Đây là một bước tiến quan trọng để khóa chặt ranh giới an toàn cho luồng điều khiển của chương trình.

---