CIS 500Software FoundationsFall 2006November 13Metatheory of SubtypingSyntax-directed rulesIn the simply typed lambda-calculus (without subtyping), each rulecan be “read from bott om to top” in a straightforward way.Γ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)If we are given some Γ and some t of the form t1t2, we can tryto find a type for t by1. finding (recursively) a type for t12. checking that it has the form T11→T123. finding (recursively) a type for t24. checking that it is the same as T11Technically, the reason this works is that we can divide the“pos itions” of the typing relation into input positions (Γ and t)and output positions (T).IFor the input positions, all metavariables appearing in thepremises also appear in the conclusion (so we can calculateinputs to the “subgoals” from the sub e xpressions of inputs tothe main goal)IFor the output positions, all metavariables appearing in theconclusions also appe ar in the premises (so we can calculateoutputs from the main goal from the outputs of the subgoals)Γ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)Syntax-directed sets of rulesThe second important point about the simply typedlambda-calculus is that the set of typing rules is syntax-directe d, inthe sense that, for every “input” Γ and t, there one rule that canbe used to derive typing statements involving t.E.g., if t is an application, then we must proceed by trying to useT-App. If we succeed, then we have found a type (indeed, theunique type) for t. If it fails, then we know that t is not typable.−→ no backtracking!Non-syntax-directedness of typingWhen we extend the system with subtyping, both aspects ofsyntax-directedness get broken.1. The set of typing rules now includes two rules that can beused to give a type to terms of a given shape (the old oneplus T-Sub)Γ ` t : S S <: TΓ ` t : T(T-Sub)2. Worse yet, the new rule T-Sub itself is not syntax directed:the inputs to the left-hand subgoal are exactly the same asthe inputs to the main goal!(If we translated the typing rules naively into a typecheckingfunction, the case corresponding to T-Sub would causedivergence.)Non-syntax-directedness of subtypingMoreover, the subtyping relation is not syntax directed either.1. There are lots of ways to derive a given subtyping statement.2. The transitivity ruleS <: U U <: TS <: T(S-Trans)is badly non-syntax-directed: the premises contain ametavariable (in an “input position”) that does not appear atall in the conclusion.To implement this rule naively, we’d have to guess a value forU!What to do?1. Observation: We don’t need 1000 ways to prove a giventyping or subtyping statement — one is enough.−→ Think more carefully about the typing and subtypingsystems to see where we can get rid of excess flexibility2. Use the resulting intuitions to formulate new “algorithmic”(i.e., syntax-directed) typing and subtyping relations3. Prove that the algorithmic relations are “the same as” theoriginal ones in an appropriate sense.What to do?1. Observation: We don’t need 1000 ways to prove a giventyping or subtyping statement — one is enough.−→ Think more carefully about the typing and subtypingsystems to see where we can get rid of excess flexibility2. Use the resulting intuitions to formulate new “algorithmic”(i.e., syntax-directed) typing and subtyping relations3. Prove that the algorithmic relations are “the same as” theoriginal ones in an appropriate sense.Developing an algorithmicsubtyping relationSubtype relationS <: S(S-Refl)S <: U U <: TS <: T(S-Trans){li:Tii∈1 ..n+k} <: {li:Tii∈1 ..n}(S-RcdWidth)for each i Si<: Ti{li:Sii∈1 ..n} <: {li:Tii∈1 ..n}(S-RcdDepth){kj:Sjj∈1 ..n} is a permutation of {li:Tii∈1 ..n}{kj:Sjj∈1 ..n} <: {li:Tii∈1 ..n}(S-RcdPerm)T1<: S1S2<: T2S1→S2<: T1→T2(S-Arrow)S <: Top(S-Top)IssuesFor a given subtyping statement, there are multiple rules thatcould be used last in a derivation.1. The conclusions of S-RcdWidth, S-RcdDepth, andS-RcdPerm overlap with each other.2. S-Refl and S-Trans overlap with every other rule.Step 1: simplify record subtypingIdea: combine all three record subtyping rules into one “macrorule” that captures all of their effects{lii∈1 ..n} ⊆ {kjj∈1 ..m} kj= liimplies Sj<: Ti{kj:Sjj∈1 ..m} <: {li:Tii∈1 ..n}(S-Rcd)Simpler subtype relationS <: S(S-Refl)S <: U U <: TS <: T(S-Trans){lii∈1 ..n} ⊆ {kjj∈1 ..m} kj= liimplies Sj<: Ti{kj:Sjj∈1 ..m} <: {li:Tii∈1 ..n}(S-Rcd)T1<: S1S2<: T2S1→S2<: T1→T2(S-Arrow)S <: Top(S-Top)Step 2: Get rid of reflexivityObservation: S-Refl is unnecessary.Lemma: S <: S can be derived for every type S without usingS-Refl.Even simpler subtype relationS <: U U <: TS <: T(S-Trans){lii∈1 ..n} ⊆ {kjj∈1 ..m} kj= liimplies Sj<: Ti{kj:Sjj∈1 ..m} <: {li:Tii∈1 ..n}(S-Rcd)T1<: S1S2<: T2S1→S2<: T1→T2(S-Arrow)S <: Top(S-Top)Step 3: Get rid of transitivityObservation: S-Trans is unnecessary.Lemma: If S <: T can be derived, then it can be derived withoutusing S-Trans.“Algorithmic” subtype relation`IS <: Top(SA-Top)`IT1<: S1`IS2<: T2`IS1→S2<: T1→T2(SA-Arrow){lii∈1 ..n} ⊆ {kjj∈1 ..m} for each kj= li, `ISj<: Ti`I{kj:Sjj∈1 ..m} <: {li:Tii∈1 ..n}(SA-Rcd)Soundness and completenessTheorem: S <: T iff `IS <: T.Proof: (Homework)Terminology:IThe algorithmic presentation of subtyping is sound withresp ec t to the original if `IS <: T implies S <: T.(Everything validated by the algorithm is actually true.)IThe algorithmic presentation of subtyping is complete withresp ec t to the original if S <: T implies `IS <: T.(Everything true is validated by the algorithm.)Subtyping Algorithm (pseudo-code)The algorithmic rules can be translated directly into code:subtype(S, T) =if T = Top, then trueelse if S = S1→S2and T = T1→T2then subtype(T1, S1) ∧ subtype(S2, T2)else if S = {kj:Sjj∈1 ..m} and T = {li:Tii∈1 ..n}then {lii∈1 ..n} ⊆ {kjj∈1 ..m}∧ for all i ∈ 1..n there is some j ∈ 1..m with kj= liand subtype(Sj, Ti)else false.Decision ProceduresRecall: A decision procedure for a relation R ⊆ U is a totalfunction p from U to {true, false} such that p(u) = true iff u ∈ R.Is our subtype function a decision procedure?Since subtype is just an implementation of the algorithmicsubtyping rules, we have1. if subtype(S, T) = true, then `IS <: T(hence, by soundness of the algorithmic rules, S <: T)2. if subtype(S, T) = false, then not `IS <: T(hence, by completeness of the algorithmic rules, not S <: T)Q: