commit 67ed49200cd9fa399474964b8bd7408f01751489 parent 64007502d433960e338e946b3ffb9e19bb999a0f Author: Georges Dupéron <georges.duperon@gmail.com> Date: Fri, 7 Jul 2017 12:53:41 +0200 Copied formalisation for row types, will make the necessary changes in the next commits. Diffstat:
| A | scribblings/adt-row-e.scrbl | | | 31 | +++++++++++++++++++++++++++++++ |
| A | scribblings/adt-row-ectx.scrbl | | | 25 | +++++++++++++++++++++++++ |
| A | scribblings/adt-row-opsem.scrbl | | | 125 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | scribblings/adt-row-pe.scrbl | | | 36 | ++++++++++++++++++++++++++++++++++++ |
| A | scribblings/adt-row-sub.scrbl | | | 50 | ++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | scribblings/adt-row-trules.scrbl | | | 134 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | scribblings/adt-row-ty.scrbl | | | 14 | ++++++++++++++ |
| A | scribblings/adt-row-v.scrbl | | | 13 | +++++++++++++ |
| M | scribblings/adt.scrbl | | | 9 | +++++++++ |
9 files changed, 437 insertions(+), 0 deletions(-)
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl @@ -0,0 +1,31 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Expressions} + +@$${ + @cases["e" #:first-sep "⩴" + @acase{…} + @acase{@ctor[@κ e]} + @acase{(@ctor-pred[@κ] e)} + @acase{(@ctor-val[@κ] e)} + @acase{@record[@repeated{@|ɐ|ᵢ = eᵢ}]} + @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] e)} + @acase{e.@|ɐ|} + @acase{@opwith[e @|ɐ| e]} + @acase{@opwithout[e @|ɐ|]}] +} + +@;{ + Note: In the @${@record[@repeated{@|ɐ|ᵢ = eᵢ}]} expression, which builds a + new record value, the @${@|ɐ|ᵢ} are ordered, and the field order defines the + order of evaluation, as indicated by the extensions to the @${E} contexts + which is given below. In other uses, the order of fields within the record is + irrelevant, i.e. the record can be assimilated to a set of 2-uples, of which + the first element is a field name, and the second a value or type. +} diff --git a/scribblings/adt-row-ectx.scrbl b/scribblings/adt-row-ectx.scrbl @@ -0,0 +1,25 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Evaluation contexts} + +@$${ + @cases["E" #:first-sep "⩴" + @acase{…} + @acase{@ctor[@κ E]} + @acase{(@ctor-pred[@κ] E)} + @acase{(@ctor-val[@κ] E)} + @acase{@record[@repeated{@|ɐ|ᵢ = vᵢ} + @${@|ɐ|ⱼ = E} + @repeated{@|ɐ|ₖ = eₖ}]} + @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] E)} + @acase{E.@|ɐ|} + @acase{@opwith[E @|ɐ| e]} + @acase{@opwith[v @|ɐ| E]} + @acase{@opwithout[E @|ɐ|]}] +} diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl @@ -0,0 +1,124 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Operational Semantics} + +@$${ + @$inferrule[ + @${\phantom{x}} + @${@ctor[@κ v] ↪ @ctor[@κ v]} + @${@textsc{E-Ctor-Build}} + ] +} + +@$${ + @$inferrule[ + @${\phantom{x}} + @${(@ctor-pred[@κ] v) ↪ δ(@ctor-pred[@κ], v)} + @${@textsc{E-Ctor-Pred}} + ] +} + +We extend the @${δ} relation to accept in its first position not only constant +functions (members of @${c}), but also members of families of operators +indexed by a constructor label or a field label, like @${@ctor-pred[@κ]}, +@${@ctor-val[@κ]} and @record-pred[@repeated{@|ɐ|ᵢ}] + +@$${ + @aligned{ + δ(@ctor-pred[@κ], v) &= \#t &@textif v = @ctor[@κ @${v'}] \\ + δ(@ctor-pred[@κ], v) &= \#f & \text{ otherwise} \\ + } +} + +@todo{Is it really necessary to use a δ-rule for E-Ctor-GetVal ?} + +@$${ + @$inferrule[ + @${\phantom{x}} + @${(@ctor-val[@κ] v) ↪ δ(@ctor-val[@κ], v)} + @${@textsc{E-Ctor-GetVal}} + ] +} + +@$${ + @aligned{ + δ(@ctor-val[@κ], @ctor[@κ @${v'}]) & = @${v'} + } +} + +@$${ + @$inferrule[ + @${\phantom{x}} + @${@record[@repeated{@|ɐ|ᵢ = vᵢ}] ↪ @record[@repeated{@|ɐ|ᵢ = vᵢ}]} + @${@textsc{E-Record-Build}} + ] +} + +@$${ + @$inferrule[ + @${\phantom{x}} + @${(@record-pred[@repeated{@|ɐ|ᵢ}] v) ↪ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v)} + @${@textsc{E-Record-Pred}} + ] +} + +@$${ + @aligned{ + δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#t + if v = @record[@repeated{@|ɐ|ⱼ = vⱼ}] ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ} + \\ + δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f otherwise + } +} + +@$${ + @$inferrule[ + @${@|ɐ|' ∈ @repeatset{@|ɐ|ᵢ} \\ @|ɐ|' = @|ɐ|ⱼ} + @${@record[@repeated{@|ɐ|ᵢ = vᵢ}].@|ɐ|' ↪ vⱼ} + @${@textsc{E-Record-GetField}} + ] +} + + +@todo{This ∖ does not make sense because we remove the label @|ɐ|' from a set of + label+value tuples. We must define a separate mathematical operator for removal + of a label+value tuple from a set based on the label.} +@$${ + @$inferrule[ + @${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}} + @${@opwith[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ} @${v'}] + ↪ @record[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}} + @${\quad @|ɐ|ⱼ = v'}] \\ + (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} + @${@textsc{E-Record-With}_1} + ] +} + +@todo{what to do with the = sign? The a = v sign is syntactical, but could + easily be understood as a meta comparison, instead of indicating the + association between the field and the value.} + +@$${ + @$inferrule[ + @${@|ɐ|' ∉ @repeatset{@|ɐ|ᵢ}} + @${@opwith[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|'} @${v'}] + ↪ @record[@repeatset{@|ɐ|ᵢ = vᵢ} @${\quad @${@|ɐ|'} = v'}]} + @${@textsc{E-Record-With}_2} + ] +} + +@$${ + @$inferrule[ + @${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}} + @${@opwithout[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ}] + ↪ @record[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}] \\ + (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} + @${@textsc{E-Record-Without}} + ] +} +\ No newline at end of file diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl @@ -0,0 +1,35 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Path elements} + +@$${pe ⩴ … @P @πctor-val @P @|ɐ|} + +We extend the metafunctions for paths given +in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${ + \mathop{update}} metafunction is used when using filters to restrict the type +of a (subpart of a) local variable in the @tt{then} and @tt{else} branches of +a conditional. + +@todo{∷ is not defined in@~cite["tobin-hochstadt_typed_2010"], we have to + define it.} + +@todo{How should I note cleanly these removals / replacements which refer to + an ɐ and its τ or @${v} inside the set of @${@|ɐ|ᵢ}?} + +@$${ + @aligned{ + \mathop{update}(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ}) + &= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}} + @${@|ɐ|ⱼ : @${\mathop{update}(τⱼ, υ_π)}}] + \\ + &\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\ + \mathop{update}(@ctor[@κ τ], υ_{π∷@πctor-val}) + &= @ctor[@κ @${\mathop{update}(τ, υ_π)}] + } +} +\ No newline at end of file diff --git a/scribblings/adt-row-sub.scrbl b/scribblings/adt-row-sub.scrbl @@ -0,0 +1,49 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Subtyping} + +@;{ + @$${ + @$inferrule[ + @${\phantom{x}} + @${⊢ @ctor[@κ τ] <: @ctorTop[τ]} + @${@textsc{S-CtorTop}} + ] + } +} + +@$${ + @$inferrule[ + @${⊢ τ <: τ'} + @${⊢ @ctor[@κ τ] <: @ctor[@κ @${τ'}]} + @${@textsc{S-Ctor}} + ] +} + +@$${ + @$inferrule[ + @${@repeated{⊢ τᵢ <: τ'ᵢ}} + @${⊢ @record[@repeated{@${@|ɐ|ᵢ : τᵢ}}] <: @record[@repeated{@${@|ɐ|ᵢ : τ'ᵢ}}]} + @${@textsc{S-Record}} + ] +} + +Permutation of the fields of a record type produces an equivalent type: + +@$${ + @$inferrule[ + @${\phantom{x}} + @${⊢ @record[@repeated{@${@|ɐ|ᵢ : τᵢ}} @repeated{@${@|ɐ|ⱼ : τⱼ}}] + <: @record[@repeated{@${@|ɐ|ⱼ : τⱼ}} @repeated{@${@|ɐ|ᵢ : τᵢ}}]} + @${@textsc{S-Record-Permuation}} + ] +} + +@todo{propagate our types up/down unions like the primitive ones (I think + Typed Racket does not do this everywhere it “should”).} +\ No newline at end of file diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl @@ -0,0 +1,134 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + scriblib/render-cond + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Typing rules} + +@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} + @${Γ ⊢ @ctor[@κ e] : @ctor[@κ τ] ; ϵ|⊥ ; ∅} + @${@textsc{T-Ctor-Build}} + ] +} + +@${\mathop{applyfilter}} is defined +in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"]. + +@htodo{their second (p. 75) definition of applyfilter does not clearly state + that ϵ in τ_ϵ means the empty path (actually, ϵ means an emtpy + \overrightarrow{?} for any such sequence. Also, τ_π matches τ, with π = ϵ (and + therefore τ_ϵ matches τ). So that's how Number|\overline{Number} gets processed + with the updated applyfilter.} + +@$${ + @$inferrule[ + @${Γ ⊢ e : τ ; φ ; o \\ + φ_r = applyfilter(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)} + @${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅} + @${@textsc{T-Ctor-Pred}} + ] +} + +@(define & @cond-element[[latex "\\savedamp"] [else "&"]]) +@(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]]) + +@$${ + @cond-element[[latex @list{\let\savedamp&}] [else ""]] + @$inferrule[ + @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@κ @${τ'}] \\ + o_r = @"\\left\\{" \begin{array}{rl} + @πctor-val(π(x)) @& @textif o = π(x) @nl + ∅ @& @otherwise + \end{array}\right. \\ + φ_r = applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val}, τ, o)} + @${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r} + @${@textsc{T-Ctor-Val}} + ] +} + +@$${ + @$inferrule[ + @${@repeated{Γ ⊢ eᵢ : τᵢ ; φᵢ ; oᵢ}} + @${Γ ⊢ @record[@repeated{@|ɐ|ᵢ = eᵢ}] + : @record[@repeated{@|ɐ|ᵢ = τᵢ}]; ϵ|⊥ ; ∅} + @${@textsc{T-Record-Build}} + ] +} + +@$${ + @$inferrule[ + @${Γ ⊢ e : τ ; φ ; o \\ + φ_r = applyfilter(@record[@repeated{@|ɐ|ᵢ : ⊤}] + |\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)} + @${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅} + @${@textsc{T-Record-Pred}} + ] +} + +@$${ + @cond-element[[latex @list{\let\savedamp&}] [else ""]] + @$inferrule[ + @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{@|ɐ|ᵢ : τᵢ}] \\ + o_r = @"\\left\\{" \begin{array}{rl} + @πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl + ∅ @& @otherwise + \end{array}\right. \\ + φ_r = applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}}, τ, o)} + @${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r} + @${@textsc{T-Record-Get}} + ] +} + +@$${ + @$inferrule[ + @${ + Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ + τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\ + Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\ + @|ɐ| ∉ \{@|ɐ|ᵢ\} + } + @${Γ ⊢ @opwith[@${e_{r}} @|ɐ| @${e_{v}}] + : @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @${@|ɐ| : τ_{v}}] + ; ϵ|⊥ ; ∅} + @${@textsc{T-Record-With}_1} + ] +} + +@$${ + @$inferrule[ + @${ + Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ + τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\ + Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\ + @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ} + } + @${Γ ⊢ @opwith[@${e_{r}} @|ɐⱼ| @${e_{v}}] + : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}} @${@|ɐ|ⱼ : τ_{v}}] + ; ϵ|⊥ ; ∅} + @${@textsc{T-Record-With}_2} + ] +} + +@$${ + @$inferrule[ + @${ + Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ + τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\ + @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ} + } + @${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|] + : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}] + ; ϵ|⊥ ; ∅} + @${@textsc{T-Record-Without}} + ] +} diff --git a/scribblings/adt-row-ty.scrbl b/scribblings/adt-row-ty.scrbl @@ -0,0 +1,14 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Types} + +@$${σ,τ ⩴ … + @P @ctor[@κ τ] @;{@P @ctorTop[τ]} + @P @record[@repeated{@|ɐ|ᵢ : τᵢ}]} + diff --git a/scribblings/adt-row-v.scrbl b/scribblings/adt-row-v.scrbl @@ -0,0 +1,13 @@ +#lang scribble/manual + +@require["util.rkt" + "adt-utils.rkt" + (for-label (only-meta-in 0 typed/racket))] +@(use-mathjax) + +@title[#:style (with-html5 manual-doc-style) + #:version (version-text)]{Values} + +@$${v ⩴ … + @P @ctor[@κ v] + @P @record[@repeated{@|ɐ|ᵢ = vᵢ}]} diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl @@ -127,4 +127,13 @@ shorthand for the above lambda functions. 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"] } \ No newline at end of file