commit 0a356299287fc18076a03264d573a63dde103669
parent bed4b0f73dec22e4fb8ad66d9d547a2be6426051
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Thu, 24 Aug 2017 15:03:11 +0200
Improved math rendering, added some subtyping rules.
Diffstat:
9 files changed, 115 insertions(+), 61 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -445,15 +445,17 @@ their inclusion in the following semantics would needlessly complicate things.
indicates that @${τ} and @${σ} are not mutually subtypes of each other (but
one can be a strict subtype of the other).
- @include-equation["subtyping.rkt" S-Reflexive]
- @include-equation["subtyping.rkt" S-Transitive]
+ @$p[@include-equation["subtyping.rkt" S-Reflexive]
+ @include-equation["subtyping.rkt" S-Transitive]]
The @${⊥} type is a shorthand for the empty union @${(∪)}. It is a subtype of
- every other type, and is not inhabited by any value. @textsc{S-Bot} can be
- derived from @textsc{S-UnionSub}, by constructing an empty union.
+ every other type, and is not inhabited by any value.
+ @refrule[@textsc{S-Bot-Sub}] can be derived from @refrule[@textsc{S-Bot}]
+ and @refrule[@textsc{S-UnionSub}], by constructing an empty union.
@$p[@include-equation["subtyping.rkt" S-Top]
- @include-equation["subtyping.rkt" S-Bot]]
+ @include-equation["subtyping.rkt" S-Bot]
+ @include-equation["subtyping.rkt" S-Bot-Sub]]
The singleton types @num-τ and @symτ[s] which are only inhabited by their
literal counterpart are subtypes of the more general @Numberτ or @Symbolτ
@@ -484,16 +486,17 @@ their inclusion in the following semantics would needlessly complicate things.
If it works.}
The following rules are concerned with recursive types built with the
- @racket[Rec] combinator. The @textsc{S-RecWrap} rule allows considering
- @Numberτ a subtype of @recτ[r Numberτ] for example (i.e. applying the
- recursive type combinator to a type which does not refer to @${r} is a no-op),
- but it also allows deriving
- @<:[@recτ[r @un[@consτ[τ r] @null-τ]] @un[@consτ[τ ⊤] @null-τ]]. The @textsc{
- S-RecElim} rule has the opposite effect, and is mainly useful to “upcast”
- members of an union containing @${r}. It allows the deriving
- @<:[@null-τ @recτ[r @un[@consτ[τ r] @null-τ]]]. The rules @textsc{S-RecStep}
- and @textsc{S-RecUnStep} allow unraveling a single step of the recursion, or
- assimilating an such an unraveled step as part of the recursive type.
+ @racket[Rec] combinator. The @refrule[@textsc{S-RecWrap}] rule allows
+ considering @Numberτ a subtype of @recτ[r Numberτ] for example (i.e. applying
+ the recursive type combinator to a type which does not refer to @${r} is a
+ no-op), but it also allows deriving
+ @<:[@recτ[r @un[@consτ[τ r] @null-τ]] @un[@consτ[τ ⊤] @null-τ]]. The
+ @refrule[@textsc{ S-RecElim}] rule has the opposite effect, and is mainly
+ useful to “upcast” members of an union containing @${r}. It allows the
+ deriving @<:[@null-τ @recτ[r @un[@consτ[τ r] @null-τ]]]. The rules
+ @refrule[@textsc{ S-RecStep}] and @refrule[@textsc{S-RecUnStep}] allow
+ unraveling a single step of the recursion, or assimilating an such an
+ unraveled step as part of the recursive type.
@todo{TODO: renamings}
@@ -534,12 +537,12 @@ their inclusion in the following semantics would needlessly complicate things.
@include-equation["operational-semantics.rkt" δe-rules]
- The @textsc{E-Context} rule indicates that when the expression has the shape
- @${E[L]}, the subpart @${L} can be evaluated and replaced by its result. The
- syntax @${E[L]} indicates the replacement of the only occurrence of @${[⋅]}
- within an evaluation context @${E}. The evaluation context can then match an
- expression with the same shape, thereby separating the @${L} part from its
- context.
+ The @refrule[@textsc{E-Context}] rule indicates that when the expression has
+ the shape @${E[L]}, the subpart @${L} can be evaluated and replaced by its
+ result. The syntax @${E[L]} indicates the replacement of the only occurrence
+ of @${[⋅]} within an evaluation context @${E}. The evaluation context can then
+ match an expression with the same shape, thereby separating the @${L} part
+ from its context.
@include-equation["operational-semantics.rkt" E-Context]
@@ -673,7 +676,8 @@ their inclusion in the following semantics would needlessly complicate things.
information concerning outer variables (those not declared within the lambda,
and therefore still available after it finishes executing).}
- @todo{Should the φ⁺ φ⁻ o be preserved in T-TAbs and T-DTAbs?}
+ @todo{Should the φ⁺ φ⁻ o be preserved in @refrule[@textsc{T-TAbs}] and
+ @refrule[@textsc{T-DTAbs?}]}
@$p[@include-equation["trules.rkt" T-AbsPred]
@include-equation["trules.rkt" T-Abs]
diff --git a/from-dissertation-tobin-hochstadt/subtyping.rkt b/from-dissertation-tobin-hochstadt/subtyping.rkt
@@ -21,17 +21,22 @@
#:S-Top
-@$inferrule[
- -
- @${@<:[τ ⊤]}
- @${@textsc{S-Top}}]
+@$inferrule[-
+ @${@<:[τ ⊤]}
+ @${@textsc{S-Top}}]
#:S-Bot
-@$inferrule[
- -
- @${@<:[⊥ τ]}
- @${@textsc{S-Bot}}]
+@$inferrule[-
+ @${@=:[⊥ @un[]]}
+ @${@textsc{S-Bot}}]
+
+#:S-Bot-Sub
+
+@$inferrule[@${@refrule[@textsc{S-Bot}] \\
+ @refrule[@textsc{S-UnionSub}]}
+ @${@<:[⊥ τ]}
+ @${@textsc{S-Bot-Sub}}]
#:S-Number
diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt
@@ -206,6 +206,7 @@
@${φ⁻'}
@${o'}])
ϵ ⊥ ∅]]}
+ #:wide 'latex
@${@textsc{T-App}}]
#:T-Inst
@@ -257,6 +258,7 @@
@nl ∅ @& @otherwise
\end{cases}}
@${@Γ[⊢ @ifop[e₁ e₂ e₃] @R[τ_r φ_r⁺ φ_r⁻ o_r]]}
+ #:wide 'latex
@${@textsc{T-If}}]
#:Γ+
diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl
@@ -52,18 +52,21 @@ a conditional.
@cond-element[
[html @${\begin{multline}}]
[else @${\begin{multlined}}]]
- @|restrict|\left(\begin{aligned}
- &@recordτ[@ρf
- @repeatset{-@|ɐ|ᵢ}
- @repeatset{-@|ɐ|ⱼ}
- @repeatset{+@|ɐ|ₗ : τₗ}
- @repeatset{+@|ɐ|ₘ : τₘ}],
+ @|restrict|\left(
+ @cond-element[
+ [html @${\begin{array}{l}}]
+ [else @$|{\begin{array}{@{}l@{}}}|]]
+ @recordτ[@ρf
+ @repeatset{-@|ɐ|ᵢ}
+ @repeatset{-@|ɐ|ⱼ}
+ @repeatset{+@|ɐ|ₗ : τₗ}
+ @repeatset{+@|ɐ|ₘ : τₘ}],
\\@; TODO: this does not handle the regular per-field update like above?
- &@recordτ[@ρf
- @repeatset{-@|ɐ|ᵢ}
- @repeatset{-@|ɐ|ₖ}
- @repeatset{+@|ɐ|ₗ : σₗ}
- @repeatset{+@|ɐ|ₙ : σₙ}]\end{aligned}\right)
+ @recordτ[@ρf
+ @repeatset{-@|ɐ|ᵢ}
+ @repeatset{-@|ɐ|ₖ}
+ @repeatset{+@|ɐ|ₗ : σₗ}
+ @repeatset{+@|ɐ|ₙ : σₙ}]\end{array}\right)
\\
= @recordτ[@repeatset{-@|ɐ|ᵢ}
@repeatset{-@|ɐ|ⱼ}
diff --git a/scribblings/adt-row-sub.scrbl b/scribblings/adt-row-sub.scrbl
@@ -8,6 +8,24 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Subtyping (with ρ)}
+Variants which do not involve a row type are nothing more than a syntactic
+restriction on a union of types. The variant only allows constructors to be
+present in the union, as specified by the type validity rule
+@refrule[@textsc{TE-Variant}].
+
+@$inferrule[-
+ @=:[@variantτ[@repeated{τ}] @un[@repeated{τ}]]
+ @${@textsc{S-Variant-Union}}]
+
+From @refrule[@textsc{S-Variant-Union}], we can derive that the empty variant is
+equivalent to the bottom type.
+
+@$inferrule[@${@textsc{S-Variant-Union} \\
+ @textsc{S-Bot}}
+ @=:[@variantτ[] ⊥]
+ @${@textsc{S-Variant-Empty}}]
+
+
@$inferrule[@${∃ i . @<:[τ @${σᵢ}]}
@${@<:[τ @variantτ[@repeated{σᵢ}]]}
@${@textsc{S-VariantSuper}}]
@@ -17,6 +35,11 @@
@${@textsc{S-VariantSub}}]
+
+
+
+
+
@;{@$inferrule[-
@<:[@ctorτ[@κof[τ]] @ctorTop[τ]]
@${@textsc{S-CtorTop}}]}
@@ -59,10 +82,6 @@
@∀c[(@repeated{@|ρc|′ᵢ}) σ]]}
@${@textsc{S-PolyC-}α@textsc{-Equiv}}]
-@$inferrule[-
- @=:[@variantτ[] ⊥]
- @${@textsc{S-Variant-Empty}}]
-
@; TODO: can these rules be used to combine a record type and a record*?
@; predicate to make sure some fields are absent, without checking anything
@; for the other fields?
diff --git a/scribblings/adt-row-te.scrbl b/scribblings/adt-row-te.scrbl
@@ -19,11 +19,11 @@
@$p[
@$inferrule[@${@ρc ∈ Δ \\
- \{@repeated{@|κ|ᵢ}\} ∩ \{@repeated{@|κ|ⱼ}\} = ∅ \\
- @alldifferent(@repeated{@|κ|ᵢ}) \\
- @alldifferent(@repeated{@|κ|ⱼ})}
+ @repeated{Δ ⊢ τᵢ} \\
+ @alldifferent(@repeated{@|κ|ᵢ} @repeated{@|κ|ⱼ})}
@${Δ ⊢ @variantτ[@ρc @repeatset{-@ctorτ[@|κ|ᵢ]}
@repeatset{+@ctorτ[@κof[ⱼ τⱼ]]}]}
+ #:wide 'latex
@${@textsc{TE-CVariant}}]
@$inferrule[@${@ρf ∈ Δ \\
@@ -43,8 +43,8 @@ where
-@$inferrule[@${@alldifferent(@repeated{@|κ|ᵢ}) \\
- @repeated{Δ ⊢ τᵢ}}
+@$inferrule[@${@repeated{Δ ⊢ τᵢ} \\
+ @alldifferent(@repeated{@|κ|ᵢ})}
@${Δ ⊢ @variantτ[@repeated{@ctorτ[@κof[ᵢ τᵢ]]}]}
@${@textsc{TE-Variant}}]
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -50,6 +50,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
= @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
+ #:wide 'latex
@${@textsc{T-Ctor-Val}}]
}
@@ -64,6 +65,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
φ_r = @applyfilter(@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]
|\overline{@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
+ #:wide 'latex
@${@textsc{T-Record-Pred}}]
@$${
@@ -78,6 +80,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
= @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
+ #:wide 'latex
@${@textsc{T-Record-GetField}}]
}
@@ -95,6 +98,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@${@|ɐ| : τ_{v}}
@${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]@;changed
; ϵ|⊥ ; ∅}
+ #:wide 'latex
@${@textsc{T-Record-With}_1}
]
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -185,11 +185,11 @@
(define-syntax ∩τ (defop "∩"))
(define-syntax-rule (f→ (from ...) R)
- @${(@(add-between (list @(stringify from) ...) "\\ ") \mathbf{→} @(stringify R))})
+ @${(@(add-between (list @(stringify from) ...) "\\ ")\ @mathbm{→}\ @(stringify R))})
(define-syntax-rule (f* (from ... rest*) R)
- (f→ (from ... @${\ \mathbf{.}\ } @${@(stringify rest*)@mathbm{*}}) R))
+ (f→ (from ... @${\ @mathbm{.}\ } @${@(stringify rest*)@mathbm{*}}) R))
(define-syntax-rule (f… (from ... polydot) R)
- (f→ (from ... @${\ \mathbf{.}\ } polydot) R))
+ (f→ (from ... @${\ @mathbm{.}\ } polydot) R))
(define-syntax (R stx)
(syntax-case stx ()
[(_ to φ⁺ φ⁻ o)
@@ -325,4 +325,7 @@
(define δe @${δ_{\mathrm{e}}})
(define alldifferent @${\operatorname{AllDifferent}})
-(define disjoint-sets @${\operatorname{DisjointSets}})
-\ No newline at end of file
+(define disjoint-sets @${\operatorname{DisjointSets}})
+
+;; Temporary placeholder, will add linking and propper names later.
+(define-syntax-rule (refrule name) name)
+\ No newline at end of file
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -163,6 +163,10 @@
(define m
(list setup-math
(tex-header #<<EOTEX
+% DRAFT ONLY
+\overfullrule=1cm\relax
+
+
\def\ifmathjax#1{}\def\iflatex#1{#1}
\renewcommand{\rmdefault}{cmr}
\newenvironment{qaligned}{%
@@ -508,6 +512,16 @@ EOTEX
(define $ooo ($ (mathtext "\\textit{ooo}")))
(define ($inferrule #:wide [wide? #f] from* to* [label '()])
+ (define-syntax-rule (if-wide wide not-wide)
+ (cond
+ [(eq? wide? #t)
+ wide]
+ [(eq? wide? #f)
+ not-wide]
+ [else
+ (cond-element
+ [html (if (eq? wide? 'html) wide not-wide)]
+ [else (if (eq? wide? 'latex) wide not-wide)])]))
@$$[
(elem #:style
(style #f (list (tex-addition
@@ -517,9 +531,9 @@ EOTEX
[html ""]
[else (string-append "\\ifcsname savedamp\\endcsname"
"\\else\\global\\let\\savedamp&\\fi")])
- (if wide?
- @${\begin{aligned}\vphantom{x}&@|label|\\ \vphantom{x}&}
- '())
+ (if-wide
+ @${\begin{aligned}\vphantom{x}&@|label|\\ \vphantom{x}&}
+ '())
(cond-element [html "\\frac{\\begin{gathered}"]
[else "\\inferrule{"])
(if (eq? from* -) "\\vphantom{x}" from*)
@@ -528,9 +542,9 @@ EOTEX
(if (eq? to* -) "\\vphantom{x}" to*)
(cond-element [html "\\end{gathered}}"]
[else "}"])
- (if wide?
- "\\end{aligned}"
- (list @${\ } label))))])
+ (if-wide
+ "\\end{aligned}"
+ (list @${\ } label))))])
(define htmldiff-css-experiment #<<EOCSS
.version:after {
