The Barrier of Objects: From Dynamical Systems to Bounded Organizations
Walter Fontana, Leo W. Buss · IIASA PURE (International Institute of Applied Systems Analysis) · 1996
ion Ax ∪ {x : τ ′} e : τ A λx.e : τ ′ → τ Let A e : σ Ax ∪ {x : σ} e′ : τ A (let x = e in e′) : τ The meaning of the Taut-rule is simply that a free variable has the type assigned to it in the boundary condition. If there is no assignment the expression x is not typable, and is barred from the universe. The meaning of rule App is also clear. It is useful, however, to know how the rule is implemented, since it introduces an important concept. Suppose that we have an object e whose type has been established to be σ, and that we want to apply it to an object e′ of type τ ′. For this to be possible e must have a type of the form τ ′ → τ where τ stands for a generic unknown type of (e)e′ that needs to be determined. Hence, for the interaction (e)e′ to be possible e’s established type σ and the required type τ ′ → τ must be made equal. This may be possible, since σ and τ ′ may contain type variables which can be made more specific in order to satisfy the equality. This means we must look for some type substitution T of the free variables in σ and in τ ′ → τ such that Tσ = T (τ ′ → τ). T is called a unifier, and the procedure for finding T is called unification. It boils down to solving a set of equations. For details about how this procedure is carried out the reader is referred to any standard textbook on type theory. The point is that a