commit afd2ae77fbdaf9c4fc6be2f90084e40ce962a34f
parent afc0bf9b12c14d525f6c6879d0a8a7f9c0ca8af2
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 9 Aug 2017 18:56:47 +0200
Simplification rules for intersections
Diffstat:
15 files changed, 119 insertions(+), 21 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/Ectx.rkt b/from-dissertation-tobin-hochstadt/Ectx.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/GammaR.rkt b/from-dissertation-tobin-hochstadt/GammaR.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/deltarules.rkt b/from-dissertation-tobin-hochstadt/deltarules.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/e.rkt b/from-dissertation-tobin-hochstadt/e.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/envrt.rkt b/from-dissertation-tobin-hochstadt/envrt.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/p.rkt b/from-dissertation-tobin-hochstadt/p.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/phi-psi-o-path.rkt b/from-dissertation-tobin-hochstadt/phi-psi-o-path.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -190,9 +190,12 @@ allows recursive types to be described with the @recτ* combinator.
@include-equation["tausigma.rkt"]
Additionally, the @Booleanτ type is defined as the union of the @true-τ and
-@false-τ singleton types.
+@false-τ singleton types, and the @Listτ type operator is a shorthand for
+describing the type of heterogeneous linked lists of pairs, with a fixed
+length.
@include-equation["tausigma.rkt" Boolean]
+@include-equation["tausigma.rkt" Listτ]
@subsubsub*section{Filters (value-dependent propositions)}
@@ -385,17 +388,11 @@ filters. @htodo{and objects}
@include-equation["te.rkt" TE-Phi]
@include-equation["te.rkt" TE-Psi]
@include-equation["te.rkt" TE-Psi-Not]
- @include-equation["te.rkt" TE-Psi-Bot]
- ]
+ @include-equation["te.rkt" TE-Psi-Bot]]
@subsubsub*section{Typing rules}
-@todo{Add rule for the (optional?) simplification of intersections}
-@$${
- \begin{aligned}
- \end{aligned}
-}
@include-equation["trules.rkt" T-Promise]
@include-equation["trules.rkt" T-Symbol]
@@ -492,6 +489,27 @@ instantiation of polymorphic abstractions.
be indicated somewhere an equivalence between these two notations (and we
should fix the @${Γ,x:update(…)}, as it is a third notation).}
+@subsubsub*section{Simplification of intersections}
+
+In some cases, intersections are simplified, and the eventual resulting @${⊥}
+types propagate outwards through pairs (and structs, which we do not model
+here). The @simplify* and @propagate⊥ operators show how these simplification
+and propagation steps are performed. The simplification step mostly consists
+in distributing intersections over unions and pairs, and collapsing pairs and
+unions which contain @${⊥}, for the traversed parts of the type.
+
+@include-equation["simplify.rkt" Simplify1]
+
+@${@simplify[τ]} is applied pointwise in other cases:
+
+@include-equation["simplify.rkt" Simplify2]
+
+@include-equation["simplify.rkt" Propagate⊥]
+
+@todo{Apply the intersections on substituted poly types after an inst (or rely
+ on the sutyping rule for intersections to recognise that ⊥ is a subtype of the
+ resulting type?)}.
+
@subsubsub*section{δ-rules}
@include-equation["deltarules.rkt"]
diff --git a/from-dissertation-tobin-hochstadt/simplify.rkt b/from-dissertation-tobin-hochstadt/simplify.rkt
@@ -0,0 +1,67 @@
+#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
+
+@; 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.
+
+#:Simplify1
+
+@$${
+ \begin{aligned}
+ @simplify[@∩τ[τ τ′ @repeatset{τ″}]]
+ &= @simplify[@∩τ[@∩τ[τ τ′] @repeatset{τ″}]] \\
+ @simplify[@∩τ[@un[@repeatset{τ}] @repeatset{σ}]]
+ &= @propagate⊥(@un[@repeatset{@simplify[@∩τ[τ @repeatset{σ}]]}])\\
+ @simplify[@∩τ[@consτ[τ τ′] @consτ[σ σ′]]]
+ &= @(∩τ @${@propagate⊥(@(consτ @simplify[@∩τ[τ σ]]
+ @simplify[@∩τ[τ′ σ′]]))})\\
+ @simplify[@∩τ[@repeatset{σ}]]
+ &= \begin{cases}
+ ⊥ & @textif ∃ τ, τ′ ∈ \{@repeatset{σ}\} . @no-overlap(τ, τ′) \\
+ @∩τ[@repeatset{@simplify[σ]}] &@otherwise
+ \end{cases}
+ \end{aligned}
+}
+
+#:Simplify2
+
+@$${
+ \begin{aligned}
+ @simplify[@f→[(@repeated{τ}) R]]
+ &= @f→[(@repeated{@simplify[τ]}) @simplify[R]] \\
+ @simplify[@f*[(@repeated{τ} @${τ*}) R]]
+ &= @f*[(@repeated{@simplify[τ]} @simplify[τ*]) @simplify[R]]\\
+ @simplify[@f…[(@repeated{τ} @polydot[τ α]) R]]
+ &= @f…[(@repeated{@simplify[τ]} @polydot[@simplify[τ] α]) @simplify[R]]\\
+ @simplify[@∀r[(@repeated{α}) τ]]
+ &= @∀r[(@repeated{α}) @simplify[τ]]\\
+ @simplify[@∀r[(@repeated{α} @polydotα[α]) τ]]
+ &= @∀r[(@repeated{α} @polydotα[α]) @simplify[τ]]\\
+ @simplify[@consτ[τ σ]]
+ &= @consτ[@${@simplify[τ]} @${@simplify[σ]}]\\
+ @simplify[@List…τ[τ α]]
+ &= @List…τ[@simplify[τ] α]\\
+ @simplify[@promiseτ[R]]
+ &= @promiseτ[@simplify[R]]\\
+ @simplify[@recτ[r τ]]
+ &= @recτ[r @simplify[τ]] \\
+ @simplify[τ] &= τ \qquad @otherwise
+ @simplify[@R[τ φ⁺ φ⁻ o]] &= @R[@simplify[τ] @simplify[φ⁺] @simplify[φ⁻] o]\\
+ @simplify[@repeatset{ψ}] &= @repeatset{@simplify[ψ]}\\
+ @simplify[@${τ_{π(loc)}}] &= @simplify[τ]_{π(loc)}\\
+ @simplify[@${@!{τ}_{π(loc)}}] &= @!{@simplify[τ]}_{π(loc)}\\
+ @simplify[⊥] = ⊥ \\
+ \end{aligned}
+}
+
+#:Propagate⊥
+
+@$${
+ \begin{aligned}
+ @propagate⊥(@consτ[τ σ]) &= ⊥ & @textif @=:[τ ⊥]\\
+ @propagate⊥(@consτ[τ σ]) &= ⊥ & @textif @=:[σ ⊥]\\
+ @propagate⊥(τ) &= ⊥ &@textif @=:[τ ⊥]\\@; For unions (subtyping will dispatch)
+ @propagate⊥(τ) &= τ &@otherwise
+ \end{aligned}
+}
diff --git a/from-dissertation-tobin-hochstadt/subtyping.rkt b/from-dissertation-tobin-hochstadt/subtyping.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/tausigma.rkt b/from-dissertation-tobin-hochstadt/tausigma.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
@@ -22,7 +22,7 @@
@tag*{variadic polymorphic type}}
@acase{α @P β@tag*{polymorphic type variable}}
@acase{@un[@repeatset{τ}]@tag*{union}}
- @acase{@∩τ[@repeatset{τ}] @tag*{any symbol}}
+ @acase{@∩τ[@repeatset{τ}] @tag*{intersection}}
@acase{@consτ[τ τ]@tag*{pair}}
@acase{@null-τ @tag*{null (end of lists)}}
@acase{@List…τ[τ α] @tag*{variadic polymorphic list}}
@@ -33,4 +33,11 @@
@$${
@=:def[@Booleanτ @un[@true-τ @false-τ]]
+}
+
+#:Listτ
+
+@$${
+ @=:def[@Listτ[τ @repeated{σ}] @consτ[τ @Listτ[@repeated{σ}]]]
+ @=:def[@Listτ[] @null-τ]
}
\ No newline at end of file
diff --git a/from-dissertation-tobin-hochstadt/te.rkt b/from-dissertation-tobin-hochstadt/te.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/from-dissertation-tobin-hochstadt/v.rkt b/from-dissertation-tobin-hochstadt/v.rkt
@@ -1,6 +1,6 @@
#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
-@; This file is not under the CC0 license, as it contains rules and definitions
+@; 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.
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -78,6 +78,8 @@
[else
;; Defined in util.rkt
@${\overrightbracedarrow{@|w|@|l|@|w|}}]))
+(define (repeatSet . l)
+ @${\{@(apply repeatset l)\}})
(define |P| @${\ |\ })
(define ρc @${\rho_{c}})
(define ρf @${\rho_{f}})
@@ -171,6 +173,7 @@
(define-syntax List…τ* (defop "List"))
(define-syntax-rule (List…τ τ α)
@List…τ*[@polydot[τ α]])
+(define-syntax Listτ (defop "List"))
@;(define-syntax →Values (defop "Values"))
(define-syntax-rule (→Values v ...) (spaces (stringify v) ...))
(define @emptypath @${ϵ})
@@ -228,6 +231,9 @@
(define no-overlap @${\operatorname{no-overlap}})
(define restrict @${\operatorname{restrict}})
(define remove @${\operatorname{remove}})
+(define simplify* @${\operatorname{simplify}})
+(define-syntax-rule (simplify τ) @${@simplify*(@(stringify τ))})
+(define propagate⊥ @${\operatorname{propagate_⊥}})
(define loc @${\mathit{loc}})
(define (! . rest) @${\overline{@rest}})
(define metatrue @${\mathrm{true}})
