subtyping.rkt (5612B)
1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang 2 3 @; This file is NOT under the CC0 license, as it contains rules and definitions 4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the 5 @; permission to copy these rules, but did not ask for a relicensing under the 6 @; CC0 license. 7 8 #:S-Eq₁ 9 10 @$inferrule[ 11 @=:[τ σ] 12 @<:[τ σ] 13 @${@textsc{S-Eq}_1}] 14 15 #:S-Eq₂ 16 17 @$inferrule[ 18 @=:[τ σ] 19 @<:[σ τ] 20 @${@textsc{S-Eq}_2}] 21 22 #:S-Eq₃ 23 24 @$inferrule[ 25 @${@<:[τ σ] \\ @<:[σ τ]} 26 @=:[τ σ] 27 @${@textsc{S-Eq}_3}] 28 29 #:S-Reflexive 30 31 @$inferrule[ 32 - 33 @${@<:[τ τ]} 34 @${@textsc{S-Reflexive}}] 35 36 #:S-Transitive 37 38 @$inferrule[ 39 @${@<:[τ τ′] \\ @<:[τ′ τ″]} 40 @${@<:[τ τ″]} 41 @${@textsc{S-Transitive}}] 42 43 #:S-Top 44 45 @$inferrule[- 46 @${@<:[τ ⊤]} 47 @${@textsc{S-Top}}] 48 49 #:S-Bot 50 51 @$inferrule[- 52 @${@=:[⊥ @un[]]} 53 @${@textsc{S-Bot}}] 54 55 #:S-Bot-Sub 56 57 @$infertree[((@refrule[@textsc{S-Bot}] ⇒ @refrule[@textsc{S-Eq₁}]) 58 @refrule[@textsc{S-UnionSub}] 59 ⇒ 60 @refrule[@textsc{S-Transitive}]) 61 ⇒ 62 @${@<:[⊥ τ]} 63 @${@textsc{S-Bot-Sub}}] 64 65 #:S-Number 66 67 @$inferrule[ 68 - 69 @${@<:[@num-τ @Numberτ]} 70 @${@textsc{S-Number}}] 71 72 #:S-Symbol 73 74 @$inferrule[ 75 - 76 @${@<:[@symτ[s] @Symbolτ]} 77 @${@textsc{S-Symbol}}] 78 79 #:S-RecWrap 80 81 @$inferrule[@${@<:[τ σ]} 82 @${@<:[@recτ[r τ] σ]} 83 @${@textsc{S-RecWrap}}] 84 85 #:S-RecElim 86 87 @$inferrule[@${@<:[τ σ]} 88 @${@<:[τ @recτ[r σ]]} 89 @${@textsc{S-RecElim}}] 90 91 #:S-RecStep 92 93 ;; This rule allows the following sort of subtyping: 94 ;; This is necessary to build recursive functions which return Rec types, 95 ;; by adding one "step" to the recursive construction of the value. 96 #;{ (Pairof Integer (Rec R (Pairof Integer R))) <: (Rec R (Pairof Integer R)) } 97 98 99 @$inferrule[- 100 @${@<:[@${σ@subst[r ↦ @recτ[r σ]]} @recτ[r σ]]} 101 @${@textsc{S-RecStep}}] 102 103 #:S-RecUnStep 104 105 @$inferrule[- 106 @${@<:[@recτ[r σ] @${σ@subst[r ↦ @recτ[r σ]]}]} 107 @${@textsc{S-RecUnStep}}] 108 109 @;{ 110 @$inferrule[- 111 @${@<:[@elim[@${r} @${τ}] @recτ[r τ]]} 112 @${@textsc{S-Rec}}] 113 114 where 115 116 @$${ 117 \begin{aligned} 118 @elim[@${r} @un[@repeatset{τ′} r]] &= @un[@repeatset[@elim[@${r} @${τ′}]]]\\ 119 @elim[@${r} @${τ}]&\hphantom{{}={}}@text{is applied pointwise otherwise} 120 \end{aligned} 121 } 122 } 123 124 #:S-Fun 125 126 @$inferrule[@${@repeated{@<:[σ_a τ_a]} \\ 127 @<:R[R @${@R'}]} 128 @${@<:[@f→[(@repeated{τ_a}) R] 129 @f→[(@repeated{σ_a}) @${@R'}]]} 130 @${@textsc{S-Fun}}] 131 132 #:S-R 133 134 @$inferrule[@${@<:[τ_r σ_r] \\ 135 @${φ⁺' ⊆ φ⁺ } \\ 136 @${φ⁻' ⊆ φ⁻ } \\ 137 o = o' ∨ o' = ∅} 138 @${@<:R[@R[τ_r 139 @${φ⁺} 140 @${φ⁻} 141 @${o}] 142 @R[σ_r 143 @${φ⁺'} 144 @${φ⁻'} 145 @${o'}]]} 146 @${@textsc{S-R}}] 147 148 #:S-Fun* 149 150 @$inferrule[ 151 @${ 152 @repeated{@<:[σ_a τ_a]} \\ 153 @<:[σ τ] \\ 154 @<:R[R @${@R'}]} 155 @${@<:[@f*[(@repeated{τ_a} τ) R] 156 @f*[(@repeated{σ_a} σ) @${@R'}]]} 157 @${@textsc{S-Fun*}}] 158 159 #:S-Fun*-Fixed 160 161 @$inferrule[ 162 @${ 163 @repeated{@<:[σ_a τ_a]} \\ 164 @repeated{@<:[σᵢ τ]} \\ 165 @<:R[R @${@R'}]} 166 @${@<:[@f*[(@repeated{τ_a} τ) R] 167 @f→[(@repeated{σ_a} @repeated{σᵢ}) @${@R'}]]} 168 @${@textsc{S-Fun*-Fixed}}] 169 170 #:S-Fun*-Fixed* 171 172 @$inferrule[ 173 @${ 174 @repeated{@<:[σ_a τ_a]} \\ 175 @repeated{@<:[σᵢ τ]} \\ 176 @<:[σ τ] \\ 177 @<:R[R @${@R'}]} 178 @${@<:[@f*[(@repeated{τ_a} τ) R] 179 @f*[(@repeated{σ_a} @repeated{σᵢ} σ) @${@R'}]]} 180 @${@textsc{S-Fun*-Fixed*}}] 181 182 #:S-DFun 183 184 @$inferrule[ 185 @${ 186 @repeated{@<:[σ_a τ_a]} \\ 187 @<:[σ τ] \\ 188 @<:R[R @${@R'}]} 189 @${@<:[@f…[(@repeated{τ_a} @polydot[τ α]) R] 190 @f…[(@repeated{σ_a} @polydot[σ α]) @${@R'}]]} 191 @${@textsc{S-DFun}}] 192 193 #:S-Poly-α-Equiv 194 195 @$inferrule[ 196 @${@<:[@${τ[@repeated{αᵢ ↦ βᵢ}]} σ]} 197 @${@<:[@∀r[(@repeated{αᵢ}) τ] 198 @∀r[(@repeated{βᵢ}) σ]]} 199 @${@textsc{S-Poly-}α@textsc{-Equiv}}] 200 201 #:S-PolyD-α-Equiv 202 203 @$inferrule[ 204 @${@<:[@${τ[@repeated{αᵢ ↦ βᵢ} α ↦ β]} σ]} 205 @${@<:[@∀r[(@repeated{αᵢ} @polydotα[α]) τ] 206 @∀r[(@repeated{βᵢ} @polydotα[β]) σ]]} 207 @${@textsc{S-PolyD-}α@textsc{-Equiv}}] 208 209 #:S-DFun-Fun* 210 211 @$inferrule[ 212 @${ 213 @repeated{@<:[σ_a τ_a]} \\ 214 @<:[σ @${τ[α ↦ ⊤]}] \\ 215 @<:R[R @${@R'}]} 216 @${@<:[@∀r[(@polydotα[α]) @f…[(@repeated{τ_a} @polydot[τ α]) R]] 217 @f*[(@repeated{σ_a} σ) @${@R'}]]} 218 @${@textsc{S-DFun-Fun*}}] 219 220 #:S-UnionSuper 221 222 @$inferrule[ 223 @${∃ i . @<:[τ @${σᵢ}]} 224 @${@<:[τ @un[@repeated{σᵢ}]]} 225 @${@textsc{S-UnionSuper}}] 226 227 #:S-UnionSub 228 229 @$inferrule[ 230 @${@repeated[@<:[τᵢ @${σ}]]} 231 @${@<:[@un[@repeated{τᵢ}] σ]} 232 @${@textsc{S-UnionSub}}] 233 234 #:S-Pair 235 236 @$inferrule[ 237 @${@<:[τ₁ σ₁] \\ 238 @<:[τ₂ σ₂]} 239 @${@<:[@consτ[τ₁ τ₂] @consτ[σ₁ σ₂]]} 240 @${@textsc{S-Pair}}] 241 242 #:S-DList 243 244 @$inferrule[ 245 @${@<:[τ σ]} 246 @${@<:[@List…τ[τ α] @recτ[r @un[@consτ[σ r] @null-τ]]]} 247 @${@textsc{S-DList}}] 248 249 #:S-IntersectionSub 250 251 @$inferrule[ 252 @${∃ i . @<:[@${σᵢ} τ]} 253 @${@<:[@${⋂ @repeated{σᵢ}} τ]} 254 @${@textsc{S-IntersectionSub}}] 255 256 #:S-IntersectionSuper 257 258 @$inferrule[ 259 @${@repeated[@<:[@${σ} τᵢ]]} 260 @${@<:[σ @${⋂ @repeated{τᵢ}}]} 261 @${@textsc{S-IntersectionSuper}}] 262 263 #:S-Promise 264 265 @$inferrule[ 266 @${@<:[τ σ]} 267 @${@<:[@promiseτ[τ] @promiseτ[σ]]} 268 @${@textsc{S-Promise}}]