commit 1e745d6159e6965975cb86713ac387720a30d3ce
parent ddcbd43180592cb816dfaeca6e584955dcbe53bb
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 16 Aug 2017 16:12:43 +0200
good
Diffstat:
10 files changed, 91 insertions(+), 73 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -164,6 +164,23 @@ the first substitution).
@todo{Define the meta substitution and equality operators precisely.}
+@subsubsub*section{Names and bindings}
+
+In the following sections, we assume that all type variable names which occur
+in binding positions are unique. This assumption could be made irrelevant by
+explicitly renaming in the rules below all type variables to fresh unique
+ones. Performing this substitution would be a way of encoding a notion of
+scope and the possibility for one identifier to hide another. However, the
+Racket language features macros which routinely produce new binding forms. The
+macro system in Racket is a hygienic one, and relies on a powerful model of
+the notion of scope@~cite["flatt2016binding"]. Extending the rules below with
+a simplistic model of Racket's notion of scope would not do justice to the
+actual system, and would needlessly complicate the rules. Furthermore,
+@typedracket only typechecks fully-expanded programs. In these programs, the
+binding of each identifier has normally been determined@note.{@Typedracket
+ actually still determines the binding for type variables by itself, but we
+ consider this is an implementation detail.}
+
@subsubsub*section{Expressions}
The following expressions are available in the subset of @typedracket which we
diff --git a/from-dissertation-tobin-hochstadt/simplify.rkt b/from-dissertation-tobin-hochstadt/simplify.rkt
@@ -30,8 +30,8 @@
\begin{aligned}
@simplify[@f→[(@repeated{τ}) R]]
&= @f→[(@repeated{@simplify[τ]}) @simplify[R]] \\
- @simplify[@f*[(@repeated{τ} @${τ*}) R]]
- &= @f*[(@repeated{@simplify[τ]} @simplify[τ*]) @simplify[R]]\\
+ @simplify[@f*[(@repeated{τ} τ) R]]
+ &= @f*[(@repeated{@simplify[τ]} @simplify[τ]) @simplify[R]]\\
@simplify[@f…[(@repeated{τ} @polydot[τ α]) R]]
&= @f…[(@repeated{@simplify[τ]} @polydot[@simplify[τ] α]) @simplify[R]]\\
@simplify[@∀r[(@repeated{α}) τ]]
diff --git a/from-dissertation-tobin-hochstadt/subtyping.rkt b/from-dissertation-tobin-hochstadt/subtyping.rkt
@@ -123,8 +123,8 @@
@repeated{@<:[σ_a τ_a]} \\
@<:[σ τ] \\
@<:R[R @${@R'}]}
- @${@<:[@f*[(@repeated{τ_a} τ*) R]
- @f*[(@repeated{σ_a} σ*) @${@R'}]]}
+ @${@<:[@f*[(@repeated{τ_a} τ) R]
+ @f*[(@repeated{σ_a} σ) @${@R'}]]}
@${@textsc{S-Fun*}}]
#:S-Fun*-Fixed
@@ -134,7 +134,7 @@
@repeated{@<:[σ_a τ_a]} \\
@repeated{@<:[σᵢ τ]} \\
@<:R[R @${@R'}]}
- @${@<:[@f*[(@repeated{τ_a} τ*) R]
+ @${@<:[@f*[(@repeated{τ_a} τ) R]
@f→[(@repeated{σ_a} @repeated{σᵢ}) @${@R'}]]}
@${@textsc{S-Fun*-Fixed}}]
@@ -146,8 +146,8 @@
@repeated{@<:[σᵢ τ]} \\
@<:[σ τ] \\
@<:R[R @${@R'}]}
- @${@<:[@f*[(@repeated{τ_a} τ*) R]
- @f*[(@repeated{σ_a} @repeated{σᵢ} σ*) @${@R'}]]}
+ @${@<:[@f*[(@repeated{τ_a} τ) R]
+ @f*[(@repeated{σ_a} @repeated{σᵢ} σ) @${@R'}]]}
@${@textsc{S-Fun*-Fixed*}}]
#:S-DFun
@@ -185,7 +185,7 @@
@<:[σ @${τ[α ↦ ⊤]}] \\
@<:R[R @${@R'}]}
@${@<:[@∀r[(@polydotα[α]) @f…[(@repeated{τ_a} @polydot[τ α]) R]]
- @f*[(@repeated{σ_a} σ*) @${@R'}]]}
+ @f*[(@repeated{σ_a} σ) @${@R'}]]}
@${@textsc{S-DFun-Fun*}}]
#:S-UnionSuper
diff --git a/from-dissertation-tobin-hochstadt/tausigma.rkt b/from-dissertation-tobin-hochstadt/tausigma.rkt
@@ -14,7 +14,7 @@
@acase{@symτ[@sym*] @tag*{symbol singleton}}
@acase{@Symbolτ @tag*{any symbol}}
@acase{@f→[(@repeated{τ}) R] @tag*{function}}
- @acase{@f*[(@repeated{τ} @${τ*}) R] @tag*{variadic function}}
+ @acase{@f*[(@repeated{τ} τ) R] @tag*{variadic function}}
@acase{@f…[(@repeated{τ} @polydot[τ α]) R]
@tag*{variadic polymorphic function}}
@acase{@∀r[(@repeated{α}) τ]@tag*{polymorphic type}}
diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt
@@ -116,7 +116,7 @@
@$inferrule[@${@Γ[@repeated{x:σ} @${x_r:@Listofτ[σ_r]} ⊢ e @R[τ φ⁺ φ⁻ o]]}
@${@Γ[⊢ @λe[(@repeated{x:σ} @${\ .\ } @${x_r:σ_r*}) e]
- @R[(f→ (@repeated{σ})
+ @R[(f* (@repeated{σ} σ_r)
@R[τ
ϵ
ϵ
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -22,9 +22,9 @@ the value stored in an instance of a constructor.
@cases*[
"e" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κ e]}
- @acase{(@ctor-pred[@κ]\ e)}
- @acase{(@ctor-val[@κ]\ e)}
+ @acase{@ctor[@κ e]@tag*{constructor instance}}
+ @acase{(@ctor-pred[@κ]\ e)@tag*{constructor predicate}}
+ @acase{(@ctor-val[@κ]\ e)@tag*{constructor value access}}
@interpar{
We also introduce expressions related to records. The first builds an instance
of a record with the given fields. We note that the order in which the fields
@@ -39,12 +39,13 @@ the value stored in an instance of a constructor.
the @ɐ field.
}
@acase{…}
- @acase{@record[@repeated{@↦e[@${@|ɐ|ᵢ} eᵢ]}]}
- @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ e)}
- @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ e)}@;added
- @acase{e.@|ɐ|}
- @acase{@opwith[e @|ɐ| e]}
- @acase{@opwithout[e @|ɐ|]}
+ @acase{@record[@repeated{@↦e[@${@|ɐ|ᵢ} eᵢ]}]@tag*{record instance}}
+ @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ e)@tag*{record predicate}}
+ @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ e)
+ @tag*{row-record predicate}}@;added
+ @acase{e.@|ɐ|@tag*{record field access}}
+ @acase{@opwith[e @|ɐ| e]@tag*{record update (new/changed field)}}
+ @acase{@opwithout[e @|ɐ|]@tag*{record update (removed field)}}
@interpar{
Finally, we define the row-polymorphic abstractions
@Λce[(@repeated{@ρc}) e] and @Λfe[(@repeated{@ρf}) e] which bind row
@@ -52,10 +53,10 @@ the value stored in an instance of a constructor.
instantiation operators are @atc[e @repeated{@ςc}] and @atf[e @repeated{@ςf}].
}
@acase{…}
- @acase{@Λce[(@repeated{@ρc}) e]}@; new
- @acase{@Λfe[(@repeated{@ρf}) e]}@; new
- @acase{@atc[e @repeated{@ςc}]}@; new
- @acase{@atf[e @repeated{@ςf}]}]@; new
+ @acase{@Λce[(@repeated{@ρc}) e]@tag*{row-polymorphic abstraction (constructors)}}@; new
+ @acase{@Λfe[(@repeated{@ρf}) e]@tag*{row-polymorphic abstraction (fields)}}@; new
+ @acase{@atc[e @repeated{@ςc}]@tag*{row-polymorphic instantiation (constructors)}}@; new
+ @acase{@atf[e @repeated{@ςf}]@tag*{row-polymorphic instantiation (fields)}}]@; new
@;{
Note: In the @${@record[@repeated{@|ɐ|ᵢ = eᵢ}]} expression, which builds a
diff --git a/scribblings/adt-row-tausigma.scrbl b/scribblings/adt-row-tausigma.scrbl
@@ -8,14 +8,12 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Types (with ρ)}
-@$${
- @cases["σ,τ" #:first-sep "⩴"
- @acase{…}
- @acase{@ctor[@κof[τ]]} @; same
- @acase{@record[@ςf]} @; changed
- @acase{@∀c[@${(@repeated{@ρc})} τ]} @; new
- @acase{@∀f[@${(@repeated{@ρf})} τ]}] @; new
-}
+@cases["σ,τ" #:first-sep "⩴"
+ @acase{…}
+ @acase{@ctor[@κof[τ]]} @; same
+ @acase{@record[@ςf]} @; changed
+ @acase{@∀c[(@repeated{@ρc}) τ]} @; new
+ @acase{@∀f[(@repeated{@ρf}) τ]}] @; new
@; new↓
@@ -36,16 +34,8 @@ constructors in the row type can be specified on variants.
@; new
@cases[@ςc #:first-sep "⩴"
@acase{@repeatset{@κof[τ]}}
- @acase{@ρc @repeatset{-@|κ|ᵢ} @repeatset{+@κof[ⱼ τⱼ]}
- @;@where \{@repeated{@|κ|ᵢ}\} ≠ \{@repeated{@|κ|ⱼ}\} ∀ i ≠ j
- }]
-
-@todo{Notation to indicate that all present and absent fields (resp.
- constructors) are different, including between the two (present vs absent)
- sets.}
+ @acase{@|ρc|\ @repeatset{-@|κ|ᵢ}\ @repeatset{+@κof[ⱼ τⱼ]}}]
@cases[@ςf #:first-sep "⩴"
@acase{@repeatset{@|ɐ|:τ}}
- @acase{@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}
- @;@where \{@repeated{@|ɐ|ᵢ}\} ≠ \{@repeated{@|ɐ|ⱼ}\} ∀ i ≠ j
- }]
+ @acase{@|ρf|\ @repeatset{-@|ɐ|ᵢ}\ @repeatset{+@|ɐ|ⱼ:τⱼ}}]
diff --git a/scribblings/adt-row-te.scrbl b/scribblings/adt-row-te.scrbl
@@ -8,29 +8,22 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Type validity rules (with ρ)}
-@$${
- @$inferrule[
- @${Δ ∪ \{ @repeated{@ρc} \} ⊢ τ}
- @${Δ ⊢ (∀_c (@repeated{@ρc}) τ)}
- @${@textsc{TE-CAll}}
- ]
-}
+@$inferrule[@${Δ ∪ \{ @repeated{@ρc} \} ⊢ τ}
+ @${Δ ⊢ @∀c[(@repeated{@ρc}) τ]}
+ @${@textsc{TE-CAll}}]
-@$${
- @$inferrule[
- @${Δ ∪ \{ @repeated{@ρf} \} ⊢ τ}
- @${Δ ⊢ (∀_f (@repeated{@ρf}) τ)}
- @${@textsc{TE-FAll}}
- ]
-}
+@$inferrule[@${Δ ∪ \{ @repeated{@ρf} \} ⊢ τ}
+ @${Δ ⊢ @∀f[(@repeated{@ρf}) τ]}
+ @${@textsc{TE-FAll}}]
-@$${
- @$inferrule[
- @${@ρf ∈ Δ \\ \{@repeated{@|ɐ|ᵢ}\} n \{@repeated{@|ɐ|ⱼ}\} = ∅ \\ @alldifferent(@repeated{@|ɐ|ᵢ}) \\ @alldifferent(@repeated{@|ɐ|ⱼ})}
+
+@$inferrule[
+ @${@ρc ∈ Δ \\
+ \{@repeated{@|ɐ|ᵢ}\} ∩ \{@repeated{@|ɐ|ⱼ}\} = ∅ \\
+ @alldifferent(@repeated{@|ɐ|ᵢ}) \\
+ @alldifferent(@repeated{@|ɐ|ⱼ})}
@${Δ ⊢ @record[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
- @${@textsc{TE-FXYZ}}
- ]
-}
+ @${@textsc{TE-FAllDifferent}}]
where
@@ -41,6 +34,14 @@ where
\end{aligned}
}
+@$inferrule[
+ @${@ρf ∈ Δ \\
+ \{@repeated{@|ɐ|ᵢ}\} ∩ \{@repeated{@|ɐ|ⱼ}\} = ∅ \\
+ @alldifferent(@repeated{@|ɐ|ᵢ}) \\
+ @alldifferent(@repeated{@|ɐ|ⱼ})}
+ @${Δ ⊢ @record[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
+ @${@textsc{TE-FAllDifferent}}]
+
@;{TODO: if we extend rows with subtraction, we may need to allow it either in
function types or within bodies too.
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -1,16 +1,16 @@
#lang at-exp racket
-@(provide (except-out (all-defined-out)
- num-e*
- num-τ*
- List…τ*
- Λc*
- Λf*))
+(provide (except-out (all-defined-out)
+ num-e*
+ num-τ*
+ List…τ*
+ Λc*
+ Λf*))
+
@require["util.rkt"
(only-in scribble/base emph)
scriblib/render-cond
(for-label (only-meta-in 0 typed/racket))]
-
@(require racket/list
(for-syntax racket/base syntax/parse racket/list))
@(begin-for-syntax
@@ -122,8 +122,12 @@
(define-syntax ∀r* (defop @${\mathbf{∀}}))
(define-syntax-rule (∀r (α ...) τ)
(∀r* @${(@(add-between (list (stringify α) ...) "\\ "))} τ))
-(define-syntax ∀c (defop @${\mathbf{∀}_{@textbf{c}}}))
-(define-syntax ∀f (defop @${\mathbf{∀}_{@textbf{f}}}))
+(define-syntax ∀c* (defop @${\mathbf{∀}_{@textbf{c}}}))
+(define-syntax ∀f* (defop @${\mathbf{∀}_{@textbf{f}}}))
+(define-syntax-rule (∀c (ρ ...) τ)
+ (∀c* @${(@(add-between (list (stringify ρ) ...) "\\ "))} τ))
+(define-syntax-rule (∀f (ρ ...) τ)
+ (∀f* @${(@(add-between (list (stringify ρ) ...) "\\ "))} τ))
(define-syntax-rule (ctor-pred c)
@${@(stringify c)@textbf{?}})
(define-syntax-rule (record-pred . f*)
@@ -174,7 +178,7 @@
(define-syntax-rule (f→ (from ...) R)
@${(@(add-between (list @(stringify from) ...) "\\ ") \mathbf{→} @(stringify R))})
(define-syntax-rule (f* (from ... rest*) R)
- (f→ (from ... @${\ \mathbf{.}\ } rest*) R))
+ (f→ (from ... @${\ \mathbf{.}\ } @${@(stringify rest*)@mathbm{*}}) R))
(define-syntax-rule (f… (from ... polydot) R)
(f→ (from ... @${\ \mathbf{.}\ } polydot) R))
(define-syntax (R stx)
@@ -311,4 +315,4 @@
tmp)]))
(define δe @${δ_{\mathrm{e}}})
-(define alldifferent @${\operatorname{alldifferent}})
-\ No newline at end of file
+(define alldifferent @${\operatorname{alldifferent}})
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -12,6 +12,7 @@
citet
generate-bibliography-section
(rename-out [note* note])
+ note.
define-footnote ;; TODO: does not use the (superscript …)
(all-from-out "abbreviations.rkt")
(all-from-out scribble-math)
@@ -215,6 +216,11 @@ html .MathJax_Display, html div.MathJax_Preview {
[latex (apply note content)]
[else (apply note content)]))
+(define (note. . content)
+ ;; TODO: move the . a bit to the left, or place the footnote number
+ ;; after it, also shifted a bit to the left.
+ (list (apply note* content) "."))
+
(define-runtime-path bib-path "bibliography.bib")
(define-bibtex-cite bib-path
~cite
