commit 92f25bef04476e1eaa7801f51beea8d345f88eff
parent b0f51da6c8d3e8d6fc3ed765aaea877087e1ad6c
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Sat, 8 Jul 2017 17:51:42 +0200
Started on row typing
Diffstat:
11 files changed, 140 insertions(+), 58 deletions(-)
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -6,7 +6,7 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Expressions}
+ #:version (version-text)]{Expressions (with ρ)}
@$${
@cases["e" #:first-sep "⩴"
@@ -18,7 +18,11 @@
@acase{(@record-pred[@repeated{@|ɐ|ᵢ}] e)}
@acase{e.@|ɐ|}
@acase{@opwith[e @|ɐ| e]}
- @acase{@opwithout[e @|ɐ|]}]
+ @acase{@opwithout[e @|ɐ|]}
+ @acase{@Λc[@${(@repeated{@ρc})} e]}@; new
+ @acase{@Λf[@${(@repeated{@ρf})} e]}@; new
+ @acase{@atc[e @repeated{@ρc}]}@; new
+ @acase{@atf[e @repeated{@ρf}]}]@; new
}
@;{
diff --git a/scribblings/adt-row-ectx.scrbl b/scribblings/adt-row-ectx.scrbl
@@ -6,7 +6,9 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Evaluation contexts}
+ #:version (version-text)]{Evaluation contexts (with ρ)}
+
+@todo{Does this need any change when adding row typing?}
@$${
@cases["E" #:first-sep "⩴"
diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl
@@ -6,7 +6,10 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Operational Semantics}
+ #:version (version-text)]{Operational Semantics (with ρ)}
+
+@todo{Does this need any change when adding row typing (they don't add any
+ rules in @~cite["tobin-hochstadt_typed_2010"])?}
@$${
@$inferrule[
@@ -71,9 +74,9 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]},
@$${
@aligned{
δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#t
- if v = @record[@repeated{@|ɐ|ⱼ = vⱼ}] ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ}
+ @textif v = @record[@repeated{@|ɐ|ⱼ = vⱼ}] ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ}
\\
- δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f otherwise
+ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f \text{ otherwise}
}
}
diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl
@@ -6,7 +6,9 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Path elements}
+ #:version (version-text)]{Path elements (with ρ)}
+
+@todo{Does this need any change when adding row typing?}
@$${pe ⩴ … @P @πctor-val @P @|ɐ|}
diff --git a/scribblings/adt-row-sub.scrbl b/scribblings/adt-row-sub.scrbl
@@ -6,7 +6,7 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Subtyping}
+ #:version (version-text)]{Subtyping (with ρ)}
@;{
@$${
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -7,12 +7,11 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Typing rules}
+ #:version (version-text)]{Typing rules (with ρ)}
@todo{Should the filter be something else than @${ϵ|ϵ} or is the filter inferred
via other rules when the ``function'' does not do anything special?}
-
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o}
@@ -21,7 +20,7 @@
]
}
-@${\mathop{applyfilter}} is defined
+@${\mathop{\textit{applyfilter}}} is defined
in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@htodo{their second (p. 75) definition of applyfilter does not clearly state
@@ -33,7 +32,8 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = applyfilter(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
+ φ_r
+ = \mathop{\textit{applyfilter}}(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
@${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Ctor-Pred}}
]
@@ -50,7 +50,9 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@πctor-val(π(x)) @& @textif o = π(x) @nl
∅ @& @otherwise
\end{array}\right. \\
- φ_r = applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val}, τ, o)}
+ φ_r
+ = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
+ τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
@${@textsc{T-Ctor-Val}}
]
@@ -68,7 +70,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = applyfilter(@record[@repeated{@|ɐ|ᵢ : ⊤}]
+ φ_r = \mathop{\textit{applyfilter}}(@record[@repeated{@|ɐ|ᵢ : ⊤}]
|\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Record-Pred}}
@@ -78,14 +80,16 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@cond-element[[latex @list{\let\savedamp&}] [else ""]]
@$inferrule[
- @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{@|ɐ|ᵢ : τᵢ}] \\
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{@|ɐ|ᵢ : τᵢ} @ρf] \\ @; changed
o_r = @"\\left\\{" \begin{array}{rl}
@πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl
∅ @& @otherwise
\end{array}\right. \\
- φ_r = applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}}, τ, o)}
+ φ_r
+ = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
+ τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
- @${@textsc{T-Record-Get}}
+ @${@textsc{T-Record-GetField}}
]
}
@@ -93,27 +97,36 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$inferrule[
@${
Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\
+ τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]\\@;c
Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
- @|ɐ| ∉ \{@|ɐ|ᵢ\}
+ @|ɐ| ∉ \{@|ɐ|ᵢ\} \\
+ @|ɐ| ∈ \{@repeated{@|ɐ|'ⱼ}\}
}
@${Γ ⊢ @opwith[@${e_{r}} @|ɐ| @${e_{v}}]
- : @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @${@|ɐ| : τ_{v}}]
+ : @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}
+ @${@|ɐ| : τ_{v}}
+ @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]@;changed
; ϵ|⊥ ; ∅}
@${@textsc{T-Record-With}_1}
]
}
+TODO: removing fields on the ρ should not matter if the fields are present in
+the main part of the record (as they are implicitly not in the ρ, because they
+are in the main part).
+
@$${
@$inferrule[
@${
Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\
+ τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\@;changed
Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
@|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
}
@${Γ ⊢ @opwith[@${e_{r}} @|ɐⱼ| @${e_{v}}]
- : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}} @${@|ɐ|ⱼ : τ_{v}}]
+ : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
+ @${@|ɐ|ⱼ : τ_{v}}
+ @ρf]@;changed
; ϵ|⊥ ; ∅}
@${@textsc{T-Record-With}_2}
]
@@ -123,11 +136,12 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$inferrule[
@${
Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\
+ τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\
@|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
}
@${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|]
- : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}]
+ : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
+ @${@ρf - @|ɐ|}]
; ϵ|⊥ ; ∅}
@${@textsc{T-Record-Without}}
]
diff --git a/scribblings/adt-row-ty.scrbl b/scribblings/adt-row-ty.scrbl
@@ -6,9 +6,72 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Types}
+ #:version (version-text)]{Types (with ρ)}
@$${σ,τ ⩴ …
- @P @ctor[@κ τ] @;{@P @ctorTop[τ]}
- @P @record[@repeated{@|ɐ|ᵢ : τᵢ}]}
+ @P @ctor[@κ τ] @; same
+ @P @variant[@repeated{@ctor[@|κ|ᵢ τᵢ]} @ρc] @; new/changed
+ @P @record[@repeated{@|ɐ|ᵢ : τᵢ} @repeatset{-@|ɐ|ᵢ} @${@ρf - @repeatset{@|ɐ|ⱼ}}] @; changed
+ @P (∀_c (@repeated{@ρc}) τ) @; new
+ @P (∀_f (@repeated{@ρf}) τ) @; new
+}
+@; new↓
+
+Type validity judgements (for well-scopedness):
+
+@todo{Just as TR distinguishes regular @${@repeated{α}} and dotted @${α
+ \mathbf{…}} type variables, we should distinguish @${@repeated{α}}, @${α
+ \mathbf{…}}, @ρc and @ρf variables (so four different notations.}
+
+@$${
+ @$inferrule[
+ @${Δ ∪ \{ @ρc \} ⊢ τ}
+ @${Δ ⊢ (∀_c (@ρc) τ)}
+ @${@textsc{TE-CAll}}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${Δ ∪ \{ @ρf \} ⊢ τ}
+ @${Δ ⊢ (∀_f (@ρf) τ)}
+ @${@textsc{TE-FAll}}
+ ]
+}
+
+@;{TODO: if we extend rows with subtraction, we may need to allow it either in
+ function types or within bodies too.
+
+ @$${
+ @$inferrule[
+ @${Δ ∪ \{ @ρc \} ⊢ τ}
+ @${Δ ⊢ ???}
+ @${@textsc{TE-CFun}}
+ ]
+ }
+
+ @$${
+ @$inferrule[
+ @${Δ ∪ \{ @ρf \} ⊢ τ}
+ @${Δ ⊢ ???}
+ @${@textsc{TE-FFun}}
+ ]
+ }
+}
+
+@$${
+ @$inferrule[
+ @${@ρc ∈ Δ \\ @repeated{Δ ⊢ τᵢ}}
+ @${Δ ⊢ @variant[@repeated{@ctor[@|κ|ᵢ τᵢ]} @ρc]}
+ @${@textsc{TE-CVariant}}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${@ρf ∈ Δ \\ @repeated{Δ ⊢ τᵢ}}
+ @${Δ ⊢ @record[@repeated{@|ɐ|ᵢ : τᵢ} @ρf]}
+ @${@textsc{TE-FRecord}}
+ ]
+}
+\ No newline at end of file
diff --git a/scribblings/adt-row-v.scrbl b/scribblings/adt-row-v.scrbl
@@ -6,7 +6,9 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Values}
+ #:version (version-text)]{Values (with ρ)}
+
+@todo{Does this need any change when adding row typing?}
@$${v ⩴ …
@P @ctor[@κ v]
diff --git a/scribblings/adt-trules.scrbl b/scribblings/adt-trules.scrbl
@@ -21,7 +21,7 @@
]
}
-@${\mathop{applyfilter}} is defined
+@${\mathop{\textit{applyfilter}}} is defined
in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@htodo{their second (p. 75) definition of applyfilter does not clearly state
@@ -33,7 +33,8 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = applyfilter(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
+ φ_r
+ = \mathop{\textit{applyfilter}}(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
@${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Ctor-Pred}}
]
@@ -50,7 +51,9 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@πctor-val(π(x)) @& @textif o = π(x) @nl
∅ @& @otherwise
\end{array}\right. \\
- φ_r = applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val}, τ, o)}
+ φ_r
+ = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
+ τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
@${@textsc{T-Ctor-Val}}
]
@@ -68,7 +71,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = applyfilter(@record[@repeated{@|ɐ|ᵢ : ⊤}]
+ φ_r = \mathop{\textit{applyfilter}}(@record[@repeated{@|ɐ|ᵢ : ⊤}]
|\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Record-Pred}}
@@ -83,9 +86,11 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl
∅ @& @otherwise
\end{array}\right. \\
- φ_r = applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}}, τ, o)}
+ φ_r
+ = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
+ τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
- @${@textsc{T-Record-Get}}
+ @${@textsc{T-Record-GetField}}
]
}
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -40,6 +40,8 @@
@(define ρf @${\rho_{f}})
@(define-syntax atc (defop "@${}_{\\textbf{c}}$"))
@(define-syntax atf (defop "@${}_{\\textbf{f}}$"))
+@(define-syntax Λc (defop "Λ${}_{\\textbf{c}}$"))
+@(define-syntax Λf (defop "Λ${}_{\\textbf{f}}$"))
@(define-syntax-rule (ctor-pred c)
@${@(stringify c)\mathbf{?}})
@(define-syntax-rule (record-pred f*)
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -110,30 +110,14 @@ The same applies to the accessor for a constructor's encapsulated value:
As a convenience, we will write @ctor[κ], @ctor-pred[κ] and @ctor-val[κ] as a
shorthand for the above lambda functions.
-
-
-
@asection{
@atitle{With row polymorphism}
-
- Types:
-
- @$${σ,τ ⩴ …
- @P (∀_c (@repeated{@ρc}) τ)
- @P (∀_c (@repeated{@ρf}) τ)
- @P @variant[@repeated{@ctor[@|κ|ᵢ τᵢ]} @ρc]
- @P @record[@repeated{@|ɐ|ᵢ : τᵢ} @ρf]}
-
- Elements:
-
- @$${e ⩴ … @P @atc[e @repeated{@ρc}] @P @atf[e @repeated{@ρf}]}
-
- @include-asection["adt-e.scrbl"]
- @include-asection["adt-v.scrbl"]
- @include-asection["adt-ectx.scrbl"]
- @include-asection["adt-ty.scrbl"]
- @include-asection["adt-sub.scrbl"]
- @include-asection["adt-pe.scrbl"]
- @include-asection["adt-trules.scrbl"]
- @include-asection["adt-opsem.scrbl"]
+ @include-asection["adt-row-e.scrbl"]
+ @include-asection["adt-row-v.scrbl"]
+ @include-asection["adt-row-ectx.scrbl"]
+ @include-asection["adt-row-ty.scrbl"]
+ @include-asection["adt-row-sub.scrbl"]
+ @include-asection["adt-row-pe.scrbl"]
+ @include-asection["adt-row-trules.scrbl"]
+ @include-asection["adt-row-opsem.scrbl"]
}
\ No newline at end of file
