We propose a language design where types can be enriched by tags corresponding to predicates written by the programmer. For instance, int&positive; is a type, where positive is a user-defined boolean function on integers. Expressions of type int&positive; are obtained by an explicit check construct, analogous to cast, e.g., (positive) 2. In this way, the fact that the value of an expression is guaranteed to succeed a runtime check is a static property which can be controlled by the type system. We formalize our proposal as an extension of the simply-typed lambda calculus, and prove, besides soundness, the fact that expressions of tagged types reduce to values which satisfy the corresponding predicates.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo