commit cfbcbafe922f8f763536a46586c54bd93820e8b5
parent d211bd115429deb37c49a2c7f1e3f191641727fc
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Sat, 20 May 2017 15:22:39 +0200
Switched to ꩜ character, fixed a typo
Diffstat:
| M | flexible-with2.hl.rkt | | | 91 | ++++++++++++++++++++++++++++++++++++++++++------------------------------------- |
1 file changed, 48 insertions(+), 43 deletions(-)
diff --git a/flexible-with2.hl.rkt b/flexible-with2.hl.rkt
@@ -1,25 +1,27 @@
-#lang hyper-literate #:♦ (dotlambda/unhygienic . type-expander/lang)
+#lang hyper-literate #:꩜ (dotlambda/unhygienic . type-expander/lang)
-♦title[#:style manual-doc-style ;#:style (with-html5 manual-doc-style)
+꩜title[#:style manual-doc-style ;#:style (with-html5 manual-doc-style)
#:tag "flexible-with"
#:tag-prefix "phc-graph/flexible-with"]{Flexible functional
modification and extension of records}
-♦(chunks-toc-prefix
+꩜(chunks-toc-prefix
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
"phc-graph/flexible-with"))
-♦section{Goals}
+꩜require[scriblib/footnote]
+
+꩜section{Goals}
Our goal here is to have strongly typed records, with row polymorphism (a
-♦racket[Rest] row type variable can range over multiple possibly-present
+꩜racket[Rest] row type variable can range over multiple possibly-present
fields), and structural type equivalence (two record types are identical if
they have the same fields and the type of the fields is the same in both record
types).
-♦section{Overview}
+꩜section{Overview}
-We represent flexible records using a tree, where the leaves are field values.
+We represent a flexible record as a tree, where the leaves are field values.
Every field which occurs anywhere in the program is assigned a constant index.
This index determines which leaf is used to store that field's values. In
order to avoid storing in-memory a huge tree for every record, the actual
@@ -28,8 +30,11 @@ node) upon access.
The type for a flexible record can support row polymorphism: the type of
fields which may optionally be present are represented by a polymorphic type
-variable. Note that this means that no only one row type variable is used, but
-several. We define below facilities to automatically generate this list of
+variable. Note that this means that not only one type variable is used, but
+several꩜note{In principle, each potentially-present field would need a
+ distinct type variable, but whole potentially-present branches may be
+ collapsed to a single type variable if no access is made to the variables
+ within.}. We define below facilities to automatically generate this list of
polymorphic type variables. In order to avoid having a huge number of type
variables, a branch containing only optional fields can be collapsed into a
single type variable. An exception to this rule is when a field needs to be
@@ -60,9 +65,9 @@ not be collapsed.
-♦section{Type of a tree-record, with a hole}
+꩜section{Type of a tree-record, with a hole}
-♦CHUNK[<tree-type-with-replacement>
+꩜CHUNK[<tree-type-with-replacement>
(define-for-syntax (tree-type-with-replacement n last τ*)
(define-values (next mod) (quotient/remainder n 2))
(cond [(null? τ*) last]
@@ -75,23 +80,23 @@ not be collapsed.
#`(Pairof #,(car τ*) #,last)
(cdr τ*))]))]
-♦section{Functionally updating a tree-record}
+꩜section{Functionally updating a tree-record}
-♦subsection{Adding and modifying fields}
+꩜subsection{Adding and modifying fields}
Since we only deal with functional updates of immutable records, modifying a
field does little more than discarding the old value, and injecting the new
value instead into the new, updated record.
Adding a new field is done using the same exact operation: missing fields are
-denoted by a special value, ♦racket['NONE], while present fields are
-represented as instances of the polymorphic struct ♦racket[(Some T)]. Adding a
-new field is therefore as simple as discarding the old ♦racket['NONE] marker,
-and replacing it with the new value, wrapped with ♦racket[Some]. A field
-update would instead discard the old instance of ♦racket[Some], and replace it
+denoted by a special value, ꩜racket['NONE], while present fields are
+represented as instances of the polymorphic struct ꩜racket[(Some T)]. Adding a
+new field is therefore as simple as discarding the old ꩜racket['NONE] marker,
+and replacing it with the new value, wrapped with ꩜racket[Some]. A field
+update would instead discard the old instance of ꩜racket[Some], and replace it
with a new one.
-♦CHUNK[<make-replace-in-tree-body>
+꩜CHUNK[<make-replace-in-tree-body>
(if (= i 1)
#'(delay/pure/stateless replacement)
(let* ([bits (to-bits i)]
@@ -106,7 +111,7 @@ with a new one.
tree-thunk
replacement))))]
-♦CHUNK[<define-replace-in-tree>
+꩜CHUNK[<define-replace-in-tree>
(define-pure/stateless
(: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C))
(Promise (Pairof A B))
@@ -125,11 +130,11 @@ with a new one.
(force (next-id (delay/pure/stateless right-subtree)
replacement))))))))
(define-pure/stateless
+ (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C))
+ (Promise (Pairof A B))
+ R
+ (Promise (Pairof C B)))))
(define
- (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C))
- (Promise (Pairof A B))
- R
- (Promise (Pairof C B)))))
#:∀ (A B C R)
(replace-left [next-id : (→ (Promise A) R (Promise C))]
[tree-thunk : (Promise (Pairof A B))]
@@ -185,12 +190,12 @@ with a new one.
(define (rm-name tree-thunk)
(low-name tree-thunk 'NONE))))]
-♦section{Auxiliary values}
+꩜section{Auxiliary values}
The following sections reuse a few values which are derived from the list of
fields:
-♦CHUNK[<utils>
+꩜CHUNK[<utils>
(define all-fields #'(field …))
(define depth-above (ceiling-log2 (length (syntax->list #'(field …)))))
(define offset (expt 2 depth-above))
@@ -211,9 +216,9 @@ fields:
(stx-map (λ (f) (format-id f "u-with-~a" f))
#'(field …)))))]
-♦section{Type of a tree-record}
+꩜section{Type of a tree-record}
-♦CHUNK[<τ-tree-with-fields>
+꩜CHUNK[<τ-tree-with-fields>
(define-for-syntax (τ-tree-with-fields struct-fields fields)
(define/with-syntax (struct-field …) struct-fields)
(define/with-syntax (field …) fields)
@@ -246,9 +251,9 @@ fields:
,(f (add1 (* i 2))))))))
(f 1))]
-♦section{Conversion to and from record-trees}
+꩜section{Conversion to and from record-trees}
-♦CHUNK[<define-struct↔tree>
+꩜CHUNK[<define-struct↔tree>
(define-for-syntax (define-struct↔tree
offset all-fields τ* struct-name fields)
(define/with-syntax (field …) fields)
@@ -283,9 +288,9 @@ fields:
(define tree (force tree-thunk))
#,(convert-back-fields (* offset 2) fields+indices))))]
-♦subsection{Creating a new tree-record}
+꩜subsection{Creating a new tree-record}
-♦CHUNK[<convert-fields>
+꩜CHUNK[<convert-fields>
(define-for-syntax (convert-fields up fields+indices)
;(displayln fields+indices)
(define (f i)
@@ -302,12 +307,12 @@ fields:
(f 1))]
-♦subsection{Extracting all the fields from a tree-record}
+꩜subsection{Extracting all the fields from a tree-record}
We traverse the tree in preorder, and accumulate definitions naming the
interesting subparts of the trees (those where there are fields).
-♦CHUNK[<convert-back-fields>
+꩜CHUNK[<convert-back-fields>
(define-for-syntax (convert-back-fields up fields+indices)
(define result '())
(define definitions '())
@@ -346,9 +351,9 @@ interesting subparts of the trees (those where there are fields).
(f 1 #'tree)
#`(begin #,@definitions (values . #,(reverse result))))]
-♦section{Defining the converters and accessors for each known record type}
+꩜section{Defining the converters and accessors for each known record type}
-♦CHUNK[<define-trees>
+꩜CHUNK[<define-trees>
(define-for-syntax (define-trees stx)
(syntax-case stx ()
[(bt-fields-id (field …) [struct struct-field …] …)
@@ -359,7 +364,7 @@ interesting subparts of the trees (those where there are fields).
(define total-nb-functions (vector-length names))
<define-trees-result>)]))]
-♦CHUNK[<bt-fields-type>
+꩜CHUNK[<bt-fields-type>
(define-for-syntax (bt-fields-type fields)
(λ (stx)
(syntax-case stx ()
@@ -367,7 +372,7 @@ interesting subparts of the trees (those where there are fields).
#`(∀ fs (Promise #,(τ-tree-with-fields #'fs
fields)))])))]
-♦CHUNK[<define-trees-result>
+꩜CHUNK[<define-trees-result>
#`(begin
(define-type-expander bt-fields-id
(bt-fields-type #'#,(syntax-local-introduce #'(field …))))
@@ -381,13 +386,13 @@ interesting subparts of the trees (those where there are fields).
(syntax->list #'(struct …))
(syntax->list #'([struct-field …] …))))]
-♦subsection{Putting it all together}
+꩜subsection{Putting it all together}
-♦chunk[<maybe>
+꩜chunk[<maybe>
(struct (T) Some ([v : T]) #:transparent)
(define-type (Maybe T) (U (Some T) 'NONE))]
-♦chunk[<*>
+꩜chunk[<*>
(require delay-pure
"flexible-with-utils.hl.rkt"
(for-syntax (rename-in racket/base [... …])
@@ -417,4 +422,4 @@ interesting subparts of the trees (those where there are fields).
<define-trees>
<bt-fields-type>]
-♦include-section[(submod "flexible-with-utils.hl.rkt" doc)]
-\ No newline at end of file
+꩜include-section[(submod "flexible-with-utils.hl.rkt" doc)]
+\ No newline at end of file
