commit d00836f0b1fcb98003c0e473ef5e06487f87c419 parent 1af3a0f761f03c70c47c56df44d1846a5a055a90 Author: Georges Dupéron <georges.duperon@gmail.com> Date: Sun, 13 Aug 2017 00:00:59 +0200 A few changes, added a paragraph describing the notations used. Diffstat:
21 files changed, 87 insertions(+), 59 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/Ectx.rkt b/from-dissertation-tobin-hochstadt/Ectx.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/GammaR.rkt b/from-dissertation-tobin-hochstadt/GammaR.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/deltarules.rkt b/from-dissertation-tobin-hochstadt/deltarules.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/e.rkt b/from-dissertation-tobin-hochstadt/e.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/envrt.rkt b/from-dissertation-tobin-hochstadt/envrt.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/operational-semantics.rkt b/from-dissertation-tobin-hochstadt/operational-semantics.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/p.rkt b/from-dissertation-tobin-hochstadt/p.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/phi-psi-o-path.rkt b/from-dissertation-tobin-hochstadt/phi-psi-o-path.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl @@ -56,6 +56,27 @@ relevant to our work@note{We informally describe a translation of our system implementation in section @todo{[??]} which does not rely on structs.}, and their inclusion in the following semantics would needlessly complicate things. +@subsubsub*section{Notations} + +We note a sequence of elements with @repeated{y}. When there is more than one +sequence involved in a rule or equation, we may use the notation +@repeated[#:n "n"]{y} to indicate that there are @${n} elements in the +sequence. Two sequences can that way be forced to have the same number of +elements. We represent a set of elements (an “unordered” sequence) with the +notation @repeatset{y}. The use of ellipses in @polydotα{α} does not indicate +the repetition of @${α}. Instead, it indicates that @${α} is a @emph{variadic} +polymorphic type variable: a placeholder for zero or more types which will be +substituted for occurrences of @${α} when the polymorphic type is +instantiated. These ellipses appear as such in the @typedracket source code, +and are the reason we use the notation @repeated{y} to indicate repetition, +instead of the ellipses commonly used for that purpose. + +We indicate the syntactical substitution of @${y} with @${z} in @${w} using +the notation @${w@subst[y ↦ z]}. When given several elements to replace, the +substitution operator performs a parallel substitution (that is, @${ + w@subst[x ↦ y y ↦ z]} will not replace the occurrences of @${y} introduced by +the first substitution). + @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 @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/subtyping.rkt b/from-dissertation-tobin-hochstadt/subtyping.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/tausigma.rkt b/from-dissertation-tobin-hochstadt/tausigma.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/te.rkt b/from-dissertation-tobin-hochstadt/te.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/from-dissertation-tobin-hochstadt/v.rkt b/from-dissertation-tobin-hochstadt/v.rkt @@ -1,4 +1,4 @@ -#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util +#lang at-exp s-exp phc-thesis/scribblings/equations-lang @; This file is NOT under the CC0 license, as it contains rules and definitions @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl @@ -20,8 +20,8 @@ the value stored in an instance of a constructor. "e" #:first-sep "⩴" @acase{…} @acase{@ctor[@κ e]} - @acase{(@ctor-pred[@κ] e)} - @acase{(@ctor-val[@κ] e)} + @acase{(@ctor-pred[@κ]\ e)} + @acase{(@ctor-val[@κ]\ e)} @intertext{@list[] We also introduce expressions related to records. The first builds an instance diff --git a/scribblings/adt-row-ectx.scrbl b/scribblings/adt-row-ectx.scrbl @@ -14,12 +14,13 @@ @cases["E" #:first-sep "⩴" @acase{…} @acase{@ctor[@κ E]} - @acase{(@ctor-pred[@κ] E)} - @acase{(@ctor-val[@κ] E)} + @acase{(@ctor-pred[@κ]\ E)} + @acase{(@ctor-val[@κ]\ E)} @acase{@record[@repeated{@|ɐ|ᵢ = vᵢ} @${@|ɐ|ⱼ = E} @repeated{@|ɐ|ₖ = eₖ}]} - @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] E)} + @acase{(@record-pred[@repeated{@|ɐ|ᵢ}]\ E)} + @acase{(@record-pred*[@repeated{@|ɐ|ᵢ} @repeated{-@|ɐ|ⱼ}]\ E)} @acase{E.@|ɐ|} @acase{@opwith[E @|ɐ| e]} @acase{@opwith[v @|ɐ| E]} diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl @@ -8,6 +8,22 @@ @title[#:style (with-html5 manual-doc-style) #:version (version-text)]{Operational Semantics (with ρ)} +@list{ + + Instantiation of the new sorts of polymorphic abstractions is a no-op at + run-time, similarly to those of @|typedracket|. + + @;; New: + @$p[@$inferrule[- + @${@atc[e @repeated{@ρc}] ↪ e} + @${@textsc{E-Inst-C}}] + + @$inferrule[- + @${@atf[e @repeated{@ρf}] ↪ e} + @${@textsc{E-Inst-F}}]] +} + + @todo{Does this need any change when adding row typing (they don't add any rules in @~cite["tobin-hochstadt_typed_2010"])?} @@ -77,7 +93,7 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]}, @textif v = @record[@repeated{@|ɐ|ⱼ = vⱼ}] ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ} \\ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f @text[" otherwise"] - } + } } @$${ @@ -98,7 +114,7 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]}, @${@opwith[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ} @${v'}] ↪ @record[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}} @${\quad @|ɐ|ⱼ = v'}] \\ - (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} + (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} @${@textsc{E-Record-With}_1} ] } @@ -121,7 +137,7 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]}, @${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}} @${@opwithout[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ}] ↪ @record[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}] \\ - (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} + (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} @${@textsc{E-Record-Without}} ] } \ No newline at end of file diff --git a/scribblings/adt-row-v.scrbl b/scribblings/adt-row-v.scrbl @@ -8,8 +8,6 @@ @title[#:style (with-html5 manual-doc-style) #:version (version-text)]{Values (with ρ)} -@todo{Does this need any change when adding row typing?} - @$${v ⩴ … @P @ctor[@κ v] @P @record[@repeated{@|ɐ|ᵢ = vᵢ}]} diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl @@ -10,40 +10,32 @@ datatypes and row polymorphism} We extend the formalisation -from@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"]: +from@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"]. @require["adt-utils.rkt"] We define the universe of constructor names @${𝒞} as being equivalent to the set of strings of unicode characters@htodo{Check in the implementation that this is not equivalent to the set of symbols, as these cannot be serialised.}, -and the universe of field names @${ℱ} likewise (the distinction is purely in -the way that they are used). Constructor and field names are compile-time +and the universe of field names @${ℱ} likewise (the distinction resides only +in their intended use). Constructor and field names are compile-time constants, i.e. they are written literally in the program source. @$${@κ ⩴ name ∈ 𝒞} @$${@ɐ ⩴ name ∈ ℱ} -@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"] - -@;{ - Primitive operations: - - @$${c ⩴ … @P @textit{ctor-val}} -} +@include-asection["adt-row-e.scrbl"] +@include-asection["adt-row-v.scrbl"] +@include-asection["adt-row-ectx.scrbl"] +@include-asection["adt-row-ty.scrbl"] We further define variants as a subset of the unions allowed by @|typedracket| (including unions of the constructors defined above). Variants are equivalent to the union of their cases, but guarantee that pattern matching can always be -performed (for example, it is not possible in @|typedracket| to distinguish the -values of two function types present in the same union). +performed (for example, it is not possible in @|typedracket| to distinguish +the values of two function types present in the same union, and it is +therefore impossible to write a pattern matching expression which handles the +two cases differently). @$${ \begin{gathered} @@ -57,24 +49,24 @@ values of two function types present in the same union). \end{gathered} } -@asection{ - @atitle{With row polymorphism} - @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"] - @include-asection["adt-row-shorthands.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"] +@include-asection["adt-row-shorthands.scrbl"] + +@;{ + Primitive operations: + + @$${c ⩴ … @P @textit{ctor-val}} +} -@todo{Argue that a type system with symbols, unique tokens (a way to create a - fresh "identity", like (cons 0 0) creates a fresh memory cell which is not eq? - to any other, past or future), untagged unions, pure case→ functions with the - usual polymorphism and row polymorphism (ranging over function cases, with +@todo{Argue that, setting aside concerns like serialisation and performance, a + type system with symbols, unique tokens (a way to create a fresh "identity", + like (cons 0 0) creates a fresh memory cell which is not eq? to any other, + past or future), untagged unions, pure case→ functions with the usual + polymorphism and row polymorphism (ranging over function cases, with negation), i.e. a simplification / generalisation of our system, is more "general" than @typedracket (i.e. Racket's existing types can be easily encoded with ours), and show how other systems of variants and records can be diff --git a/from-dissertation-tobin-hochstadt/lang-util.rkt b/scribblings/equations-lang.rkt