Các loại không thể chấp nhận trong lý thuyết loại: Tìm hiểu các thuộc tính và ràng buộc không thể quyết định

Trong ngữ cảnh của lý thuyết loại, loại không thể cấp được là loại không thể được suy ra hoặc xây dựng bằng cách sử dụng các hàm tạo và ràng buộc loại có sẵn.

Ví dụ: trong phép tính lambda được gõ đơn giản chỉ có các loại cơ bản `Nat` (số tự nhiên) và ` Prop` (mệnh đề), không thể suy ra loại `Nat x Prop` vì không có cách nào để kết hợp hai loại bằng cách sử dụng các hàm tạo kiểu có sẵn. Loại này được cho là không thể cấp được.

Trong các hệ thống loại tiên tiến hơn, chẳng hạn như lý thuyết loại phụ thuộc hoặc lý thuyết loại đồng luân, các loại không thể cấp phép có thể phát sinh do sự hiện diện của các phụ thuộc hoặc ràng buộc mà bất kỳ hàm tạo kiểu có sẵn nào cũng không thể thỏa mãn. Ví dụ: trong lý thuyết loại phụ thuộc với loại sản phẩm phụ thuộc `A x B`, trong đó `A` và `B` là các loại phụ thuộc lẫn nhau, có thể không suy ra được loại `A x B` nếu không có cách nào để xây dựng `A` và `B` bằng cách sử dụng các hàm tạo và ràng buộc kiểu có sẵn.

Nói chung, các kiểu không thể cấp phép có thể dùng như một cách để mã hóa các thuộc tính hoặc ràng buộc không thể quyết định trong một hệ thống kiểu và có thể được sử dụng để suy luận về những hạn chế của chính hệ thống loại.