From e9255ca439636f2a5c6e48a22c79a5cb7b207369 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 30 Dec 2016 02:25:20 +0100 Subject: [PATCH] Started writing phantom invariants representation, optimized flex records. --- Graph-notes-copy2.vue | 299 ++++++++++++++++----- flexible-with.hl.rkt | 111 +++++--- invariants-phantom.hl.rkt | 98 +++++++ scribblings/phc-graph-implementation.scrbl | 3 +- test/test-flexible-with.rkt | 12 +- times.rkt | 58 ++++ 6 files changed, 476 insertions(+), 105 deletions(-) create mode 100644 invariants-phantom.hl.rkt create mode 100644 times.rkt diff --git a/Graph-notes-copy2.vue b/Graph-notes-copy2.vue index e73fd5f..e863db8 100644 --- a/Graph-notes-copy2.vue +++ b/Graph-notes-copy2.vue @@ -1,14 +1,14 @@ - + - + - Graph-notes-copy2.vue @@ -30,35 +30,25 @@ + created="1479309887096" x="1577.3673" y="857.9207" width="203.0" + height="23.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> #8AEE95 #776D6D #000000 SansSerif-plain-12 http://vue.tufts.edu/rdf/resource/6dbf6afec0a80026548592b88abb8384 - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b00c0a80026548592b8a0766ac6 - - - #404040 #404040 SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/6dbf6affc0a80026548592b80b4ee7cc - - + + 6 7 @@ -300,9 +290,9 @@ 29 + width="327.0" height="38.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> #F2AE45 #776D6D #000000 @@ -310,16 +300,16 @@ http://vue.tufts.edu/rdf/resource/6dc1a30bc0a80026548592b8e12add9f - #404040 #404040 SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/6dc1a30cc0a80026548592b879e5ac96 - - + + 33 36 @@ -366,7 +356,7 @@ #FEFEC9 #EA2218 @@ -375,19 +365,6 @@ http://vue.tufts.edu/rdf/resource/6dd89bd5c0a80026548592b8ddb5b6c7 - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dd89bd5c0a80026548592b81da96232 - - - 90 - 103 - @@ -789,7 +766,7 @@ - #BDE5F2 + #FFC63B #776D6D #000000 SansSerif-plain-12 @@ -1345,7 +1322,7 @@ - #F2AE45 + #C1F780 #776D6D #000000 SansSerif-plain-12 @@ -1368,7 +1345,7 @@ - #F2AE45 + #A6A6A6 #776D6D #000000 SansSerif-plain-12 @@ -1391,7 +1368,7 @@ - #F2AE45 + #A6A6A6 #776D6D #000000 SansSerif-plain-12 @@ -2191,7 +2168,7 @@ - #F2AE45 + #A6A6A6 #776D6D #000000 SansSerif-plain-12 @@ -2259,7 +2236,7 @@ - #F2AE45 + #FEFD8C #776D6D #000000 SansSerif-plain-12 @@ -2267,7 +2244,7 @@ - #F2AE45 + #C1F780 #776D6D #000000 SansSerif-plain-12 @@ -2315,7 +2292,7 @@ - #F2AE45 + #FEFD8C #776D6D #000000 SansSerif-plain-12 @@ -2323,7 +2300,7 @@ - #F2AE45 + #FEFD8C #776D6D #000000 SansSerif-plain-12 @@ -2333,7 +2310,7 @@ - #F2AE45 + #FEFD8C #776D6D #000000 SansSerif-plain-12 @@ -2359,7 +2336,7 @@ label="What about invariants? * Just copy them over syntactically? * Require that they are re-specified (at least by explicitly copying them by their name)" layerID="1" created="1479346589797" x="788.9707" y="332.74475" width="329.0" height="68.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #F2AE45 + #DD7B11 #776D6D #000000 SansSerif-plain-12 @@ -2673,7 +2650,7 @@ label="Already implemented for tagged structures, should not be too hard to make it work for graphs" layerID="1" created="1479389260693" x="1793.6375" y="790.74475" width="338.0" height="38.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #F2AE45 + #FEFD8C #776D6D #000000 SansSerif-plain-12 @@ -3484,9 +3461,9 @@ 512 + label="Problem: how do we make the field accessors "hyb id", i.e. working both on fixed records and flex records? We don't want nested field accesses to build up a tower of U types, which makes acceesses very costly for the typechecker" + layerID="1" created="1482936685798" x="3909.6375" y="310.24475" + width="454.0" height="68.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> #FC938D #776D6D #000000 @@ -3494,21 +3471,22 @@ http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a19adbd4d - + #404040 #404040 SansSerif-plain-12 http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a0c6770e9 - - + + 512 514 #FFC63B #776D6D @@ -3517,25 +3495,216 @@ http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a0944806f - #404040 #404040 SansSerif-plain-12 http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a1c61af46 - - + + 514 517 + + #FC938D + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86a7563260a + + + + #404040 + #404040 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86a3bbe533b + + + 512 + 519 + + + #FFC63B + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86afd00a858 + + + + #404040 + #404040 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86ae4487e0b + + + 519 + 521 + + + #FFC63B + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86a297e96f8 + + + + #404040 + #404040 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86ae98942d0 + + + 510 + 523 + + + #FC938D + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86a64c609f2 + + + + #404040 + #404040 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86ac3110955 + + + 523 + 525 + + + #FEFD8C + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4c0c7efe534430712734d86a6143bf3b + + + + #404040 + #404040 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4c0c7efe534430712734d86a20138645 + + + 523 + 528 + + + #404040 + #404040 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4c0c7efe534430712734d86a22d85a28 + + + 525 + 528 + + + #F2AE45 + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/6dbf6b00c0a80026548592b8a0766ac6 + + + + #404040 + #404040 + SansSerif-plain-11 + http://vue.tufts.edu/rdf/resource/4c709721534430712734d86a3c298a33 + + + 7 + 9 + + + #404040 + #404040 + SansSerif-plain-11 + http://vue.tufts.edu/rdf/resource/4c7aa01c534430712734d86a674135d7 + + + 90 + 103 + + + #F2AE45 + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/4c7aa01c534430712734d86af85a0d62 + + + + #404040 + #404040 + SansSerif-plain-11 + http://vue.tufts.edu/rdf/resource/4c7aa01c534430712734d86aedc8c725 + + + 103 + 535 + http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2 1.0 - + #FFFFFF (if (= i 1) - replacement-thunk + #'(delay/pure/stateless replacement) (let* ([bits (to-bits i)] [next (from-bits (cons #t (cddr bits)))] [mod (cadr bits)]) - (define/with-syntax next-id (vector-ref names (sub1 next))) + (define/with-syntax next-id (vector-ref low-names (sub1 next))) (if mod #`(delay/pure/stateless - (let ([tree (force tree-thunk)]) - (let ([left-subtree (car tree)] - [right-subtree (cdr tree)]) - (cons left-subtree - (force (next-id (delay/pure/stateless right-subtree) - . replacement?)))))) + (let ([tree (force tree-thunk)]) + (let ([left-subtree (car tree)] + [right-subtree (cdr tree)]) + (cons left-subtree + (force (next-id (delay/pure/stateless right-subtree) + . replacement?)))))) #`(delay/pure/stateless - (let ([tree (force tree-thunk)]) - (let ([left-subtree (car tree)] - [right-subtree (cdr tree)]) - (cons (force (next-id (delay/pure/stateless left-subtree) - . replacement?)) - right-subtree)))))))] + (let ([tree (force tree-thunk)]) + (let ([left-subtree (car tree)] + [right-subtree (cdr tree)]) + (cons (force (next-id (delay/pure/stateless left-subtree) + . replacement?)) + right-subtree)))))))] @CHUNK[ - (define-for-syntax (define-replace-in-tree names τ* i depth) + (define-for-syntax (define-replace-in-tree low-names names rm-names τ* i depth) (define/with-syntax name (vector-ref names (sub1 i))) + (define/with-syntax rm-name (vector-ref rm-names (sub1 i))) + (define/with-syntax low-name (vector-ref low-names (sub1 i))) + (define/with-syntax tree-type-with-replacement-name (gensym 'tree-type-with-replacement)) (define/with-syntax replacement? #'(replacement)) (define τ*-limited (take τ* depth)) #`(begin - (provide name) - (: name + (provide name rm-name) + (define-type (tree-type-with-replacement-name #,@τ*-limited T) + (Promise #,(tree-type-with-replacement i #'T τ*-limited))) + (: low-name (∀ (#,@τ*-limited T) - (→ (Promise #,(tree-type-with-replacement i #'Any τ*-limited)) + (→ (tree-type-with-replacement-name #,@τ*-limited Any) T - (Promise #,(tree-type-with-replacement i #'(Some T) τ*-limited))))) + (tree-type-with-replacement-name #,@τ*-limited T)))) (define-pure/stateless #:∀ (#,@τ*-limited T) - (name [tree-thunk : (Promise #,(tree-type-with-replacement i #'Any τ*-limited))] + (low-name [tree-thunk : (tree-type-with-replacement-name #,@τ*-limited Any)] + [replacement : T]) + : (Promise #,(tree-type-with-replacement i #'T τ*-limited)) + #,) + + (: name + (∀ (#,@τ*-limited T) + (→ (tree-type-with-replacement-name #,@τ*-limited Any) + T + (tree-type-with-replacement-name #,@τ*-limited (Some T))))) + (define (name tree-thunk replacement) + (low-name tree-thunk (Some replacement))) + #;(define-pure/stateless + #:∀ (#,@τ*-limited T) + (name [tree-thunk : (tree-type-with-replacement-name #,@τ*-limited Any)] [replacement : T]) - : (Promise #,(tree-type-with-replacement i #'(Some T) τ*-limited)) - #,(let ([replacement-thunk #'(delay/pure/stateless (Some replacement))]) - ))))] + (low-name tree-thunk (Some replacement))) + + (: rm-name + (∀ (#,@τ*-limited) + (→ (tree-type-with-replacement-name #,@τ*-limited (Some Any)) + (tree-type-with-replacement-name #,@τ*-limited 'NONE)))) + (define (rm-name tree-thunk) + (low-name tree-thunk 'NONE)) + #;(define-pure/stateless + #:∀ (#,@τ*-limited) + (rm-name [tree-thunk : (tree-type-with-replacement-name #,@τ*-limited (Some Any))]) + (low-name tree-thunk 'NONE))))] @subsection{Removing fields} @@ -126,7 +154,12 @@ fields: (append (map (λ (i) (format-id #'here "-without-~a" i)) i*-above) (stx-map (λ (f) (format-id f "without-~a" f)) - #'(field …)))))] + #'(field …))))) + (define low-names (list->vector + (append (map (λ (i) (format-id #'here "-u-with-~a" i)) + i*-above) + (stx-map (λ (f) (format-id f "u-with-~a" f)) + #'(field …)))))] @section{Type of a tree-record} @@ -190,7 +223,7 @@ fields: all-fields))))) (define (fields→tree-name field …) (delay/pure/stateless - #,(convert-fields (* offset 2) fields+indices))) + #,(convert-fields (* offset 2) fields+indices))) (: tree→fields-name (∀ (field …) (→ (Promise #,(τ-tree-with-fields #'(field …) @@ -265,7 +298,7 @@ interesting subparts of the trees (those where there are fields). @section{Defining the converters and accessors for each known record type} -@chunk[ +@CHUNK[ (define-for-syntax (define-trees stx) (syntax-case stx () [(bt-fields-id (field …) [struct struct-field …] …) @@ -276,17 +309,22 @@ interesting subparts of the trees (those where there are fields). (define total-nb-functions (vector-length names)) )]))] +@CHUNK[ + (define-for-syntax (bt-fields-type fields) + (λ (stx) + (syntax-case stx () + [(_ . fs) + #`(∀ fs (Promise #,(τ-tree-with-fields #'fs + fields)))])))] + @CHUNK[ #`(begin - (define-type-expander (bt-fields-id stx) - (syntax-case stx () - [(_ . fs) - #`(∀ fs (Promise #,(τ-tree-with-fields #'fs - #'(field …))))])) - #,@(map #λ(define-replace-in-tree names ∀-types % (floor-log2 %)) - (range 1 (add1 total-nb-functions))) - #,@(map #λ(define-remove-in-tree rm-names ∀-types % (floor-log2 %)) + (define-type-expander bt-fields-id + (bt-fields-type #'#,(syntax-local-introduce #'(field …)))) + #,@(map #λ(define-replace-in-tree low-names names rm-names ∀-types % (floor-log2 %)) (range 1 (add1 total-nb-functions))) + #;#,@(map #λ(define-remove-in-tree rm-names ∀-types % (floor-log2 %)) + (range 1 (add1 total-nb-functions))) #,@(map #λ(define-struct↔tree offset all-fields ∀-types %1 %2) (syntax->list #'(struct …)) @@ -320,11 +358,12 @@ interesting subparts of the trees (those where there are fields). - + ; <τ-tree-with-fields> - ] + + ] @include-section[(submod "flexible-with-utils.hl.rkt" doc)] \ No newline at end of file diff --git a/invariants-phantom.hl.rkt b/invariants-phantom.hl.rkt new file mode 100644 index 0000000..b9b0a9d --- /dev/null +++ b/invariants-phantom.hl.rkt @@ -0,0 +1,98 @@ +#lang aful/unhygienic hyper-literate type-expander/lang + +@title[#;#:style #;(with-html5 manual-doc-style) + #:tag "invariants-phantom" + #:tag-prefix "phc-graph/invariants-phantom"]{Tracking checked contracts + via phantom types} + +@(chunks-toc-prefix + '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" + "phc-graph/invariants-phantom")) + +@section{Overview} + +The cautious compiler writer will no doubt want to check that the graph used +to represent the program verifies some structural properties. For example, the +compiled language might not allow cycles between types. Another desirable +property is that the @racket[in-method] field of an instruction points back to +the method containing it. We will use this second property as a running +example in this section. + +It is possible to express with Typed/Racket that a @racket[Method] should +contain a list of @racket[Instruction]s, and that @racket[Instruction]s should +point to a @racket[Method]@note{We are not concerned here about the ability to + create such values, which necessarily contain some form of cycle. The goal of + the graph library is indeed to handle the creation and traversal of such + cyclic data structures in a safe way}: + +@chunk[ + (struct Instruction ([opcode : Byte] + [in-method : Method])) + (struct Method ([body : (Listof Instruction)]))] + +This type does not, however, encode the fact that an instruction should point +to the method containing it. Typed/Racket does not really have a notion of +singleton types, aside from symbols and other primitive data. It also lacks a +way to type "the value itself" (e.g. to describe a single-field structure +pointing to itself, possibly via a @racket[Promise]). This means that the +property could only be expressed in a rather contrived way, if it is at all +possible. + +@; (define-type Self-Loop (∀ (A) (→ (Pairof Integer (Self-Loop A))))) + +We decide to rely instead on a run-time check, i.e. a sort of contract which +checks the structural invariant on the whole graph. In order to let the +type-checker know whether a value was checked against that contract or not, we +include within the node a phantom type which is used as a flag, indicating +that the graph was checked against that contract. + +@chunk[ + (struct (Flag) Instruction ([opcode : Byte] + [in-method : (Method Flag)])) + (struct (Flag) Method ([body : (Listof (Instruction Flag))]))] + +We would then write a function accepting a @racket[Method] for which the +contract @racket[method→instruction→same-method] was checked like this: + +@chunk[ + (λ ([m : (Method 'method→instruction→same-method)]) + …)] + +Unfortunately, this attempt fails to catch errors as one would expect, because +Typed/Racket discards unused polymorphic arguments, as can be seen in the +following example, which type-checks without any complaint: + +@chunk[ + (struct (Phantom) S ([x : Integer])) + (define inst-sa : (S 'a) (S 1)) + (ann inst-sa (S 'b))] + +We must therefore make a field with the @racket[Flag] type actually appear +within the instance: + +@chunk[ + (struct (Flag) Instruction ([opcode : Byte] + [in-method : (Method Flag)] + [flag : Flag])) + (struct (Flag) Method ([body : (Listof (Instruction Flag))] + [flag : Flag]))] + +Another issue is that the flag can easily be forged. We would therefore like +to wrap it in a struct type which is only accessible by the graph library: + +@chunk[ + (struct (Flag) Flag-Wrapper-Struct ([flag : Flag])) + (define-type Flag-Wrapper Flag-Wrapper-Struct) + (code:comment "provide only the type, not the constructor or accessor") + (provide Flag-Wrapper)] + +@; size → use a dummy function which errors when called +@; (accepts an opaque token to prevent calling) + +@; Subtyping: multiple contracts with case→ + +@; Subtyping: when C1 ⇒ C2, +@; make the marker for C1 a subtype of the marker for C2 + +@chunk[<*> + (void)] \ No newline at end of file diff --git a/scribblings/phc-graph-implementation.scrbl b/scribblings/phc-graph-implementation.scrbl index 5a4a309..fd383dd 100644 --- a/scribblings/phc-graph-implementation.scrbl +++ b/scribblings/phc-graph-implementation.scrbl @@ -12,4 +12,5 @@ the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document. @(table-of-contents) @include-section[(submod "../traversal.hl.rkt" doc)] -@include-section[(submod "../flexible-with.hl.rkt" doc)] \ No newline at end of file +@include-section[(submod "../flexible-with.hl.rkt" doc)] +@include-section[(submod "../invariants-phantom.hl.rkt" doc)] \ No newline at end of file diff --git a/test/test-flexible-with.rkt b/test/test-flexible-with.rkt index 8799d78..2938bb6 100644 --- a/test/test-flexible-with.rkt +++ b/test/test-flexible-with.rkt @@ -5,7 +5,8 @@ racket/list (rename-in racket/base [... …])) phc-toolkit - typed-map) + typed-map + type-expander) (define-syntax (gs stx) (syntax-case stx () @@ -21,12 +22,16 @@ [struct struct-field …] …)))])) (gs bt-fields - 16 + 512 (a b c) [sab a b] [sbc b c] [sabc a b c]) +;(define-type btac (bt-fields a c)) + +#| + (check-equal?: (~> (ann (with-c (sab→tree 1 2) 'nine) ((bt-fields a b c) One Positive-Byte 'nine)) @@ -73,4 +78,5 @@ (call-with-values #λ(tree→sbc (without-a (with-c (sab→tree 1 2) 3))) list) - '(2 3)) \ No newline at end of file + '(2 3)) +|# \ No newline at end of file diff --git a/times.rkt b/times.rkt new file mode 100644 index 0000000..398f2b0 --- /dev/null +++ b/times.rkt @@ -0,0 +1,58 @@ +#lang racket +(require plot) +(parameterize ([plot-x-transform log-transform] + [plot-x-ticks (log-ticks #:base 2)] + [plot-y-transform log-transform] + [plot-y-ticks (log-ticks #:base 2)]) + (plot + #:x-min 1 #:x-max 3000 + #:y-min 1 #:y-max 3000 + (points '(#(16 16) + #(17 25) + #(20 26) + #(24 29) + #(28 31) + #(32 35) ;; 20 with shared implementation & type, 22 shrd impl only + #(33 60) + #(40 67) + #(48 77) + #(56 80) + #(64 92) ;; 46 + #(65 168) + #(80 189) + #(96 216) + #(128 276) + #(129 562) + #(256 911) + #(257 2078) + #(512 3000) ;; rough estimation + )))) + +;; with shared implementation & type: +(parameterize ([plot-x-transform log-transform] + [plot-x-ticks (log-ticks #:base 2)] + [plot-y-transform log-transform] + [plot-y-ticks (log-ticks #:base 2)]) + (plot + #:x-min 1 #:x-max 600 + #:y-min 1 #:y-max 600 + (points '(#(16 11) + ;#(17 25) + ;#(20 26) + ;#(24 29) + ;#(28 31) + #(32 20) + ;#(33 60) + ;#(40 67) + ;#(48 77) + ;#(56 80) + #(64 46) + ;#(65 168) + ;#(80 189) + ;#(96 216) + #(128 120) + ;#(129 562) + #(256 363) + ;#(257 2078) + ;#(512 3000) ;; rough estimation + )))) \ No newline at end of file