diff --git a/flexible-with2.hl.rkt b/flexible-with2.hl.rkt index f137ed4..ae5b423 100644 --- 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[ +꩜CHUNK[ (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[ +꩜CHUNK[ (if (= i 1) #'(delay/pure/stateless replacement) (let* ([bits (to-bits i)] @@ -106,7 +111,7 @@ with a new one. tree-thunk replacement))))] -♦CHUNK[ +꩜CHUNK[ (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[ +꩜CHUNK[ (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[ +꩜CHUNK[ (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[ +꩜CHUNK[ (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[ +꩜CHUNK[ (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[ +꩜CHUNK[ (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)) )]))] -♦CHUNK[ +꩜CHUNK[ (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[ +꩜CHUNK[ #`(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[ +꩜chunk[ (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). ] -♦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