commit 490cc6ead334216ef81f148f0919c9b3aabac9f1
parent e338b93d2ec4f61f983b26a0359ac2601584bdc7
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Thu, 6 Jul 2017 14:42:45 +0200
Before talking with David on Thursday
Diffstat:
5 files changed, 211 insertions(+), 32 deletions(-)
diff --git a/passes of the example compiler for Nanopass.odt b/passes of the example compiler for Nanopass.odt
Binary files differ.
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -23,18 +23,31 @@ from@~cite[#:precision "pp.62, 72 and 92" "tobin-hochstadt_typed_2010"]:
@(define-for-syntax (defop op)
(syntax-parser
[(_ :stringify ...)
- #`@${(\mathbf{@#,op}\ @(add-between (list #,@(syntax->list #'(→str ...)))
- "\\ "))}]))
+ #`@${(@(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 atc @${@"@"_{c}})
-@(define atf @${@"@"_{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)})
We define the universe of constructor names @${𝒞} as being equivalent to the
set of strings of unicode characters@htodo{Check in the implementation that
@@ -43,36 +56,71 @@ 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 ∈ 𝒞}
@$${ɐ ⩴ name ∈ ℱ}
-@$${e ⩴ … @P @ctor[ↄ e] @P @record[@repeated{ɐᵢ ↦ eᵢ}]}
+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:
-@$${v ⩴ … @P @ctor[ↄ v] @P @record[@repeated{ɐᵢ ↦ vᵢ}]}
+@$${v ⩴ … @P @ctor[@ↄ v] @P @record[@repeated{ɐᵢ ↦ vᵢ}]}
-The primitive operations are not modified.
+Primitive operations:
+
+@$${c ⩴ … @P \textit{ctor-val}}
Evaluation contexts:
-@$${E ⩴ …
- @P @ctor[ↄ E]
- @P @record[@repeated{ɐᵢ ↦ vᵢ} ɐⱼ ↦ E @repeated{ɐₖ ↦ eₖ}]}
+@$${
+ @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 ɐ]}]
+}
Types:
-@$${σ,τ ⩴ … @P @ctor[ↄ τ] @P @record[@repeated{ɐᵢ ↦ τᵢ}]}
+@$${σ,τ ⩴ … @P @ctor[@ↄ τ] @P @ctorTop[τ] @P @record[@repeated{ɐᵢ ↦ τᵢ}]}
-With row polymorphism;:
+Subtyping:
-@$${σ,τ ⩴ …
- @P (∀_c (@repeated{@ρc}) τ)
- @P (∀_c (@repeated{@ρf}) τ)
- @P @ctor[ↄ τ @ρc]
- @P @record[@repeated{ɐᵢ ↦ τᵢ} @ρf]}
+@$${
+ @$inferrule[
+ @${\phantom{x}}
+ @${⊢ @ctor[@ↄ τ] <: @ctorTop[τ]}
+ @${@textsc{S-CtorTop}}
+ ]
+}
-@$${e ⩴ … @P (@atc e @repeated{@ρc}) @P (@atf e @repeated{@ρf})}
+@$${
+ @$inferrule[
+ @${⊢ τ <: τ'}
+ @${⊢ @ctor[@ↄ τ] <: @ctor[@ↄ @${τ'}]}
+ @${@textsc{S-Ctor}}
+ ]
+}
We further define variants as a subset of the unions allowed by @|typedracket|
(including unions of the constructors defined above). Variants are equivalent
@@ -80,29 +128,153 @@ 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).
-@todo{What about rows here?}
@$${
\begin{gathered}
σ,τ ⩴ …
@P @variant[
- @repeated{@ctor[ↄᵢ τᵢ]}
- @repeated{@record[@repeated{ɐⱼₗ ↦ τⱼₗ}]}
- @${τ_{last}}]\\
- @where \{ɐⱼₗ …\} ≠ \{ɐₖₗ …\} ∀ j ≠ k
+ @repeated{@ctor[@ↄᵢ τᵢ]}
+ @;@repeated{@record[@repeated{ɐⱼₗ ↦ τⱼₗ}]}
+ @;@${τ_{last}}
+ ]@;\\
+ @;@where \{@repeated{ɐⱼₗ}\} ≠ \{@repeated{ɐₖₗ}\} ∀ j ≠ k
\end{gathered}
}
Path elements:
-@$${pe ⩴ … @P \mathbf{ctor-val} @P ɐ}
+@$${pe ⩴ … @P \textbf{ctor-val} @P ɐ}
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?}
+
+@$${
+ δ_τ(\textit{ctor-val})
+ = (∀ (τ) @ctorTop[τ] \xrightarrow[\textbf{ctor-val}]{ϵ|ϵ} τ)
+}
+
+@;{
+ @$${
+ @$inferrule[
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@ↄ @${τ'}]}
+ @${Γ ⊢ (\textit{ctor-val} e) : τ' ; ϵ|ϵ ; \textbf{ctor-val}(o)}
+ @${@textsc{T-Ctor-Val}}
+ ]
+ }
+}
+
+@$${
+ @$inferrule[
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{ɐᵢ ↦ τᵢ}]}
+ @${Γ ⊢ e.ɐⱼ : τ' ; ϵ|ϵ ; \textbf{ɐⱼ}(o)}
+ @${@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} \\
+ ɐ = ɐⱼ
+ }
+ @${Γ ⊢ @opwith[@${e_{r}} ɐ @${e_{v}}]
+ : @record[@repeated{ɐᵢ ↦ τᵢ}@${{}^{i≠j}} @${ɐ ↦ τ_{v}}]
+ ; ϵ|ϵ ; ∅}
+ @${@textsc{T-Record-With}_2}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${
+ Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
+ τ_{r} <: @record[@repeated{ɐᵢ ↦ τ'ᵢ}] \\
+ ɐ = ɐⱼ
+ }
+ @${Γ ⊢ @opwith[@${e_{r}} ɐ @${e_{v}}]
+ : @record[@repeated{ɐᵢ ↦ τᵢ}@${{}^{i≠j}}]
+ ; ϵ|ϵ ; ∅}
+ @${@textsc{T-Record-Without}}
+ ]
+}
+
+Semantics:
+
+@$${
+ @aligned{
+ δ(\textit{ctor-val}, @ctor[@ↄ v]) & = v
+ }
+}
+
+@$${
+ @$inferrule[
+ @${\phantom{x}}
+ @${(@ctor-pred[@ↄ] @ctor[@ↄ v]) ↪ \textit{\#t}}
+ @${@textsc{E-Ctor-Pred-True}}
+ ]
+}
+
+@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.}
+
+@$${
+ @$inferrule[
+ @${∄ v \text{ such that } w = @ctor[@ↄ v]}
+ @${(@ctor-pred[@ↄ] w) ↪ \textit{\#f}}
+ @${@textsc{E-Ctor-Pred-False}}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${\phantom{x}}
+ @${@opwith[E ɐ e] ↪ v}
+ @${@textsc{E-Record-With}}
+ ]
+}
+
+@;{
+ @$${
+ @$inferrule[
@${a \\ b}
@${c \\ d(e)}
@${@textsc{Foo}_y}
]
+ }
+
+ @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}]}
+ }
}
\ No newline at end of file
diff --git a/scribblings/phc-thesis.scrbl b/scribblings/phc-thesis.scrbl
@@ -38,6 +38,7 @@
@include-asection{introduction.scrbl}
@include-asection{state-of-the-art.scrbl}
@include-asection{initial-examples.scrbl}
+@include-asection{tr.scrbl}
@include-asection{tr-te-adt.scrbl}
@asection{ @atitle{Typed nanopass}
@asection{@atitle[#:tag "typed-nanotrees-chap"]{Typed nanopass on trees}}
diff --git a/scribblings/tr-te-adt.scrbl b/scribblings/tr-te-adt.scrbl
@@ -5,8 +5,7 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
- #:version (version-text)]{Type systems and Algebraic Datatypes}
+ #:version (version-text)]{Extensible type system and algebraic datatypes}
-@include-asection{tr.scrbl}
@include-asection{te.scrbl}
@include-asection{adt.scrbl}
\ No newline at end of file
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -149,6 +149,10 @@
height: auto !important;
clear: right;
margin-bottom: 1em !important;
+}
+
+.MathJax_Display {
+ margin: 2em 0 !important;
}"))))))
(define my-title
;; TODO: use this for the other wrapped procs in this file
@@ -530,11 +534,14 @@ EOCSS
($* (cond-element
[html (list "{\\rm "
(for/list ([c (in-string str)])
- (if (char-upper-case? c)
- (string c)
- (list "{\\small "
- (string (char-upcase c))
- "}")))
+ (cond
+ [(char=? c #\-)
+ "\\text{-}"]
+ [(char-upper-case? c)
+ (string c)]
+ [else (list "{\\small "
+ (string (char-upcase c))
+ "}")]))
"}")]
[else (list "\\text{\\textsc{" str "}}")])))
