commit bed4b0f73dec22e4fb8ad66d9d547a2be6426051
parent 30f4d29c56fd29de55a9f076ffcf4c7e7545e4c0
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 23 Aug 2017 21:03:26 +0200
Used propper subsections for the Typed Racket formalisation.
Diffstat:
2 files changed, 672 insertions(+), 613 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -56,544 +56,588 @@ 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 be forced to have the same number of elements in
-that way. 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. FInally,
-an empty sequence of repeated elements is sometimes noted @${ϵ}
-
-The judgements are written following the usual convention, where @${Γ} is the
-environment which associates variables to their type. The @${Δ} environment
-contains the type variables within scope, and is mostly used to determine the
-validity of types.
-
-@$${@Γ[⊢ e R]}
-
-The environments can be extended as follows:
-
-@$${@Γ[@${x : τ} Δ @${\{α\}} ⊢ e R]}
-
-The typing information @R associated with an expression contains the type of
-the expression, as well as aliasing information and other propositions which
-are known to be conditionally true depending on the value of the expression at
-run-time. These pieces of information are described in more detail
-@tech[#:key "R-typing-info"]{below}. Since the typing information @R is often
-inlined in the typing judgement, a typing judgement will generally have the
-following form:
-
-@$${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]]}
-
-In this notation, the @${+} and @${-} signs in @${φ⁺} and @${φ⁻} are purely
-syntactical, and serve to distinguish the positive and negative filters, which
-are instances of the nonterminal @${φ}.
-
-The various nonterminals used throughout the language are written in italics
-and are defined using the notation:
-
-@cases[@textit{nonterminal} #:first-sep "⩴"
- @acase{@textit{first case}}
- @acase{@textit{second case}}
- @acase{@textit{and so on}}]
-
-Additionally, a symbol assigned to a nonterminal may be used as a placeholder
-in rules and definitions, implicitly indicating that the element used to fill
-in that placeholder should be an instance of the corresponding nonterminal.
-When multiple such placeholders are present in a rule, they will be
-subscripted to distinguish between the different occurrences. The subscripts
-@${i}, @${j}, @${k} and @${l} are often used for repeated sequences.
-
-In later chapters, we extend already-defined non-terminals using the notation:
+@asection{
+ @atitle{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 be forced to have the same number of elements in
+ that way. 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. FInally,
+ an empty sequence of repeated elements is sometimes noted @${ϵ}
+
+ The judgements are written following the usual convention, where @${Γ} is the
+ environment which associates variables to their type. The @${Δ} environment
+ contains the type variables within scope, and is mostly used to determine the
+ validity of types.
+
+ @$${@Γ[⊢ e R]}
+
+ The environments can be extended as follows:
+
+ @$${@Γ[@${x : τ} Δ @${\{α\}} ⊢ e R]}
+
+ The typing information @R associated with an expression contains the type of
+ the expression, as well as aliasing information and other propositions which
+ are known to be conditionally true depending on the value of the expression at
+ run-time. These pieces of information are described in more detail
+ @tech[#:key "R-typing-info"]{below}. Since the typing information @R is often
+ inlined in the typing judgement, a typing judgement will generally have the
+ following form:
+
+ @$${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]]}
+
+ In this notation, the @${+} and @${-} signs in @${φ⁺} and @${φ⁻} are purely
+ syntactical, and serve to distinguish the positive and negative filters, which
+ are instances of the nonterminal @${φ}.
+
+ The various nonterminals used throughout the language are written in italics
+ and are defined using the notation:
+
+ @cases[@textit{nonterminal} #:first-sep "⩴"
+ @acase{@textit{first case}}
+ @acase{@textit{second case}}
+ @acase{@textit{and so on}}]
+
+ Additionally, a symbol assigned to a nonterminal may be used as a placeholder
+ in rules and definitions, implicitly indicating that the element used to fill
+ in that placeholder should be an instance of the corresponding nonterminal.
+ When multiple such placeholders are present in a rule, they will be
+ subscripted to distinguish between the different occurrences. The subscripts
+ @${i}, @${j}, @${k} and @${l} are often used for repeated sequences.
+
+ In later chapters, we extend already-defined non-terminals using the notation:
-@cases[@textit{nonterminal} #:first-sep "⩴"
- @acase{…}
- @acase{@textit{new case}}
- @acase{@textit{other new case}}]
-
-Typing rules and other rules are described following the usual natural
-deduction notation.
+ @cases[@textit{nonterminal} #:first-sep "⩴"
+ @acase{…}
+ @acase{@textit{new case}}
+ @acase{@textit{other new case}}]
-@$inferrule[@${@textit{hypothesis}\\ @textit{other hypothesis}}
- @${@textit{deduction}}
- @${@textsc{Rule-Name}}]
+ Typing rules and other rules are described following the usual natural
+ deduction notation.
-Metafunctions (i.e. functions which operate on types as syntactical elements,
-or on other terms of the language) are written in a roman font. The meta-values
-@|metatrue| and @|metafalse| indicate logical truth and falsehood respectively.
+ @$inferrule[@${@textit{hypothesis}\\ @textit{other hypothesis}}
+ @${@textit{deduction}}
+ @${@textsc{Rule-Name}}]
-@$${\mathrm{metafunction}(x,y) = \begin{cases}
- @metatrue &@textif x = y + 1\\
- @metafalse &@otherwise
- \end{cases}}
+ Metafunctions (i.e. functions which operate on types as syntactical elements,
+ or on other terms of the language) are written in a roman font. The meta-values
+ @|metatrue| and @|metafalse| indicate logical truth and falsehood respectively.
-Language operators are written in bold face:
+ @$${\mathrm{metafunction}(x,y) = \begin{cases}
+ @metatrue &@textif x = y + 1\\
+ @metafalse &@otherwise
+ \end{cases}}
-@cases["e" #:first-sep "⩴"
- @acase{@num-e}
- @acase{…}]
+ Language operators are written in bold face:
-Values are written using a bold italic font:
+ @cases["e" #:first-sep "⩴"
+ @acase{@num-e}
+ @acase{…}]
-@cases["v" #:first-sep "⩴"
- @acase{@num-v}
- @acase{…}]
+ Values are written using a bold italic font:
-Type names start with a capital letter, and are written using a bold font:
+ @cases["v" #:first-sep "⩴"
+ @acase{@num-v}
+ @acase{…}]
-@cases["τ,σ" #:first-sep "⩴"
- @acase{@num-τ}
- @acase{…}]
+ Type names start with a capital letter, and are written using a bold font:
-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).
+ @cases["τ,σ" #:first-sep "⩴"
+ @acase{@num-τ}
+ @acase{…}]
-@todo{Succinctly describe the other conventions used in the thesis, if any
- were omitted above.}
+ 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).
-@todo{Define the meta substitution and equality operators precisely.}
+ @todo{Succinctly describe the other conventions used in the thesis, if any
+ were omitted above.}
-@subsubsub*section{Names and bindings}
+ @todo{Define the meta substitution and equality operators precisely.}
-In the following sections, we assume that all type variable names which occur
-in binding positions are unique. This assumption could be made irrelevant by
-explicitly renaming in the rules below all type variables to fresh unique
-ones. Performing this substitution would be a way of encoding a notion of
-scope and the possibility for one identifier to hide another. However, the
-Racket language features macros which routinely produce new binding forms. The
-macro system in Racket is a hygienic one, and relies on a powerful model of
-the notion of scope@~cite["flatt2016binding"]. Extending the rules below with
-a simplistic model of Racket's notion of scope would not do justice to the
-actual system, and would needlessly complicate the rules. Furthermore,
-@typedracket only typechecks fully-expanded programs. In these programs, the
-binding of each identifier has normally been determined@note.{@Typedracket
- actually still determines the binding for type variables by itself, but we
- consider this is an implementation detail.}
+}
+
+@asection{
+ @atitle{Names and bindings}
+
+ In the following sections, we assume that all type variable names which occur
+ in binding positions are unique. This assumption could be made irrelevant by
+ explicitly renaming in the rules below all type variables to fresh unique
+ ones. Performing this substitution would be a way of encoding a notion of
+ scope and the possibility for one identifier to hide another. However, the
+ Racket language features macros which routinely produce new binding forms. The
+ macro system in Racket is a hygienic one, and relies on a powerful model of
+ the notion of scope@~cite["flatt2016binding"]. Extending the rules below with
+ a simplistic model of Racket's notion of scope would not do justice to the
+ actual system, and would needlessly complicate the rules. Furthermore,
+ @typedracket only typechecks fully-expanded programs. In these programs, the
+ binding of each identifier has normally been determined@note.{@Typedracket
+ actually still determines the binding for type variables by itself, but we
+ consider this is an implementation detail.}
+
+}
+
+@asection{
+ @atitle{Expressions}
+
+ The following expressions are available in the subset of @typedracket which we
+ consider. These expressions include references to variables, creation of basic
+ values (numbers, booleans, lists of pairs ending with @null-v, symbols,
+ promises), a variety of lambda functions with different handling of @emph{
+ rest} arguments (fixed number of arguments, polymorphic functions with a
+ uniform list of @emph{rest} arguments and variadic polymorphic functions, as
+ well as polymorphic abstractions), a small sample of primitive functions which
+ are part of Racket's library and a few operations manipulating these values
+ (function application and polymorphic instantiation, forcing promises, symbol
+ comparison and so on).
-@subsubsub*section{Expressions}
+ @include-equation["e.rkt"]
-The following expressions are available in the subset of @typedracket which we
-consider. These expressions include references to variables, creation of basic
-values (numbers, booleans, lists of pairs ending with @null-v, symbols,
-promises), a variety of lambda functions with different handling of @emph{
- rest} arguments (fixed number of arguments, polymorphic functions with a
-uniform list of @emph{rest} arguments and variadic polymorphic functions, as
-well as polymorphic abstractions), a small sample of primitive functions which
-are part of Racket's library and a few operations manipulating these values
-(function application and polymorphic instantiation, forcing promises, symbol
-comparison and so on).
+ Symbol literals are noted as @${s ∈ 𝒮} and the universe of symbols (which
+ includes symbol literals and fresh symbols created via @gensyme[]) is noted as
+ @${@sym* ∈ @𝒮*}.
-@include-equation["e.rkt"]
+ @include-equation["e.rkt" sym]
-Symbol literals are noted as @${s ∈ 𝒮} and the universe of symbols (which
-includes symbol literals and fresh symbols created via @gensyme[]) is noted as
-@${@sym* ∈ @𝒮*}.
+}
-@include-equation["e.rkt" sym]
+@asection{
+ @atitle{Primitive operations (library functions)}
-@subsubsub*section{Primitive operations (library functions)}
+ Racket offers a large selection of library functions, which we consider as
+ primitive operations. A few of these are listed below, and their type is given
+ later after, once the type system has been introduced. @textit{number?},
+ @textit{pair?} and @textit{null?} are predicates for the corresponding type.
+ @textit{car} and @textit{cdr} are accessors for the first and second elements
+ of a pair, which can be created using @|consp|. The @textit{identity} function
+ returns its argument unmodified, and @textit{add1} returns its numeric
+ argument plus 1. These last two functions are simply listed as examples.
-Racket offers a large selection of library functions, which we consider as
-primitive operations. A few of these are listed below, and their type is given
-later after, once the type system has been introduced. @textit{number?},
-@textit{pair?} and @textit{null?} are predicates for the corresponding type.
-@textit{car} and @textit{cdr} are accessors for the first and second elements
-of a pair, which can be created using @|consp|. The @textit{identity} function
-returns its argument unmodified, and @textit{add1} returns its numeric
-argument plus 1. These last two functions are simply listed as examples.
+ @include-equation["p.rkt"]
-@include-equation["p.rkt"]
+}
-@subsubsub*section{Values}
+@asection{
+ @atitle{Values}
-These expressions and primitive functions may produce or manipulate the
-following values:
+ These expressions and primitive functions may produce or manipulate the
+ following values:
-@include-equation["v.rkt"]
+ @include-equation["v.rkt"]
-The @listv value notation is defined as a shorthand for a @|null-v|-terminated
-linked list of pairs.
+ The @listv value notation is defined as a shorthand for a @|null-v|-terminated
+ linked list of pairs.
-@include-equation["v.rkt" listv]
+ @include-equation["v.rkt" listv]
+}
@;{
- @subsubsub*section{Run-time environment}
-
- Lambda functions are closures over their execution environment. The execution
- environment maps to their value those variables which were within the scope of
- the closure. In principle, it also maps type variables and dotted type
- variables to the type or types used to instantiate the polymorphic functions
- which are part of the scope of the closure. Typed Racket uses @emph{type
- erasure} however, that is to say that the compile-time type of values does not
- persist at run-time. Primitive types are still implicitly tagged with their
- type (which allows for untagged unions and predicates such as
- @racket[number?]), but the type of a function cannot be determined at run-time
- for example. This means that the type-variable-to-type mapping of @${ℰ} is not
- effectively present at run-time with the current implementation of Typed
- Racket.
-
- @include-equation["envrt.rkt"]
+ @asection{
+ @atitle{Run-time environment}
+
+ Lambda functions are closures over their execution environment. The execution
+ environment maps to their value those variables which were within the scope of
+ the closure. In principle, it also maps type variables and dotted type
+ variables to the type or types used to instantiate the polymorphic functions
+ which are part of the scope of the closure. Typed Racket uses @emph{type
+ erasure} however, that is to say that the compile-time type of values does
+ not persist at run-time. Primitive types are still implicitly tagged with
+ their type (which allows for untagged unions and predicates such as
+ @racket[number?]), but the type of a function cannot be determined at run-time
+ for example. This means that the type-variable-to-type mapping of @${ℰ} is
+ not effectively present at run-time with the current implementation of Typed
+ Racket.
+
+ @include-equation["envrt.rkt"]
+ }
}
-@subsubsub*section{Evaluation contexts}
+@asection{
+ @atitle{Evaluation contexts}
-The operational semantics given below rely on the following evaluation
-contexts:
+ The operational semantics given below rely on the following evaluation
+ contexts:
-@include-equation["Ectx.rkt"]
+ @include-equation["Ectx.rkt"]
-@; TODO: are other cases needed?
+ @; TODO: are other cases needed?
-@subsubsub*section{Typing judgement}
+}
+
+@asection{
+ @atitle{Typing judgement}
+
+ @;{
+ The type system of @typedracket relies on the following typing judgement. It
+ indicates that the expression @${e} has type @${τ}. Additionally, if the
+ run-time value of @${e} is @false-v then the propositions contained in @${φ⁻}
+ are valid. If the run-time value of @${e} is not @false-v, then the
+ propositions contained in @${φ⁺} are valid. Finally, @${e} is an alias for the
+ @object @${o}. We use here the same terminology as
+ @~cite["tobin-hochstadt_typed_2010"], which denotes by @object a sub-element
+ of a variable (or a sub-element of the first argument of the function, when
+ @R[τ @${φ⁺} @${φ⁻} @${o}] is the return type of a function).
+ }
+
+ @include-equation["GammaR.rkt" Γ]
+
+ @deftech[#:key "R-typing-info"]{}
+ @include-equation["GammaR.rkt" R]
+
+ The @Γ[⊢ e R] typing judgement indicates that the expression @${e} has type
+ @${τ}. The @${Γ} typing environment maps variables to their type (and to extra
+ information), while the @${Δ} environment stores the polymorphic type
+ variables, variadic polymorphic type variables and recursive type variables
+ which are in scope.
+
+ Additionally, the typing judgement indicates a set of propositions @${φ⁻}
+ which are known to be true when the run-time value of @${e} is @|false-v|, and
+ a set of propositions @${φ⁺} which are known to be true when the run-time
+ value of @${e} is @|true-v|@note{Any other value is treated in the same way as
+ @|true-v|, as values other than @|false-v| are traditionally considered as
+ true in language of the @lisp family.}. The propositions will indicate that
+ the value of a separate variable belongs (or does not belong) to a given type.
+ For example, the @${φ⁻} proposition @${@|Numberτ|_y} indicates that when @${e}
+ evaluates to @|false-v|, the variable @${y} necessarily holds an integer.
+
+ Finally, the typing judgement can indicate with @${o} that the expression @${
+ e} is an alias for a sub-element of another variable in the environment. For
+ example, if the object @${o} is @${@carπ ∷ @cdrπ(y)}, it indicates that the
+ expression @${e} produces the same value that @racket[(car (cdr y))] would,
+ i.e. that it returns the second element of a (possibly improper) list stored
+ in @racket[y].
+
+ Readers familiar with abstract interpretation can compare the @${φ}
+ propositions to the Cartesian product of the abstract domains of pairs of
+ variables. A static analyser can track possible pairs of values contained in
+ pairs of distinct variables, and will represent this information using an
+ abstract domain which combinations of values may be possible, and which may
+ not. Occurrence typing similarly exploits the fact that the type of other
+ variables may depend on the value of @${τ}. @htodo{is this some weak form of
+ dependent typing?}
+
+}
+
+@asection{
+ @atitle{Types}
+
+ @Typedracket handles the types listed below. Aside from the top type (@${⊤})
+ which is the supertype of all other types, this list includes singleton types
+ for numbers, booleans, symbols and the @null-v value. The types @Numberτ and
+ @Symbolτ are the infinite unions of all number and symbol singletons,
+ respectively. Also present are function types (with fixed arguments,
+ homogeneous @emph{rest} arguments and the variadic polymorphic functions which
+ accept heterogeneous @emph{rest} arguments, as well as polymorphic
+ abstractions), unions of other types, intersections of other types, the type
+ of pairs and promises. The value assigned to a variadic polymorphic function's
+ rest argument will have a type of the form @List…τ[τ α]. Finally, @typedracket
+ allows recursive types to be described with the @recτ* combinator.
+
+ @include-equation["tausigma.rkt"]
+
+ Additionally, the @Booleanτ type is defined as the union of the @true-τ and
+ @false-τ singleton types, and the @Listτ type operator is a shorthand for
+ describing the type of @|null-v|-terminated heterogeneous linked lists of
+ pairs, with a fixed length. The @Listofτ type operator is a shorthand for
+ describing the type of @|null-v|-terminated homogeneous linked lists of pairs,
+ with an unspecified length.
+
+ @include-equation["tausigma.rkt" Boolean]
+ @include-equation["tausigma.rkt" Listτ]
+ @include-equation["tausigma.rkt" Listofτ]
+
+}
+
+@asection{
+ @atitle{Filters (value-dependent propositions)}
+
+ The filters associated with an expression are a set of positive (resp.
+ negative) propositions which are valid when the expression is true (resp.
+ false).
+
+ @include-equation["phi-psi-o-path.rkt" φ]
+
+ These propositions indicate that a specific subelement of a location has a
+ given type.
+
+ @include-equation["phi-psi-o-path.rkt" ψ]
+
+ The location can be a variable, or the special @${•} token, which denotes a
+ function's first parameter, when the propositions are associated with that
+ function's result. This allows us to express relations between the output of a
+ function and its input, without referring to the actual name of the parameter,
+ which is irrelevant. In other words, @${•} occurs in an α-normal form of a
+ function's type.
+
+ @include-equation["phi-psi-o-path.rkt" loc]
+
+ @Objects, which represent aliasing information, can either indicate that the
+ expression being considered is an alias for a sub-element of a variable, or
+ that no aliasing information is known.
+
+}
+
+@asection{
+ @atitle{Objects (aliasing information)}
+
+ @include-equation["phi-psi-o-path.rkt" o]
+
+ Sub-elements are described via a chain of path elements which are used to
+ access the sub-element starting from the variable.
-@;{
- The type system of @typedracket relies on the following typing judgement. It
- indicates that the expression @${e} has type @${τ}. Additionally, if the
- run-time value of @${e} is @false-v then the propositions contained in @${φ⁻}
- are valid. If the run-time value of @${e} is not @false-v, then the
- propositions contained in @${φ⁺} are valid. Finally, @${e} is an alias for the
- @object @${o}. We use here the same terminology as
- @~cite["tobin-hochstadt_typed_2010"], which denotes by @object a sub-element
- of a variable (or a sub-element of the first argument of the function, when
- @R[τ @${φ⁺} @${φ⁻} @${o}] is the return type of a function).
}
-@include-equation["GammaR.rkt" Γ]
+@asection{
+ @atitle{Paths}
+
+ @include-equation["phi-psi-o-path.rkt" π]
+
+ The path concatenation operator @${∷} is associative. @htodo{Actually, we
+ define it for pe∷π above, not for π∷π}. The @${@emptypath} is omitted from
+ paths with one or more elements, so we write @${car∷cdr} instead of @${
+ car∷cdr∷@emptypath}.
-@deftech[#:key "R-typing-info"]{}
-@include-equation["GammaR.rkt" R]
-
-The @Γ[⊢ e R] typing judgement indicates that the expression @${e} has type
-@${τ}. The @${Γ} typing environment maps variables to their type (and to extra
-information), while the @${Δ} environment stores the polymorphic type
-variables, variadic polymorphic type variables and recursive type variables
-which are in scope.
-
-Additionally, the typing judgement indicates a set of propositions @${φ⁻}
-which are known to be true when the run-time value of @${e} is @|false-v|, and
-a set of propositions @${φ⁺} which are known to be true when the run-time
-value of @${e} is @|true-v|@note{Any other value is treated in the same way as
- @|true-v|, as values other than @|false-v| are traditionally considered as
- true in language of the @lisp family.}. The propositions will indicate that the
-value of a separate variable belongs (or does not belong) to a given type. For
-example, the @${φ⁻} proposition @${@|Numberτ|_y} indicates that when @${e}
-evaluates to @|false-v|, the variable @${y} necessarily holds an integer.
-
-Finally, the typing judgement can indicate with @${o} that the expression @${
- e} is an alias for a sub-element of another variable in the environment. For
-example, if the object @${o} is @${@carπ ∷ @cdrπ(y)}, it indicates that the
-expression @${e} produces the same value that @racket[(car (cdr y))] would,
-i.e. that it returns the second element of a (possibly improper) list stored
-in @racket[y].
-
-Readers familiar with abstract interpretation can compare the @${φ}
-propositions to the Cartesian product of the abstract domains of pairs of
-variables. A static analyser can track possible pairs of values contained in
-pairs of distinct variables, and will represent this information using an
-abstract domain which combinations of values may be possible, and which may
-not. Occurrence typing similarly exploits the fact that the type of other
-variables may depend on the value of @${τ}. @htodo{is this some weak form of
- dependent typing?}
-
-@subsubsub*section{Types}
-
-@Typedracket handles the types listed below. Aside from the top type (@${⊤})
-which is the supertype of all other types, this list includes singleton types
-for numbers, booleans, symbols and the @null-v value. The types @Numberτ and
-@Symbolτ are the infinite unions of all number and symbol singletons,
-respectively. Also present are function types (with fixed arguments,
-homogeneous @emph{rest} arguments and the variadic polymorphic functions which
-accept heterogeneous @emph{rest} arguments, as well as polymorphic
-abstractions), unions of other types, intersections of other types, the type
-of pairs and promises. The value assigned to a variadic polymorphic function's
-rest argument will have a type of the form @List…τ[τ α]. Finally, @typedracket
-allows recursive types to be described with the @recτ* combinator.
-
-@include-equation["tausigma.rkt"]
-
-Additionally, the @Booleanτ type is defined as the union of the @true-τ and
-@false-τ singleton types, and the @Listτ type operator is a shorthand for
-describing the type of @|null-v|-terminated heterogeneous linked lists of
-pairs, with a fixed length. The @Listofτ type operator is a shorthand for
-describing the type of @|null-v|-terminated homogeneous linked lists of pairs,
-with an unspecified length.
-
-@include-equation["tausigma.rkt" Boolean]
-@include-equation["tausigma.rkt" Listτ]
-@include-equation["tausigma.rkt" Listofτ]
-
-@subsubsub*section{Filters (value-dependent propositions)}
-
-The filters associated with an expression are a set of positive (resp.
-negative) propositions which are valid when the expression is true (resp.
-false).
-
-@include-equation["phi-psi-o-path.rkt" φ]
-
-These propositions indicate that a specific subelement of a location has a
-given type.
-
-@include-equation["phi-psi-o-path.rkt" ψ]
-
-The location can be a variable, or the special @${•} token, which denotes a
-function's first parameter, when the propositions are associated with that
-function's result. This allows us to express relations between the output of a
-function and its input, without referring to the actual name of the parameter,
-which is irrelevant. In other words, @${•} occurs in an α-normal form of a
-function's type.
-
-@include-equation["phi-psi-o-path.rkt" loc]
-
-@Objects, which represent aliasing information, can either indicate that the
-expression being considered is an alias for a sub-element of a variable, or
-that no aliasing information is known.
-
-@subsubsub*section{Objects (aliasing information)}
-
-@include-equation["phi-psi-o-path.rkt" o]
-
-Sub-elements are described via a chain of path elements which are used to
-access the sub-element starting from the variable.
-
-@subsubsub*section{Paths}
-
-@include-equation["phi-psi-o-path.rkt" π]
-
-The path concatenation operator @${∷} is associative. @htodo{Actually, we
- define it for pe∷π above, not for π∷π}. The @${@emptypath} is omitted from
-paths with one or more elements, so we write @${car∷cdr} instead of @${
- car∷cdr∷@emptypath}.
-
-@subsubsub*section{Path elements}
-
-Path elements can be @carπ and @cdrπ, to indicate access to a pair's first or
-second element, and @forceπ, to indicate that the proposition or object
-targets the result obtained after forcing a promise. We will note here that
-this obviously is only sound if forcing a promise always returns the same
-result (otherwise the properties and object which held on a former value may
-hold on the new result). Racket features promises which do not cache their
-result. These could return a different result each time they are forced by
-relying on external state. However, forcing a promise is generally assumed to
-be an idempotent operation, and not respecting this implicit contract in
-production code would be bad practice. Typed Racket disallows non-cached
-promises altogether. We introduced a small module @racketmodname[delay-pure]
-which allows the safe creation of non-cached promises.
-@racketmodname[delay-pure] restricts the language to a small subset of
-functions and operators which are known to not perform any mutation, and
-prevents access to mutable variables. This ensures that the promises created
-that way always produce the same value, without the need to actually cache
-their result.
-
-@include-equation["phi-psi-o-path.rkt" pe]
-
-@subsubsub*section{Subtyping}
-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
-subtypes of each other, they form an equivalence class. They are considered
-different notations for the same type, and we note @=:[τ σ], whereas @≠:[τ σ]
-indicates that @${τ} and @${σ} are not mutually subtypes of each other (but
-one can be a strict subtype of the other).
-
-@include-equation["subtyping.rkt" S-Reflexive]
-@include-equation["subtyping.rkt" S-Transitive]
-
-The @${⊥} type is a shorthand for the empty union @${(∪)}. It is a subtype of
-every other type, and is not inhabited by any value. @textsc{S-Bot} can be
-derived from @textsc{S-UnionSub}, by constructing an empty union.
-
-@$p[@include-equation["subtyping.rkt" S-Top]
- @include-equation["subtyping.rkt" S-Bot]]
-
-The singleton types @num-τ and @symτ[s] which are only inhabited by their
-literal counterpart are subtypes of the more general @Numberτ or @Symbolτ
-types, respectively.
-
-@$p[@include-equation["subtyping.rkt" S-Number]
- @include-equation["subtyping.rkt" S-Symbol]]
-
-The following subtyping rules are concerned with function types and
-polymorphic types:
+}
+
+@asection{
+ @atitle{Path elements}
+
+ Path elements can be @carπ and @cdrπ, to indicate access to a pair's first or
+ second element, and @forceπ, to indicate that the proposition or object
+ targets the result obtained after forcing a promise. We will note here that
+ this obviously is only sound if forcing a promise always returns the same
+ result (otherwise the properties and object which held on a former value may
+ hold on the new result). Racket features promises which do not cache their
+ result. These could return a different result each time they are forced by
+ relying on external state. However, forcing a promise is generally assumed to
+ be an idempotent operation, and not respecting this implicit contract in
+ production code would be bad practice. Typed Racket disallows non-cached
+ promises altogether. We introduced a small module @racketmodname[delay-pure]
+ which allows the safe creation of non-cached promises.
+ @racketmodname[delay-pure] restricts the language to a small subset of
+ functions and operators which are known to not perform any mutation, and
+ prevents access to mutable variables. This ensures that the promises created
+ that way always produce the same value, without the need to actually cache
+ their result.
+
+ @include-equation["phi-psi-o-path.rkt" pe]
-@$p[@include-equation["subtyping.rkt" S-Fun]
- @include-equation["subtyping.rkt" S-R]
- @include-equation["subtyping.rkt" S-Fun*]
- @include-equation["subtyping.rkt" S-Fun*-Fixed]
- @include-equation["subtyping.rkt" S-Fun*-Fixed*]
- @include-equation["subtyping.rkt" S-DFun]
- @include-equation["subtyping.rkt" S-Poly-α-Equiv]
- @include-equation["subtyping.rkt" S-PolyD-α-Equiv]
- @include-equation["subtyping.rkt" S-DFun-Fun*]]
-
-@todo{@textsc{S-PolyD-α-Equiv} should use the substitution for a polydot
- (subst-dots?), not the usual subst.}
-
-@todo{check the @textsc{S-DFun-Fun*} rule.}
-
-@htodo{Try to detach the ∀ from the →, in case the → is nested further deep.
- If it works.}
-
-The following rules are concerned with recursive types built with the
-@racket[Rec] combinator. The @textsc{S-RecWrap} rule allows considering
-@Numberτ a subtype of @recτ[r Numberτ] for example (i.e. applying the
-recursive type combinator to a type which does not refer to @${r} is a no-op),
-but it also allows deriving
-@<:[@recτ[r @un[@consτ[τ r] @null-τ]] @un[@consτ[τ ⊤] @null-τ]]. The @textsc{
- S-RecElim} rule has the opposite effect, and is mainly useful to “upcast”
-members of an union containing @${r}. It allows the deriving
-@<:[@null-τ @recτ[r @un[@consτ[τ r] @null-τ]]]. The rules @textsc{S-RecStep}
-and @textsc{S-RecUnStep} allow unraveling a single step of the recursion, or
-assimilating an such an unraveled step as part of the recursive type.
-
-@todo{TODO: renamings}
-
-@$p[
+}
+
+@asection{
+ @atitle{Subtyping}
+ 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
+ subtypes of each other, they form an equivalence class. They are considered
+ different notations for the same type, and we note @=:[τ σ], whereas @≠:[τ σ]
+ indicates that @${τ} and @${σ} are not mutually subtypes of each other (but
+ one can be a strict subtype of the other).
+
+ @include-equation["subtyping.rkt" S-Reflexive]
+ @include-equation["subtyping.rkt" S-Transitive]
+
+ The @${⊥} type is a shorthand for the empty union @${(∪)}. It is a subtype of
+ every other type, and is not inhabited by any value. @textsc{S-Bot} can be
+ derived from @textsc{S-UnionSub}, by constructing an empty union.
+
+ @$p[@include-equation["subtyping.rkt" S-Top]
+ @include-equation["subtyping.rkt" S-Bot]]
+
+ The singleton types @num-τ and @symτ[s] which are only inhabited by their
+ literal counterpart are subtypes of the more general @Numberτ or @Symbolτ
+ types, respectively.
+
+ @$p[@include-equation["subtyping.rkt" S-Number]
+ @include-equation["subtyping.rkt" S-Symbol]]
+
+ The following subtyping rules are concerned with function types and
+ polymorphic types:
+
+ @$p[@include-equation["subtyping.rkt" S-Fun]
+ @include-equation["subtyping.rkt" S-R]
+ @include-equation["subtyping.rkt" S-Fun*]
+ @include-equation["subtyping.rkt" S-Fun*-Fixed]
+ @include-equation["subtyping.rkt" S-Fun*-Fixed*]
+ @include-equation["subtyping.rkt" S-DFun]
+ @include-equation["subtyping.rkt" S-Poly-α-Equiv]
+ @include-equation["subtyping.rkt" S-PolyD-α-Equiv]
+ @include-equation["subtyping.rkt" S-DFun-Fun*]]
+
+ @todo{@textsc{S-PolyD-α-Equiv} should use the substitution for a polydot
+ (subst-dots?), not the usual subst.}
+
+ @todo{check the @textsc{S-DFun-Fun*} rule.}
+
+ @htodo{Try to detach the ∀ from the →, in case the → is nested further deep.
+ If it works.}
+
+ The following rules are concerned with recursive types built with the
+ @racket[Rec] combinator. The @textsc{S-RecWrap} rule allows considering
+ @Numberτ a subtype of @recτ[r Numberτ] for example (i.e. applying the
+ recursive type combinator to a type which does not refer to @${r} is a no-op),
+ but it also allows deriving
+ @<:[@recτ[r @un[@consτ[τ r] @null-τ]] @un[@consτ[τ ⊤] @null-τ]]. The @textsc{
+ S-RecElim} rule has the opposite effect, and is mainly useful to “upcast”
+ members of an union containing @${r}. It allows the deriving
+ @<:[@null-τ @recτ[r @un[@consτ[τ r] @null-τ]]]. The rules @textsc{S-RecStep}
+ and @textsc{S-RecUnStep} allow unraveling a single step of the recursion, or
+ assimilating an such an unraveled step as part of the recursive type.
+
+ @todo{TODO: renamings}
+
+ @$p[
@include-equation["subtyping.rkt" S-RecWrap]
@include-equation["subtyping.rkt" S-RecElim]
@include-equation["subtyping.rkt" S-RecStep]
@include-equation["subtyping.rkt" S-RecUnStep]]
-The rules below describe how union and intersection types compare.
+ The rules below describe how union and intersection types compare.
+
+ @$p[@include-equation["subtyping.rkt" S-UnionSuper]
+ @include-equation["subtyping.rkt" S-UnionSub]
+ @include-equation["subtyping.rkt" S-IntersectionSub]
+ @include-equation["subtyping.rkt" S-IntersectionSuper]]
+
+ Finally, promises are handled by comparing the type that they produce when
+ forced, and pairs are compared pointwise. Dotted lists types, which usually
+ represent the type of the value assigned to a variadic polymorphic function's
+ “rest” argument
-@$p[@include-equation["subtyping.rkt" S-UnionSuper]
- @include-equation["subtyping.rkt" S-UnionSub]
- @include-equation["subtyping.rkt" S-IntersectionSub]
- @include-equation["subtyping.rkt" S-IntersectionSuper]]
+ @$p[@include-equation["subtyping.rkt" S-Promise]
+ @include-equation["subtyping.rkt" S-Pair]
+ @include-equation["subtyping.rkt" S-DList]]
-Finally, promises are handled by comparing the type that they produce when
-forced, and pairs are compared pointwise. Dotted lists types, which usually
-represent the type of the value assigned to a variadic polymorphic function's
-“rest” argument
+}
-@$p[@include-equation["subtyping.rkt" S-Promise]
- @include-equation["subtyping.rkt" S-Pair]
- @include-equation["subtyping.rkt" S-DList]]
+@asection{
+ @atitle{Operational semantics}
-@subsubsub*section{Operational semantics}
+ The semantics for the simplest expressions and for primitive functions are
+ expressed using δ-rules.
-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]]
-@$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" δ-rules]
+ @include-equation["operational-semantics.rkt" δe-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.
-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]
-@include-equation["operational-semantics.rkt" E-Context]
+ The next rules handle β-reduction for the various flavours of functions.
-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]]
-@$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).
-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]]
-@$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
+ expressions relying on external state, and caches the value obtained after
+ forcing the promise for the first time. The subset of the language which we
+ present here does not contain any mutable value, and does not allow mutation
+ of variables either, so the expression wrapped by promises is, by definition,
+ 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.
-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
-expressions relying on external state, and caches the value obtained after
-forcing the promise for the first time. The subset of the language which we
-present here does not contain any mutable value, and does not allow mutation
-of variables either, so the expression wrapped by promises is, by definition,
-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.
+ @include-equation["operational-semantics.rkt" E-Force]
-@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.
-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]]
-@$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|.
-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]]
-@$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.
-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]]
-@$p[@include-equation["operational-semantics.rkt" E-Map-Pair]
- @include-equation["operational-semantics.rkt" E-Map-Null]]
+}
-@subsubsub*section{Type validity rules}
+@asection{
+ @atitle{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.
+ 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.
-@$p[@include-equation["te.rkt" TE-Var]
- @include-equation["te.rkt" TE-DList]]
+ @$p[@include-equation["te.rkt" TE-Var]
+ @include-equation["te.rkt" TE-DList]]
-@htodo{There are more rules needed (one for building every type, most are
- trivial).}
+ @htodo{There are more rules needed (one for building every type, most are
+ trivial).}
-@htodo{isn't there any well-scopedness constraint for the φ?}
+ @htodo{isn't there any well-scopedness constraint for the φ?}
-The following rules indicate that function types are valid if their use of
-polymorphic type variables is well-scoped.
+ The following rules indicate that function types are valid if their use of
+ polymorphic type variables is well-scoped.
-@$p[@include-equation["te.rkt" TE-DFun]
- @include-equation["te.rkt" TE-All]
- @include-equation["te.rkt" TE-DAll]
- @include-equation["te.rkt" TE-DPretype]]
+ @$p[@include-equation["te.rkt" TE-DFun]
+ @include-equation["te.rkt" TE-All]
+ @include-equation["te.rkt" TE-DAll]
+ @include-equation["te.rkt" TE-DPretype]]
-The following rule indicates that types built using the recursive type
-combinator @recτ* are valid if their use of the recursive type variable @${r}
-is well-scoped.
+ The following rule indicates that types built using the recursive type
+ combinator @recτ* are valid if their use of the recursive type variable @${r}
+ is well-scoped.
-@include-equation["te.rkt" TE-Rec]
+ @include-equation["te.rkt" TE-Rec]
-The next rules are trivial, and state that the base types are valid, or simply
-examine validity pointwise for unions, intersections, pairs, promises and
-filters. @htodo{and objects}
+ The next rules are trivial, and state that the base types are valid, or simply
+ examine validity pointwise for unions, intersections, pairs, promises and
+ filters. @htodo{and objects}
-@$p[
+ @$p[
@include-equation["te.rkt" TE-Trivial]
@include-equation["te.rkt" TE-R]
@include-equation["te.rkt" TE-Phi]
@@ -601,189 +645,202 @@ filters. @htodo{and objects}
@include-equation["te.rkt" TE-Psi-Not]
@include-equation["te.rkt" TE-Psi-Bot]]
-@subsubsub*section{Typing rules}
+}
-The rules below relate the simple expressions to their type.
+@asection{
+ @atitle{Typing rules}
-@htodo{Are the hypotheses for T-Eq? necessary? After all, in Racket eq? works
- on Any.}
+ The rules below relate the simple expressions to their type.
-@$p[@include-equation["trules.rkt" T-Symbol]
- @include-equation["trules.rkt" T-Gensym]
- @include-equation["trules.rkt" T-Promise]
- @include-equation["trules.rkt" T-Var]
- @include-equation["trules.rkt" T-Primop]
- @include-equation["trules.rkt" T-True]
- @include-equation["trules.rkt" T-False]
- @include-equation["trules.rkt" T-Num]
- @include-equation["trules.rkt" T-Null]
- @include-equation["trules.rkt" T-Eq?]]
+ @htodo{Are the hypotheses for T-Eq? necessary? After all, in Racket eq? works
+ on Any.}
-Below are the rules for the various flavours of lambda functions and
-polymorphic abstractions.
+ @$p[@include-equation["trules.rkt" T-Symbol]
+ @include-equation["trules.rkt" T-Gensym]
+ @include-equation["trules.rkt" T-Promise]
+ @include-equation["trules.rkt" T-Var]
+ @include-equation["trules.rkt" T-Primop]
+ @include-equation["trules.rkt" T-True]
+ @include-equation["trules.rkt" T-False]
+ @include-equation["trules.rkt" T-Num]
+ @include-equation["trules.rkt" T-Null]
+ @include-equation["trules.rkt" T-Eq?]]
-@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).}
+ Below are the rules for the various flavours of lambda functions and
+ polymorphic abstractions.
-@todo{Should the φ⁺ φ⁻ o be preserved in T-TAbs and T-DTAbs?}
+ @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).}
-@$p[@include-equation["trules.rkt" T-AbsPred]
- @include-equation["trules.rkt" T-Abs]
- @include-equation["trules.rkt" T-Abs*]
- @include-equation["trules.rkt" T-DAbs]
- @include-equation["trules.rkt" T-TAbs]
- @include-equation["trules.rkt" T-DTAbs]]
+ @todo{Should the φ⁺ φ⁻ o be preserved in T-TAbs and T-DTAbs?}
-The @${\vphantom{φ}@substφo[x ↦ z]} operation restricts the information
-contained within a @${φ} or @${o} so that the result only contains information
-about the variable @${x}, and renames it to @${z}. When applied to a filter
-@${φ}, it corresponds to the @${\operatorname{abo}} and @${\operatorname{
- apo}} operators from
-@~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"].
+ @$p[@include-equation["trules.rkt" T-AbsPred]
+ @include-equation["trules.rkt" T-Abs]
+ @include-equation["trules.rkt" T-Abs*]
+ @include-equation["trules.rkt" T-DAbs]
+ @include-equation["trules.rkt" T-TAbs]
+ @include-equation["trules.rkt" T-DTAbs]]
-The @${⊥} cases of the @${\operatorname{apo}} operator
-from@~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"] are covered
-by the corresponding cases in the @${@restrict} and @${@remove} operators
-defined below, and therefore should not need to be included in our @${
- \vphantom{φ}@substφo[x ↦ z]} operator. The subst
+ The @${\vphantom{φ}@substφo[x ↦ z]} operation restricts the information
+ contained within a @${φ} or @${o} so that the result only contains information
+ about the variable @${x}, and renames it to @${z}. When applied to a filter
+ @${φ}, it corresponds to the @${\operatorname{abo}} and @${\operatorname{
+ apo}} operators from
+ @~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"].
-@include-equation["trules.rkt" substφ]
-@include-equation["trules.rkt" substo]
+ The @${⊥} cases of the @${\operatorname{apo}} operator
+ from@~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"] are covered
+ by the corresponding cases in the @${@restrict} and @${@remove} operators
+ defined below, and therefore should not need to be included in our @${
+ \vphantom{φ}@substφo[x ↦ z]} operator. The subst
-@htodo{The definition of Γ' does not specify what the other cases ≠ x are
- (they are the same as the original Γ, but this is only implicit).}
+ @include-equation["trules.rkt" substφ]
+ @include-equation["trules.rkt" substo]
-The @racket[map] function can be called like any other function, but also has
-a specific rule allowing a more precise result type when mapping a polymorphic
-function over a @List…τ[τ α]. @racket[ormap], @racket[andmap] and
-@racket[apply] similarly have special rules for variadic polymorphic lists. We
-include the rule for @racket[map] below as an example. The other rules are
-present in @~cite[#:precision "pp. 96" "tobin-hochstadt_typed_2010"].
+ @htodo{The definition of Γ' does not specify what the other cases ≠ x are
+ (they are the same as the original Γ, but this is only implicit).}
-@htodo{The original TD-Map rule (p.95) seems wrong, as it allows un-dotted
- references to α in the function's type. But it is impossible to construct such
- a function, and the meaning of α in that case is unclear. I think the rule
- should instead expect a polymorphic function, with occurrences of α in τ_r
- replaced with the new β variable, as shown below.}
+ The @racket[map] function can be called like any other function, but also has
+ a specific rule allowing a more precise result type when mapping a polymorphic
+ function over a @List…τ[τ α]. @racket[ormap], @racket[andmap] and
+ @racket[apply] similarly have special rules for variadic polymorphic lists. We
+ include the rule for @racket[map] below as an example. The other rules are
+ present in @~cite[#:precision "pp. 96" "tobin-hochstadt_typed_2010"].
-@include-equation["trules.rkt" T-DMap]
+ @htodo{The original TD-Map rule (p.95) seems wrong, as it allows un-dotted
+ references to α in the function's type. But it is impossible to construct such
+ a function, and the meaning of α in that case is unclear. I think the rule
+ should instead expect a polymorphic function, with occurrences of α in τ_r
+ replaced with the new β variable, as shown below.}
-Below are the typing rules for the various flavours of function application and
-instantiation of polymorphic abstractions.
+ @include-equation["trules.rkt" T-DMap]
-@todo{For the inst rules, are the φ⁺ φ⁻ o preserved?}
+ Below are the typing rules for the various flavours of function application and
+ instantiation of polymorphic abstractions.
-@$p[@include-equation["trules.rkt" T-App]
- @include-equation["trules.rkt" T-Inst]
- @include-equation["trules.rkt" T-DInst]
- @include-equation["trules.rkt" T-DInstD]]
+ @todo{For the inst rules, are the φ⁺ φ⁻ o preserved?}
-@;=====================TODO:write something vvvvvvvvvvvv
+ @$p[@include-equation["trules.rkt" T-App]
+ @include-equation["trules.rkt" T-Inst]
+ @include-equation["trules.rkt" T-DInst]
+ @include-equation["trules.rkt" T-DInstD]]
-The rule for @ifop uses the information gained in the condition to narrow the
-type of variables in the @emph{then} and @emph{else} branches. This is the
-core rule of the occurrence typing aspect of @|typedracket|.
+ @;=====================TODO:write something vvvvvvvvvvvv
-@include-equation["trules.rkt" T-If]
+ The rule for @ifop uses the information gained in the condition to narrow the
+ type of variables in the @emph{then} and @emph{else} branches. This is the
+ core rule of the occurrence typing aspect of @|typedracket|.
-The @${Γ + φ} operator narrows the type of variables in the environment using
-the information contained within @${φ}.
+ @include-equation["trules.rkt" T-If]
-@include-equation["trules.rkt" Γ+]
+ The @${Γ + φ} operator narrows the type of variables in the environment using
+ the information contained within @${φ}.
-The @update operator propagates the information contained within a @${ψ} down
-to the affected part of the type.
+ @include-equation["trules.rkt" Γ+]
-@include-equation["trules.rkt" update]
+ The @update operator propagates the information contained within a @${ψ} down
+ to the affected part of the type.
-The @update operator can then apply @restrict to perform the intersection of
-the type indicated by the @|ifop|'s condition and the currently-known type for
-the subpart of the considered variable.
+ @include-equation["trules.rkt" update]
-@todo{How do @restrict and @remove behave on intersections?}
+ The @update operator can then apply @restrict to perform the intersection of
+ the type indicated by the @|ifop|'s condition and the currently-known type for
+ the subpart of the considered variable.
-@include-equation["trules.rkt" restrict]
+ @todo{How do @restrict and @remove behave on intersections?}
-The @update operator can also apply
-the @remove operator when the condition determined that the subpart of the
-considered variable is @emph{not} of a given type.
+ @include-equation["trules.rkt" restrict]
-@include-equation["trules.rkt" remove]
+ The @update operator can also apply
+ the @remove operator when the condition determined that the subpart of the
+ considered variable is @emph{not} of a given type.
-@;{Shouldn't no-overlap be simplified to @${@no-overlap(τ, τ') = (@<:[σ τ]
- ∧ @<:[σ τ′] ⇒ σ = ⊥)}? Then @${@restrict(τ,σ)} can be simplified to returning
- the most general type which is a subtype of τ and σ if one exists (or maybe
- simply returning the intersection of τ and σ).}
+ @include-equation["trules.rkt" remove]
-@todo{Δ is not available here.}
-@todo{The non-nested use of σ is not quite correct syntactically speaking}
+ @;{Shouldn't no-overlap be simplified to @${@no-overlap(τ, τ') = (@<:[σ τ]
+ ∧ @<:[σ τ′] ⇒ σ = ⊥)}? Then @${@restrict(τ,σ)} can be simplified to returning
+ the most general type which is a subtype of τ and σ if one exists (or maybe
+ simply returning the intersection of τ and σ).}
-The @restrict operator and the @simplify* operator described later both rely
-on @no-overlap to determine whether two types have no intersection, aside from
-the @${⊥} type.
+ @todo{Δ is not available here.}
+ @todo{The non-nested use of σ is not quite correct syntactically speaking}
-@include-equation["trules.rkt" no-overlap]
+ The @restrict operator and the @simplify* operator described later both rely
+ on @no-overlap to determine whether two types have no intersection, aside from
+ the @${⊥} type.
-@htodo{Say that there are more rules in the implementation, to handle various
- boolean operations.}
+ @include-equation["trules.rkt" no-overlap]
-The @combinefilter operator is used to combine the @${φ} information from the
-two branches of the @ifop expression, based on the @${φ} information of the
-condition. This allows @typedracket to correctly interpret @racket[and],
-@racket[or] as well as other boolean operations, which are implemented as
-macros translating down to nested @racket[if] conditionals. @Typedracket will
-therefore be able to determine that in the @emph{then} branch of
-@racket[(if (and (string? x) (number? y)) 'then 'else)], the type of
-@racketid[x] is @racket[String], and the type of @racketid[y] is
-@racket[Number]. We only detail a few cases of combinefilter here, a more
-complete description of the operator can be found
-in@~cite[#:precision "pp. 69,75–84" "tobin-hochstadt_typed_2010"].
+ @htodo{Say that there are more rules in the implementation, to handle various
+ boolean operations.}
-@include-equation["trules.rkt" combinefilter]
+ The @combinefilter operator is used to combine the @${φ} information from the
+ two branches of the @ifop expression, based on the @${φ} information of the
+ condition. This allows @typedracket to correctly interpret @racket[and],
+ @racket[or] as well as other boolean operations, which are implemented as
+ macros translating down to nested @racket[if] conditionals. @Typedracket will
+ therefore be able to determine that in the @emph{then} branch of
+ @racket[(if (and (string? x) (number? y)) 'then 'else)], the type of
+ @racketid[x] is @racket[String], and the type of @racketid[y] is
+ @racket[Number]. We only detail a few cases of combinefilter here, a more
+ complete description of the operator can be found
+ in@~cite[#:precision "pp. 69,75–84" "tobin-hochstadt_typed_2010"].
-@htodo{The Γ ⊢ x : τ … does not generate a Γ(x) = τ, I suspect. There should
- be indicated somewhere an equivalence between these two notations (and we
- should fix the @${Γ,x:update(…)}, as it is a third notation).}
+ @include-equation["trules.rkt" combinefilter]
-@subsubsub*section{Simplification of intersections}
+ @htodo{The Γ ⊢ x : τ … does not generate a Γ(x) = τ, I suspect. There should
+ be indicated somewhere an equivalence between these two notations (and we
+ should fix the @${Γ,x:update(…)}, as it is a third notation).}
-In some cases, intersections are simplified, and the eventual resulting @${⊥}
-types propagate outwards through pairs (and structs, which we do not model
-here). The @simplify* and @propagate⊥ operators show how these simplification
-and propagation steps are performed. The simplification step mostly consists
-in distributing intersections over unions and pairs, and collapsing pairs and
-unions which contain @${⊥}, for the traversed parts of the type.
+}
+
+@asection{
+ @atitle{Simplification of intersections}
-@include-equation["simplify.rkt" Simplify1]
+ In some cases, intersections are simplified, and the eventual resulting @${⊥}
+ types propagate outwards through pairs (and structs, which we do not model
+ here). The @simplify* and @propagate⊥ operators show how these simplification
+ and propagation steps are performed. The simplification step mostly consists
+ in distributing intersections over unions and pairs, and collapsing pairs and
+ unions which contain @${⊥}, for the traversed parts of the type.
-@${@simplify[τ]} is applied pointwise in other cases:
+ @include-equation["simplify.rkt" Simplify1]
-@include-equation["simplify.rkt" Simplify2]
+ @${@simplify[τ]} is applied pointwise in other cases:
-@include-equation["simplify.rkt" Propagate⊥]
+ @include-equation["simplify.rkt" Simplify2]
-@todo{Apply the intersections on substituted poly types after an inst (or rely
- on the sutyping rule for intersections to recognise that ⊥ is a subtype of the
- resulting type?)}.
+ @include-equation["simplify.rkt" Propagate⊥]
-@subsubsub*section{δ-rules}
+ @todo{Apply the intersections on substituted poly types after an inst (or rely
+ on the sutyping rule for intersections to recognise that ⊥ is a subtype of the
+ resulting type?)}.
-Finally, the type and semantics of primitive functions are expressed using the
-δ-rules given below.
+}
-@include-equation["deltarules.rkt"]
+@asection{
+ @atitle{δ-rules}
-@subsubsub*section{Soundness}
+ Finally, the type and semantics of primitive functions are expressed using the
+ δ-rules given below.
-Since @typedracket is an existing language which we use for our
-implementation, and not a new language, we do not provide here a full proof of
-correctness.
+ @include-equation["deltarules.rkt"]
+
+}
-We invite instead the interested reader to refer to the proof sketches given
-in@~cite[#:precision "pp. 68–84" "tobin-hochstadt_typed_2010"]. These proof
-sketches only cover a subset of the language presented here, namely a language
-with variables, function applictation, functions of a single argument, pairs,
-booleans, numbers and @ifop conditionals with support for occurrence typing.
-Since occurrence typing is the main focus of the proof, the other extensions
-aggregated here should not significantly threaten its validity.
-\ No newline at end of file
+@asection{
+ @atitle{Soundness}
+
+ Since @typedracket is an existing language which we use for our
+ implementation, and not a new language, we do not provide here a full proof of
+ correctness.
+
+ We invite instead the interested reader to refer to the proof sketches given
+ in@~cite[#:precision "pp. 68–84" "tobin-hochstadt_typed_2010"]. These proof
+ sketches only cover a subset of the language presented here, namely a language
+ with variables, function applictation, functions of a single argument, pairs,
+ booleans, numbers and @ifop conditionals with support for occurrence typing.
+ Since occurrence typing is the main focus of the proof, the other extensions
+ aggregated here should not significantly threaten its validity.
+}
+\ No newline at end of file
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -14,26 +14,28 @@ from@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"].
@require["adt-utils.rkt"]
-@subsubsub*section{Notations}
+@asection{
+ @atitle{Notations}
-We use the same notations as in
-@secref["from-dissertation-tobin-hochstadt"
- #:doc '(lib "phc-thesis/scribblings/phc-thesis.scrbl")]. Additionally,
-we use @ρc to denote a row type variable abstracting over a set of constructors,
-and we use @ρf to denote a row type variable abstracting over a set of fields.
-The occurrences of @${c} and @${f} in this context are purely syntactical, and
-only serve the purpose of distinguishing between the two notations — the one for
-constructors, and the one for fields.
+ We use the same notations as in
+ @secref["from-dissertation-tobin-hochstadt"
+ #:doc '(lib "phc-thesis/scribblings/phc-thesis.scrbl")]. Additionally,
+ we use @ρc to denote a row type variable abstracting over a set of
+ constructors, and we use @ρf to denote a row type variable abstracting over a
+ set of fields. The occurrences of @${c} and @${f} in this context are purely
+ syntactical, and only serve the purpose of distinguishing between the two
+ notations — the one for constructors, and the one for fields.
-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 resides only
-in their intended use). Constructor and field names are compile-time
-constants, i.e. they are written literally in the program source.
+ 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 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 ∈ ℱ}
+ @$${@κ ⩴ name ∈ 𝒞}
+ @$${@ɐ ⩴ name ∈ ℱ}
+}
@include-asection["adt-row-tausigma.scrbl"]
@include-asection["adt-row-e.scrbl"]
