commit f1afb7e65c8c2f82974bdbb08eb459599c70bfce
parent f553454767c54d1bd7b2403158e050126cc19d19
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Fri, 11 Aug 2017 14:41:18 +0200
Finished operational semantics for Typed Racket.
Diffstat:
5 files changed, 189 insertions(+), 36 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/Ectx.rkt b/from-dissertation-tobin-hochstadt/Ectx.rkt
@@ -6,9 +6,11 @@
@; CC0 license.
@cases["E" #:first-sep "⩴"
- @acase{[] @tag*{program entry point}}
+ @acase{[⋅] @tag*{program entry point}}
;@acase{@app[E @repeated{e}]}; I think this case is not needed.
@acase{@app[@repeated{v} E @repeated{e}]@tag*{function application}}
@acase{@ifop[E e e]@tag*{conditional}}
@acase{@eq?op[E e]@tag*{symbol equality}}
- @acase{@eq?op[v E]}]
-\ No newline at end of file
+ @acase{@eq?op[v E]}
+ @acase{@mapop[E e]}
+ @acase{@mapop[v E]}]
+\ No newline at end of file
diff --git a/from-dissertation-tobin-hochstadt/operational-semantics.rkt b/from-dissertation-tobin-hochstadt/operational-semantics.rkt
@@ -7,14 +7,56 @@
#:E-Delta
-@$inferrule[@${δ(c,v) = v'}
- @${(c v) ↪ v'}
+@$inferrule[@${δ(@primop,@repeated{v}) = v'}
+ @${@app[@primop @repeated{v}] ↪ v'}
@${@textsc{E-Delta}}]
+#:E-DeltaE
+
+@$inferrule[@${@δe(e) = v}
+ @${e ↪ v'}
+ @${@textsc{E-DeltaE}}]
+
+#:δ-rules
+
+@$${
+ \begin{aligned}
+ δ(@textit{add1}, @num-v*{n}) &= @num-v*{n+1} & \\
+ δ(@textit{number?}, @num-v) &= @true-v & \\
+ δ(@textit{number?}, v) &= @false-v & @text{otherwise} \\
+ δ(@consp, v₁, v₂) &= @consv[v₁ v₂] & \\
+ δ(@textit{pair?}, @consv[v v]) &= @true-v & \\
+ δ(@textit{pair?}, v) &= @false-v & @text{otherwise} \\
+ δ(@textit{null?}, @null-v) &= @true-v & \\
+ δ(@textit{null?}, v) &= @false-v & @text{otherwise} \\
+ δ(@textit{identity}, v) &= v & \\
+ \end{aligned}
+}
+
+#:δe-rules
+
+@$${
+ \begin{aligned}
+ @δe(@num-e) = @num-v \\
+ @δe(@true-e) = @true-v \\
+ @δe(@false-e) = @false-v \\
+ @δe(@null-e) = @null-v \\
+ @δe(@λe[(@repeated{x:τ}) e]) = @λv[(@repeated{x_r:τ}) e] \\
+ @δe(@λe[(@repeated{x:τ} @${\ .\ } @${x_r:σ*}) e])
+ = @λv[(@repeated{x:τ} @${\ .\ } @${x:σ*}) e] \\
+ @δe(@λe[(@repeated{x:τ} @${\ .\ } @${x_r:@polydot[σ α]}) e])
+ = @λv[(@repeated{x:τ} @${\ .\ } @${x_r:@polydot[σ α]}) e] \\
+ @δe(@Λe[(@repeated{α}) e]) = @Λv[(@repeated{α}) e] \\
+ @δe(@Λe[(@repeated{α} @polydotα[β]) e]) = @Λe[(@repeated{α} @polydotα[β]) e] \\
+ @δe(@promisee[e]) = @promisev[e] \\
+ @δe(@syme[s]) = @symv[s]
+ \end{aligned}
+}
+
#:E-Beta
@$inferrule[-
- @${@app[@λe[(@repeated{x:τ}) e_b] @repeated{e_a}]
+ @${@app[@λv[(@repeated{x:τ}) e_b] @repeated{e_a}]
↪ e_b@subst[@repeated{x ↦ e_a}]}
@${@textsc{E-Beta}}]
@@ -22,41 +64,88 @@
@$inferrule[-
@${
- @app[@λe[(@repeated[#:n "n"]{x:τ} @${\ .\ } @${x_r:τ_r*}) e_b]
+ @app[@λv[(@repeated[#:n "n"]{x:τ} @${\ .\ } @${x_r:τ_r*}) e_b]
@repeated[#:n "n"]{e_a} @repeated[#:n "m"]{e_r}]
↪ e_b@subst[x_r ↦ @listv[@repeated[#:n "m"]{e_r}]
@repeated[#:n "n"]{x ↦ e_a}]}
@${@textsc{E-Beta*}}]
+#:E-BetaD
+
+@$inferrule[-
+ @${
+ @app[@λv[(@repeated[#:n "n"]{x:τ} @${\ .\ }
+ @${x_r:@polydot[τ_r α]}) e_b]
+ @repeated[#:n "n"]{e_a} @repeated[#:n "m"]{e_r}]
+ ↪ e_b@subst[x_r ↦ @listv[@repeated[#:n "m"]{e_r}]
+ @repeated[#:n "n"]{x ↦ e_a}]}
+ @${@textsc{E-BetaD}}]
+
#:E-TBeta
@$inferrule[-
- @${@at[@Λe[(@repeated{α}) e] @repeated{τ}] ↪ e}
+ @${@at[@Λv[(@repeated{α}) e] @repeated{τ}] ↪ e}
@${@textsc{E-TBeta}}]
#:E-TDBeta
@$inferrule[-
- @${@at[@Λe[(@repeated{α} @polydotα[β]) e] @repeated{τ}] ↪ e}
+ @${@at[@Λv[(@repeated{α} @polydotα[β]) e] @repeated{τ}] ↪ e}
@${@textsc{E-TDBeta}}]
@λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e]
-#:E-IfFalse
+#:E-If-False
@$inferrule[-
@${@ifop[@false-v e₂ e₃] ↪ e₃}
- @${@textsc{E-IfFalse}}]
+ @${@textsc{E-If-False}}]
-#:E-IfTrue
+#:E-If-True
-@$inferrule[-
- @${@ifop[@false-v e₂ e₃] ↪ e₃}
- @${@textsc{E-IfTrue}}]
+@$inferrule[@${v ≠ @false-v}
+ @${@ifop[v e₂ e₃] ↪ e₃}
+ @${@textsc{E-If-True}}]
+
+#:E-Force
+
+@$inferrule[@${e ↪ v}
+ @${@forcee[@promisev[e]] ↪ v}
+ @${@textsc{E-Force}}]
+
+#:E-Gensym
+
+@$inferrule[@${v = @sym* @text{ fresh}}
+ @${@gensyme[] ↪ v}
+ @${@textsc{E-Gensym}}]
+
+#:E-Eq?-True
+
+@$inferrule[@${v₁ = v₂}
+ @${@eq?op[v₁ v₂] ↪ @true-v}
+ @${@textsc{E-Eq?-True}}]
+
+#:E-Eq?-False
+
+@$inferrule[@${v₁ ≠ v₂}
+ @${@eq?op[v₁ v₂] ↪ @false-v}
+ @${@textsc{E-Eq?-False}}]
+
+#:E-Map-Pair
+
+@$inferrule[@${}
+ @${@mapop[v_f @consv[v₁ v₂]] ↪ @consp[@app[v_f v₁] @mapop[v_f v₂]]}
+ @${@textsc{E-Map-Pair}}]
+
+#:E-Map-Null
+
+@$inferrule[@${}
+ @${@mapop[v_f @null-v] ↪ @null-v}
+ @${@textsc{E-Map-Null}}]
#:E-Context
;; TODO: check what this means (and is it the right kind of arrow?)
@$inferrule[@${L ↪ R}
- @${E[L] → E[R]}
- @${@textsc{E-Context}}]
-\ No newline at end of file
+ @${E[L] ↪ E[R]}
+ @${@textsc{E-Context}}]
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -272,7 +272,7 @@ their result.
@include-equation["phi-psi-o-path.rkt" pe]
@subsubsub*section{Subtyping}
-The subtyping judgement is @${@<:[τ δ]}. It indicates that @${τ} is a
+The subtyping judgement is @${@<:[τ σ]}. It indicates that @${τ} is a
subtype of @${σ} (or that @${τ} and @${σ} are the same type).
The @<:* relation is reflexive and transitive. When two or more types are all
@@ -357,6 +357,40 @@ represent the type of the value assigned to a variadic polymorphic function's
@subsubsub*section{Operational semantics}
+The semantics for the simplest expressions and for primitive functions are
+expressed using δ-rules.
+
+@$p[@include-equation["operational-semantics.rkt" E-Delta]
+ @include-equation["operational-semantics.rkt" E-DeltaE]]
+
+@include-equation["operational-semantics.rkt" δ-rules]
+
+@include-equation["operational-semantics.rkt" δe-rules]
+
+The @textsc{E-Context} rule indicates that when the expression has the shape
+@${E[L]}, the subpart @${L} can be evaluated and replaced by its result. The
+syntax @${E[L]} indicates the replacement of the only occurrence of @${[⋅]}
+within an evaluation context @${E}. The evaluation context can then match an
+expression with the same shape, thereby separating the @${L} part from its
+context.
+
+@include-equation["operational-semantics.rkt" E-Context]
+
+The next rules handle β-reduction for the various flavours of functions.
+
+@$p[@include-equation["operational-semantics.rkt" E-Beta]
+ @include-equation["operational-semantics.rkt" E-Beta*]
+ @include-equation["operational-semantics.rkt" E-BetaD]]
+
+Instantiation of polymorphic abstractions is a no-op at run-time, because
+@typedracket performs type erasure (no typing information subsists at
+run-time, aside from the implicit tags used to distinguish the various
+primitive data types: pairs, numbers, symbols, @null-v, @true-v, @false-v,
+functions and promises).
+
+@$p[@include-equation["operational-semantics.rkt" E-TBeta]
+ @include-equation["operational-semantics.rkt" E-TDBeta]]
+
For simplicity, we assume that promises only contain pure expressions, and
therefore that the expression always produces the same value (modulo object
identity, i.e. pointer equality issues). In practice, @typedracket allows
@@ -368,21 +402,44 @@ pure. We note here that we implemented a small library for @typedracket which
allows the creation of promises encapsulating a pure expression, and whose
result is not cached.
-@$p[@include-equation["operational-semantics.rkt" E-Delta]
- @include-equation["operational-semantics.rkt" E-Beta]
- @include-equation["operational-semantics.rkt" E-Beta*]
- @include-equation["operational-semantics.rkt" E-TBeta]
- @include-equation["operational-semantics.rkt" E-TDBeta]
- @include-equation["operational-semantics.rkt" E-IfFalse]
- @include-equation["operational-semantics.rkt" E-IfTrue]
- @include-equation["operational-semantics.rkt" E-Context]]
+@include-equation["operational-semantics.rkt" E-Force]
+
+Once the evaluation context rule has been applied to evaluate the condition of
+an @ifop expression, the evaluation continues with the @emph{then} branch or
+with the @emph{else} branch, depending on the condition's value. Following
+@lisp tradition, all values other than @false-v are interpreted as a true
+condition.
+
+@$p[@include-equation["operational-semantics.rkt" E-If-False]
+ @include-equation["operational-semantics.rkt" E-If-True]]
+
+The @gensyme expression produces a fresh symbol @${@sym* ∈ 𝒮*}, which is
+guaranteed to be different from all symbol literals @${s ∈ 𝒮}, and different
+from all previous and future symbols returned by @|gensyme|. The @eq?op
+operator can then be used to compare symbol literals and symbols produced by
+@|gensyme|.
+
+@$p[@include-equation["operational-semantics.rkt" E-Gensym]
+ @include-equation["operational-semantics.rkt" E-Eq?-True]
+ @include-equation["operational-semantics.rkt" E-Eq?-False]]
+
+The semantics of @mapop are standard. We note here that @mapop can also be
+used as a first-class function in @typedracket, and the same can be achieved
+with the simplified semantics using the η-expansion
+@;
+@Λe[(α β) @λv[(@${x_f:@f→[(α) @R[β ϵ ϵ ∅]]}
+ @${x_l:@Listofτ[α]}) @mapop[x_f x_l]]]
+of the @mapop operator.
+
+@$p[@include-equation["operational-semantics.rkt" E-Map-Pair]
+ @include-equation["operational-semantics.rkt" E-Map-Null]]
@subsubsub*section{Type validity rules}
Polymorphic type variables valid types if they are bound, that is if they are
present in the @${Δ} environment. Additionally variadic (i.e. dotted)
polymorphic type variables may be present in the environment. When this is the
-case, they can be used as part of a @List…τ[τ α] type
+case, they can be used as part of a @List…τ[τ α] type.
@$p[@include-equation["te.rkt" TE-Var]
@include-equation["te.rkt" TE-DList]]
@@ -439,9 +496,9 @@ The rules below relate the simple expressions to their type.
Below are the rules for the various flavours of lambda functions and
polymorphic abstractions.
-@htodo{Technically, in the rules T-Abs and T-DAbs, we should keep any φ and o information concerning outer
- variables (those not declared within the lambda, and therefore still available
- after it finishes executing).}
+@htodo{Technically, in the rules T-Abs and T-DAbs, we should keep any φ and o
+ information concerning outer variables (those not declared within the lambda,
+ and therefore still available after it finishes executing).}
@todo{Should the φ⁺ φ⁻ o be preserved in T-TAbs and T-DTAbs?}
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -1,7 +1,6 @@
#lang at-exp racket
@(provide (except-out (all-defined-out)
num-e*
- num-v*
num-τ*
List…τ*))
@require["util.rkt"
@@ -279,4 +278,6 @@
[(_ filename eq)
(let ()
(local-require (only-in filename [eq tmp]))
- tmp)]))
-\ No newline at end of file
+ tmp)]))
+
+(define δe @${δ_{\mathrm{e}}})
+\ No newline at end of file
diff --git a/scribblings/state-of-the-art.scrbl b/scribblings/state-of-the-art.scrbl
@@ -71,8 +71,13 @@
spirit of implementing languages as
libraries@~cite["tobin-hochstadt_languages_as_libraries_2011"]}
-@asection{
- @atitle[#:tag "related-adt"]{Algebraic datatypes for compilers}
+@asection{ @atitle[#:tag "related-adt"]{Algebraic datatypes for compilers}
+ @epigraph["Personal communication from a friend"]{I used polymorphic variants
+ @htodo{this winter} to solve the @tt{assert false} problems in my @htodo{put
+ the language name here if I'm allowed to quote} lexical analyser, along with
+ some subtyping. You have to write the typecasts explicitly, but that aside it
+ is very powerful (a constructor can “belong” to several types etc.).}
+
The @tt{phc-adt} library implements algebraic datatypes (variants and
structures) which are adapted to compiler-writing.
