commit 6b34eb8ba35de40995773b552e7058667f337d04
parent d0c5e6fac175d87680fc695d6318609706d42387
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Mon, 17 Jul 2017 22:17:38 +0200
Copied most expression, type etc. definitions from Sam Tobin-Hochstadt. Copied the subtyping rules. Started copying the typing rules.
Diffstat:
9 files changed, 540 insertions(+), 60 deletions(-)
diff --git a/LICENSE-more.md b/LICENSE-more.md
@@ -1,9 +1,11 @@
-anaphoric
+phc-thesis
Copyright (c) 2016-2017 Georges Dupéron
-This package is in distributed under the Creative Commons CC0 license
+This package (with the exception of the files in the
+./from-dissertation-tobin-hochstadt/ folder)
+is in distributed under the Creative Commons CC0 license
https://creativecommons.org/publicdomain/zero/1.0/, as specified by
the LICENSE.txt file.
diff --git a/Makefile b/Makefile
@@ -1,7 +1,7 @@
.PHONY: all
all: doc/pdf/phc-thesis.pdf
-doc/pdf/phc-thesis.pdf: scribblings/*.scrbl scribblings/*.rkt
+doc/pdf/phc-thesis.pdf: from-dissertation-tobin-hochstadt/*.scrbl scribblings/*.scrbl scribblings/*.rkt
raco setup --doc-pdf doc/pdf/ --pkgs phc-thesis > pdf.log 2>&1 || (cat pdf.log && exit 1)
gs -dNOPAUSE -dBATCH -sDEVICE=pdfwrite -dFastWebView=true -sOutputFile=doc/pdf/phc-thesis-linearized.pdf doc/pdf/phc-thesis.pdf
mv doc/pdf/phc-thesis-linearized.pdf doc/pdf/phc-thesis.pdf
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -0,0 +1,332 @@
+#lang scribble/manual
+
+@; This file is not under the CC0 license, as it contains rules and definitions
+@; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the
+@; permission to copy these rules, but did not ask for a relicensing under the
+@; CC0 license.
+
+The following definitions and rules are copied and adjusted
+from@~cite["tobin-hochstadt_typed_2010"], with the author's permission. Some
+of the notations were changed to use those of@~cite["kent2016occurrence"]
+
+@require["../scribblings/util.rkt"
+ "../scribblings/adt-utils.rkt"
+ (for-label (only-meta-in 0 typed/racket)
+ typed/racket/class)
+ scribble/example
+ racket/string]
+@(use-mathjax)
+
+@(define tr-eval (make-eval-factory '(typed/racket)))
+
+@title[#:style (with-html5 manual-doc-style)
+ #:version (version-text)
+ #:tag "from-dissertation-tobin-hochstadt"]{Formal semantics for part of
+ @|typedracket|'s type system}
+
+Expressions:
+
+@cases["e" #:first-sep "⩴"
+ @acase{x}
+ @acase{@num-e}
+ @acase{@true-e}
+ @acase{@false-e}
+ @acase{@primop}
+ @acase{@app[e @repeated{e}]}
+ @acase{@ifop[e e e]}
+ @acase{@λe[(@repeated{x:τ}) e]}
+ @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e]}
+ @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]}
+ @acase{@Λe[(@repeated{α}) e]}
+ @acase{@Λe[(@repeated{α} @polydotα[α]) e]}
+ @acase{@conse[e e]} @; TODO: shouldn't it be a primop?
+ @acase{@at[e @repeated{τ}]}]
+
+Primitive operations:
+
+@cases[@primop #:first-sep "⩴"
+ @acase{@textit{add1}} ;; only here as an example
+ @acase{@textit{number?}} ;; probably used in some explanation
+ @acase{@textit{cons?}}
+ @acase{@textit{null?}}
+ @acase{@textit{car}}
+ @acase{@textit{cdr}}
+ @acase{…}]
+
+Values:
+
+@cases["v" #:first-sep "⩴"
+ @acase{c}
+ @acase{@num-v}
+ @acase{@true-v}
+ @acase{@false-v}
+ @acase{@primop}
+ @acase{@λv[ℰ (@repeated{x:τ}) e]}
+ @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:τ*}) e]}
+ @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]}
+ @acase{@Λv[ℰ (@repeated{α}) e]}
+ @acase{@Λv[ℰ (@repeated{α} @polydotα[α]) e]}
+ @acase{@consv[v v]}]
+
+Execution environment:
+
+@cases["ℰ" #:first-sep "⩴"
+ @acase{@repeated{@↦v[x v]}\ @repeated{@↦v[α τ]}}]
+
+Evaluation context:
+
+@cases["E" #:first-sep "⩴"
+ @acase{[]}
+ @acase{@app[E @repeated{e}]}
+ @acase{@app[v @repeated{v} E @repeated{e}]}
+ @acase{@ifop[E e e]}
+ @acase{@conse[E e]} @; TODO: shouldn't it be a primop?
+ @acase{@conse[v E]}] @; TODO: shouldn't it be a primop?
+
+@; TODO: are other cases needed?
+
+Typing judgement:
+
+@$${
+ @Γ[⊢ e τ φ⁺ φ⁻ o]
+}
+
+@todo{Explain…}
+
+Types:
+
+@cases["τ,σ" #:first-sep "⩴"
+ @acase{⊤}
+ @acase{@num-τ}
+ @acase{@true-τ}
+ @acase{@false-τ}
+ @acase{@f→[(@repeated{τ}) R]}
+ @acase{@f→[(@repeated{τ} @${\ .\ } @${τ*}) R]}
+ @acase{@f→[(@repeated{τ} @${\ .\ } @polydot[τ α]) R]}
+ @acase{@∀r[@${(@repeated{α})} @repeated{τ}]}
+ @acase{@∀r[@${(@repeated{α} @polydotα[α])} @repeated{τ}]}
+ @acase{@un[@repeated{τ}]}
+ @acase{@consτ[τ τ]}]
+
+@cases[@R #:first-sep "⩴"
+ @R[@→Values[@repeated{τ}]
+ @${φ⁺}
+ @${φ⁻}
+ @${o}]]
+
+
+Filters (conditional typing information):
+
+@cases[@${φ} #:first-sep "⩴" @acase{@repeatset{ψ}}]
+
+@cases["ψ" #:first-sep "⩴"
+ @acase{τₓ}
+ @acase{\overline{τ}ₓ}
+ @acase{⊥}]
+
+Objects (aliasing information):
+
+@cases[@textrm{o} #:first-sep "⩴"
+ @acase{π}
+ @acase{∅}]
+
+Paths:
+
+@cases[@textit{π} #:first-sep "⩴"
+ @acase{pe∷π}
+ @acase{@emptypath \qquad\qquad\text{empty path}}]
+
+The path concatenation operator @${∷} is associative. @htodo{Actually, we
+ define it for pe∷π above, not for π∷π}. The @${@emptypath} is omitted from
+paths with one or more elements, so we write @${car∷cdr} instead of @${
+ car∷cdr∷@emptypath}.
+
+Path elements (aliasing information):
+
+@cases[@textit{pe} #:first-sep "⩴"
+ @acase{car}
+ @acase{cdr}]
+
+Subtyping:
+
+@$inferrule[
+ @${}
+ @${⊢ τ <: τ}
+ @${@textsc{S-Refl}}
+ ]
+
+@$inferrule[
+ @${}
+ @${⊢ τ <: ⊤}
+ @${@textsc{S-Top}}
+ ]
+
+@textsc{S-Bot} can be derived from @textsc{S-UnionSub}, by constructing an
+empty union. The @${⊥} type is a shorthand for @${(∪)}. It is a subtype of
+every other type, and is not inhabited by any value.
+
+@$inferrule[
+ @${}
+ @${⊢ ⊥ <: τ}
+ @${@textsc{S-Bot}}
+ ]
+
+@$inferrule[
+ @${
+ @repeated{@<:[σ_a τ_a]} \\
+ @<:R[R @${@R'}]}
+ @${@<:[@f→[(@repeated{τ_a}) R]
+ @f→[(@repeated{σ_a}) @${@R'}]]}
+ @${@textsc{S-Fun}}
+ ]
+
+@$inferrule[
+ @${
+ @repeated{@<:[τ_r σ_r]} \\
+ @${φ⁺' ⊆ φ⁺ } \\
+ @${φ⁻' ⊆ φ⁻ } \\
+ o = o' ∨ o' = ∅}
+ @${@<:R[@R[@→Values[@repeated{τ_r}]
+ @${φ⁺}
+ @${φ⁻}
+ @${o}]
+ @R[@→Values[@repeated{σ_r}]
+ @${φ'⁺}
+ @${φ'⁻}
+ @${o'}]]}
+ @${@textsc{S-R}}
+ ]
+
+@$inferrule[
+ @${
+ @repeated{@<:[σ_a τ_a]} \\
+ @<:[σ τ] \\
+ @<:R[R @${@R'}]}
+ @${@<:[@f→[(@repeated{τ_a} @${\ .\ } τ*) R]
+ @f→[(@repeated{σ_a} @${\ .\ } σ*) @${@R'}]]}
+ @${@textsc{S-Fun*}}
+ ]
+
+@$inferrule[
+ @${
+ @repeated{@<:[σ_a τ_a]} \\
+ @repeated{@<:[σᵢ τ]} \\
+ @<:R[R @${@R'}]}
+ @${@<:[@f→[(@repeated{τ_a} @${\ .\ } τ*) R]
+ @f→[(@repeated{σ_a} @repeated{σᵢ}) @${@R'}]]}
+ @${@textsc{S-Fun*-Fixed}}
+ ]
+
+@$inferrule[
+ @${
+ @repeated{@<:[σ_a τ_a]} \\
+ @repeated{@<:[σᵢ τ]} \\
+ @<:[σ τ] \\
+ @<:R[R @${@R'}]}
+ @${@<:[@f→[(@repeated{τ_a} @${\ .\ } τ*) R]
+ @f→[(@repeated{σ_a} @repeated{σᵢ} @${\ .\ } σ*) @${@R'}]]}
+ @${@textsc{S-Fun*-Fixed*}}
+ ]
+
+@$inferrule[
+ @${
+ @repeated{@<:[σ_a τ_a]} \\
+ @<:[σ τ] \\
+ @<:R[R @${@R'}]}
+ @${@<:[@f→[(@repeated{τ_a} @${\ .\ } @polydot[τ α]) R]
+ @f→[(@repeated{σ_a} @${\ .\ } @polydot[σ α]) @${@R'}]]}
+ @${@textsc{S-DFun}}
+ ]
+
+@$inferrule[
+ @${@<:[@${τ[@repeated{αᵢ ↦ βᵢ}]} σ]}
+ @${@<:[@∀r[@${(@repeated{αᵢ})} τ]
+ @∀r[@${(@repeated{βᵢ})} σ]]}
+ @${@textsc{S-Poly-}α@textsc{-Equiv}}
+ ]
+
+@todo{This should use the substitution for a polydot (subst-dots?), not the
+ usual subst.}
+
+@$inferrule[
+ @${@<:[@${τ[@repeated{αᵢ ↦ βᵢ} α ↦ β]} σ]}
+ @${@<:[@∀r[@${(@repeated{αᵢ} @polydotα[α])} τ]
+ @∀r[@${(@repeated{βᵢ} @polydotα[β])} σ]]}
+ @${@textsc{S-PolyD-}α@textsc{-Equiv}}
+ ]
+
+@todo{check the following rule:}
+
+@htodo{Try to detach the ∀ from the →, in case the → is nested further deep.
+ If it works.}
+
+@$inferrule[
+ @${
+ @repeated{@<:[σ_a τ_a]} \\
+ @<:[σ @${τ[α ↦ ⊤]}] \\
+ @<:R[R @${@R'}]}
+ @${@<:[@∀r[@${(@polydotα[α])} @f→[(@repeated{τ_a} @polydot[τ α]) R]]
+ @f→[(@repeated{σ_a} σ*) @${@R'}]]}
+ @${@textsc{S-DFun-Fun*}}
+ ]
+
+@todo{What if some tvars are unbound in the types above, how do they compare?}
+
+@$inferrule[
+ @${∃ i . @<:[τ @${σᵢ}]}
+ @${@<:[τ @${\bigcup @repeated{σᵢ}}]}
+ @${@textsc{S-UnionSuper}}
+ ]
+
+@$inferrule[
+ @${@repeated[@<:[τᵢ @${σ}]]}
+ @${@<:[@${\bigcup @repeated{τᵢ}} σ]}
+ @${@textsc{S-UnionSub}}
+ ]
+
+@$inferrule[
+ @${@<:[τ₁ σ₁] \\
+ @<:[τ₂ σ₂]}
+ @${@<:[@consτ[τ₁ τ₂] @consτ[σ₁ σ₂]]}
+ @${@textsc{S-Pair}}
+ ]
+
+Operational semantics:
+
+
+
+Typing rules:
+
+@$inferrule[@${}
+ @${@Γ[⊢ x @${Γ(x)} @${\overline{@false-τ}} @true-τ x]}
+ @${@textsc{T-Var}}]
+
+@$inferrule[@${}
+ @${@Γ[⊢ p @${δ_τ(p)} ϵ ⊥ ∅]}
+ @${@textsc{T-Primop}}]
+
+@$inferrule[@${}
+ @${@Γ[⊢ @truev @true-τ ϵ ⊥ ∅]}
+ @${@textsc{T-True}}]
+
+@$inferrule[@${}
+ @${@Γ[⊢ @falsev @false-τ ⊥ ϵ ∅]}
+ @${@textsc{T-False}}]
+
+@$inferrule[@${}
+ @${@Γ[⊢ @num-v @num-τ ϵ ⊥ ∅]}
+ @${@textsc{T-Num}}]
+
+
+TODO: Drop the object and filters which are not in terms of x₀, rename
+otherwise.
+
+@$inferrule[@${@Γ[@repeated{x:σ} ⊢ e τ φ⁺ φ⁻ o]}
+ @${@Γ[⊢ @λe[(@repeated{x:σ}) e]
+ (f→ (@repeated{σ})
+ @R[@→Values[τ]
+ @${φ⁺[x ↦ ?]}
+ @${φ⁻[x ↦ ?]}
+ @${o[x ↦ ?]}])
+ ϵ ⊥ ∅]}
+ @${@textsc{T-Abs}}]
+\ No newline at end of file
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -39,7 +39,7 @@ the value stored in an instance of a constructor.
@list[]}
@acase{…}
- @acase{@record[@repeated{@|ɐ|ᵢ = eᵢ}]}
+ @acase{@record[@repeated{@↦e[@${@|ɐ|ᵢ} eᵢ]}]}
@acase{(@record-pred[@repeated{@|ɐ|ᵢ}]\ e)}
@acase{(@record-pred*[@repeated{@|ɐ|ᵢ} @repeated{-@|ɐ|ⱼ}]\ e)}@;added
@acase{e.@|ɐ|}
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -1,6 +1,10 @@
#lang at-exp racket
-@(provide (all-defined-out))
+@(provide (except-out (all-defined-out)
+ num-e*
+ num-v*
+ num-τ*))
@require["util.rkt"
+ scriblib/render-cond
(for-label (only-meta-in 0 typed/racket))]
@@ -19,7 +23,10 @@
[(_ :stringify ...)
#`@${(@(add-between (list @textbf{@#,op}
#,@(syntax->list #'(→str ...)))
- "\\ "))}]))
+ "\\ "))}]
+ [self
+ (identifier? #'self)
+ #`@textbf{@#,op}]))
@(begin-for-syntax
(require (for-syntax racket/base))
@@ -36,34 +43,124 @@
[(_ :stringify ...)
#'(add-between (list →str ...) "\\ ")]))
-@(define-syntax ctor (defop "ctor"))
-@(define κ @${κ})
-@(define ɐ @${a})
-@(define-syntax ctorTop (defop "CtorTop"))
-@(define-syntax-rule (ctor-val κ)
- @${\mathbf{getval}_@κ})
-@(define-syntax record (defop "record"))
-@(define-syntax variant (defop "V"))
-@(define (repeated . l) @${\overrightarrow{@l}})
-@(define (repeatset . l) @${\{\overrightarrow{@l}\}})
-@(define |P| @${\ |\ })
-@(define ρc @${\rho_{c}})
-@(define ρf @${\rho_{f}})
-@(define-syntax atc (defop (list "@" @${{}_{@textbf{c}}})))
-@(define-syntax atf (defop (list "@" @${{}_{@textbf{f}}})))
-@(define-syntax Λc (defop (list "Λ" @${{}_{@textbf{c}}})))
-@(define-syntax Λf (defop (list "Λ" @${{}_{@textbf{f}}})))
-@(define-syntax ∀c (defop @${\mathbf{∀}_{@textbf{c}}}))
-@(define-syntax ∀f (defop @${\mathbf{∀}_{@textbf{f}}}))
-@(define-syntax-rule (ctor-pred c)
- @${@(stringify c)\mathbf{?}})
-@(define-syntax-rule (record-pred . f*)
- @${(@textbf{record?}\ @(stringify . f*))})
-@(define-syntax-rule (record-pred* . f*)
- @${(@textbf{record$\mathbf{*}$?}\ @(stringify . f*))});; TODO text vs math!!!
-@(define-syntax-rule (opwith rec a v)
- @list{@(stringify rec) @textbf[" with "] @(stringify a) = @(stringify v)})
-@(define-syntax-rule (opwithout rec a)
- @list{@(stringify rec) @textbf[" without "] @(stringify a)})
-@(define πctor-val @${@textbf{getval}})
-@(define (πɐ . ɐ) @${\mathbf{@ɐ}})
-\ No newline at end of file
+(define (spaces . l)
+ (add-between l "\\ "))
+
+(define-syntax ctor (defop "ctor"))
+(define κ @${κ})
+(define ɐ @${a})
+(define-syntax ctorTop (defop "CtorTop"))
+(define-syntax-rule (ctor-val κ)
+ @${\mathbf{getval}_@κ})
+(define-syntax record (defop "record"))
+(define-syntax variant (defop "V"))
+(define-syntax ifop (defop "if"))
+(define-syntax-rule (λv env (arg ...) expr)
+ @${[@(stringify env), λ(@(list (stringify arg) ...)).@(stringify expr)]})
+(define-syntax-rule (λe (arg ...) expr)
+ @${λ(@(spaces (stringify arg) ...)).@(stringify expr)})
+(define-syntax-rule (Λe (arg ...) expr)
+ @${Λ(@(spaces (stringify arg) ...)).@(stringify expr)})
+(define-syntax-rule (Λv env (arg ...) expr)
+ @${[@(stringify env), Λ(@(spaces (stringify arg) ...)).@(stringify expr)]}) ;; TODO: is the env necessary here? It's a type env, right?
+(define (repeated . l) @${\overrightarrow{@l}})
+(define (repeatset . l)
+ (cond-element
+ [html
+ @${\def\overrightbracedarrow#1{\overset{\scriptscriptstyle{\raise1mu{\{}}}{\vphantom{#1}}\overrightarrow{#1}\overset{\scriptscriptstyle{\raise1mu{\}}}}{\vphantom{#1}}}\overrightbracedarrow{@l}}]
+ [else
+ ;; Defined in util.rkt
+ @${\overrightbracedarrow{@l}}]))
+(define |P| @${\ |\ })
+(define ρc @${\rho_{c}})
+(define ρf @${\rho_{f}})
+(define-syntax at (defop "@"))
+(define-syntax atc (defop (list "@" @${{}_{@textbf{c}}})))
+(define-syntax atf (defop (list "@" @${{}_{@textbf{f}}})))
+(define-syntax Λc (defop (list "Λ" @${{}_{@textbf{c}}})))
+(define-syntax Λf (defop (list "Λ" @${{}_{@textbf{f}}})))
+(define-syntax ∀r (defop @${\mathbf{∀}}))
+(define-syntax ∀c (defop @${\mathbf{∀}_{@textbf{c}}}))
+(define-syntax ∀f (defop @${\mathbf{∀}_{@textbf{f}}}))
+(define-syntax-rule (ctor-pred c)
+ @${@(stringify c)\mathbf{?}})
+(define-syntax-rule (record-pred . f*)
+ @${(@textbf{record?}\ @(stringify . f*))})
+(define-syntax-rule (record-pred* . f*)
+ @${(@textbf{record$\mathbf{*}$?}\ @(stringify . f*))});; TODO text vs math!!!
+(define-syntax-rule (opwith rec a v)
+ @list{@(stringify rec) @textbf[" with "] @(stringify a) = @(stringify v)})
+(define-syntax-rule (opwithout rec a)
+ @list{@(stringify rec) @textbf[" without "] @(stringify a)})
+(define πctor-val @${@textbf{getval}})
+(define (πɐ . ɐ) @${\mathbf{@ɐ}})
+;; Associates a variable name or record field name with a value, type or
+;; evaluation context.
+(define-syntax-rule (↦v name val)
+ @${@(stringify name)↦@(stringify val)})
+(define-syntax-rule (↦e name val) @${@(stringify name)↦@(stringify val)})
+(define-syntax-rule (↦E name val) @${@(stringify name)↦@(stringify val)})
+(define-syntax-rule (↦τ name val) @${@(stringify name)↦@(stringify val)})
+(define-syntax-rule (app f+args ...)
+ @${(@(add-between (list (stringify f+args) ...) "\\ "))})
+
+(define-syntax num-e* (defop "num"))
+(define-syntax num-v* (defop "num"))
+(define-syntax num-τ* (defop "num"))
+(define num-e @num-e*[n])
+(define num-v @num-v*[n])
+(define num-τ @num-τ*[n])
+
+(define-syntax true-e (defop "true"))
+(define-syntax true-v (defop @${@textit{true}}))
+(define-syntax true-τ (defop "true"))
+
+(define-syntax false-e (defop "false"))
+(define-syntax false-v (defop @${@textit{false}}))
+(define-syntax false-τ (defop "false"))
+
+(define-syntax un (defop "∪"))
+
+(define-syntax-rule (f→ (from ...) R)
+ @${(@(add-between (list @(stringify from) ...) "\\ ") → @(stringify R))})
+(define-syntax (R stx)
+ (syntax-case stx ()
+ [(_ to φ⁺ φ⁻ o)
+ #'@${❲@(stringify to)
+ ; @(stringify φ⁺) / @(stringify φ⁻)
+ ; @(stringify o)❳}]
+ [self (identifier? #'self)
+ #'@${\mathrm{R}}]))
+#;(define-syntax-rule (f→ (from ...) to φ O)
+ @${
+ (@list[@(stringify from) ...]
+ \xrightarrow[@(stringify O)]{@(stringify φ)}
+ @(stringify to))
+ })
+
+(define primop "p")
+
+(define-syntax conse (defop "cons"))
+(define-syntax-rule (consv a b) @${⟨@(stringify a), @(stringify b)⟩})
+(define-syntax-rule (consτ a b) @${⟨@(stringify a), @(stringify b)⟩})
+(define-syntax-rule (polydot τ α)
+ @${@(stringify τ) \mathbf{…}_{@(stringify α)}})
+(define-syntax-rule (polydotα α)
+ @${@(stringify α) \mathbf{…}})
+@;(define-syntax →Values (defop "Values"))
+(define-syntax-rule (→Values v ...) (spaces (stringify v) ...))
+(define @emptypath @${ϵ} #;@${•})
+(define-syntax-rule (<: a b)
+ @${⊢ @(stringify a) \mathrel{<:} @(stringify b)})
+
+(define-syntax-rule (<:R a b)
+ @${⊢ @(stringify a) \mathrel{{<:}_R} @(stringify b)})
+
+@(define-syntax (Γ stx)
+ (syntax-case stx (⊢)
+ [(_ more ... ⊢ x τ φ+ φ- o)
+ #'@${@(add-between (list "Γ" (stringify more) ...) ", ") ⊢
+ @(stringify x)
+ : @(stringify τ)
+ ; @(stringify φ+) / @(stringify φ-)
+ ; @(stringify o)}]))
+\ No newline at end of file
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -69,3 +69,14 @@ values of two function types present in the same union).
@include-asection["adt-row-opsem.scrbl"]
@include-asection["adt-row-shorthands.scrbl"]
}
+
+
+@todo{Argue that a type system with symbols, unique tokens (a way to create a
+ fresh "identity", like (cons 0 0) creates a fresh memory cell which is not eq?
+ to any other, past or future), untagged unions, pure case→ functions with the
+ usual polymorphism and row polymorphism (ranging over function cases, with
+ negation), i.e. a simplification / generalisation of our system, is more
+ "general" than @typedracket (i.e. Racket's existing types can be easily
+ encoded with ours), and show how other systems of variants and records can be
+ encoded with it (try the one from @CAML + the "backtick" cases of variants;
+ try to see if the one from tinybang is more general, less or different).}
+\ No newline at end of file
diff --git a/scribblings/bibliography.bib b/scribblings/bibliography.bib
@@ -1,3 +1,14 @@
+@inproceedings{kent2016occurrence,
+ title={Occurrence typing modulo theories},
+ author={Kent, Andrew M and Kempe, David and Tobin-Hochstadt, Sam},
+ booktitle={ACM SIGPLAN Notices},
+ volume={51},
+ number={6},
+ pages={296--309},
+ year={2016},
+ organization={ACM}
+}
+
@article{HMMilner78,
title={A theory of type polymorphism in programming},
author={Milner, Robin},
diff --git a/scribblings/tr.scrbl b/scribblings/tr.scrbl
@@ -840,6 +840,15 @@ therefore keep our overview succinct and gloss over most details.
@${@v & ∈ τ(@t)}
@${@v ∈ τ(@t)})))
+@include-asection["../from-dissertation-tobin-hochstadt/rules.scrbl"]
+
+@;{
+@asection{
+ @atitle{Formal semantics for part of Typed Racket's type system}
+
+}
+}
+
@htodo{
@asection{
@atitle{Formal semantics for part of Typed Racket's type system}
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -152,7 +152,24 @@
;; TODO: merge the handling of unicode chars into scribble-math.
(define m
(list setup-math
- (tex-header "\\renewcommand{\\rmdefault}{cmr}")
+ (tex-header #<<EOTEX
+ \renewcommand{\rmdefault}{cmr}
+ \newenvironment{qaligned}{%
+ \begin{array}[t]{@{}r@{}c@{}l@{}}%
+ }{%
+ \end{array}
+ }%
+ \def\overrightbracedarrow#1{%
+ \overset{\raisebox{-0.75pt}[\height][-0.75pt]{%
+ $\scriptscriptstyle{\{}$}}{\vphantom{#1}%
+ }%
+ \overrightarrow{#1}%
+ \overset{\raisebox{-0.75pt}[\height][-0.75pt]{%
+ $\scriptscriptstyle{\}}$}}{\vphantom{#1}%
+ }%
+ }%
+EOTEX
+ )
(elem #:style (style #f (list (css-addition
#".NoteBox {
height: auto !important;
@@ -471,19 +488,20 @@ EOTEX
(define $ooo ($ (mathtext "\\textit{ooo}")))
(define ($inferrule from* to* [label '()])
- (elem #:style
- (style #f (list (tex-addition
- (string->bytes/utf-8
- "\\usepackage{mathpartir}"))))
- ($ (cond-element [html "\\frac{\\begin{gathered}"]
- [else "\\inferrule{"])
- from*
- (cond-element [html "\\end{gathered}}{\\begin{gathered}"]
- [else "}{"])
- to*
- (cond-element [html "\\end{gathered}}"]
- [else "}"])
- label)))
+ @$$[
+ (elem #:style
+ (style #f (list (tex-addition
+ (string->bytes/utf-8
+ "\\usepackage{mathpartir}"))))
+ ($ (cond-element [html "\\frac{\\begin{gathered}"]
+ [else "\\inferrule{"])
+ from*
+ (cond-element [html "\\end{gathered}}{\\begin{gathered}"]
+ [else "}{"])
+ to*
+ (cond-element [html "\\end{gathered}}"]
+ [else "}"])
+ label))])
(define htmldiff-css-experiment #<<EOCSS
.version:after {
@@ -536,8 +554,7 @@ EOCSS
\begin{aligned}[@valign-letter]
@lines
\end{aligned}
-}
- )
+})
(define acase list)
(define cases
@@ -623,11 +640,11 @@ EOCSS
(define (frac x . y)
@list{\frac{@x}{@y}})
-(define where (mathtext @${\text{ where }}))
-(define textif (mathtext @${\text{ if }}))
-(define otherwise (mathtext @${\text{ otherwise }}))
-(define quad (mathtext @${\quad}))
+(define where @mathtext{\text{ where }})
+(define textif @mathtext{\text{ if }})
+(define otherwise @mathtext{\text{ otherwise }})
+(define quad @${\quad})
(define (textbf . l) (mathtext "\\textbf{" l "}"))
(define (textit . l) (mathtext "\\textit{" l "}"))
(define (textrm . l) (mathtext "\\textrm{" l "}"))
-(define (text . l) (mathtext "\\text{" l "}"))
-\ No newline at end of file
+(define (text . l) (mathtext "\\text{" l "}"))
