Thesis
1 Introduction
1.1 Warm-up
1.2 The challenges of writing compilers
1.2.1 Large monolithic passes
1.2.2 Overusing a single intermediate representation
1.2.3 Graphs
1.2.4 Expressing the data dependencies of a pass via row types
1.2.5 Verification
1.3 Summary
1.3.1 Extensible type system
1.3.2 Compiler-writing framework
1.3.3 Overview
2 State of the art
2.1 Extending the type system via macros
2.2 Algebraic datatypes for compilers
2.2.1 The case for bounded row polymorphism
2.3 Writing compilers using many small passes
2.4 Cycles in intermediate representations of programs
2.4.1 Mutable data structures
2.4.2 Unique identifiers used as a replacement for pointers
2.4.3 Explicit use of other common graph representations
2.4.4 Using lazy programming languages
2.4.5 True graph representations using immutable data structures
3 Goals, constraints and examples
4 Typed Racket
4.1 Overview of Typed Racket’s type system
4.1.1 Simple primitive types
4.1.2 Pairs and lists
4.1.3 Symbols
4.1.4 Unions
4.1.5 Intersections
4.1.6 Structs
4.1.7 Functions
4.1.8 Occurrence typing
4.1.9 Recursive types
4.1.10 Classes
4.1.11 Local type inference
4.2 Formal semantics for part of Typed Racket’s type system
4.2.1 Notations
4.2.2 Names and bindings
4.2.3 Expressions
4.2.4 Primitive operations (library functions)
4.2.5 Values
4.2.6 Evaluation contexts
4.2.7 Typing judgement
4.2.8 Types
4.2.9 Filters (value-dependent propositions)
4.2.10 Objects (aliasing information)
4.2.11 Paths
4.2.12 Path elements
4.2.13 Subtyping
4.2.14 Operational semantics
4.2.15 Type validity rules
4.2.16 Typing rules
4.2.17 Simplification of intersections
4.2.18 δ-rules
4.2.19 Soundness
5 Extensible type system and algebraic datatypes
5.1 Extensible type systems via type-level macros
5.2 Extension of Typed Racket with algebraic datatypes and row polymorphism
5.2.1 Notations
5.2.2 Types (with ρ)
5.2.3 Expressions (with ρ)
5.2.4 Values (with ρ)
5.2.5 Evaluation contexts (with ρ)
5.2.6 Type validity rules (with ρ)
5.2.7 Subtyping (with ρ)
5.2.8 Path elements (with ρ)
5.2.9 Typing rules (with ρ)
5.2.10 Operational Semantics (with ρ)
5.2.11 Shorthands (with ρ)
6 Typed nanopass
6.1 Typed nanopass on trees
6.2 Typed nanopass on DAGs
6.3 Typed nanopass on graphs
6.4 Structural invariants
6.5 Further possible extensions
7 Examples and results
8 Conclusion and future work directions
9 Bibliography
A Ph.C Graph library:   Implementation
A.1 Parametric replacement of parts of data structures
A.1.1 Introduction
define-fold
A.1.2 Implementation
A.1.2.1 Caching the results of define-fold
«with-folds»
«api»1
«api»2
«fold-τ»
«cached»
«api»3
«api»4
«fold-f»
«fold-f-proc»
«fold-f-type»
«f-cases»1
«type-cases»1
«type-cases»2
«f-cases»2
«type-cases»3
«f-cases»3
«type-cases»4
«f-cases»4
«type-cases»5
«ftype-cases»
«type-cases»6
«f-cases»5
«f-list-car»
«f-list-cdr»
«type-cases»7
«f-cases»6
«type-cases»8
«f-cases»7
«type-cases»9
«f-cases»8
«foldl-map»
A.1.3 Putting it all together
«*»
A.2 Flexible functional modification and extension of records
A.2.1 Goals
A.2.2 Overview
A.2.3 Generating the tree type with polymorphic holes
A.2.4 From a selection of field indieces to a tree shape
«idx→tree»
«idx→tree/ctc»1
«idx→tree/ctc»2
«idx→tree cases»1
«dichotomy»
A.2.5 Empty branches (branches only containing missing fields)
«empty-branches»
A.2.6 Creating a record builder given a set of field indices
«record-builder»
«record-builder/wrappers»1
A.2.7 Row typing
«ρ-wrapper»1
«ρ-wrapper»2
«ρ-table»
«record-type»1
«record-type/wrappers»1
«current-patch-table»
«with-ρ»
«with-ρ-chain»
A.2.7.1 Type of a record, with a multiple fields
«∀ρ»
«delayed-∀ρ»
«record-type»3
«make-lifo-set»
«lifo-member?»
«lifo-set-add!»
«lifo-set→list»
«patch»
«expand-ρ»
A.2.8 Type of a record, with a single hole
«tree-type-with-replacement»
A.2.9 Functionally updating a tree-record
A.2.9.1 Adding and modifying fields
«make-replace-in-tree-body»
«define-replace-in-tree»
A.2.10 Auxiliary values
«utils»
A.2.11 Type of a tree-record
«τ-tree-with-fields»
A.2.12 Conversion to and from record-trees
«define-struct↔tree»
A.2.12.1 Creating a new tree-record
«convert-fields»
A.2.12.2 Extracting all the fields from a tree-record
«convert-back-fields»
A.2.13 Defining the converters and accessors for each known record type
«define-trees»
«bt-fields-type»
«define-trees-result»
A.2.13.1 Putting it all together
«maybe»
«*»
A.2.14 Utility math functions for binary tree manipulation
«*»
to-bits
«to-bits»
«test-to-bits»
from-bits
«from-bits»
«test-from-bits»
floor-log2
«floor-log2»
ceiling-log2
«ceiling-log2»
A.3 Tracking checked contracts via refinement types
A.3.1 Introduction
A.3.2 Implementation overview :   subtyping, variance and phantom types
«invariant-1»
«invariant-2»
«invariant-2-use»
«phantom-types-ignored»
«invariant-3»
«invariant-4»
«invariant-set-as-List+Rec»
«invariant-set-as-List+Rec-use»
«invariant-set-as-contravariant-U»
«invariant-contract-subtyping»1
«invariant-contract-subtyping»2
«invariant-contract-subtyping»3
A.3.3 Encoding property implication as subtyping
«structural-draft»
A.3.3.1 Properties applying to all reachable nodes from x
«expanded-path-set»
A.3.3.2 Prefix trees to the rescue
«prefixes»1
«prefixes»2
A.3.3.3 Cycles in properties
A.3.3.4 Partial paths
A.3.3.5 Array and list indices
A.3.3.6 Other richer properties
A.3.4 Implementation
A.3.4.1 The witness value
«witness-value»
A.3.4.2 Grouping multiple invariants
«Or»
«grouping-invariants»
A.3.4.3 Structural (in)equality and (non-)membership invariants
A.3.4.3.1 Invariants and their relationships
A.3.4.4 Parsing paths
«parse»1
«parse»2
«π»
«Invariant»
«=»
«Invariants»
«Any*»
A.3.4.4.1 Comparison operator tokens
«comparison-operators»
«≡»
«cycles»
A.3.4.5 Putting it all together
«*»
A.4 Compile-time graph metadata
A.4.1 Graph type information
«graph-info»
A.4.2 Graph builder information
«graph-builder-info»
A.4.3 Node information
«node-info»
A.4.4 Field information
«field-info»
A.4.5 Invariant information
«invariant-info»
«gen:equal+hash free-id-tree=?»
A.4.6 Dependent invariant information
«dependent-invariant-info»
A.4.7 Mapping information
«mapping-info»
A.4.8 Printing
«printer»
«*»
A.5 Declaring graph types
«signature»
A.5.1 Implementation
«define-graph-type»
A.5.2 Declaring the node types
«declare-node-types»
A.5.3 Creating the graph-info instance
«build-graph-info»
«graph-info»
«node-info»
«field-info»
«invariant-info-op»
«invariant-info-p»
A.5.4 Putting it all together
«*»
A.6 Implementation of the graph macro
«graph»
«signature»
«implementation»
A.6.1 Overview of the implementation (draft)
«implementation-draft»
«define-indices»
«define-index»
«create-Qₖ»
«re-bind-mappings»
«entry-pointₖ»
«entry-point»
«process-queues»
«*»
A.7 Draft of the implementation of the graph macro
«overview»1
«signature+metadata»
«signature»
«metadata»
«phase 1: call mappings and extract placeholders»1
«phase~1: call mappings and extract placeholders»
«phase 1: call mappings and extract placeholders»2
«phase 2: inline placeholders within node boundaries»
«phase 3: replace indices with promises»
«equality-coalescing»
«invariants+auto-fill»
«inflexible-row-polymorphism»
«flexible-row-polymorphism»
«polymorphic-node-types-and-mappings»
«overview»2
«*»
A.8 Generalised constructor functions for flexible structures
«*»
«builder-τ»
«builder-τ-with-1»
«builder-function-type»
«builder-τ-with-2»
«Some or None»
«(Some Xⱼ) if Kⱼ = NSymᵢ»
«builder-τ-with-3»1
«builder-τ-with-3»2
«None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ»
«builder-function-type′»1
«propagate-τ»
«oracle-τ»
«oracle»
«builder-function-type″»1
«builder-f»
«builder-τ-with-4»
«builder-function-implementation»
B Algebraic Data Types for compilers:   Implementation
B.1 Algebraic Data Types
B.1.1 A note on polysemy
B.1.2 Introduction
B.1.3 Remembered data types and pre-declarations
«require-modules»1
B.1.4 The initialisation process
«require-modules»2
B.1.5 Tagged structures, untagged structures, constructors, and variants
«require-modules»3
«require-modules»4
«require-modules»5
«require-modules»6
«require-modules»7
«require-modules»8
«*»
B.2 Low-level implementation of tagged structures
B.2.1 Overview
B.2.2 Implementation using Racket structs
«define-tagged»
«define-common»
B.2.2.1 Nodes as subtypes of their corresponding tagged struct type
«define-node»
B.2.3 Common ancestor to all tagged structures:   Tagged  Top-struct
Tagged  Top-struct
«TaggedTop»
B.2.4 Printing and comparing structures and nodes
B.2.4.1 Printing tagged structures
«custom-write»
«format-field»
B.2.5 Comparing tagged structures
«equal+hash»
B.2.6 Pre-declaring structs
B.2.6.1 Why pre-declare the structs?
«pre-declare-all-tagged-structure-structs»1
«pre-declare-all-tagged-structure-structs»2
«pre-declare-all-tagged-structure-structs»3
B.2.6.2 Remembering tagged structures across compilations
«all-remembered-tagged-structures»
«remember-structure!»
check-remembered-common!
check-remembered-tagged!
check-remembered-node!
check-remembered-?!
«check-remembered!»1
«check-remembered!»2
«make-struct-identifier-from-list»
«make-struct-identifier-common»
«make-struct-identifier-tagged»
«make-struct-identifier-node»
«make-struct-identifier-tagged-pred»
B.2.6.3 Sorting the set of fields
«sort-fields»
«sort-fields-alist»
B.2.6.4 Not-yet-remembered structs should cause an error
«not-remembered»
«remember-empty-tagged-structure»
«remember-one-constructor»
B.2.7 Creating instances of a tagged structure
tagged-builder!
«tagged-builder!»
tagged-∀-builder!
«tagged-∀-builder!»
tagged-infer-builder!
«tagged-infer-builder!»
B.2.8 Predicate for a tagged structure
tagged-any-predicate!
«tagged-any-predicate!»
tagged-any-fields-predicate
«tagged-any-fields»
«tagged-any-fields-predicate»
B.2.8.1 A predicate over the contents of the fields
tagged-predicate!
«tagged-pred-lambda»
«tagged-pred-simple-type»
«tagged-pred-correct-type»
«define-tagged-pred»
«tagged-predicate!»
tagged-pred-predicate!
«tagged-pred-predicate!»
B.2.9 Matching against tagged structures
tagged-match!
«tagged-match!»
«match-not-remembered»
tagged-anytag-match!
«tagged-anytag-match!»
B.2.10 Type of a tagged structure
tagged-type!
«tagged-type!»
tagged-∀-type!
«tagged-∀-type!»
tagged-infer-type!
«tagged-infer-type!»
tagged-any-fields-type
«tagged-any-fields-type»
B.2.11 Accessing fields of tagged structures
tagged-get-field
«tagged-get-field»
λ-tagged-get-field
«λ-tagged-get-field»
B.2.12 Row polymorphism
B.2.12.1 Type for any tagged structure containing a given set of fields
has-fields
«has-fields»1
has-fields/  common
«has-fields»2
has-fields/  type
«has-fields/type»
B.2.12.2 Changing the tag of a tagged structure
change-tag
«change-tag»
«change-tag-factored-out»
«change-tag-case»
B.2.12.3 Splitting a tagged structure
split
«split»1
«split-compute-extra-fields»
«split-case-factored-out»
«split-case»
«split-check»
«split-error»
split/  type
«split»2
B.2.12.4 Merging two tagged structures
merge
«merge»1
«merge-case»
«merge-check»
«merge-error»
merge/  type
«merge»2
«merge-type-case»
B.2.12.5 Updating a tagged structure
with+
«with+»
«with+-check»
«with+-error»
with!
«with!»
«with!-case»
«with!-fieldⱼ-assoc»
«with!-fieldⱼ-overwritten»
with!!
«with!!»
«with!!-check»
«with!!-error»
tagged-struct-id?
«tagged-struct-id?»
«tagged-struct-ids-init-cache»
B.2.13 Putting it all together
«*»
«module-sorting-and-identifiers»
«module-pre-declare»
«main-module»
B.3 Implementation of nodes:   printing and equality
B.3.1 Printing nodes
«write-node-depth»
«node-custom-write»
«format-field»
B.3.2 Comparing and hashing nodes
«raw-node»
«raw-node-equality»
«same-node?»
«seen-hash-table»
«node-equal+hash»
B.3.2.1 Hashing nodes
«node-equal-hash-code»
«node-equal-secondary-hash-code»
«node-hash»
«hash-init-table-and-recur»
«find-in-table»
«make-unique-copy-node»
«compute-hash»
«combine-hash-codes»
B.3.2.2 Caching node equality
«equality-cache»
«with-node-equality-cache»
«make-equality-cache»
«memoize-equality»
B.3.2.3 Comparing nodes for equality
«node-equal?»
«equality-init-table-and-recur»
«compare»
«*»
Bibliography
B.4 Implementation of ADTs:   syntax scopes
«adt-context»1
«ctx-introduce»
«adt-context»2
«adt-context»3
«fresh-introducer»
«adt-context?»
«check-adt-context»
B.4.1 Putting it all together
«*»
B.5 User API for tagged structures
B.5.1 Overview of the implementation of structures
B.5.2 A polyvalent identifier:   type, match, constructor and instance
«tagged»
B.5.3 The tagged call expander (builder and instance)
«call [fieldᵢ] …+»
«no-values-error»
«call [fieldᵢ : τᵢ] …+»
«values-error»
«call [fieldᵢ valueᵢ] …+»
(no-values-error)
«call [fieldᵢ valueᵢ : τᵢ] …+»
(values-error)
B.5.3.1 Call to tagged with no fields: instance or constructor?
B.5.3.2 Signature for the tagged call expander
«name-id-mixin»
«∀-mixin»
«tagged-call-instance-or-builder-mixin»
«tagged-call-fields-mixin»
«empty-err»
«name-after-field-error»
«tagged-call-args-mixin»
B.5.3.3 Implementation
«call-expander»
«call-expander-cases»1
«call-expander-cases»2
B.5.4 Type expander
«tagged-type-fields-mixin»
«[fieldᵢ τᵢ] …+»
«[fieldᵢ] …+»
(name-after-field-error)
«tagged-type-args-mixin»
«type-expander»
«type-expander-cases»
B.5.4.1 The Tagged  Top type
«TaggedTop»1
«TaggedTop»2
B.5.5 Match expander
«tagged-match-no-implicit-bind-mixin»
«tagged-match-fields-mixin»
«[fieldᵢ patᵢⱼ …] …+»
(name-after-field-error)
«tagged-match-args-mixin»
«match-expander»
«match-expander-body»
B.5.6 Predicates for tagged structures
«tagged?»
B.5.6.1 The Tagged  Top? predicate
«provide TaggedTop?»
B.5.7 Defining shorthands with define-tagged
«tag-kw-mixin»
«default-tag-name»
«predicate?-mixin»
«default-name?»
«define-tagged-args-mixin»
«define-tagged»
«type-expander/define»
«match-expander/define»
«else-expander/define»
«predicate/define»
B.5.8 Implementation of uniform-get
B.5.9 Putting it all together
«*»
B.6 Supertypes of tagged structures
B.6.1 type-expander
«tagged-supertype»
«tagged-supertype-type-expander-signature-types»
«tagged-supertype-type-expander-signature-infer»
«tagged-supertype-type-expander-impl-types»
«tagged-supertype-type-expander-impl-infer»
«tagged-supertype-type-expander»
B.6.2 Match
«tagged-supertype-match-expander»
«tagged-anytag-match»
«maybe-pat…»
B.6.3 Nested supertype
«tagged-supertype*»
B.6.4 Conclusion
«*»
B.7 User API for untagged structures
B.7.1 Introduction
«structure»
«expand-to-tagged»
«structure?»
B.7.2 Defining untagged structures with define-structure
«define-structure»
B.7.3 Implementation of Structure  Top and Structure  Top?
«StructureTop?»
«StructureTop»
B.7.4 Supertypes for structures
«structure-supertype»
«expand-to-tagged-supertype»
B.7.5 Putting it all together
«*»
B.8 User API for constructors
B.8.1 Introduction
B.8.2 The polyvalent identifier constructor: type, match, builder and instance
«constructor»
«constructor?»
B.8.3 Type-expander
«name-id-mixin»
«∀-mixin»
«constructor-type-types-mixin»
«name-after-field-error»
«constructor-type-args-mixin»
«type-expander»
B.8.4 Match-expander
«match-expander»
B.8.5 Predicate
«predicate»
B.8.6 Instance creation
«infer-pat»
«call-expander-cases»1
«colon-pat»
«call-expander-cases»2
«!-pat»
«call-expander-cases»3
«dcolon-pat»
«call-expander-cases»4
«call-expander-cases»5
«value-maybe-type»
«literal-value»
«replace-chars»
«call-expander-rest»
«call-expander-rest-keyword»
«call-expander-empty-rest»
«call-expander-dotted-rest»
«type-label-syntax-class»
«call-expander»
B.8.7 Defining shorthands for constructors with define-constructor
«tag-kw-mixin»
«default-tag-name»
«predicate?-mixin»
«default-name?»
(colon-pat)
(!-pat)
(dcolon-pat)
«define-constructor»
«multi-id/define»
«type-expander/define»
«call-expander/define»
«normalize-type/define»1
«with-normalize»
«normalize-type/define»2
«match-expander/define»
«match-rest-signature/define»
«match-xlist/define»
«predicate/define»
B.8.8 Miscellanea
«constructor-values»
«ConstructorTop?»
«ConstructorTop»
B.8.9 Putting it all together
«*»
B.9 User API for variants
B.9.1 Introduction
B.9.2 Implementation of variant
«constructor-or-tagged-stx-class»
«variant»
B.9.3 Predicate
«variant?»
B.9.4 define-variant
«define-variant»
B.9.5 Conclusion
«*»
B.10 Somewhat outdated overview of the implementation choices for structures, graphs and passes
B.10.1 Structures
«example-simple-structure»
«example-simple-structure-occurrence»
B.10.2 Passes, subtyping and tests
«example-pass-which-extends-input»1
«example-pass-which-extends-input»2
«example-pass-which-extends-input»3
B.10.3 Graphs
«test-promise-occurence-typing»
B.10.4 Conclusion
«*»
C Implementation of Remember
C.1 remember
«remembered-values»1
«remembered-values»2
«remember-file»
«remember»
«delayed-errors»
«error»
«remember-all-hard-error»
«disable-remember-errors»
«lift-maybe-delayed-errors»
«get-remembered»
«provide»
«*»
D Implementation of the multi-id library
D.1 Syntax properties implemented by the defined multi-id
«props»1
«maybe-define-type»1
«maybe-define-type»2
«props»2
«props»3
«props»4
«props»5
«multi-id-body»
D.2 Signature of the multi-id macro
«multi-id»
«type-expander-kws»
«match-expander-kws»
«custom-write-kw»
«set!-transformer-kws»
«stx-class-kw-else»
«stx-class-kw-set!+call+id»
«fail-set!»
«fallback-kw»
«prop-keyword-syntax-class»
D.3 Tests for multi-id
«test-multi-id»1
«test-multi-id»2
«test-multi-id»3
D.4 Conclusion
«*»
E Type expander:   Implementation
E.1 Implementation of the type expander library
E.1.1 Introduction
E.1.2 Expansion model for type expanders
E.1.2.1 Comparison with Te  X’s macro expansion model
E.1.2.2 Interactions between type expanders and scopes
E.1.3 The prop:  type-expander structure type property
«prop:type-expander»
«prop-guard»
«prop-guard-field-index»
«prop-guard-field-value»
«prop-guard-procedure»
«prop-guard-else-error»
E.1.3.1 The type-expander struct
«type-expander-struct»
E.1.4 Associating type expanders to identifiers
E.1.4.1 The type-expander syntax class
«expand-type-syntax-classes»
«type-syntax-class»
«type-contract»
«type-expand-syntax-class»
E.1.4.2 Calling type expanders
«apply-type-expander»
«apply-type-expander-checks»
E.1.4.3 Associating type expanders to already existing identifiers
«patched»
«patch»
E.1.4.4 Defining new type expanders
«define-type-expander»
E.1.4.5 Locally binding type expanders
E.1.5 Expanding types
«expand-type»
E.1.5.1 Cases handled by expand-type
E.1.5.2 Applying type expanders
«expand-type-case-expander»1
«expand-type-case-expander»2
«expand-type-case-app-expander»
«expand-type-case-app-other»
E.1.5.2.1 Polymorphic types with
«expand-type-case-∀-through»
«shadowed»
«expand-type-case-∀-later»
«expand-type-case-∀-app»
«app-args-error»
E.1.5.2.2 Recursive types with Rec
«expand-type-case-Rec»
E.1.5.2.3 Local bindings with Let and Letrec
«expand-type-case-Let»
«expand-type-case-Letrec»
E.1.5.2.4 Anonymous types with Λ
«eval-anonymous-expander-code»
«expand-type-case-app-Λ»
«expand-type-case-just-Λ/not-applicable»
«expand-type-case-Λ-later»
E.1.5.2.5 Preventing the expansion of types with No-Expand
«expand-type-case-noexpand»
E.1.5.2.6 The overloaded : identifier
«expand-type-case-:»
E.1.5.2.7 Last resort cases:   leaving the type unchanged
«expand-type-case-app-fallback»
«expand-type-case-fallback-T»
E.1.5.3 Debugging type expanders
«expand-type-debug-outer»1
«debug-type-expander»
«expand-type-debug-outer»2
«expand-type-debug-indent»
«expand-type-debug-before»
«expand-type-debug-after»
«expand-type-debug-rules»
E.1.6 Overloading typed/  racket forms
E.1.6.1 syntax classes
«remove-ddd»
«syntax-classes»1
E.1.6.2 Overview of the overloaded primitives
E.1.6.3 :
«:»
E.1.6.4 define-type
«define-type»
E.1.6.5 define
«define»
E.1.6.6 lambda
«lambda»
E.1.6.7 case-lambda
«case-lambda»
E.1.6.8 struct
«struct»
E.1.6.9 define-struct/  exec
«define-struct/exec»
E.1.6.10 ann
«ann»
E.1.6.11 cast
«cast»
E.1.6.12 unsafe-cast
«unsafe-cast»
E.1.6.13 inst
«inst»
E.1.6.14 row-inst
«row-inst»
E.1.6.15 let
«let»
E.1.6.16 let*
«let*»
E.1.6.17 let-values
«let-values»
E.1.6.18 make-predicate
«make-predicate»
E.1.6.19 :  type, :  print-type, :  query-type/  args, :  query-type/  result
«:type»
«:print-type»
«:query-type/args»
«:query-type/result»
E.1.6.20 Type expanders for the typed classes
«syntax-classes»2
«syntax-classes»3
«syntax-classes»4
«syntax-classes»5
«class»
E.1.6.21 Other typed/  racket forms
«other-forms»
E.1.7 Future work
E.1.8 Conclusion
«module-expander»
«module-main»
«*»
E.2 Some example type expanders
E.2.1 Example type expanders:   quasiquote and quasisyntax
«quotes»1
«quotes»2
«quotes»3
«quotes»4
«expand-quasiquote»
E.2.2 Implementation of the Let* special type expander form
«Let*»
E.2.3 curry
«curry»
E.2.4 Putting it all together
«*»
2017-08-24--efa7621--6.9

Thesis

Georges Dupéron <georges.duperon@gmail.com>

\def\ifmathjax#1{#1}\def\iflatex#1{}

Download a PDF version of this document. Download a Zip archive of the HTML and PDF versions of this document.

    1 Introduction

      1.1 Warm-up

      1.2 The challenges of writing compilers

        1.2.1 Large monolithic passes

        1.2.2 Overusing a single intermediate representation

        1.2.3 Graphs

        1.2.4 Expressing the data dependencies of a pass via row types

        1.2.5 Verification

      1.3 Summary

        1.3.1 Extensible type system

        1.3.2 Compiler-writing framework

        1.3.3 Overview

    2 State of the art

      2.1 Extending the type system via macros

      2.2 Algebraic datatypes for compilers

        2.2.1 The case for bounded row polymorphism

      2.3 Writing compilers using many small passes (a.k.a following the Nanopass Compiler Framework philosophy)

      2.4 Cycles in intermediate representations of programs

        2.4.1 Mutable data structures

        2.4.2 Unique identifiers used as a replacement for pointers

        2.4.3 Explicit use of other common graph representations

        2.4.4 Using lazy programming languages

        2.4.5 True graph representations using immutable data structures

    3 Goals, constraints and examples

    4 Typed Racket

      4.1 Overview of Typed Racket’s type system

        4.1.1 Simple primitive types

        4.1.2 Pairs and lists

        4.1.3 Symbols

        4.1.4 Unions

        4.1.5 Intersections

        4.1.6 Structs

        4.1.7 Functions

        4.1.8 Occurrence typing

        4.1.9 Recursive types

        4.1.10 Classes

        4.1.11 Local type inference

      4.2 Formal semantics for part of Typed Racket’s type system

        4.2.1 Notations

        4.2.2 Names and bindings

        4.2.3 Expressions

        4.2.4 Primitive operations (library functions)

        4.2.5 Values

        4.2.6 Evaluation contexts

        4.2.7 Typing judgement

        4.2.8 Types

        4.2.9 Filters (value-dependent propositions)

        4.2.10 Objects (aliasing information)

        4.2.11 Paths

        4.2.12 Path elements

        4.2.13 Subtyping

        4.2.14 Operational semantics

        4.2.15 Type validity rules

        4.2.16 Typing rules

        4.2.17 Simplification of intersections

        4.2.18 δ-rules

        4.2.19 Soundness

    5 Extensible type system and algebraic datatypes

      5.1 Extensible type systems via type-level macros

      5.2 Extension of Typed Racket with algebraic datatypes and row polymorphism

        5.2.1 Notations

        5.2.2 Types (with ρ)

        5.2.3 Expressions (with ρ)

        5.2.4 Values (with ρ)

        5.2.5 Evaluation contexts (with ρ)

        5.2.6 Type validity rules (with ρ)

        5.2.7 Subtyping (with ρ)

        5.2.8 Path elements (with ρ)

        5.2.9 Typing rules (with ρ)

        5.2.10 Operational Semantics (with ρ)

        5.2.11 Shorthands (with ρ)

    6 Typed nanopass

      6.1 Typed nanopass on trees

      6.2 Typed nanopass on DAGs

      6.3 Typed nanopass on graphs

      6.4 Structural invariants

      6.5 Further possible extensions

    7 Examples and results

    8 Conclusion and future work directions

    9 Bibliography

    A Ph.C Graph library: Implementation

      A.1 Parametric replacement of parts of data structures

        A.1.1 Introduction

        A.1.2 Implementation

          A.1.2.1 Caching the results of define-fold

        A.1.3 Putting it all together

      A.2 Flexible functional modification and extension of records

        A.2.1 Goals

        A.2.2 Overview

        A.2.3 Generating the tree type with polymorphic holes

        A.2.4 From a selection of field indieces to a tree shape

        A.2.5 Empty branches (branches only containing missing fields)

        A.2.6 Creating a record builder given a set of field indices

        A.2.7 Row typing

          A.2.7.1 Type of a record, with a multiple fields

        A.2.8 Type of a record, with a single hole

        A.2.9 Functionally updating a tree-record

          A.2.9.1 Adding and modifying fields

        A.2.10 Auxiliary values

        A.2.11 Type of a tree-record

        A.2.12 Conversion to and from record-trees

          A.2.12.1 Creating a new tree-record

          A.2.12.2 Extracting all the fields from a tree-record

        A.2.13 Defining the converters and accessors for each known record type

          A.2.13.1 Putting it all together

        A.2.14 Utility math functions for binary tree manipulation

      A.3 Tracking checked contracts via refinement types

        A.3.1 Introduction

        A.3.2 Implementation overview : subtyping, variance and phantom types

        A.3.3 Encoding property implication as subtyping

          A.3.3.1 Properties applying to all reachable nodes from x

          A.3.3.2 Prefix trees to the rescue

          A.3.3.3 Cycles in properties

          A.3.3.4 Partial paths

          A.3.3.5 Array and list indices

          A.3.3.6 Other richer properties

        A.3.4 Implementation

          A.3.4.1 The witness value

          A.3.4.2 Grouping multiple invariants

          A.3.4.3 Structural (in)equality and (non-)membership invariants

            A.3.4.3.1 Invariants and their relationships

          A.3.4.4 Parsing paths

            A.3.4.4.1 Comparison operator tokens

          A.3.4.5 Putting it all together

      A.4 Compile-time graph metadata

        A.4.1 Graph type information

        A.4.2 Graph builder information

        A.4.3 Node information

        A.4.4 Field information

        A.4.5 Invariant information

        A.4.6 Dependent invariant information

        A.4.7 Mapping information

        A.4.8 Printing

      A.5 Declaring graph types

        A.5.1 Implementation

        A.5.2 Declaring the node types

        A.5.3 Creating the graph-info instance

        A.5.4 Putting it all together

      A.6 Implementation of the graph macro

        A.6.1 Overview of the implementation (draft)

      A.7 Draft of the implementation of the graph macro

      A.8 Generalised constructor functions for flexible structures

    B Algebraic Data Types for compilers: Implementation

      B.1 Algebraic Data Types

        B.1.1 A note on polysemy

        B.1.2 Introduction

        B.1.3 Remembered data types and pre-declarations

        B.1.4 The initialisation process

        B.1.5 Tagged structures, untagged structures, constructors, and variants

      B.2 Low-level implementation of tagged structures

        B.2.1 Overview

        B.2.2 Implementation using Racket structs

          B.2.2.1 Nodes as subtypes of their corresponding tagged struct type

        B.2.3 Common ancestor to all tagged structures: TaggedTop-struct

        B.2.4 Printing and comparing structures and nodes

          B.2.4.1 Printing tagged structures

        B.2.5 Comparing tagged structures

        B.2.6 Pre-declaring structs

          B.2.6.1 Why pre-declare the structs?

          B.2.6.2 Remembering tagged structures across compilations

          B.2.6.3 Sorting the set of fields

          B.2.6.4 Not-yet-remembered structs should cause an error

        B.2.7 Creating instances of a tagged structure

        B.2.8 Predicate for a tagged structure

          B.2.8.1 A predicate over the contents of the fields

        B.2.9 Matching against tagged structures

        B.2.10 Type of a tagged structure

        B.2.11 Accessing fields of tagged structures

        B.2.12 Row polymorphism

          B.2.12.1 Type for any tagged structure containing a given set of fields

          B.2.12.2 Changing the tag of a tagged structure

          B.2.12.3 Splitting a tagged structure

          B.2.12.4 Merging two tagged structures

          B.2.12.5 Updating a tagged structure

        B.2.13 Putting it all together

      B.3 Implementation of nodes: printing and equality

        B.3.1 Printing nodes

        B.3.2 Comparing and hashing nodes

          B.3.2.1 Hashing nodes

          B.3.2.2 Caching node equality

          B.3.2.3 Comparing nodes for equality

        Bibliography

      B.4 Implementation of ADTs: syntax scopes

        B.4.1 Putting it all together

      B.5 User API for tagged structures

        B.5.1 Overview of the implementation of structures

        B.5.2 A polyvalent identifier: type, match, constructor and instance

        B.5.3 The tagged call expander (builder and instance)

          B.5.3.1 Call to tagged with no fields: instance or constructor?

          B.5.3.2 Signature for the tagged call expander

          B.5.3.3 Implementation

        B.5.4 Type expander

          B.5.4.1 The TaggedTop type

        B.5.5 Match expander

        B.5.6 Predicates for tagged structures

          B.5.6.1 The TaggedTop? predicate

        B.5.7 Defining shorthands with define-tagged

        B.5.8 Implementation of uniform-get

        B.5.9 Putting it all together

      B.6 Supertypes of tagged structures

        B.6.1 type-expander

        B.6.2 Match

        B.6.3 Nested supertype

        B.6.4 Conclusion

      B.7 User API for untagged structures

        B.7.1 Introduction

        B.7.2 Defining untagged structures with define-structure

        B.7.3 Implementation of StructureTop and StructureTop?

        B.7.4 Supertypes for structures

        B.7.5 Putting it all together

      B.8 User API for constructors

        B.8.1 Introduction

        B.8.2 The polyvalent identifier constructor: type, match, builder and instance

        B.8.3 Type-expander

        B.8.4 Match-expander

        B.8.5 Predicate

        B.8.6 Instance creation

        B.8.7 Defining shorthands for constructors with define-constructor

        B.8.8 Miscellanea

        B.8.9 Putting it all together

      B.9 User API for variants

        B.9.1 Introduction

        B.9.2 Implementation of variant

        B.9.3 Predicate

        B.9.4 define-variant

        B.9.5 Conclusion

      B.10 Somewhat outdated overview of the implementation choices for structures, graphs and passes

        B.10.1 Structures

        B.10.2 Passes, subtyping and tests

        B.10.3 Graphs

        B.10.4 Conclusion

    C Implementation of Remember

      C.1 remember

    D Implementation of the multi-id library

      D.1 Syntax properties implemented by the defined multi-id

      D.2 Signature of the multi-id macro

      D.3 Tests for multi-id

      D.4 Conclusion

    E Type expander: Implementation

      E.1 Implementation of the type expander library

        E.1.1 Introduction

        E.1.2 Expansion model for type expanders

          E.1.2.1 Comparison with TeX’s macro expansion model

          E.1.2.2 Interactions between type expanders and scopes

        E.1.3 The prop:type-expander structure type property

          E.1.3.1 The type-expander struct

        E.1.4 Associating type expanders to identifiers

          E.1.4.1 The type-expander syntax class

          E.1.4.2 Calling type expanders

          E.1.4.3 Associating type expanders to already existing identifiers

          E.1.4.4 Defining new type expanders

          E.1.4.5 Locally binding type expanders

        E.1.5 Expanding types

          E.1.5.1 Cases handled by expand-type

          E.1.5.2 Applying type expanders

            E.1.5.2.1 Polymorphic types with

            E.1.5.2.2 Recursive types with Rec

            E.1.5.2.3 Local bindings with Let and Letrec

            E.1.5.2.4 Anonymous types with Λ

            E.1.5.2.5 Preventing the expansion of types with No-Expand

            E.1.5.2.6 The overloaded : identifier

            E.1.5.2.7 Last resort cases: leaving the type unchanged

          E.1.5.3 Debugging type expanders

        E.1.6 Overloading typed/racket forms

          E.1.6.1 syntax classes

          E.1.6.2 Overview of the overloaded primitives

          E.1.6.3 :

          E.1.6.4 define-type

          E.1.6.5 define

          E.1.6.6 lambda

          E.1.6.7 case-lambda

          E.1.6.8 struct

          E.1.6.9 define-struct/exec

          E.1.6.10 ann

          E.1.6.11 cast

          E.1.6.12 unsafe-cast

          E.1.6.13 inst

          E.1.6.14 row-inst

          E.1.6.15 let

          E.1.6.16 let*

          E.1.6.17 let-values

          E.1.6.18 make-predicate

          E.1.6.19 :type, :print-type, :query-type/args, :query-type/result

          E.1.6.20 Type expanders for the typed classes

          E.1.6.21 Other typed/racket forms

        E.1.7 Future work

        E.1.8 Conclusion

      E.2 Some example type expanders

        E.2.1 Example type expanders: quasiquote and quasisyntax

        E.2.2 Implementation of the Let* special type expander form

        E.2.3 curry

        E.2.4 Putting it all together

1 Introduction

\def\ifmathjax#1{#1}\def\iflatex#1{}

1.1 Warm-up

[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)]Todo

1.2 The challenges of writing compilers

Brain surgery? — It’s not exactly rocket science, is it?

That Mitchell & Webb Look, Series 3 — BBC Two

Compilers are an essential part of today’s software systems. Compilers translate high-level languages with complex semantics into lower-level 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, 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. 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[ (Sandberg 1988)]Todo.

Given their broad role, the complexity of the transformations involved, and the stringent requirements, writing compilers is a difficult task. Multiple pitfalls await the compiler engineer, which we will discuss in more detail below. This thesis aims to improve the compiler-writing toolkit currently available, in order to help compiler developers produce compilers which are closer to correctness, and easier to maintain.


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 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. 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:

The first two issues are prone to manifestations of some form or another of the “god object” anti-pattern11 The “god object” anti-pattern describes object-oriented classes which do too much or know too much. The size of these classes tends to grow out of control, and there is usually a tight coupling between the methods of the object, which in turn means that performing small changes may require understanding the interactions between random parts of a very large file, in order to avoid breaking existing functionality.. The last issue is merely caused by the choice of an abstraction which does not accurately represent the domain. We will discuss each of these ailments in more detail in the following sections, and detail the undesirable symptoms associated with them.

1.2.1 Large monolithic passes

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 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 test), harder to debug (as many unrelated concerns interact to some extent with each other), and harder to extend (for example, adding a new special form to the language will necessitate changes to several transformations, but if these are mingled in a single pass, the changes may be scattered through it, and interact with a significant amount of surrounding code). This higher maintenance cost also comes with another drawback: formal verification of the compiler will clearly be more difficult when large, tangled chunks of code which handle different semantic aspects are involved.

[Talk a bit about compcert here (one of the few/ the only formally verified compilers).]Todo

1.2.2 Overusing a single intermediate representation

The static analysis, optimisation and code generation phases could in principle work on the same intermediate representation. However, several issues arise from this situation.

In principle, new information gained by the static analysis may be added to the existing representation via mutation, or the optimiser could directly alter the IR. This means that the IR will initially contain holes (e.g. represented by null values), which will get filled in gradually. Manipulating these parts is then risky, as it is easy to accidentally attempt to retrieve a value before it was actually computed. Using the same IR throughout the compiler also makes it difficult for later passes to assume that some constructions have been eliminated by previous simplification passes, and correctness relies on a fixed order of execution of the passes; parts of the code which access data introduced or modified by other passes are more brittle and may be disrupted when code is refactored (for example, when moving the computation of some information to a later pass).

This situation becomes worse during the maintenance phase of the compiler’s lifecycle: when considering the data manipulated by a small portion of code (in order to fix or improve said code), it is unclear which parts are supposed to be filled in at that point, as well as which parts have been eliminated by prior simplification passes.

Furthermore, a mutable IR hinders parallel execution of compiler passes. Indeed, some compiler passes will perform global transformations or analyses, and such code may be intrinsically difficult to parallelise. 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 synchronise concurrent accesses or modifications.

Using immutable intermediate representations (and performing shallow copies when updating data) can help with this second issue. However, there is more to gain if, instead of having many instances of the same type, each intermediate representation is given a distinct, precise type. The presence or absence of computed information can be known from the input and output type of a pass, instead of relying on the order of execution of the passes in order to know what the input data structure may contain.

1.2.3 Graphs

Nontrivial programs are inherently graphs: they may contain mutually recursive functions (which directly refer to each other, and therefore will form a cycle in a representation of the program), circular and (possibly mutually) recursive datatypes may syntactically contain (possibly indirect) references to themselves, and the control flow graph of a function or method can, as its name implies, contain instructions which perform conditional or unconditional backwards branches.

However, nearly every compiler textbook will mention the use of Abstract Syntax Trees (ASTs) to represent the program. This means that a structure, which intrinsically has the shape of a graph, is encoded as a tree.

Edges in the graph which may embody backward references can be made explicit in various ways:

Although some of these seem like viable solutions (e.g. explicitly freezing objects), they still involve low-level mechanisms to create the graph. When functionally replacing a node with a new version of itself, all references to it must be updated to point to the new version. Furthermore, code traversing the graph to gather information or perform updates needs to deal with cycles, in order to avoid running into an infinite loop (or infinite recursion). Finally, backward edges are not represented in the same way as forward edges, introducing an arbitrary distinction when fetching data from the neighbours of a node. This last aspect reduces the extensibility of code which manipulates graphs where access to fields is not done uniformly: supposing new features of the language to be compiled require turning a “seamless” edge into one which must be explicitly resolved in some way (e.g. because this node, in the updated IR, may now be part of cycles), this change of interface will likely break old code which relied on seamless access to that field.

We think that the compiler engineer could benefit from abstracting over these implementation details, and think of compiler passes in terms of graph transformations. Programmers using functional languages often write list transformations using functions like map, foldl, filter, zip and so on, instead of explicitly writing recursive functions.

The graph can be manipulated by updating some or all nodes of a given type, using an old-node to new-node transformation function. This transformation function could produce more than one node, by referencing the extra nodes from the replacement one. It should furthermore be possible to locally navigate through the graph, from its root and from the node currently being transformed. This interface would allow to seamlessly handle cycles — transformations which apply over a whole collection of nodes need not be concerned with cycles — and still allow local navigation, without distinguishing backward and forward edges.

1.2.4 Expressing the data dependencies of a pass via row types

It is easy enough to test a compiler by feeding it sample programs and checking that the compiled output behaves as expected. However, a specific set of conditions inside a given pass, in order to achieve reasonably complete code coverage, may prove to be a harder task: previous passes may modify the input program in unexpected ways, and obtaining a certain data configuration at some point in the compiler requires the developer to mentally execute the compiler’s code backwards from that point, in order to determine the initial conditions which will produce the desired configuration many steps later. This means that extensively testing corner cases which may occur in principle, but are the result of unlikely combinations of features in the input program, is a cumbersome task.

If the compiler consists of many small passes, whose inputs and outputs are serializable, then it becomes possible to thoroughly test a single pass in isolation, by supplying an artificial, crafted input, and checking some properties of its output.

However, a compiler written following the Nanopass philosophy will feature many small passes which read and update only a small part of their input. Specifying actual values for the irrelevant parts of the data not only makes the test cases more verbose than they need to be, but also hides out of plain sight which variations of the input matter (and may thus allow the detection of new errors), and which parts of the input are mere placeholders whose actual value will not influence the outcome of the pass, aside from being copied over without changes.

It is desirable to express, in a statically verifiable way, which parts of the input are relevant, and which parts are copied verbatim (modulo updated sub-elements). Furthermore, it would be useful to be able to only specify the relevant parts of tests, and omit the rest (instead of supplying dummy values).

Row polymorphism allows us to satisfy both expectations. The irrelevant fields of a record and the irrelevant cases of a variant type can be abstracted away under a single row type variable. “Row” operations on records allow reading and updating relevant fields, while keeping the part abstracted by the row type variable intact. When invoking a compiler pass, the row type variables may be instantiated to the full set of extra fields present in the real IR, when the pass is called as part of the actual compilation; it is also possible, when the pass is called during testing, to instantiate them to an empty set of fields (or to use a single field containing a unique identifier, used to track “object identity”).

1.2.5 Verification

[Needs a transition from the previous section, or this should be moved elsewhere.]Todo

The implementation presented in this thesis cannot be immediately extended to support end-to-end formal verification of the compiler being written. However, it contributes to pave the way for writing formally verified compilers: firstly, the smaller passes are easier to verify. Secondly, the use of intermediate representations which closely match the input and output data can be used, given a formal semantic of each IR, to assert that a transformation pass is systematically preserving the semantics of the input. Thirdly, the use of a typed language instead of the currently “untyped” Nanopass framework means that a lot of properties can be ensured by relying on the type system. Typed Racket’s type checker is not formally verified itself and would have to be trusted (alternatively, the adventurous researcher could attempt to derive well-typedness proofs automatically by hijacking the type checker to generate traces of the steps involved, or manually, only using the type checker as a helper tool to detect and weed out issues during development. Fourthly, the explicit specification of the dependencies of passes on their input via row types is a form of frame specification, and can significantly ease the verification effort, as the engineer can rely on the fact that irrelevant parts were not modified in the output. These are statically enforced by our extension of Typed Racket’s type system, which we formalise in chapter [??]Todo. This relies on trusting Typed Racket itself once again, and on the correctness of the implementation of our translation from the extended type system to Typed Racket’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 references. We are hopeful that eliminating this mismatch will be beneficial to the formal verification of the transformation passes.

These advantages would be directly available to engineers attempting a formal proof of their compiler, while trusting the correctness of Typed Racket, as well as that of our framework. The implementation of our framework is not hardened, and Typed Racket itself suffers from a small number of known sources of unsoundness22 See https://github.com/racket/typed-racket/issues., however. In order to do an end-to-end verification of a compiler, it would be necessary to port our approach to a language better suited to formal verification. Alternatively, Racket could in principle be extended to help formalisation efforts. Two approaches come to mind: the first consists in proving that the macros correctly implement the abstraction which they attempt to model; the second would be to have the macros inject annotations and hints indicating properties that must be proven, in the same way that type annotations are currently inserted. These hints could then be used by the prover to generate proof obligations, which could then be solved manually or automatically.

Mixing macros and language features which help obtaining static guarantees is a trending topic in the Racket ecosystem and in other communities.

Typed Racket is still in active development, and several other projects were presented recently.

Hackett33 https://github.com/lexi-lambda/hackett, mainly developed by King, is a recent effort to bring a Haskell 98-like type system to Racket.

Hackett is built on the techniques developed by Chang, Knauth and Greenman in  (Chang et al. 2017), which lead to the Turnstile library44 https://bitbucket.org/stchang/macrotypes.git. Turnstile is a helper library which facilitates the creation of typed languages in Racket. Macros are amended with typing rules, which are used to thread type information through uses of macros, definition forms and other special forms. Type checking is therefore performed during macro-expansion, and does not rely on an external type checker which would work on the expanded code. As a result, new languages built with Racket and Turnstile are not limited to a pre-existing type system, but can rather devise their own from the ground up. This approach brings a lot of flexibility, the drawback being that more trust is put in the language designer.

The work presented in this thesis aims to follow a different path than that followed by Turnstile: we chose to implement our extended type system as an abstraction over the existing type system of Typed Racket. This means that we do not rely so much on the correctness of our typing rules: instead of verifying ourselves the well-typedness of compilers written using our framework, we inject type annotations in the expanded code, which are then verified by Typed Racket. Therefore, we are confident that type errors will be caught by Typed Racket, safe in the knowledge that the code obtained after macro-expansion is type-safe55 We actually use on a few occasions unsafe-cast. Such a blunt instrument is however only used in cases where Typed Racket already has the required type information, but the type checker fails to deduce the equivalence between two formulations of the same type, or does not acknowledge that the term being checked has the expected type. These issues are being worked on by the developers of Typed Racket, however, and we hope to be able to remove these uses of unsafe-cast in later versions.. This increased serenity comes at the cost of flexibility, as Typed Racket’s type system was not able to express the type constructs that we wanted to add. We therefore had to resort to a few hacks to translate our types into constructs that could be expressed using Typed Racket.

The approach of building more complex type constructs atop a small trusted kernel has been pursued by Cur66 https://github.com/wilbowma/cur, developed by Bowman. Cur is a dependently typed language which permits theorem proving and verified programming. It is based on a small kernel (the Curnel), which does not contain language features which can be expressed by macro transformations. Most notably, the prover’s tactics are defined using metaprogramming tools, and are not part of the core language.

Another tool worth mentioning is Rosette77 https://github.com/emina/rosette[reference]Todo. Rosette, mainly developed by Torlak, is a solver-aided language: it tightly integrates an SMT solver with some Racket constructs, so that powerful queries can be performed and answered, for example “what input values to the function f will generate outputs which satisfy the predicate p?”. It can also generate simple functions which satisfy given conditions. These features allow it to be used both as a helper tool during development, for engineers coming from various domains, and as a verifier, as the solver can be used to assert that a function will never give an erroneous output, given a set of constraints on its input.

The idea of expressing the type of macro transformations at some level (e.g. by indicating the type of the resulting expression in terms of the type of the input terms, as is allowed by Turnstile) is not new: in 2001, Ganz, Sabry and Taha already presented in 2001 MacroML (Ganz et al. 2001), an experimental language which allows type checking programs before macro-expansion. However, it seems that there is interest, both in the Racket community and elsewhere, for languages with powerful metaprogramming facilities, coupled with an expressive type system. We are hopeful that this will lead to innovations concerning the formal verification of programs making heavy use of complex macros.

1.3 Summary

Once upon a time…

Unknown

1.3.1 Extensible type system

We implemented a different type system on top of Typed Racket, using macros. Macros have been used not only to extend a language’s syntax (control structures, contract annotations, and so on), but also to reduce the amount of “boilerplate” code and obtain clearer syntax for common or occasional tasks. Macros have further been used to extend the language with new paradigms, like adding an object system (CLOS (Bobrow et al. 1988)[is it really implemented using macros?]Todo, Racket classes (Flatt et al. 2006)) or supporting logic programming (Racket Datalog and Racklog, Rosette (Torlak and Bodik 2013, 2014)). In the past, Typed Racket (Tobin-Hochstadt and Felleisen 2008) has proved that a type system can be successfully fitted onto an existing “untyped” language, using macros. We implemented the type-expander library atop Typed Racket, without altering Typed Racket itself. Our type-expander library allows macros to be used in contexts where a type is expected.

This shows that an existing type system can be made extensible using macros, without altering the core implementation of the type system. We further use these type expanders to build new kinds of types which were not initially supported by Typed Racket: non-nominal algebraic types, with row polymorphism. Typed Racket has successfully been extended in the past (for example by adding type primitives for Racket’s class system, which incidentally also support row polymorphism), but these extensions required modifications to the trusted core of Typed Racket. Aside from a small hack (needed to obtain non-nominal algebraic types which remain equivalent across multiple files), our extension integrates seamlessly with other built-in types, and code using these types can use idiomatic Typed Racket features.

Typed Racket was not initially designed with this extension in mind, nor, that we know of, was it designed with the goal of being extensible. We therefore argue that a better choice of primitive types supported by the core implementation could enable many extensions without the need to resort to hacks the like of which was needed in our case. In other words, a better design of the core types with extensibility in mind would have made our job easier.

In particular, Types in Typed Clojure (Bonnaire-Sergeant et al. 2016) support fine-grained typing of heterogeneous hash tables, this would likely allow us to build much more easily the “strong duck typing” primitives on which our algebraic data types are based, and without the need to resort to hacks.

In languages making heavy uses of macros, it would be beneficial to design type systems with a well-chosen set of primitive types, on top of which more complex types can be built using macros.

Building the type system via macros atop a small kernel is an approach that has been pursued by Cur, a dependently-typed language developed with Racket, in which the tactics language is entirely built using macros, and does not depend on Cur’s trusted type-checking core.

1.3.2 Compiler-writing framework

Our goal was to introduce a compiler-writing framework, which:
  • Supports writing a compiler using many small passes (in the spirit of Nanopass)

  • Allows writing the compiler in a strongly-typed language

  • Uses immutable data structures for the Intermediate Representations (ASTs)

  • Supports backwards branches in the AST, making it rather an Abstract Syntax Graph (this is challenging due to the use of immutable data structures).

  • 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 backwards arcs.

  • 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.

  • Has extensive support for testing the compiler, by allowing the generation of random ASTs [(note that the user guides the random generation, it’s not fully automatic like quickcheck)]Todo, making it possible to read and write ASTs from files and compare them, and allows compiler passes to consume ASTs containing only the relevant fields (using row polymorphism).

1.3.3 Overview

The rest of this document is structured as follows:

2 State of the art

\def\ifmathjax#1{#1}\def\iflatex#1{}

2.1 Extending the type system via macros

Our work explores one interesting use of macros: their use to extend a programming language’s type system.

Chang, Knauth and Greenman (Chang et al. 2017) took the decision to depart from Typed Racket, and implemented a new approach, which allows type systems to be implemented as macros. Typing information about identifiers is threaded across the program at compile-time, and macros can decide whether a term is well-typed or not.

Another related project is Cur88 https://github.com/wilbowma/cur, a dependent type system implemented using Racket macros.

Bracha suggests that pluggable type systems should be used (Bracha 2004). Such a system, JavaCOP is presented by Andreae, Noble, Markstrum and Shane (Andreae et al. 2006) as a tool which “enforces user-defined typing constraints written in a declarative and expressive rule language”.

In contrast, Typed Racket (Tobin-Hochstadt and Felleisen 2008) was implemented using macros on top of “untyped” Racket, but was not designed as an extensible system: new rules in the type system must be added to the core implementation, a system which is complex to approach.

Following work by Asumu Takikawa99 https://github.com/racket/racket/pull/604, we extended Typed Racket with support for macros in the type declarations and annotations. We call this sort of macro “type expanders”, following the commonly-used naming convention (e.g. “match expanders” are macros which operate within patterns in pattern-matching forms). These type expanders allow users to easily extend the type system with new kinds of types, as long as these can be translated back to the types offered natively by Typed Racket.

While the Type Systems as Macros by Chang, Knauth and Greenman (Chang et al. 2017) allows greater flexibility by not relying on a fixed set of core types, it also places on the programmer the burden of ensuring that the type checking macros are sound. In contrast, our type expanders rely on Typed Racket’s type checker, which will still catch type errors in the fully-expanded types. In other words, writing type expanders is safe, because they do not require any specific trust, and translate down to plain Typed Racket types, where any type error would be caught at that level.

An interesting aspect of our work is that the support for type expanders was implemented without any change to the core of Typed Racket. Instead, the support for type expanders itself is available as a library, which overrides special forms like define, lambda or cast, enhancing them by pre-processing type expanders, and translating back to the “official” forms from Typed Racket. It is worth noting that Typed Racket itself is implemented in a similar way: special forms like define and lambda support plain type annotations, and translate back to the “official” forms from so-called “untyped” Racket. In both cases, this approach goes with the Racket spirit of implementing languages as libraries (Tobin-Hochstadt et al. 2011)

2.2 Algebraic datatypes for compilers

I used polymorphic variants to solve the assert false problems in my lexical analyser, along with some subtyping. You have to write the typecasts explicitly, but that aside it is very powerful (a constructor can “belong” to several types etc.).

Personal communication from a friend

The phc-adt library implements algebraic datatypes (variants and structures) which are adapted to compiler-writing.

There is an existing “simple” datatype library for Typed Racket (source code available at https://github.com/pnwamk/datatype). It differs from our library on several points:
  • “datatype” uses nominal typing, while we use structural typing (i.e. two identical type declarations in distinct modules yield the same type in our case). This avoids the need to centralize the type definition of ASTs.

  • “datatype” uses closed variants, where a constructor can only belong to one variant. We simply define variants as a union of constructors, where a constructor can belong to several variants. This allows later passes in the compiler to add or remove cases of variants, without the need to duplicate all the constructors under slightly different names.

  • “datatype” does not support row polymorphism, or similarly the update and extension of its product types with values for existing and new fields, regardless of optional fields. We implement the latter.

[Cite the variations on variants paper (for Haskell)]Todo

2.2.1 The case for bounded row polymorphism

[Explain the “expression problem”.]Todo [Talk about the various ways in which it can be “solved”, and which tradeoffs we aim for. Mention extensible-functions, another solution to the expression problem in Racket, but with rather different tradeoffs.]Todo

We strive to implement compilers using many passes. A pass should be able to accept a real-world AST, and produce accordingly a real-world transformed AST as its output. It should also be possible to use lightweight “mock” ASTs, containing only the values relevant to the passes under test (possibly only the pass being called, or multiple passes tested from end to end). The pass should then return a corresponding simplified output AST, omitting the fields which are irrelevant to this pass (and were not part of the input). Since the results of the pass on a real input and on a test input are equivalent modulo the irrelevant fields, this allows testing the pass in isolation with simple data, without having to fill in each irrelevant field with null (and hope that they are indeed irrelevant, without a comforting guarantee that this is the case), as is commonly done when creating “mocks” to test object-oriented programs.

This can be identified as a problem similar to the “expression problem”. In our context, we do not strive to build a compiler which can be extended in an “open world”, by adding new node types to the AST, or new operations handling these nodes. Rather, the desired outcome is to allow passes to support multiple known subsets of the same AST type, from the start.

We succinctly list below some of the different sorts of polymorphism, and argue that row polymorphism is well-suited for our purpose. More specifically, bounded row polymorphism gives the flexibility needed when defining passes which keep some fields intact (without reading their value), but the boundedness ensures that changes in the input type of a pass do not go unnoticed, so that the pass can be amended to handle the new information, or its type can be updated to ignore this new information.

Subtyping, polymorphism and alternatives
  • Subtyping (also called inclusion polymorphism, subtype polymorphism, or nominal subtyping ?): Subclasses and interfaces in C# and Java, sub-structs and union types in Typed Racket, polymorphic variants in CAML  (Minsky et al. 2013a), chap. 6, sec. Polymorphic Variants

  • Multiple inheritance. NIT, CLOS, C++, C# interfaces, Java interfaces. As an extension in “untyped” Racket with Alexis King’s safe multimethods1010 https://lexi-lambda.github.io/blog/2016/02/18/simple-safe-multimethods-in-racket/.

    This in principle could help in our case: AST nodes would have .withField(value) methods returning a copy of the node with the field’s value updated, or a node of a different type with that new field, if it is not present in the initial node type. This would however require the declaration of many such methods in advance, so that they can be used when needed (or with a recording mechanism like the one we use, so that between compilations the methods called are remembered and generated on the fly by a macro). Furthermore, Typed Racket lacks support for multiple inheritance on structs. It supports multiple inheritance for classes [?]Todo, but classes currently lack the ability to declare immutable fields, which in turn causes problems with occurrence typing (see the note in the “row polymorphism” point below).

  • Parametric polymorphism: Generics in C# and Java, polymorphic types in CAML and Typed Racket

  • F-bounded polymorphism: Java, C#, C++, Eiffel. Possible to mimic to some extent in Typed Racket with (unbounded) parametric polymorphism and intersection types. [Discuss how it would work/not work in our case.]Todo

  • Operator overloading (also called overloading polymorphism?) and multiple dispatch:
    • Operator overloading in C#

    • Nothing in Java aside from the built-in cases for arithmetic and string concatenation, but those are not extensible

    • C++

    • typeclasses in Haskell? [I’m not proficient enough in Haskell to be sure or give a detailed description, I have to ask around to double-check.]Todo

    • LISP (CLOS): has multiple dispatch

    • nothing built-in in Typed Racket.

    • CAML?

  • Coercion polymorphism (automatic casts to a given type). This includes Scala’s implicits, C# implicit coercion operators (user-extensible, but at most one coercion operator is applied automatically, so if there is a coercion operator A \rightarrow{} B, and a coercion operator B \rightarrow{} C, it is still impossible to supply an A where a C is expected without manually coercing the value), and C++’s implicit conversions, where single-argument constructors are treated as implicit conversion operators, unless annotated with the explicit keyword. Similarly to C#, C++ allows only one implicit conversion, not two or more in a chain.

    Struct type properties in untyped Racket can somewhat be used to that effect, although they are closer to Java’s interfaces than to coercion polymorphism. Struct type properties are unsound in Typed Racket and are not represented within the type system, so their use is subject to caution anyway.

  • Coercion (downcasts). Present in most typed languages. This would not help in our case, as the different AST types are incomparable (especially since Typed Racket lacks multiple inheritance)

  • Higher-kinded polymorphism: Type which is parameterized by a \mathit{Type} \rightarrow{} \mathit{Type} function. Scala, Haskell. Maybe CAML?

    The type expander library which we developed for Typed Racket supports \Lambda{}, used to describe anonymous type-level macros. They enable some limited form of \mathit{Type} \rightarrow{} \mathit{Type} functions, but are actually applied at macro-expansion time, before typechecking is performed, which diminishes their use in some cases. For example, they cannot cooperate with type inference. Also, any recursive use of type-level macros must terminate, unless the type “function” manually falls back to using \mathit{Rec} to create a regular recursive type. This means that a declaration like F(X) := X × F(F(X)) is not possible using anonymous type-level macros only.

    As an example of this use of the type expander library, our cycle-handling code uses internally a “type traversal” macro. In the type of a node, it performs a substitution on some subparts of the type. It is more or less a limited form of application of a whole family of type functions a{}_i \rightarrow{} b{}_i, which have the same inputs a{}_i \ldots{}, part of the initial type, but different outputs b{}_i \ldots{} which are substituted in place of the a{}_i \ldots{} in the resulting type. The “type traversal” macro expands the initial type into a standard polymorphic type, which accepts the desired outputs b{}_i \ldots{} as type arguments.

  • Lenses. Can be in a way compared to explicit coercions, where the coercion is reversible and the accessible parts can be altered.

  • Structural polymorphism (also sometimes called static duck-typing): Scala, TypeScript. It is also possible in Typed Racket, using the algebraic datatypes library which we implemented. Possible to mimic in Java and C# with interfaces “selecting” the desired fields, but the interface has to be explicitly implemented by the class (i.e. at the definition site, not at the use-site).

    Palmer et al. present TinyBang (Palmer et al. 2014), a typed language in which flexible manipulation of objects is possible, including adding and removing fields, as well as changing the type of a field. They implement in this way a sound, decidable form of static duck typing, with functional updates which can add new fields and replace the value of existing fields. Their approach is based on two main aspects:
    • Type-indexed records supporting asymmetric concatenation: by concatenating two records r{}_1 \& r{}_2, a new record is obtained containing all the fields from r{}_1 (associated to their value in r{}_1), as well as the fields from r{}_2 which do not appear in r{}_1 (associated to their value in r{}_2). Primitive types are eliminated by allowing the use of type names as keys in the records: integers then become simply records with a int key, for example.

    • Dependently-typed first-class cases: pattern-matching functions are expressed as pattern \mathbin{\texttt{->}} expression, and can be concatenated with the \& operator, to obtain functions matching against different cases, possibly with a different result type for each case. The leftmost cases can shadow existing cases (i.e. the case which is used is the leftmost case for which the pattern matches successfully).

    TinyBang uses an approach which is very different from the one we followed in our Algebraic Data Types library, but contains the adequate primitives to build algebraic data types which would fulfill our requirements (aside from the ability to bound the set of extra “row” fields). We note that our flexible structs, which are used within the body of node-to-node functions in passes, do support an extension operation, which is similar to TinyBang’s \&, with the left-hand side containing a constant and fixed set of fields.

  • Row polymorphism: Apparently, quoting a post on Quora1111 https://www.quora.com/Object-Oriented-Programming-What-is-a-concise-definition­-of-polymorphism\label{quora-url-footnote}:

    Mostly only concatenative and functional languages (like Elm and PureScript) support this.

    Classes in Typed Racket can have a row type argument (but classes in Typed Racket cannot have immutable fields (yet), and therefore occurrence typing does not work on class fields. Occurrence typing is an important idiom in Typed Racket, used to achieve safe but concise pattern-matching, which is a feature frequently used when writing compilers).

    Our Algebraic Data Types library implements a bounded form of row polymorphism, and a separate implementation (used within the body of node-to-node functions in passes) allows unbounded row polymorphism.

  • [Virtual types]Todo

  • So-called “untyped” or “uni-typed” languages: naturally support most of the above, but without static checks.

    Operator overloading can be present in “untyped” languages, but is really an incarnation of single or multiple dispatch, based on the run-time, dynamic type (as there is no static type based on which the operation could be chosen). However it is not possible in “untyped” languages and languages compiled with type erasure to dispatch on “types” with a non-empty intersection: it is impossible to distinguish the values, and they are not annotated statically with a type.

    As mentioned above, Typed Racket does not have operator overloading, and since the inferred types cannot be accessed reflectively at compile-time, it is not really possible to construct it as a compile-time feature via macros. Typed Racket also uses type erasure, so the same limitation as for untyped languages applies when implementing some form of single or multiple dispatch at run-time — namely the intersection of the types must be empty. [Here, mention (and explain in more detail later) our compile-time “empty-intersection check” feature (does not work with polymorphic variables).]Todo

[Overview of the existing “solutions” to the expression problems, make a summary table of their tradeoffs (verbosity, weaknesses, strengths).]Todo

[Compare the various sorts of subtyping and polymorphism in that light (possibly in the same table), even those which do not directly pose as a solution to the expression problem.]Todo

“Nominal types”: our tagged structures and node types are not nominal types.

The “trivial” Racket library tracks static information about the types in simple cases. The “turnstile” Racket language [is a follow-up]Todo work, and allows to define new typed Racket languages. It tracks the types of values, as they are assigned to variables or passed as arguments to functions or macros. These libraries could be used to implement operator overloads which are based on the static type of the arguments. It could also be used to implement unbounded row polymorphism in a way that does not cause a combinatorial explosion of the size of the expanded code.[Have a look at the implementation of row polymorphism in Typed Racket classes, cite their work if there is something already published about it.]Todo

From the literate program (tagged-structure-low-level):

Row polymorphism, also known as "static duck typing" is a type system feature which allows a single type variable to be used as a place holder for several omitted fields, along with their types. The phc-adt library supports a limited form of row polymorphism: for most operations, a set of tuples of omitted field names must be specified, thereby indicating a bound on the row type variable.

This is both a limitation of our implementation (to reduce the combinatorial explosion of possible input and output types), as well as a desirable feature. Indeed, this library is intended to be used to write compilers, and a compiler pass should have precise knowledge of the intermediate representation it manipulates. It is possible that a compiler pass may operate on several similar intermediate representations (for example a full-blown representation for actual compilation and a minimal representation for testing purposes), which makes row polymorphism desirable. It is however risky to allow as an input to a compiler pass any data structure containing at least the minimum set of required fields: changes in the intermediate representation may add new fields which should, semantically, be handled by the compiler pass. A catch-all row type variable would simply ignore the extra fields, without raising an error. Thanks to the bound which specifies the possible tuples of omitted field names, changes to the the input type will raise a type error, bringing the programmer’s attention to the issue. If the new type is legit, and does not warrant a modification of the pass, the fix is easy to implement: simply adding a new tuple of possibly omitted fields to the bound (or replacing an existing tuple) will allow the pass to work with the new type. If, on the other hand, the pass needs to be modified, the type system will have successfully caught a potential issue.

2.3 Writing compilers using many small passes (a.k.a following the Nanopass Compiler Framework philosophy)

2.4 Cycles in intermediate representations of programs

[There already were a few references in my proposal for JFLA.]Todo [Look for articles about graph rewriting systems.]Todo

The following sections present the many ways in which cycles within the AST, CFG and other intermediate representations can be represented.

2.4.1 Mutable data structures

  • Hard to debug

  • When e.g. using lazy-loading, it is easy to mistakenly load a class or method after the Intermediate Representation was frozen. Furthermore, unless a .freeze() method actually enforces this conceptual change from a mutable to an immutable representation, it can be unclear at which point the IR (or parts of it) is guaranteed to be complete and its state frozen. This is another factor making maintenance of such code difficult.

Quote from (Ramsey and Dias 2006):

We are using ML to build a compiler that does low-level optimization. To support optimizations in classic imperative style, we built a control-flow graph using mutable pointers and other mutable state in the nodes. This decision proved unfortunate: the mutable flow graph was big and complex, and it led to many bugs. We have replaced it by a smaller, simpler, applicative flow graph based on Huet’s (1997) zipper. The new flow graph is a success; this paper presents its design and shows how it leads to a gratifyingly simple implementation of the dataflow framework developed by Lerner, Grove, and Chambers (2002).

2.4.2 Unique identifiers used as a replacement for pointers

Mono uses that (Evain and others 2008; Köplinger et al. 2014), it is very easy to use an identifier which is supposed to reference a missing object, or an object from another version of the AST. It is also very easy to get things wrong when duplicating nodes (e.g. while specializing methods based on their caller), or when merging or removing nodes.

2.4.3 Explicit use of other common graph representations

Adjacency lists, De Bruijn indices.

2.4.4 Using lazy programming languages
2.4.5 True graph representations using immutable data structures

3 Goals, constraints and examples

\def\ifmathjax#1{#1}\def\iflatex#1{}

4 Typed Racket

\def\ifmathjax#1{#1}\def\iflatex#1{}

We start this section with some history: Lisp, 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 (McCarthy 1981). 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 (Abelson et al. 1998; Shinn et al. 2013; Sperber et al. 2009) 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 (Felleisen et al. 2015) 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:

In the remainder of this section, we will present the features of Typed Racket’s type system, and then present formal semantics for a subset of those, namely the part which is relevant to our work. The Typed Racket Guide and The Typed Racket Reference provide good documentation for programmers who desire to use Typed Racket; we will therefore keep our overview succinct and gloss over most details.

4.1 Overview of Typed Racket’s type system

4.1.1 Simple primitive types

Typed Racket has types matching Racket’s baggage of primitive values: Number, Boolean, Char, String, Void1313 The Void type contains only a single value, #<void>, and is equivalent to the void type in C. It is the equivalent of 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 Nothing, the bottom type which is not inhabited by any value, and is similar to the type of Haskell’s undefined. Nothing can be used for example as the type of functions which never return — in that way it is similar to C’s __attribute__ ((__noreturn__)). and so on.

> (ann #true Boolean)

- : Boolean

#t

> 243

- : Integer [more precisely: Positive-Byte]

243

> "Hello world"

- : String

"Hello world"

> #\c

- : Char

#\c

; The void function produces the void value
; Void values on their own are not printed,
; so we place it in a list to make it visible.
> (list (void))

- : (Listof Void) [more precisely: (List Void)]

'(#<void>)

For numbers, Typed Racket offers a “numeric tower” of partially-overlapping types: Positive-Integer is a subtype of Integer, which is itself a subtype of Number. Zero, the type containing only the number 0, is a both a subtype of Nonnegative-Integer (numbers ≥ 0) and of Nonpositive-Integer (numbers ≤ 0).

Typed Racket also includes a singleton type for each primitive value of these types: we already mentioned Zero, which is an alias of the 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, 243 belongs to the singleton type 243, which is a subtype of Positive-Integer.

> 0

- : Integer [more precisely: Zero]

0

> (ann 243 243)

- : Integer [more precisely: 243]

243

> #t

- : Boolean [more precisely: True]

#t

4.1.2 Pairs and lists

Pairs are the central data structure of most Lisp dialects. They are used to build linked lists of pairs, terminated by '(), the null element. The null element has the type Null, while the pairs which build the list have the type (Pairof A B), where A and B are replaced by the actual types for the first and second elements of the pair. For example, the pair built using (cons 729 #true), which contains 729 as its first element, and #true as its second element, has the type (Pairof Number Boolean), or using the most precise singleton types, (Pairof 729 #true).

> (cons 729 #true)

- : (Pairof Positive-Index True)

'(729 . #t)

> '(729 . #true)

- : (Pairof Positive-Index True)

'(729 . #t)

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 (list 81 #true 'hello) has the type (List Number Boolean Symbol), which is a shorthand for the type (Pairof Number (Pairof Boolean (Pairof Symbol Null))). Lists in Typed Racket 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 Pair<A, B>, where the generic type argument B could be instantiated by another instance of Pair, and so on.

> (cons 81 (cons #true (cons 'hello null)))

- : (Listof (U 'hello Positive-Byte True))

'(81 #t hello)

> (ann (list 81 #true 'hello)
       (Pairof Number (Pairof Boolean (Pairof Symbol Null))))

- : (Listof (U Boolean Complex Symbol)) [more precisely: (List Number Boolean Symbol)]

'(81 #t hello)

The type of variable-length homogeneous linked lists can be described using the Listof type operator. The type (Listof Integer) is equivalent to (Rec R (U (Pairof Integer R) Null)). The Rec type operator describes recursive types, and U describes unions. Both of these features are described below, for now we will simply say that the previously given type is a recursive type R, which can be a (Pairof Integer R) or Null (to terminate the linked list).

> (ann (range 0 5) (Listof Number))

- : (Listof Number)

'(0 1 2 3 4)

4.1.3 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)1414 This is true with the exception of symbols created with gensym and the like. 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..

Typed Racket includes the Symbol type, to which all symbols belong. Additionally, there is a singleton type for each symbol: the type 'foo is only inhabited by the symbol 'foo.

> 'foo

- : Symbol [more precisely: 'foo]

'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 Typed Racket will produce identical values and types. A way of seeing this is that symbols are similar to constructors (in the functional programming sense) or enums which are implicitly declared globally.

> (module m1 typed/racket
    (define sym1 'foo)
    (provide sym1))
> (module m2 typed/racket
    (define sym2 'foo)
    (provide sym2))
> (require 'm1 'm2)
; The tow independent uses of 'foo are identical:
> (eq? sym1 sym2)

- : Boolean

#t

4.1.4 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 U type operator.

The union type (U 0 1 2) is inhabited by the values 0, 1 and 2, and by no other value. The Boolean type is actually defined as (U #true #false), i.e. the union of the singleton types containing the #true and #false values, respectively. The Nothing type, which is not inhabited by any value, is defined as the empty union (U). The type 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.

> (define v : (U 'foo 'bar) 'foo)
> v

- : Symbol [more precisely: (U 'bar 'foo)]

'foo

> (set! v 'bar)
> v

- : Symbol [more precisely: (U 'bar 'foo)]

'bar

; This throws an error at compile-time:
> (set! v 'oops)

eval:5:0: Type Checker: type mismatch;

 mutation only allowed with compatible types

  expected: (U 'bar 'foo)

  given: 'oops

  in: oops

A union such as (U 'ca (List 'cb Number) (List 'cc String Symbol)) can be seen as roughly the equivalent of a variant with three constructors, ca, cb and cc, where the first has no arguments, the second has one argument (a Number), and the third has two arguments (a String and a Symbol).

The main difference is that a symbol can be used as parts of several unions, e.g. (U 'a 'b) and (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 (Minsky et al. 2013b) than to regular variants.

> (define-type my-variant (U 'ca
                             (List 'cb Number)
                             (List 'cc String Symbol)))
> (define v₁ : my-variant 'ca)
> (define v₂ : my-variant (list 'cb 2187))
> (define v3 : my-variant (list 'cc "Hello" 'world))

Finally, it is possible to mix different sorts of types within the same union: the type (U 0 #true 'other) is inhabited by the number 0, the boolean #true, and the symbol 'other. Translating such an union to a language like CAML could be done by explicitly tagging each case of the union with a distinct constructor.

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: number?, string?, symbol? etc.

4.1.5 Intersections

Intersections are the converse of unions: instead of allowing a mixture of values of different types, an intersection type, described using the type operator, only allows values which belong to all types.

The intersection type ( Nonnegative-Integer Nonpositive-Integer) is the singleton type 0. The intersection of (U 'a 'b 'c) and (U 'b 'c 'd) will be (U 'b 'c), as 'b and 'c belong to both unions.

; :type shows the given type, or a simplified version of it
> (:type ( (U 'a 'b 'c) (U 'b 'c 'd)))

(U 'b 'c)

Typed Racket 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 (describled below can, using special properties, impersonate functions. This mechanism is similar to PHP’s __invoke, the ability to overload operator() in C++. Typed Racket 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 ( s ( Number String)), where s is a struct type, cannot be reduced to Nothing, because Typed Racket cannot determine whether the struct s can act as a function or not.

Another situation where Typed Racket cannot reduce the intersection is when intersecting two function types (presented below).

( ( Number String) ( Number Symbol))
( ( Number String) ( Boolean String))

The first intersection seems like could be simplified to ( Number String) ( Number Symbol), and the second one could be simplified to ( (U Number Boolean) String), however the equivalence between these types has not been implemented (yet) in Typed Racket, 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 Typed Racket is able to perform a simplification, occurrences of Nothing (the bottom type) propagate outwards in some cases, pairs and struct types which contain Nothing as one of their elements being collapsed to Nothing. This propagation of Nothing starts from occurrences of Nothing in the parts of the resulting type which are traversed by the intersection operator. It collapses the containing pairs and struct types to Nothing, moving outwards until the operator itself is reached. In principle, the propagation could go on past that point, but this is not implemented yet in Typed Racket1515 See Issue #552 on Typed Racket’s GitHub repository for more details on what prevents implementing a more aggressive propagation of Nothing..

The type ( 'a 'b) therefore gets simplified to Nothing, and the type ( (Pairof 'a 'x) (Pairof 'b 'x)) also simplifies to Nothing (Typed Racket initially pushes the intersection down the pairs, so that the type first becomes (Pairof ( 'a 'b) ( 'x 'x)), which is simplified to (Pairof Nothing 'x), and the occurrence of Nothing propagates outwards). However, if the user directly specifies the type (Pairof ( 'a 'b) Integer), it is simplified to (Pairof Nothing Integer), but the Nothing does not propagate outwards beyond the initial use of .

> (:type ( 'a 'b))

Nothing

> (:type ( (Pairof 'a 'x) (Pairof 'b 'x)))

Nothing

> (:type (Pairof ( 'a 'b) Integer))

(Pairof Nothing Integer)

[can expand further: Integer]

A simple workaround exists: the outer type, which could be collapsed to Nothing, can be intersected again with a type of the same shape. The outer intersection will traverse both types (the desired one and the “shape”), and propagate the leftover Nothing further out.

> (:type (Pairof ( 'a 'b) Integer))

(Pairof Nothing Integer)

[can expand further: Integer]

> (:type ( (Pairof ( 'a 'b) Integer)
            (Pairof Any Any)))

Nothing

These intersections are not very interesting on their own, as in most cases it is possible to express the resulting simplified type without using the intersection operator. They become more useful when mixed with polymorphic types: intersecting a polymorphic type variable with another type can be used to restrict the actual values that may be used. The type ( A T), where A is a polymorphic type variable and T is a type defined elsewhere, is equivalent to the use of bounded type parameters in Java or C#. In C#, for example, the type ( A T) would be written using an where A : T clause.

4.1.6 Structs

Racket also supports structs, 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 C# 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 Typed Racket program additionally declares corresponding type.

> (struct parent ([field₁ : (Pairof String Symbol)])
    #:transparent)
> (struct s parent ([field₂ : Integer]
                    [field₃ : Symbol])
    #:transparent)
> (s (cons "x" 'y) 123 'z)

- : s

(s '("x" . y) 123 'z)

In Typed Racket, structs can have polymorphic type arguments, which can be used inside the types of the struct’s fields.

> (struct (A B) poly-s ([field₁ : (Pairof A B)]
                        [field₂ : Integer]
                        [field₃ : B])
    #:transparent)
> (poly-s (cons "x" 'y) 123 'z)

- : (poly-s String (U 'y 'z))

(poly-s '("x" . y) 123 'z)

Racket further supports 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.

Struct type properties are often considered a low-level mechanism in Racket. Among other things, a struct type property can only be used to define a single property at a time. When multiple “methods” have to be defined at once (for example, when defining the prop:equal+hash property, which requires the definition of an equality comparison function, and two hashing functions), these can be grouped together in a list of functions, which is then used as the property’s value. “Generic interfaces” are a higher-level feature, which among other things allow the definition of multiple “methods” as part of a single generic interface, and offers a friendlier API for specifying the “generic interface” itself (i.e. what Object Oriented languages call an interfece), as and for specifying the implementation of said interface.

Typed Racket unfortunately offers no support for struct type properties and generic interfaces for now. It is impossible to assert that a struct implements 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 properties1616 We built a thin macro wrapper which allows typechecking the implementation and signature of the functions bound to these two properties.: prop:custom-write which is the equivalent of Java’s void toString(), and prop:equal+hash which is equivalent to Java’s boolean equals(Object o) and int hashCode().

4.1.7 Functions

Typed Racket provides rich function types, to support some of the flexible use patterns allowed by Racket.

The simple function type below indicates that the function expects two arguments (an integer and a string), and returns a boolean:

( Integer String Boolean)

We note that unlike Haskell and CAML functions, Racket functions are not implicitly curried. To express the corresponding curried function type, one would write:

( Integer ( String Boolean))

A function may additionally accept optional positional arguments, and keyword (i.e. named) arguments, both mandatory and optional:

; Mandatory string, optional integer and boolean arguments:
(->* (String) (Integer Boolean) Boolean)
; Mandatory keyword arguments:
( #:size Integer #:str String Boolean)
; Mandatory #:str, optional #:size and #:opt:
(->* (#:str String) (#:size Integer #:opt Boolean) Boolean)

Furthermore, functions in Racket accept a catch-all “rest” argument, which allows for the definition of variadic functions. Typed racket also allows expressing this at the type level, as long as the arguments covered by the “rest” clause all have the same type:

; The function accepts one integer and any number of strings:
(-> Integer String * Boolean)
; Same thing with an optional symbol inbetween:
(->* (Integer) (Symbol) #:rest String Boolean)

One of Typed Racket’s main goals is to be able to typecheck idiomatic Racket programs. Such programs may include functions whose return type depends on the values of the input arguments. Similarly, case-lambda can be used to create lambda functions which dispatch to multiple behaviours based on the number of arguments passed to the function.

Typed Racket provides the case→ type operator, which can be used to describe the type of these functions:

; Allows 1 or 3 arguments, with the same return type.
(case→ ( Integer Boolean)
       ( Integer String Symbol Boolean))
; A similar type based on optional arguments allows 1, 2 or 3
;  arguments in contrast:
(->* (Integer) (String Symbol) Boolean)
; The output type can depend on the input type:
(case→ ( Integer Boolean)
       ( String Symbol))
; Both features (arity and dependent output type) can be mixed
(case→ ( Integer Boolean)
       ( Integer String (Listof Boolean)))

Another important feature, which can be found in the type system of most functional programming languages, and most object-oriented languages, is parametric polymorphism. Typed Racket allows the definition of polymorphic structs, as detailed above, as well as polymorphic functions. For example, the function cons can be considered as a polymorphic function with two polymorphic type arguments A and B, which takes an argument of type A, an argument of type B, and returns a pair of A and B.

( (A B) ( A B (Pairof A B)))

Typed Racket supports polymorphic functions with multiple polymorphic type variables, as the one shown above. Furthermore, it allows one of the polymorphic variables to be followed by ellipses, indicating a variable-arity polymorphic type (Tobin-Hochstadt 2010). The dotted polymorphic type variable can be instantiated with a tuple of types, and will be replaced with that tuple where it appears. For example, the type

( (A B ...) ( (List A A B ...) Void))

can be instantiated with Number String Boolean, which would yield the type for a function accepting a list of four elements: two numbers, a string and a boolean.

( (List Number Number String Boolean) Void)

Dotted polymorphic type variables can only appear in some places. A dotted type variable can be used as the tail of a List type, so (List Number B ...) (a String followed by any number of Bs) is a valid type, but (List B ... String) (any number of Bs followed by a String) is not. A dotted type variable can also be used to describe the type of a variadic function, as long as it appears after all other arguments, so ( String B ... Void) (a function taking a String, any number of Bs, and returning Void) is a valid type, but ( String B ... Void) (a function taking any number of Bs, and a String, and returning Void) is not. Finally, a dotted type variable can be used to represent the last element of the tuple of returned values, for functions which return multiple values (which are described below).

When the context makes it unclear whether an ellipsis \ldots{} indicates a dotted type variable, or is used to indicate a metasyntactic repetition at the level of mathematical formulas, we will write the first using τ{}_1 \ldots{} τ{}_n, explicitly indicating the first and last elements, or using \overline{τ} [and we will write the second using \textit{tvar}\ \textit{ooo}]Todo

Functions in Racket can return one or several values. When the number of values returned is different from one, the result tuple can be destructured using special functions such as (call-with-values f g), which passes each value returned by f as a distinct argument to g. The special form (let-values ([(v₁ vₙ) e]) body) binds each value returned by e to the corresponding vᵢ (the expression e must produce exactly n values). The type of a function returning multiple values can be expressed using the following notation:

( In₁ Inₙ (Values Out₁ Outₘ))

Finally, predicates (functions whose results can be interpreted as booleans) can be used to gain information about the type of their argument, depending on the result. The type of a predicate can include positive and negative filters, indicated with #:+ and #:-, respectively. The type of the string? predicate is:

( Any Boolean : #:+ String #:- (! String))

In this notation, the positive filter #:+ String indicates that when the predicate returns #true, the argument is known to be a String. Conversely, when the predicate exits with #false, the negative filter #:- (! String) indicates that the input could not (!) possibly have been a string. The information gained this way allows regular conditionals based on arbitrary predicates to work like pattern-matching:

> (define (f [x : (U String Number Symbol)])
    (if (string? x)
        ; x is known to be a String here:
        (ann x String)
        ; x is known to be a Number or a Symbol here:
        (ann x (U Number Symbol))))

The propositions do not necessarily need to refer to the value as a whole, and can instead give information about a sub-part of the value. Right now, the user interface for specifying paths can only target the left and right members of cons pairs, recursively. Internally, Typed Racket supports richer paths, and the type inference can produce filters which give information about individual structure fields, or about the result of forced promises, for example.

4.1.8 Occurrence typing

Typed Racket is built atop Racket, which does not natively support pattern matching. Instead, pattern matching forms are implemented as macros, and expand to nested uses of if.

As a result, Typed Racket needs to typecheck code with the following structure:

(λ ([v : (U Number String)])
  (if (string? v)
      (string-append v ".")
      (+ v 1)))

In this short example, the type of v is a union type including Number and String. After applying the string? predicate, the type of v is narrowed down to String in the then branch, and it is narrowed down to Number in the else branch. The type information gained thanks to the predicate comes from the filter part of the predicate’s type (as explained in Functions).

Occurrence typing only works on immutable variables and values. Indeed, if the variable is modified with set!, or if the subpart of the value stored within which is targeted by the predicate is mutable, it is possible for that value to change between the moment the predicate is executed, and the moment when the value is actually used. This places a strong incentive to mostly use immutable variables and values in Typed Racket programs, so that pattern-matching and other forms work well.

In principle, it is always possible to copy the contents of a mutated variable to a temporary one (or copy a mutable subpart of the value to a new temporary variable), and use the predicate on that temporary copy. The code in the then and else branches should also use the temporary copy, to benefit from the typing information gained via the predicate. In our experience, however, it seems that most macros which perform tasks similar to pattern-matching do not provide an easy means to achieve this copy. It therefore remains more practical to avoid mutation altogether when possible.

4.1.9 Recursive types

Typed Racket allows recursive types, both via (possibly mutually-recursive) named declarations, and via the Rec type operator.

In the following examples, the types Foo and Bar are mutually recursive. The type Foo matches lists with an even number of alternating Integer and String elements, starting with an Integer,

(define-type Foo (Pairof Integer Bar))
(define-type Bar (Pairof String (U Foo Null)))

This same type could alternatively be defined using the Rec operator. The notation (Rec R T) builds the type T, where occurrences of R are interpreted as recursive occurrences of T itself.

(Rec R
     (Pairof Integer
             (Pairof String
                     (U R Null))))
4.1.10 Classes

The racket/class module provides an object-oriented system for Racket. It supports the definition of a hierarchy of classes with single inheritance, interfaces with multiple inheritance, mixins and traits (methods and fields which may be injected at compile-time into other classes), method renaming, and other features.

The typed/racket/class module makes most of the features of racket/class available to Typed Racket. In particular, it defines the following type operators:

We will not further describe this object system here, as our work does not rely on this aspect of Typed Racket’s type system. We invite the curious reader to refer to the documentation for racket/class and typed/racket/class for more details.

We will simply note one feature which is so far missing from Typed Racket’s object system: immutability. It is not possible yet to indicate in the type of a class that a field is immutable, or that a method is pure (in the sense of always returning the same value given the same input arguments). The absence of immutability means that occurrence typing does not work on fields. After testing the value of a field against a predicate, it is not possible to narrow the type of that field, because it could be mutated by a third party between the check and future uses of the field.

4.1.11 Local type inference

Unlike many other statically typed functional languages, Typed Racket does not rely on a Hindley–Milner type system (Hindley 1969; Milner 1978). This choice was made for several reasons (Tobin-Hochstadt 2010):
  • Typed Racket’s type system is rich and contains many features. Among other things, it mixes polymorphism and subtyping, which notoriously make typechecking difficult.

  • The authors of Typed Racket claim that global type inference often produces indecipherable error messages, with a small change having repercussions on the type of terms located in other distant parts of the program.

  • The authors of Typed Racket suggest that type annotations are often beneficial as documentation. Since the type annotations are checked at compile-time, they additionally will stay synchronised with the code that they describe, and will not become out of date.

Instead of relying on global type inference, Typed Racket uses local type inference to determine the type of local variables and expressions. Typed Racket’s type inference can also determine the correct instantiation for most calls to polymorphic functions. It however requires type annotations in some places. For example, it is usually necessary to indicate the type of the parameters when defining a function.

4.2 Formal semantics for part of Typed Racket’s type system

\def\ifmathjax#1{#1}\def\iflatex#1{}

The following definitions and rules are copied and adjusted from (Tobin-Hochstadt 2010), with the author’s permission. Some of the notations were changed to use those of (Kent et al. 2016).

We include below the grammar, semantics and typing rules related to the minimal core of the Typed Racket language1717 The core language is defined in (Tobin-Hochstadt 2010), pp. 61–70., dubbed λ_{\mathit{TS}}, including extensions which add pairs1818 The extensions needed to handle pairs are described in (Tobin-Hochstadt 2010), pp. 71–75., functions of multiple arguments, variadic functions and variadic polymorphic functions1919 The extensions needed to handle functions of multiple arguments, variadic functions, and variadic functions where the type of the “rest” arguments are not uniform are described in (Tobin-Hochstadt 2010), pp. 91–77., intersection types, recursive types, symbols and promises. These features have been informally described in Overview of Typed Racket’s type system.

We purposefully omit extensions which allow advanced logic reasoning when propagating information gained by complex combinations of conditionals2020 The extensions which allow advanced logic reasoning are described in (Tobin-Hochstadt 2010), pp. 75–78., refinement types2121 The extensions which introduce refinement types are described in (Tobin-Hochstadt 2010), pp. 85–89., dependent refinement types2222 Dependent refinement types are presented in  (Kent et al. 2016). (which allow using theories from external solvers to reason about values and their type, e.g. using bitvector theory to ensure that a sequence of operations does not produce a result exceeding a certain machine integer size), structs and classes. These extensions are not relevant to our work2323 We informally describe a translation of our system of records into structs in section [[??]]Todo, but settle for an alternative implementation in section [[??]]Todo which does not rely on structs., and their inclusion in the following semantics would needlessly complicate things.

4.2.1 Notations

We note a sequence of elements with \overrightarrow{y}. When there is more than one sequence involved in a rule or equation, we may use the notation \overrightarrow{y}\overset{\scriptscriptstyle\,\ifmathjax{\raise1mu{n}}\iflatex{n}}{\vphantom{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 \def\overrightbracedarrow#1{\overset{\scriptscriptstyle{\raise1mu{\{}}}{\vphantom{#1}}\overrightarrow{#1}\overset{\scriptscriptstyle{\raise1mu{\}}}}{\vphantom{#1}}}\overrightbracedarrow{y}. The use of ellipses in α \mathbf{\ldots{}} does not indicate the repetition of α. Instead, it indicates that α is a 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 Typed Racket source code, and are the reason we use the notation \overrightarrow{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 : \mathrm{R}

The environments can be extended as follows:

Γ, x : τ ; Δ\cup\{α\} ⊢ e : \mathrm{R}

The typing information \mathrm{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 below. Since the typing information \mathrm{R} is often inlined in the typing judgement, a typing judgement will generally have the following form:

Γ ; Δ ⊢ e : {\mathbf{\ifmathjax{\unicode{x2772}}\iflatex{❲}}}τ \;{\mathbf{;}}\; \phi{}^+ {\mathbf{{/}}} \phi{}^- \;{\mathbf{;}}\; o{\mathbf{\ifmathjax{\unicode{x2773}}\iflatex{❳}}}

In this notation, the + and - signs in \phi{}^+ and \phi{}^- are purely syntactical, and serve to distinguish the positive and negative filters, which are instances of the nonterminal \phi.

The various nonterminals used throughout the language are written in italics and are defined using the notation:

\begin{qaligned} \textit{nonterminal} & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & \textit{first case}\\ & {}\mathrel{|}{} & \textit{second case}\\ & {}\mathrel{|}{} & \textit{and so on} \end{qaligned}

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:

\begin{qaligned} \textit{nonterminal} & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & \ldots{}\\ & {}\mathrel{|}{} & \textit{new case}\\ & {}\mathrel{|}{} & \textit{other new case} \end{qaligned}

Typing rules and other rules are described following the usual natural deduction notation.

\frac{\begin{gathered}\textit{hypothesis}\\ \textit{other hypothesis}\end{gathered}}{\begin{gathered}\textit{deduction}\end{gathered}}\ {\rm R{\small U}{\small L}{\small E}\text{-}N{\small A}{\small M}{\small E}}

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 \mathrm{true} and \mathrm{false} indicate logical truth and falsehood respectively.

\mathrm{metafunction}(x,y) = \begin{cases} \mathrm{true} &\text{ if } x = y + 1\\ \mathrm{false} &\text{ otherwise } \end{cases}

Language operators are written in bold face:

\begin{qaligned} e & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & (\textbf{num}\ n)\\ & {}\mathrel{|}{} & \ldots{} \end{qaligned}

Values are written using a bold italic font:

\begin{qaligned} v & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & (\textbf{$\mathord{{\bfit \text{num}}}$}\ n)\\ & {}\mathrel{|}{} & \ldots{} \end{qaligned}

Type names start with a capital letter, and are written using a bold font:

\begin{qaligned} τ,σ & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & (\textbf{Num}\ n)\\ & {}\mathrel{|}{} & \ldots{} \end{qaligned}

We indicate the syntactical substitution of y with z in w using the notation w[y↦z]. When given several elements to replace, the substitution operator performs a parallel substitution (that is, w[x↦y\ y↦z] will not replace the occurrences of y introduced by the first substitution).

[Succinctly describe the other conventions used in the thesis, if any were omitted above.]Todo

[Define the meta substitution and equality operators precisely.]Todo

4.2.2 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 (Flatt 2016). 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, Typed Racket only typechecks fully-expanded programs. In these programs, the binding of each identifier has normally been determined2424 Typed Racket actually still determines the binding for type variables by itself, but we consider this is an implementation detail..

4.2.3 Expressions

The following expressions are available in the subset of Typed Racket which we consider. These expressions include references to variables, creation of basic values (numbers, booleans, lists of pairs ending with \textbf{$\mathord{{\bfit \text{null}}}$}, symbols, promises), a variety of lambda functions with different handling of rest arguments (fixed number of arguments, polymorphic functions with a uniform list of 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).

\begin{qaligned} e & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & x \ |\ y \ |\ z\hphantom{\text{variable}}\tag*{$\llap{\text{variable}}$}\\ & {}\mathrel{|}{} & (\textbf{num}\ n) \hphantom{\text{number}}\tag*{$\llap{\text{number}}$}\\ & {}\mathrel{|}{} & \textbf{true} \hphantom{\text{booleans}}\tag*{$\llap{\text{booleans}}$}\\ & {}\mathrel{|}{} & \textbf{false}\\ & {}\mathrel{|}{} & \textbf{null} \hphantom{\text{null constant}}\tag*{$\llap{\text{null constant}}$}\\ & {}\mathrel{|}{} & p \hphantom{\text{primitive functions}}\tag*{$\llap{\text{primitive functions}}$}\\ & {}\mathrel{|}{} & \mathbf{(}e\ \overrightarrow{e}\mathbf{)} \hphantom{\text{function application}}\tag*{$\llap{\text{function application}}$}\\ & {}\mathrel{|}{} & (\textbf{if}\ e\ e\ e) \hphantom{\text{conditional}}\tag*{$\llap{\text{conditional}}$}\\ & {}\mathrel{|}{} & \mathbf{λ}(\overrightarrow{x:τ}).e \hphantom{\text{lambda function}}\tag*{$\llap{\text{lambda function}}$}\\ & {}\mathrel{|}{} & \mathbf{λ}(\overrightarrow{x:τ}\ \ .\ \ x:τ*).e \hphantom{\text{variadic function}}\tag*{$\llap{\text{variadic function}}$}\\ & {}\mathrel{|}{} & \mathbf{λ}(\overrightarrow{x:τ}\ \ .\ \ x:τ \mathbf{\ldots{}}_{α}).e \hphantom{\text{variadic polymorpic function}}\tag*{$\llap{\text{variadic polymorpic function}}$}\\ & {}\mathrel{|}{} & \mathbf{\Lambda{}}(\overrightarrow{α}).e\hphantom{\text{polymorphic abstraction}}\tag*{$\llap{\text{polymorphic abstraction}}$}\\ & {}\mathrel{|}{} & \mathbf{\Lambda{}}(\overrightarrow{α}\ α \mathbf{\ldots{}}).e \hphantom{\text{variadic polymorphic abstraction}}\tag*{$\llap{\text{variadic polymorphic abstraction}}$}\\ & {}\mathrel{|}{} & (\textbf{@}\ e\ \overrightarrow{τ}) \hphantom{\text{polymorphic instantiation}}\tag*{$\llap{\text{polymorphic instantiation}}$}\\ & {}\mathrel{|}{} & (\textbf{delay}\ e) \hphantom{\text{create promise}}\tag*{$\llap{\text{create promise}}$}\\ & {}\mathrel{|}{} & (\textbf{force}\ e) \hphantom{\text{force promise}}\tag*{$\llap{\text{force promise}}$}\\ & {}\mathrel{|}{} & (\textbf{symbol}\ s) \hphantom{\text{symbol literal}}\tag*{$\llap{\text{symbol literal}}$}\\ & {}\mathrel{|}{} & (\textbf{gensym}) \hphantom{\text{fresh uninterned symbol}}\tag*{$\llap{\text{fresh uninterned symbol}}$}\\ & {}\mathrel{|}{} & (\textbf{eq?}\ e\ e) \hphantom{\text{symbol equality}}\tag*{$\llap{\text{symbol equality}}$}\\ & {}\mathrel{|}{} & (\textbf{map}\ e\ e) \end{qaligned}

Symbol literals are noted as s \in{} \mathcal{S} and the universe of symbols (which includes symbol literals and fresh symbols created via (\textbf{gensym})) is noted as s{}’ \in{} \mathcal{S}{}’.

\begin{aligned} s & \in{} \mathcal{S}\\ s{}’ & \in{} \mathcal{S}{}’ \\ \mathcal{S} & \subset{} \mathcal{S}{}’ \end{aligned}

4.2.4 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 \mathit{cons}. 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.

\begin{qaligned} p & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & \textit{add1}\hphantom{\text{returns its argument plus $1$}}\tag*{$\llap{\text{returns its argument plus $1$}}$}\\ & {}\mathrel{|}{} & \textit{number?}\hphantom{\text{number predicate}}\tag*{$\llap{\text{number predicate}}$}\\ & {}\mathrel{|}{} & \textit{pair?}\hphantom{\text{pair predicate}}\tag*{$\llap{\text{pair predicate}}$}\\ & {}\mathrel{|}{} & \textit{null?}\hphantom{\text{$\textbf{$\mathord{{\bfit \text{null}}}$}$ predicate}}\tag*{$\llap{\text{$\textbf{$\mathord{{\bfit \text{null}}}$}$ predicate}}$}\\ & {}\mathrel{|}{} & \textit{identity}\hphantom{\text{identity function}}\tag*{$\llap{\text{identity function}}$}\\ & {}\mathrel{|}{} & \mathit{cons} \hphantom{\text{pair construction}}\tag*{$\llap{\text{pair construction}}$}\\ & {}\mathrel{|}{} & \textit{car}\hphantom{\text{first element of pair}}\tag*{$\llap{\text{first element of pair}}$}\\ & {}\mathrel{|}{} & \textit{cdr}\hphantom{\text{second element of pair}}\tag*{$\llap{\text{second element of pair}}$}\\ & {}\mathrel{|}{} & \ldots{} \end{qaligned}

4.2.5 Values

These expressions and primitive functions may produce or manipulate the following values:

\begin{qaligned} v & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & p \hphantom{\text{primitive function}}\tag*{$\llap{\text{primitive function}}$}\\ & {}\mathrel{|}{} & (\textbf{$\mathord{{\bfit \text{num}}}$}\ n) \hphantom{\text{number}}\tag*{$\llap{\text{number}}$}\\ & {}\mathrel{|}{} & \textbf{$\mathord{{\bfit \text{true}}}$} \hphantom{\text{booleans}}\tag*{$\llap{\text{booleans}}$}\\ & {}\mathrel{|}{} & \textbf{$\mathord{{\bfit \text{false}}}$}\\ & {}\mathrel{|}{} & {\bfit λ}(\overrightarrow{x:τ}).e \hphantom{\text{lambda function}}\tag*{$\llap{\text{lambda function}}$}\\ & {}\mathrel{|}{} & {\bfit λ}(\overrightarrow{x:τ}\ .\ x:τ*).e \hphantom{\text{variadic function}}\tag*{$\llap{\text{variadic function}}$}\\ & {}\mathrel{|}{} & {\bfit λ}(\overrightarrow{x:τ}\ .\ x:τ \mathbf{\ldots{}}_{α}).e \hphantom{\text{variadic polymorphic function}}\tag*{$\llap{\text{variadic polymorphic function}}$}\\ & {}\mathrel{|}{} & {\bfit \Lambda{}}(\overrightarrow{α}).e \hphantom{\text{polymorphic abstraction}}\tag*{$\llap{\text{polymorphic abstraction}}$}\\ & {}\mathrel{|}{} & {\bfit \Lambda{}}(\overrightarrow{α}\ α \mathbf{\ldots{}}).e \hphantom{\text{variadic polymorphic abstraction}}\tag*{$\llap{\text{variadic polymorphic abstraction}}$}\\ & {}\mathrel{|}{} & \langle{}v, v\rangle{} \hphantom{\text{pair}}\tag*{$\llap{\text{pair}}$}\\ & {}\mathrel{|}{} & \textbf{$\mathord{{\bfit \text{null}}}$} \hphantom{\text{null}}\tag*{$\llap{\text{null}}$}\\ & {}\mathrel{|}{} & (\textbf{$\mathord{{\bfit \text{promise}}}$}\ e) \hphantom{\text{promise}}\tag*{$\llap{\text{promise}}$}\\ & {}\mathrel{|}{} & (\textbf{$\mathord{{\bfit \text{symbol}}}$}\ s{}’) \hphantom{\text{symbol}}\tag*{$\llap{\text{symbol}}$} \end{qaligned}

The \textbf{$\mathord{{\bfit \text{list}}}$} value notation is defined as a shorthand for a \textbf{$\mathord{{\bfit \text{null}}}$}-terminated linked list of pairs.

\begin{aligned} (\textbf{$\mathord{{\bfit \text{list}}}$}\ v{}_0\ \overrightarrow{v{}_i}) &\stackrel{\scriptscriptstyle\mathsf{def}}{=} \langle{}v{}_0, (\textbf{$\mathord{{\bfit \text{list}}}$}\ \overrightarrow{v{}_i})\rangle{} \\ (\textbf{$\mathord{{\bfit \text{list}}}$}) &\stackrel{\scriptscriptstyle\mathsf{def}}{=} \textbf{$\mathord{{\bfit \text{null}}}$} \\ \end{aligned}

4.2.6 Evaluation contexts

The operational semantics given below rely on the following evaluation contexts:

\begin{qaligned} E & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & [\cdot{}] \hphantom{\text{program entry point}}\tag*{$\llap{\text{program entry point}}$}\\ & {}\mathrel{|}{} & \mathbf{(}\overrightarrow{v}\ E\ \overrightarrow{e}\mathbf{)}\hphantom{\text{function application}}\tag*{$\llap{\text{function application}}$}\\ & {}\mathrel{|}{} & (\textbf{if}\ E\ e\ e)\hphantom{\text{conditional}}\tag*{$\llap{\text{conditional}}$}\\ & {}\mathrel{|}{} & (\textbf{eq?}\ E\ e)\hphantom{\text{symbol equality}}\tag*{$\llap{\text{symbol equality}}$}\\ & {}\mathrel{|}{} & (\textbf{eq?}\ v\ E)\\ & {}\mathrel{|}{} & (\textbf{map}\ E\ e)\hphantom{\text{map function over list}}\tag*{$\llap{\text{map function over list}}$}\\ & {}\mathrel{|}{} & (\textbf{map}\ v\ E) \end{qaligned}

4.2.7 Typing judgement

Γ ; Δ ⊢ e : \mathrm{R}

\begin{qaligned} \mathrm{R} & {}\ifmathjax{\mathrel{{\raise0.9mu{::}\hspace{-4mu}=}}}\iflatex{\Coloneqq}{} & {\mathbf{\ifmathjax{\unicode{x2772}}\iflatex{❲}}}τ \;{\mathbf{;}}\; \phi{}^+ {\mathbf{{/}}} \phi{}^- \;{\mathbf{;}}\; o{\mathbf{\ifmathjax{\unicode{x2773}}\iflatex{❳}}} \end{qaligned}

The Γ ; Δ ⊢ e : \mathrm{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 \phi{}^- which are known to be true when the run-time value of e is \textbf{$\mathord{{\bfit \text{false}}}$}, and a set of propositions \phi{}^+ which are known to be true when the run-time value of e is \textbf{$\mathord{{\bfit \text{true}}}$}2525 Any other value is treated in the same way as \textbf{$\mathord{{\bfit \text{true}}}$}, as values other than \textbf{$\mathord{{\bfit \text{false}}}$} 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 \phi{}^- proposition \mathbf{Number}_y indicates that when e evaluates to \textbf{$\mathord{{\bfit \text{false}}}$}, 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