commit e35b7db170c12a39a8fd08617a5f08f9620cdf84
parent 490cc6ead334216ef81f148f0919c9b3aabac9f1
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Fri, 7 Jul 2017 01:09:38 +0200
Mostly finished formalisation of ADTs without row polymorphism
Diffstat:
12 files changed, 544 insertions(+), 214 deletions(-)
diff --git a/scribblings/adt-e.scrbl b/scribblings/adt-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-ectx.scrbl b/scribblings/adt-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-opsem.scrbl b/scribblings/adt-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-pe.scrbl b/scribblings/adt-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-sub.scrbl b/scribblings/adt-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-trules.scrbl b/scribblings/adt-trules.scrbl
@@ -0,0 +1,128 @@
+#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)]{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}}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@κ @${τ'}] \\
+ o_r = @"\\left\\{" \begin{aligned}
+ @πctor-val(π(x)) & @textif o = π(x) \\
+ ∅ & @otherwise
+ \end{aligned}\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}}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{@|ɐ|ᵢ : τᵢ}] \\
+ o_r = @"\\left\\{" \begin{aligned}
+ @πɐ{@|ɐ|ⱼ}(π(x)) & @textif o = π(x) \\
+ ∅ & @otherwise
+ \end{aligned}\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{@|ɐ|ᵢ : τ'ᵢ}
+ }
+ @${Γ ⊢ @opwith[@${e_{r}} @|ɐ| @${e_{v}}]
+ : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}]
+ ; ϵ|⊥ ; ∅}
+ @${@textsc{T-Record-Without}}
+ ]
+}
diff --git a/scribblings/adt-ty.scrbl b/scribblings/adt-ty.scrbl
@@ -0,0 +1,15 @@
+#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-utils.rkt b/scribblings/adt-utils.rkt
@@ -0,0 +1,52 @@
+#lang at-exp racket
+@(provide (all-defined-out))
+@require["util.rkt"
+ (for-label (only-meta-in 0 typed/racket))]
+
+
+@(require racket/list
+ (for-syntax racket/base syntax/parse racket/list))
+@(begin-for-syntax
+ (define-syntax-class stringify
+ [pattern x:id #:when (identifier-binding #'x)
+ #:with →str #'x]
+ [pattern x:id #:with →str (datum->syntax #'x
+ (symbol->string (syntax-e #'x))
+ #'x)]
+ [pattern e #:with →str #'e]))
+@(define-for-syntax (defop op)
+ (syntax-parser
+ [(_ :stringify ...)
+ #`@${(@(add-between (list (string-append "\\textbf{" #,op "}")
+ #,@(syntax->list #'(→str ...)))
+ "\\ "))}]))
+@(define-syntax stringify
+ (syntax-parser
+ [(_ :stringify)
+ #'→str]))
+
+@(define-syntax ctor (defop "ctor"))
+@(define κ @${κ})
+@(define ɐ @${a})
+@(define-syntax ctorTop (defop "CtorTop"))
+@(define-syntax-rule (ctor-val κ)
+ @${\mathbf{getval}_@κ})
+@(define-syntax record (defop "record"))
+@(define-syntax variant (defop "V"))
+@(define (repeated . l) @${\overrightarrow{@l}})
+@(define (repeatset . l) @${\{\overrightarrow{@l}\}})
+@(define |P| @${\ |\ })
+@(define ρc @${\rho_{c}})
+@(define ρf @${\rho_{f}})
+@(define-syntax atc (defop "@${}_{\\textbf{c}}$"))
+@(define-syntax atf (defop "@${}_{\\textbf{f}}$"))
+@(define-syntax-rule (ctor-pred c)
+ @${@(stringify c)\mathbf{?}})
+@(define-syntax-rule (record-pred f*)
+ @${(\textbf{record?}\ @(stringify f*))})
+@(define-syntax-rule (opwith rec a v)
+ @list{@(stringify rec) \textbf{ with } @(stringify a) = @(stringify v)})
+@(define-syntax-rule (opwithout rec a)
+ @list{@(stringify rec) \textbf{ without } @(stringify a)})
+@(define πctor-val @${\textbf{getval}})
+@(define (πɐ . ɐ) @${\mathbf{@ɐ}})
+\ No newline at end of file
diff --git a/scribblings/adt-v.scrbl b/scribblings/adt-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
@@ -10,44 +10,9 @@
datatypes and row polymorphism}
We extend the formalisation
-from@~cite[#:precision "pp.62, 72 and 92" "tobin-hochstadt_typed_2010"]:
-
-@(require racket/list
- (for-syntax racket/base syntax/parse racket/list))
-@(begin-for-syntax
- (define-syntax-class stringify
- [pattern x:id #:with →str (datum->syntax #'x
- (symbol->string (syntax-e #'x))
- #'x)]
- [pattern e #:with →str #'e]))
-@(define-for-syntax (defop op)
- (syntax-parser
- [(_ :stringify ...)
- #`@${(@(add-between (list (string-append "\\textbf{" #,op "}")
- #,@(syntax->list #'(→str ...)))
- "\\ "))}]))
-@(define-syntax stringify
- (syntax-parser
- [(_ :stringify)
- #'→str]))
-
-@(define-syntax ctor (defop "ctor"))
-@(define ↄ @${ↄ})
-@(define-syntax ctorTop (defop "CtorTop"))
-@(define-syntax ctor-val (defop "ctor"))
-@(define-syntax record (defop "record"))
-@(define-syntax variant (defop "V"))
-@(define (repeated . l) @${\overrightarrow{@l}})
-@(define |P| @${\ |\ })
-@(define ρc @${\rho_{c}})
-@(define ρf @${\rho_{f}})
-@(define-syntax atc (defop "@${}_{\\textbf{c}}$"))
-@(define-syntax atf (defop "@${}_{\\textbf{f}}$"))
-@(define-syntax ctor-pred (defop "ctor-pred"))
-@(define-syntax-rule (opwith rec a v)
- @list{@(stringify rec) \textbf{ with } @(stringify a) = @(stringify v)})
-@(define-syntax-rule (opwithout rec a)
- @list{@(stringify rec) \textbf{ without } @(stringify a)})
+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
@@ -56,70 +21,22 @@ 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
constants, i.e. they are written literally in the program source.
-@$${@ↄ ⩴ name ∈ 𝒞}
-@$${ɐ ⩴ name ∈ ℱ}
-
-Expressions:
-
-@$${
- @cases["e" #:first-sep "⩴"
- @acase{…}
- @acase{@ctor[@ↄ e]}
- @acase{(@ctor-pred[@ↄ] e)}
- @acase{@record[@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.
-
-Values:
+@$${@κ ⩴ name ∈ 𝒞}
+@$${@ɐ ⩴ name ∈ ℱ}
-@$${v ⩴ … @P @ctor[@ↄ v] @P @record[@repeated{ɐᵢ ↦ vᵢ}]}
-
-Primitive operations:
-
-@$${c ⩴ … @P \textit{ctor-val}}
-
-Evaluation contexts:
-
-@$${
- @cases["E" #:first-sep "⩴"
- @acase{…}
- @acase{@ctor[@ↄ E]}
- @acase{(@ctor-pred[@ↄ] E)}
- @acase{@record[@repeated{ɐᵢ ↦ vᵢ} ɐⱼ ↦ E @repeated{ɐₖ ↦ eₖ}]}
- @acase{@opwith[E ɐ e]}
- @acase{@opwith[v ɐ E]}
- @acase{@opwithout[E ɐ]}]
-}
+@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"]
-Types:
-
-@$${σ,τ ⩴ … @P @ctor[@ↄ τ] @P @ctorTop[τ] @P @record[@repeated{ɐᵢ ↦ τᵢ}]}
-
-Subtyping:
-
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${⊢ @ctor[@ↄ τ] <: @ctorTop[τ]}
- @${@textsc{S-CtorTop}}
- ]
-}
+@;{
+ Primitive operations:
-@$${
- @$inferrule[
- @${⊢ τ <: τ'}
- @${⊢ @ctor[@ↄ τ] <: @ctor[@ↄ @${τ'}]}
- @${@textsc{S-Ctor}}
- ]
+ @$${c ⩴ … @P \textit{ctor-val}}
}
We further define variants as a subset of the unions allowed by @|typedracket|
@@ -132,149 +49,82 @@ values of two function types present in the same union).
\begin{gathered}
σ,τ ⩴ …
@P @variant[
- @repeated{@ctor[@ↄᵢ τᵢ]}
- @;@repeated{@record[@repeated{ɐⱼₗ ↦ τⱼₗ}]}
+ @repeated{@ctor[@|κ|ᵢ τᵢ]}
+ @;@repeated{@record[@repeated{@|ɐ|ⱼₗ : τⱼₗ}]}
@;@${τ_{last}}
]@;\\
- @;@where \{@repeated{ɐⱼₗ}\} ≠ \{@repeated{ɐₖₗ}\} ∀ j ≠ k
+ @;@where \{@repeated{@|ɐ|ⱼₗ}\} ≠ \{@repeated{@|ɐ|ₖₗ}\} ∀ j ≠ k
\end{gathered}
}
-Path elements:
+Notes: the polymorphic builder function for the @κ constructor which
+intuitively corresponds to @ctor[κ] can be written as the η-expansion of the
+@ctor[κ e] operator:
-@$${pe ⩴ … @P \textbf{ctor-val} @P ɐ}
+@$${(Λ (α) (λ ([x : α]) @ctor[κ x]))}
+The same applies to the predicate form of constructors:
-Typing rules:
+@$${(λ ([x : ⊤]) (@ctor-pred[κ] x))}
-@todo{Should the filter be something else than @${ϵ|ϵ} or is the filter inferred
- via other rules when the ``function'' does not do anything special?}
+The same applies to the accessor for a constructor's encapsulated value:
-@$${
- δ_τ(\textit{ctor-val})
- = (∀ (τ) @ctorTop[τ] \xrightarrow[\textbf{ctor-val}]{ϵ|ϵ} τ)
-}
+@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
-@;{
- @$${
- @$inferrule[
- @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@ↄ @${τ'}]}
- @${Γ ⊢ (\textit{ctor-val} e) : τ' ; ϵ|ϵ ; \textbf{ctor-val}(o)}
- @${@textsc{T-Ctor-Val}}
- ]
- }
-}
+@todo{Write their types here too.}
-@$${
- @$inferrule[
- @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{ɐᵢ ↦ τᵢ}]}
- @${Γ ⊢ e.ɐⱼ : τ' ; ϵ|ϵ ; \textbf{ɐⱼ}(o)}
- @${@textsc{T-Record-Get}}
- ]
-}
+As a convenience, we will write @ctor[κ], @ctor-pred[κ] and @ctor-val[κ] as a
+shorthand for the above lambda functions.
-@$${
- @$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} \\
- ɐ = ɐⱼ
- }
- @${Γ ⊢ @opwith[@${e_{r}} ɐ @${e_{v}}]
- : @record[@repeated{ɐᵢ ↦ τᵢ}@${{}^{i≠j}} @${ɐ ↦ τ_{v}}]
- ; ϵ|ϵ ; ∅}
- @${@textsc{T-Record-With}_2}
- ]
-}
+The polymorphic builder function for a record which
+intuitively corresponds to @record[@repeated{ɐ}] can be written as the
+η-expansion of the @record[@repeated{ɐ = e}] operator:
-@$${
- @$inferrule[
- @${
- Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{ɐᵢ ↦ τ'ᵢ}] \\
- ɐ = ɐⱼ
- }
- @${Γ ⊢ @opwith[@${e_{r}} ɐ @${e_{v}}]
- : @record[@repeated{ɐᵢ ↦ τᵢ}@${{}^{i≠j}}]
- ; ϵ|ϵ ; ∅}
- @${@textsc{T-Record-Without}}
- ]
-}
+@$${(Λ (@repeated{αᵢ}) (λ (@repeated{[xᵢ : αᵢ]}) @record[@repeated{ɐᵢ = xᵢ}]))}
-Semantics:
+The same applies to the predicate form of records:
-@$${
- @aligned{
- δ(\textit{ctor-val}, @ctor[@ↄ v]) & = v
+@;{
+ @$${
+ @aligned{
+ &(λ ([x : ⊤])\\
+ &\quad(Λ (@repeated{αᵢ})\\
+ &\qquad(λ (@repeated{[pᵢ : (⊤ \xrightarrow[∅]{αᵢ|\overline{αᵢ}} Boolean)]})\\
+ &\qquad\quad(@record-pred[@repeated{@|ɐ|ᵢ ? pᵢ}] x))}\\
}
}
@$${
- @$inferrule[
- @${\phantom{x}}
- @${(@ctor-pred[@ↄ] @ctor[@ↄ v]) ↪ \textit{\#t}}
- @${@textsc{E-Ctor-Pred-True}}
- ]
+ @aligned{
+ &(λ ([x : ⊤])\\
+ &\quad(@record-pred[@repeated{@|ɐ|ᵢ}] x))}\\
}
-@todo{The @${@ctor-pred[@ↄ]} should be a value too, and be a procedure type. Or
- we can say that the user manually wraps it in a λ if they need to pass it
- around as a value.}
+The same applies to the accessor for a constructor's encapsulated value:
-@$${
- @$inferrule[
- @${∄ v \text{ such that } w = @ctor[@ↄ v]}
- @${(@ctor-pred[@ↄ] w) ↪ \textit{\#f}}
- @${@textsc{E-Ctor-Pred-False}}
- ]
-}
+@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${@opwith[E ɐ e] ↪ v}
- @${@textsc{E-Record-With}}
- ]
-}
+@todo{Write their types here too.}
-@;{
- @$${
- @$inferrule[
- @${a \\ b}
- @${c \\ d(e)}
- @${@textsc{Foo}_y}
- ]
- }
+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:
+@asection{
+ @atitle{With row polymorphism}
- @$${e ⩴ … @P @atc[e @repeated{@ρc}] @P @atf[e @repeated{@ρf}]}
- }
+ 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}]}
}
\ No newline at end of file
diff --git a/scribblings/phc-thesis.scrbl b/scribblings/phc-thesis.scrbl
@@ -64,6 +64,7 @@
(add1 a)))
1))
+@;{
@aappendix{
@include-asection[(lib "phc-graph/scribblings/phc-graph-implementation.scrbl")]
@include-asection[(lib "phc-adt/scribblings/phc-adt-implementation.scrbl")]
@@ -72,6 +73,7 @@
@include-asection[
(lib "type-expander/scribblings/type-expander-implementation.scrbl")]
}
+}
@;{
Notes concerning tikz → SVG conversion:
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -37,8 +37,9 @@
acase
cases
frac
- textif
where
+ textif
+ otherwise
quad)
(require racket/stxparam
@@ -573,4 +574,5 @@ EOCSS
@list{\frac{@x}{@y}})
(define where @${\text{ where }})
(define textif @${\text{ if }})
+(define otherwise @${\text{ otherwise }})
(define quad @${\quad})
