Nem engedélyezhető típusok a típuselméletben: A meg nem határozható tulajdonságok és korlátok megértése

A típuselmélet kontextusában a nem engedélyezhető típus olyan típus, amelyre nem lehet következtetni vagy létrehozni a rendelkezésre álló típuskonstruktorok és megszorítások segítségével.

Például egy egyszerűen begépelt lambda-kalkulusban csak a `Nat` (természetes számok) és ` alaptípusok vannak. Prop` (propozíciók), nem lehet a `Nat x Prop` típusra következtetni, mert nincs mód a két típus kombinálására a rendelkezésre álló típuskonstruktorok segítségével. Ezt a típust nem engedélyezhetőnek mondják.

A fejlettebb típusrendszerekben, mint például a függő típuselmélet vagy a homotópiatípuselmélet, nem engedélyezhető típusok keletkezhetnek olyan függőségek vagy megszorítások miatt, amelyeket egyetlen elérhető típuskonstruktor sem tud kielégíteni. Például egy függő típuselméletben egy "A x B" függő terméktípussal, ahol az "A" és "B" egymástól függő típusok, előfordulhat, hogy nem lehet következtetni az "A x B" típusra, ha nincs mód "A" és "B" létrehozására a rendelkezésre álló típuskonstruktorok és megszorítások felhasználásával.

Általában a nem engedélyezhető típusok szolgálhatnak meghatározhatatlan tulajdonságok vagy megszorítások kódolására egy típusrendszerben, és felhasználhatók a magának a típusrendszernek a korlátai.