commit aca7532322c7dbdb11401b8dff5522253c59c635
parent d9a17169703ab04204db009ef9eea3b9c6737f01
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Fri, 16 Jun 2017 18:53:45 +0200
Started writing presentation of TR
Diffstat:
9 files changed, 510 insertions(+), 29 deletions(-)
diff --git a/info.rkt b/info.rkt
@@ -11,6 +11,14 @@
"phc-toolkit"
"srfi-doc"
"srfi-lite-lib"
+ "datalog"
+ "racklog"
+ "scribble-doc"
+ "slideshow-doc"
+ "r5rs-doc"
+ "r6rs-doc"
+ "redex-doc"
+ "turnstile"
;; Literate programming dependencies:
;; phc-graph:
"aful"
diff --git a/scribblings/abbreviations.rkt b/scribblings/abbreviations.rkt
@@ -1,7 +1,7 @@
#lang at-exp racket
(provide typedracket Typedracket csharp CAML CLOS NIT CPP DeBruijn HOAS PHOAS
monocecil dotnet DLL nanopass nanopass-c-f haskell haskell98 Hackett
- turnstile Turnstile cur Cur)
+ turnstile Turnstile cur Cur LaTeX C-language java)
(require scribble/base
scribble/core
@@ -42,4 +42,8 @@
(define turnstile "Turnstile")
(define Turnstile "Turnstile")
(define cur "Cur")
-(define Cur "Cur")
-\ No newline at end of file
+(define Cur "Cur")
+(define LaTeX (cond-element [latex (elem #:style (style "LaTeX" '()))]
+ [else "LaTeX"]))
+(define C-language "C")
+(define java "Java")
+\ No newline at end of file
diff --git a/scribblings/bibliography.bib b/scribblings/bibliography.bib
@@ -1,3 +1,61 @@
+@book{minskyRealWorldOCaml,
+ title={Real World OCaml: Functional programming for the masses},
+ author={Minsky, Yaron and Madhavapeddy, Anil and Hickey, Jason},
+ year={2013},
+ publisher={" O'Reilly Media, Inc."}
+}
+
+@inproceedings{racketmanifesto,
+ title={The racket manifesto},
+ author={Felleisen, Matthias and Findler, Robert Bruce and Flatt, Matthew and Krishnamurthi, Shriram and Barzilay, Eli and McCarthy, Jay and Tobin-Hochstadt, Sam},
+ booktitle={LIPIcs-Leibniz International Proceedings in Informatics},
+ volume={32},
+ year={2015},
+ organization={Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik}
+}
+
+@article{r5rs,
+ title={Revised 5 report on the algorithmic language Scheme},
+ author={Abelson, Harold and Dybvig, R Kent and Haynes, Christopher T and Rozas, Guillermo Juan and Adams, NI and Friedman, Daniel P and Kohlbecker, E and Steele, GL and Bartley, David H and Halstead, Robert and others},
+ journal={Higher-order and symbolic computation},
+ volume={11},
+ number={1},
+ pages={7--105},
+ year={1998},
+ publisher={Springer}
+}
+
+@article{r6rs,
+ title={Revised 6 report on the algorithmic language Scheme},
+ author={Sperber, Michael and Dybvig, R Kent and Flatt, Matthew and Van Straaten, Anton and Findler, Robby and Matthews, Jacob},
+ journal={Journal of Functional Programming},
+ volume={19},
+ number={S1},
+ pages={1--301},
+ year={2009},
+ publisher={Cambridge Univ Press}
+}
+
+@techreport{r7rs,
+ title={Revised 7 report on the algorithmic language scheme},
+ author={Shinn, Alex and Cowan, JOHN and Gleckler, Arthur A and others},
+ year={2013},
+}
+
+@incollection{McCarthyHistoryLisp,
+ author = {McCarthy, John},
+ chapter = {History of LISP},
+ title = {History of Programming Languages I},
+ editor = {Wexelblat, Richard L.},
+ year = {1981},
+ isbn = {0-12-745040-8},
+ pages = {173--185},
+ numpages = {13},
+ doi = {10.1145/800025.1198360},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
@article{ganz2001macros-as-multi-stage-computations,
title={Macros as multi-stage computations: type-safe, generative, binding macros in MacroML},
author={Ganz, Steven E and Sabry, Amr and Taha, Walid},
diff --git a/scribblings/initial-examples.scrbl b/scribblings/initial-examples.scrbl
@@ -0,0 +1,8 @@
+#lang scribble/manual
+
+@require["util.rkt"
+ (for-label racket)]
+@(use-mathjax)
+
+@title[#:style (with-html5 manual-doc-style)
+ #:version (version-text)]{Goals, constraints and examples}
diff --git a/scribblings/introduction.scrbl b/scribblings/introduction.scrbl
@@ -5,10 +5,28 @@
(only-in srfi/1 zip))]
@(use-mathjax)
+@htodo{No parsers}
+
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Introduction}
@asection{
+ @atitle{Warm-up}
+
+ @todo{What does a compiler do}
+
+ @todo{This thesis aims to build a framework which helps write compilers.}
+
+ @todo{Our focus is on compilers, not virtual machines or other run-time
+ systems. We are also not concerned with parsers — there are lots of existing
+ approaches and libraries which help writing parsers, although parsing in
+ general is not yet a solved problem on all accounts.}
+
+ @todo{IR = the macroscopic structure of the program (i.e. the meta-model
+ (explain what it is)) + the code of functions and/or methods (statements and
+ expressions, basic blocks of statements, or bytecode instructions)}}
+
+@asection{
@atitle{The challenges of writing compilers}
@epigraph[#:width "8cm"
@@ -20,10 +38,16 @@
languages. A compiler will parse the program, transform it in various ways,
perform some more or less advanced static checks, and optimise the input
program before producing an output in the desired target language. A compiler
- must be correct, extensible and fast: correct because programmers are
+ must be correct, reusable and fast. It must be correct because programmers are
concerned with logical errors in their own code, and should not fear that the
- compiler introduces erroneous behaviour on its own; extensible because the
- language is likely to evolve over time; and fast because the programmer's
+ compiler introduces erroneous behaviour on its own. It must be also
+ well-architectured: extensible, because the language is likely to evolve over
+ time, modular in the hope that some components can be improved independently
+ of the rest of the compiler (e.g. replacing or improving an optimisation
+ phase, or changing the compiler's front-end, to support another input
+ language), and more generally reusable, so that parts can be repurposed to
+ build other compilers, or other tools (analysers, IDEs, code instrumentation
+ and so on). Finally, a fast compiler is desirable because the programmer's
edit-build-test cycle should be as frequent as
possible@todo{@~cite["smalltalk-programmer-efficiency-cycle"]}.
@@ -39,31 +63,31 @@
@hr
The overall structure of a compiler will usually include a lexer and parser,
- which turn the program's source into an in-memory representation. This
- initial representation will often be translated into an @deftech[#:key "IR"]{
+ which turn the program's source into an in-memory representation. This initial
+ representation will often be translated into an @deftech[#:key "IR"]{
intermediate representation} (IR) better suited to the subsequent steps. At
some early point, the program will be analysed for syntactical or semantic
inconsistencies (ranging from missing parentheses to duplicate definitions of
- the same variable), and may also perform a more thorough static analysis. The
- translation can then include an optimisation phase, based on
- locally-recognisable patterns or on the results of the program-wide analysis
- performed separately. Finally, code in the target language or for the target
- architecture is generated.
+ the same variable), and may also perform a more thorough static analysis.
+ Finally, code in the target language or for the target architecture is
+ generated. The translation can additionally include optimisation phases in
+ several spots: during code generation, using locally-recognisable patterns, or
+ for example earlier, using the results of the program-wide analysis performed
+ separately.
We identify three pitfalls which await the compiler-writer:
@itemlist[
@item{It is easy to reuse excessively a single @usetech{intermediate
- representation}, instead of properly distinguishing the features of the
- input and output of each pass;}
+ representation} type, instead of properly distinguishing the specifics of
+ the input and output type of each pass;}
@item{There is a high risk
associated with the definition of large, monolithic passes, which are hard to
test, debug, and extend;}
@item{The fundamental structure of the program being compiled is often a
graph, but compilers often work on an Abstract Syntax Tree, which requires
- explicit handling of the backward and transversal arcs; This is a source of
- bugs which could easily be avoided by using a higher-level abstraction
- specifically aiming to represent a graph.}]
+ explicit handling of the backward arcs; This is a source of bugs which could
+ be avoided by using a better abstraction.}]
The first two issues are prone to manifestations of some form or another of
the ``god object'' anti-pattern@note{The ``god object'' anti-pattern describes
@@ -80,12 +104,12 @@
@asection{
@atitle{Large monolithic passes}
- Large, monolithic passes, which perform many transformations in parallel have
- the advantage of possibly being faster than several smaller passes chained one
- after another. Furthermore, as one begins writing a compiler, it is tempting
- to incrementally extend an initial pass to perform more work, rather than
- starting all over again with a new @usetech{intermediate representation}, and
- a new scaffolding to support its traversal.
+ Large, monolithic passes, which perform many transformations simultaneously
+ have the advantage of possibly being faster than several smaller passes
+ chained one after another. Furthermore, as one begins writing a compiler, it
+ is tempting to incrementally extend an initial pass to perform more work,
+ rather than starting all over again with a new @usetech{intermediate
+ representation}, and a new scaffolding to support its traversal.
However, the drawback is that large compiler passes are harder to test (as
there are many more combinations of paths through the compiler's code to
@@ -132,7 +156,7 @@
Furthermore, a mutable @tech{IR} hinders parallel execution of compiler
passes. Indeed, some compiler passes will perform global transformations or
- transversal analyses, and such code may be intrinsically difficult to
+ analyses, and such code may be intrinsically difficult to
parallelise. @htodo{is "parallelise" the right word?} Many other passes
however are mere local transformations, and can readily be executed on
distinct parts of the abstract syntax tree, as long as there is no need to
@@ -390,7 +414,7 @@
of our translation from the extended type system to @|typedracket|'s core type
system. Fifthly, we provide means to express graph transformations as such
instead of working with an encoding of graphs as abstract syntax trees (or
- directed acyclic graphs), with explicit backward and transversal references.
+ directed acyclic graphs), with explicit backward references.
We are hopeful that eliminating this mismatch will be beneficial to the formal
verification of the transformation passes.
@@ -581,14 +605,14 @@
@item{Allows writing the compiler in a strongly-typed language}
@item{Uses immutable data structures for the Intermediate Representations
(ASTs)}
- @item{Supports transversal and backwards branches in the AST, making it
+ @item{Supports backwards branches in the AST, making it
rather an Abstract Syntax Graph (this is challenging due to the use of
immutable data structures).}
@item{Provides easy manipulation of the Intermediate Representations: local
navigation from node to node, global higher-order operations over many
nodes, easy construction, easy serialization, with the guarantee that at
no point an incomplete representation can be manipulated. These operations
- should handle seamlessly transversal and backwards arcs.}
+ should handle seamlessly backwards arcs.}
@item{Enforces structural invariants (either at compile-time or at
run-time), and ensures via the type system that unchecked values cannot be
used where a value respecting the invariant is expected.}
diff --git a/scribblings/phc-thesis.scrbl b/scribblings/phc-thesis.scrbl
@@ -37,6 +37,8 @@
@include-asection{introduction.scrbl}
@include-asection{state-of-the-art.scrbl}
+@include-asection{initial-examples.scrbl}
+@include-asection{tr-te-adt.scrbl}
@;@(generate-bibliography-section)
@; Generate the bibliography with a numbered section:
diff --git a/scribblings/tr-te-adt.scrbl b/scribblings/tr-te-adt.scrbl
@@ -0,0 +1,10 @@
+#lang scribble/manual
+
+@require["util.rkt"
+ (for-label racket)]
+@(use-mathjax)
+
+@title[#:style (with-html5 manual-doc-style)
+ #:version (version-text)]{Type systems and Algebraic Datatypes}
+
+@include-asection{tr.scrbl}
+\ No newline at end of file
diff --git a/scribblings/tr.scrbl b/scribblings/tr.scrbl
@@ -0,0 +1,359 @@
+#lang scribble/manual
+
+@require["util.rkt"
+ (for-label (only-meta-in 0 typed/racket))]
+@(use-mathjax)
+
+@title[#:style (with-html5 manual-doc-style)
+ #:version (version-text)]{@|Typedracket|}
+
+We start this section with some history: Lisp, @emph{the} language with lots
+of parentheses, shortly following Fortran as one of the first high-level
+programming languages, was initially designed between 1956 and 1958, and
+subsequently implemented@~cite["McCarthyHistoryLisp"]. Dialects of Lisp
+generally support a variety of programming paradigms, including (but not
+limited to) functional programming and object-oriented programming (e.g. via
+CLOS, the Common Lisp Object System). One of the the most proeminent aspects
+of Lisp is homoiconicity, the fact that programs and data structures look the
+same. This enables programs to easily manipulate other programs, and led to
+the extensive use of macros. Uses of macros usually look like function
+applications, but, instead of invoking a target function at run-time, a macro
+will perform some computation at compile-time, and expand to some new code,
+which is injected as a replacement of the macro's use.
+
+The two main dialects of Lisp are Common Lisp and Scheme. Scheme follows a
+minimalist philosophy, where a small core is
+standardised@~cite["r5rs" "r6rs" "r7rs"] and subsequently extended via macros
+and additional function definitions.
+
+Racket, formerly named PLT Scheme, started as a Scheme implementation. Racket
+evolved, and the Racket Manifesto@~cite["racketmanifesto"] presents it as a
+``programming-language programming language'', a language which helps with the
+creation of small linguistic extensions as well as entirely new languages. The
+Racket ecosystem features many languages covering many paradigms:
+
+@itemlist[
+ @item{The @racketmodname[racket/base] language is a full-featured programming
+ language which mostly encourages functional programming.}
+ @item{@racketmodname[racket/class] implements
+ @seclink["classes" #:doc '(lib "scribblings/guide/guide.scrbl")]{an
+ object-oriented system}, implemented atop @racketmodname[racket/base] using
+ macros, and can be used along with the rest of the @racketmodname[racket/base]
+ language.}
+ @item{@racketmodname[racklog] is a logic programming language in the style of
+ prolog. The Racket ecosystem also includes an implementation of
+ @racketmodname[datalog].}
+ @item{@seclink["top" #:doc '(lib "scribblings/scribble/scribble.scrbl")]{
+ Scribble} can be seen as an alternative to @|LaTeX|, and is used to create
+ the @seclink["top" #:doc '(lib "scribblings/main/start.scrbl")]{Racket
+ documentation}. It also supports literate programming, by embedding chunks of
+ code in the document which are then aggregated together. This thesis is
+ in fact written using Scribble.}
+ @item{@racketmodname[slideshow] is a @deftech{DSL} (domain-specific language)
+ for the creation of presentations, and can be thought as an alternative to
+ Beamer and SliTeX.}
+ @item{@racketmodname[r5rs] and @racketmodname[r6rs] are implementations of
+ the corresponding scheme standards.}
+ @item{@seclink["top" #:doc '(lib "redex/redex.scrbl")]{Redex} is a
+ @usetech{DSL} which allows the specification of reduction
+ semantics for programming languages. It features tools to explore and test
+ the defined semantics.}
+ @item{@|Typedracket|@~cite["tobin-hochstadt_design_2008"
+ "tobin-hochstadt_typed_2010"] is a typed variant of
+ the main @racketmodname[racket] language. It is implemented as a macro which
+ takes over the whole body of the program. That macro fully expands all other
+ macros in the program, and then typechecks the expanded program.}
+ @item{@seclink["top" #:doc '(lib "turnstile/scribblings/turnstile.scrbl")]{
+ @|Turnstile|} allows the creation of new typed languages. It takes a
+ different approach when compared to @|typedracket|, and threads the type
+ information through assignments and special forms, in order to be able to
+ typecheck the program during expansion, instead of doing so afterwards.}]
+
+In the remainder of this section, we will present the features of
+@|typedracket|'s type system, and then present formal semantics for a subset
+of those, namely the part which is relevant to our work.
+@other-doc['(lib "typed-racket/scribblings/ts-guide.scrbl")] and
+@other-doc['(lib "typed-racket/scribblings/ts-reference.scrbl")] provide good
+documentation for programmers who desire to use @|typedracket|; we will
+therefore keep our overview succinct and gloss over most details.
+
+@asection{
+ @atitle{Overview of Typed Racket's type system}
+
+ @asection{
+ @atitle{Simple primitive types}
+
+ @Typedracket has types matching Racket's baggage of primitive values:
+ @racket[Number], @racket[Boolean], @racket[Char], @racket[String],
+ @racket[Void]@note{The @racket[Void] type contains only a single value,
+ @racket[#,(void)], and is equivalent to the @racketid[void] type in
+ @|C-language|. It is the equivalent of @racketid[unit] of @CAML and
+ @|haskell|, and is often used as the return type of functions which perform
+ side-effects. It should not be confused with @racket[Nothing], the bottom
+ type which is not inhabited by any value, and is similar to the type of
+ @|haskell|'s @racketid[undefined]. @racket[Nothing] can be used for example
+ as the type of functions which never return — in that way it is similar to
+ @|C-language|'s @tt["__attribute__ ((__noreturn__))"].} and so on.
+
+ For numbers, @|typedracket| offers a ``numeric tower'' of
+ partially-overlapping types: @racket[Positive-Integer] is a subtype of
+ @racket[Integer], which is itself a subtype of @racket[Number]. @racket[Zero],
+ the type containing only the number 0, is a both a subtype of
+ @racket[Nonnegative-Integer] (numbers ≥ 0) and of @racket[Nonpositive-Integer]
+ (numbers ≤ 0).
+
+ @|Typedracket| also includes a singleton type for each primitive value of
+ these types: we already mentioned @racket[Zero], which is an alias of the
+ @racket[0] type. Every number, character, string and boolean value can be used
+ as a type, which is only inhabited by the same number, character, string or
+ boolean value. For example, @racket[243] belongs to the singleton type
+ @racket[243], which is a subtype of @racket[Positive-Integer].}
+
+ @asection{
+ @atitle{Pairs and lists}
+
+ Pairs are the central data structure of most Lisp dialects. They are used to
+ build linked lists of pairs, terminated by @racket['()], the null element. The
+ null element has the type @racket[Null], while the pairs which build the list
+ have the type @racket[(Pairof _A _B)], where @racketid[_A] and @racketid[_B]
+ are replaced by the actual types for the first and second elements of the
+ pair. For example, the pair built using @racket[(cons 729 #true)], which
+ contains @racket[729] as its first element, and @racket[#true] as its second
+ element, has the type @racket[(Pairof Number Boolean)], or using the most
+ precise singleton types, @racket[(Pairof 729 #true)].
+
+ Heterogeneous linked lists of fixed length can be given a precise type by
+ nesting the same number of pairs at the type level. For example, the list
+ built with @racket[(list 81 #true 'hello)] has the type
+ @racket[(List Number Boolean Symbol)], which is a shorthand for the type
+ @racket[(Pairof Number (Pairof Boolean (Pairof Symbol Null)))]. Lists in
+ @|typedracket| can thus be seen as the equivalent of a chain of nested
+ 2-tuples in languages like @|CAML| or @|haskell|. The analog in
+ object-oriented languages with support for generics would be a class
+ @tt["Pair<A, B>"], where the generic type argument @racketid[B] could be
+ instantiated by another instance of @racketid[Pair], and so on.
+
+ The type of variable-length homogeneous linked lists can be described using
+ the @racket[Listof] type operator. The type @racket[(Listof Integer)] is
+ equivalent to @racket[(Rec R (U (Pairof Integer R) Null))]. The @racket[Rec]
+ type operator describes @seclink["tr-presentation-recursive-types"]{recursive
+ types}, and @racket[U] describes @seclink["tr-presentation-unions"]{unions}.
+ Both of these features are described below, for now we will simply say that
+ the previously given type is a recursive type @racket[R], which can be a
+ @racket[(Pairof Integer R)] or @racket[Null] (to terminate the linked list).}
+
+ @asection{
+ @atitle{Symbols}
+
+ Another of Racket's primitive datatypes is symbols. Symbols are interned
+ strings: two occurrences of a symbol produce values which are pointer-equal if
+ the symbols are equal (i.e. they represent the same string)@note{This is true
+ with the exception of symbols created with @racket[gensym] and the like.
+ @racket[gensym] produces a fresh symbol which is not interned, and therefore
+ different from all existing symbols, and different from all symbols created
+ in the future.}.
+
+ @|Typedracket| includes the @racket[Symbol] type, to which all symbols
+ belong. Additionally, there is a singleton type for each symbol: the type
+ @racket['foo] is only inhabited by the symbol @racket['foo].
+
+ Singleton types containing symbols can be seen as similar to constructors
+ without arguments in @|CAML| and @|haskell|, and as globally unique enum
+ values in object-oriented languages. The main difference resides in the scope
+ of the declaration: two constructor declarations with identical names in two
+ separate files will usually give distinct types and values. Similarly, when
+ using the ``type-safe enum'' design pattern, two otherwise identical
+ declarations of an enum will yield objects of different types. In contrast,
+ two uses of an interned symbols in Racket and @|typedracket| will produce
+ identical values and types. A way of seeing this is that symbols act as uses
+ of constructors which are implicitly declared globally.}
+
+ @asection{
+ @atitle[#:tag "tr-presentation-unions"]{Unions}
+
+ These singleton types may not seem very useful on their own. They can however
+ be combined together with union types, which are built using the @racket[U]
+ type operator.
+
+ The union type @racket[(U 0 1 2)] is inhabited by the values @racket[0],
+ @racket[1] and @racket[2], and by no other value. The @racket[Boolean] type is
+ actually defined as @racket[(U #true #false)], i.e. the union of the singleton
+ types containing the @racket[#true] and @racket[#false] values, respectively.
+ The @racket[Nothing] type, which is not inhabited by any value, is defined as
+ the empty union @racket[(U)]. The type @racket[Any] is the top type, i.e. it
+ is a super-type of all other types, and can be seen as a large union including
+ all other types, including those which will be declared later or in other
+ units of code.
+
+ Unions of symbols are similar to variants which contain zero-argument
+ constructors, in @|CAML| or @|haskell|. A union such as
+ @racket[(U 'ca (List 'cb Number) (List 'cc String Symbol))] can be seen as
+ roughly the equivalent of a variant with three constructors, @racketid[ca],
+ @racket[cb] and @racketid[cc], where the first has no arguments, the second
+ has one argument (a @racket[Number]), and the third has two arguments (a
+ @racket[String] and a @racket[Symbol]). The main difference is that a symbol
+ can be used as parts of several unions, e.g. @racket[(U 'a 'b)] and
+ @racket[(U 'b 'c)], while constructors can often only be part of the variant
+ used to declare them. Unions of symbols are in this sense closer to @|CAML|'s
+ so-called polymorphic variants@~cite["minskyRealWorldOCaml"] than to regular
+ variants.
+
+ Finally, it is possible to mix different sorts of types within the same
+ union: the type @racket[(U 0 #true 'other)] is inhabited by the number
+ @racket[0], the boolean @racket[#true], and the symbol @racket['other].
+
+ Implementation-wise, all values in the so-called ``untyped'' version of
+ Racket are tagged: a few bits within the value's representation are reserved
+ and used to encode the value's type. When considering the target of a pointer
+ in memory, Racket is therefore able to determine if the pointed-to value is a
+ number, boolean, string, symbol and so on. Typed Racket preserves these
+ run-time tags. They can then be used to detect the concrete type of a value
+ when its static type is a union. This detection is done simply by using
+ Racket's predicates: @racket[number?], @racket[string?], @racket[symbol?]
+ etc.}
+
+ @asection{
+ @atitle{Intersections}
+
+ Intersections are the converse of unions: instead of allowing a mixture of
+ values of different types, an intersection type, described using the
+ @racket[∩] type operator, only allows values which belong to all types.
+
+ The intersection type @racket[(∩ Nonnegative-Integer Nonpositive-Integer)] is
+ the singleton type @racket[0]. The intersection of @racket[(U 'a 'b 'c)] and
+ @racket[(U 'b 'c 'd)] will be @racket[(U 'b 'c)], as @racket['b] and
+ @racket['c] belong to both unions.
+
+ @|Typedracket| is able to reduce some intersections such as those given above
+ at compile-time. However, in some cases, it is forced to keep the intersection
+ type as-is. For example, structs (@seclink["tr-presentation-structs"]{
+ describled below} can, using special properties, impersonate functions.
+ @|Typedracket| does not handle these properties (yet), and therefore cannot
+ determine whether a given struct type also impersonates a function or not.
+ This means that the intersection @racket[(∩ s (→ Number String))], where
+ @racket[s] is a struct type, cannot be reduced to @racket[Nothing], because
+ @|typedracket| cannot determine whether the struct @racket[s] can act as a
+ function or not.
+
+ Another situation where @|typedracket| cannot reduce the intersection of two
+ function types (@seclink["tr-presentation-functions"]{presented below}).
+
+ @racketblock[
+ (∩ (→ Number String) (→ Number Symbol))
+ (∩ (→ Number String) (→ Boolean String))]
+
+ The first intersection seems like could be simplified to
+ @racket[(→ Number String) (→ Number Symbol)], and the second one could be
+ simplified to @racket[(→ (U Number Boolean) String)], however the equivalence
+ between these types has not been implemented (yet) in @|typedracket|, so we do
+ not rely on them. Note that this issue is not a soundness issue: it only
+ prevents passing values types to which they belong in principle, but it
+ cannot be exploited to assign a value to a variable with an incompatible type.
+
+ Finally, when some types are intersected with a polymorphic type variable,
+ the intersection cannot be computed until the polymorphic type is
+ instantiated.
+
+ When @|typedracket| is able to perform a simplification, occurrences of
+ @racket[Nothing] (the bottom type) propagate outwards in some cases, pairs and
+ struct types which contain @racket[Nothing] as one of their elements being
+ collapsed to @racket[Nothing]. This propagation of @racket[Nothing] starts
+ from occurrences of @racket[Nothing] in the parts of the resulting type which
+ are traversed by the intersection operator. It collapses the containing pairs
+ and struct types to @racket[Nothing], moving outwards until the @racket[∩]
+ operator itself is reached. In principle, the propagation could go on past
+ that point, but this is not implemented yet in @|typedracket|@note{See
+ @hyperlink["https://github.com/racket/typed-racket/issues/552"]{Issue #552}
+ on @|typedracket|'s GitHub repository for more details on what prevents
+ implementing a more aggressive propagation of @racket[Nothing].}.
+
+ The type @racket[(∩ 'a 'b)] therefore gets simplified to @racket[Nothing],
+ and the type @racket[(∩ (Pairof 'a 'x) (Pairof 'b 'x))] also simplifies to
+ @racket[Nothing] (@|typedracket| initially pushes the intersection down the
+ pairs, so that the type first becomes @racket[(Pairof (∩ 'a 'b) (∩ 'x 'x))],
+ which is simplified to @racket[(Pairof Nothing 'x)], and the occurrence of
+ @racket[Nothing] propagates outwards). However, if the user directly specifies
+ the type @racket[(Pairof (∩ 'a 'b) Integer)], it is simplified to
+ @racket[(Pairof Nothing Integer)], but the @racket[Nothing] does not propagate
+ outwards beyond the initial use of @racket[∩].}
+
+ @asection{
+ @atitle[#:tag "tr-presentation-structs"]{Structs}
+
+ Racket also supports @racket[struct]s, which are mappings from fields to
+ values. A struct is further distinguished by its struct type: instances of two
+ struct types with the same name and fields, declared in separate files, can be
+ differentiated using the predicates associated with these structs. Structs in
+ Racket can be seen as the analog of classes containing only fields (but no
+ methods) in @csharp or @|java|. Such classes are sometimes called ``Plain Old
+ Data (POD) Objects''. Structs belong to a single-inheritance hierarchy:
+ instances of the descendents of a struct type are recognised by their
+ ancestor's predicate. When a struct inherits from another, it includes its
+ parent's fields, and can add extra fields of its own.
+
+ Each struct declaration within a @|typedracket| program also declares a
+ corresponding type. In @|typedracket|, structs have a number of polymorphic
+ type arguments, which can be used within the types of the struct's fields.
+
+ Racket further supports
+ @tech[#:doc '(lib "scribblings/reference/reference.scrbl")]{ struct type
+ properties}, which can be seen as a limited form of method definitions for a
+ struct, thereby making them closer to real objects. The same struct type
+ property can be implemented by many structs, and the declaration of a struct
+ type property is therefore roughly equivalent to the declaration of an
+ interface with a single method.
+
+ @todo{Briefly talk about Racket's
+ ``@seclink["struct-generics"
+ #:doc '(lib "scribblings/reference/reference.scrbl")]{
+ generic interfaces}'', which are an abstraction over struct type
+ properties and support the definition of several ``methods'' as part of a
+ single generic interface.}
+
+ @|Typedracket| offers no support for struct type properties and generic
+ interfaces, however. It is impossible to specify that a struct implement a
+ given property at the type level, and it is also for example not possible to
+ describe the type of a function accepting any struct implementing a given
+ property or generic interface. Finally, no type checks are performed on the
+ body of functions bound to such properties, and to check verifies that a
+ function implementation with the right signature is supplied to a given
+ property. Since struct type properties and generics cannot be used in a
+ type-safe way for now, we refrain from using these features, and only use them
+ to implement some very common properties@note{We built a thin macro wrapper
+ which allows typechecking the implementation and signature of the functions
+ bound to these two properties.}: @racket[prop:custom-write] which is the
+ equivalent of @|java|'s @tt["void toString()"], and @racket[prop:equal+hash]
+ which is equivalent to @|java|'s @tt["boolean equals(Object o)"] and
+ @tt["int hashCode()"].
+
+ }
+
+ @asection{
+ @atitle[#:tag "tr-presentation-functions"]{Functions}
+ @itemlist[
+ @item{Simple function types}
+ @item{Rest arguments}
+ @item{Case functions (i.e. lightweight dependent function types)}
+ @item{Polymorphic functions}
+ @item{Keyword and optional arguments}
+ @item{Filters (information gained on the input when a predicate returns true
+ or false)}]
+ }
+
+ @asection{
+ @atitle[#:tag "tr-presentation-recursive-types"]{Recursive types}
+ + recursion via named types
+ }
+
+ @asection{
+ @atitle{Classes}
+ }
+
+ @asection{
+ @atitle{Occurrence typing}
+ }
+
+ @asection{
+ @atitle{Global type inference}
+ }
+}
+\ No newline at end of file
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -129,7 +129,13 @@
;; TODO: merge the handling of unicode chars into scribble-math.
(define m
(list setup-math
- (tex-header "\\renewcommand{\\rmdefault}{cmr}")))
+ (tex-header "\\renewcommand{\\rmdefault}{cmr}")
+ (elem #:style (style #f (list (css-addition
+ #".NoteBox {
+ height: auto !important;
+ clear: right;
+ margin-bottom: 1em !important;
+}"))))))
(define my-title
;; TODO: use this for the other wrapped procs in this file
(make-keyword-procedure
