Writeup
This commit is contained in:
Georges Dupéron
parent
63e1a77ef1
commit
e3074a37e4
|
|
@ -30,76 +30,71 @@
|
||||||
'none))
|
'none))
|
||||||
|#
|
|#
|
||||||
|
|
||||||
(struct (A) Some ([f : A]) #:transparent)
|
|
||||||
(struct (A) Some0 Some () #:transparent)
|
|
||||||
(struct (A) Some1 Some () #:transparent)
|
|
||||||
(struct (A) Some2 Some () #:transparent)
|
|
||||||
(struct (A) Some3 Some () #:transparent)
|
|
||||||
(struct (A) None ([f : A]) #:transparent)
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;; Actual good implementation:
|
||||||
|
|
||||||
|
;(struct (A) Some ([f : A]) #:transparent)
|
||||||
|
;(struct (A) Some0 Some () #:transparent)
|
||||||
|
;(struct (A) Some1 Some () #:transparent)
|
||||||
|
;(struct (A) Some2 Some () #:transparent)
|
||||||
|
;(struct (A) Some3 Some () #:transparent)
|
||||||
|
;(struct (A) None ([f : A]) #:transparent)
|
||||||
|
|
||||||
;; A is:
|
;; A is:
|
||||||
#;(U (Pairof Any (None (Listof (Some Any))))
|
#;(Pairof Any (U (Some Any) (None (Listof Any))))
|
||||||
(Some Any))
|
|
||||||
|
|
||||||
(struct |0| ())
|
(: f (builder-τ 4 2))
|
||||||
(struct |1| ())
|
|
||||||
(struct |2| ())
|
|
||||||
(struct |3| ())
|
|
||||||
|
|
||||||
(: f (∀ (A 0/K 0/X 1/K 1/X)
|
(define (f oracle kx x ky y)
|
||||||
(→ (∩ 0/K (U |0| |1| |2| |3|))
|
|
||||||
0/X
|
|
||||||
(∩ 1/K (U |0| |1| |2| |3|))
|
|
||||||
1/X
|
|
||||||
(List
|
|
||||||
(∩
|
|
||||||
(U
|
|
||||||
(Pairof |0| (None (List (∩ 0/K (U |1| |2| |3|)) (∩ 1/K (U |1| |2| |3|)))))
|
|
||||||
(∩ (Pairof 0/K (Some 0/X)) (Pairof |0| Any))
|
|
||||||
(∩ (Pairof 1/K (Some 1/X)) (Pairof |0| Any)))
|
|
||||||
A)
|
|
||||||
(∩
|
|
||||||
(U
|
|
||||||
(Pairof |1| (None (List (∩ 0/K (U |0| |2| |3|)) (∩ 1/K (U |0| |2| |3|)))))
|
|
||||||
(∩ (Pairof 0/K (Some 0/X)) (Pairof |1| Any))
|
|
||||||
(∩ (Pairof 1/K (Some 1/X)) (Pairof |1| Any)))
|
|
||||||
A)
|
|
||||||
(∩
|
|
||||||
(U
|
|
||||||
(Pairof |2| (None (List (∩ 0/K (U |0| |1| |3|)) (∩ 1/K (U |0| |1| |3|)))))
|
|
||||||
(∩ (Pairof 0/K (Some 0/X)) (Pairof |2| Any))
|
|
||||||
(∩ (Pairof 1/K (Some 1/X)) (Pairof |2| Any)))
|
|
||||||
A)
|
|
||||||
(∩
|
|
||||||
(U
|
|
||||||
(Pairof |3| (None (List (∩ 0/K (U |0| |1| |2|)) (∩ 1/K (U |0| |1| |2|)))))
|
|
||||||
(∩ (Pairof 0/K (Some 0/X)) (Pairof |3| Any))
|
|
||||||
(∩ (Pairof 1/K (Some 1/X)) (Pairof |3| Any)))
|
|
||||||
A)))))
|
|
||||||
|
|
||||||
(define (f kx x ky y)
|
|
||||||
(list (cond
|
(list (cond
|
||||||
[((make-predicate |0|) kx) (cons kx (Some x))]
|
[((make-predicate '|0|) kx)
|
||||||
[((make-predicate |0|) ky) (cons ky (Some y))]
|
(ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|0| Any))) (cons kx (Some x)))
|
||||||
[else (cons |0| (None (list kx ky)))])
|
(∩ (Pairof 0/K (Some 0/X)) (Pairof '|0| Any) A))]
|
||||||
|
[((make-predicate '|0|) ky)
|
||||||
|
(ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|0| Any))) (cons ky (Some y)))
|
||||||
|
(∩ (Pairof 1/K (Some 1/X)) (Pairof '|0| Any) A))]
|
||||||
|
[else
|
||||||
|
((inst oracle (Pairof '|0| (None (List (∩ 0/K (U '|1| '|2| '|3|)) (∩ 1/K (U '|1| '|2| '|3|))))))
|
||||||
|
(cons '|0| (None (list kx ky))))])
|
||||||
(cond
|
(cond
|
||||||
[((make-predicate |1|) kx) (cons kx (Some x))]
|
[((make-predicate '|1|) kx)
|
||||||
[((make-predicate |1|) ky) (cons ky (Some y))]
|
(ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|1| Any))) (cons kx (Some x)))
|
||||||
[else (cons |1| (None (list kx ky)))])
|
(∩ (Pairof 0/K (Some 0/X)) (Pairof '|1| Any) A))]
|
||||||
|
[((make-predicate '|1|) ky)
|
||||||
|
(ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|1| Any))) (cons ky (Some y)))
|
||||||
|
(∩ (Pairof 1/K (Some 1/X)) (Pairof '|1| Any) A))]
|
||||||
|
[else
|
||||||
|
((inst oracle (Pairof '|1| (None (List (∩ 0/K (U '|0| '|2| '|3|)) (∩ 1/K (U '|0| '|2| '|3|))))))
|
||||||
|
(cons '|1| (None (list kx ky))))])
|
||||||
(cond
|
(cond
|
||||||
[((make-predicate |2|) kx) (cons kx (Some x))]
|
[((make-predicate '|2|) kx)
|
||||||
[((make-predicate |2|) ky) (cons ky (Some y))]
|
(ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|2| Any))) (cons kx (Some x)))
|
||||||
[else (cons |2| (None (list kx ky)))])
|
(∩ (Pairof 0/K (Some 0/X)) (Pairof '|2| Any) A))]
|
||||||
|
[((make-predicate '|2|) ky)
|
||||||
|
(ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|2| Any))) (cons ky (Some y)))
|
||||||
|
(∩ (Pairof 1/K (Some 1/X)) (Pairof '|2| Any) A))]
|
||||||
|
[else
|
||||||
|
((inst oracle (Pairof '|2| (None (List (∩ 0/K (U '|0| '|1| '|3|)) (∩ 1/K (U '|0| '|1| '|3|))))))
|
||||||
|
(cons '|2| (None (list kx ky))))])
|
||||||
(cond
|
(cond
|
||||||
[((make-predicate |3|) kx) (cons kx (Some x))]
|
[((make-predicate '|3|) kx)
|
||||||
[((make-predicate |3|) ky) (cons ky (Some y))]
|
(ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|3| Any))) (cons kx (Some x)))
|
||||||
[else (cons |3| (None (list kx ky)))]))
|
(∩ (Pairof 0/K (Some 0/X)) (Pairof '|3| Any) A))]
|
||||||
((λ () (error "not yet"))))
|
[((make-predicate '|3|) ky)
|
||||||
|
(ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|3| Any))) (cons ky (Some y)))
|
||||||
|
(∩ (Pairof 1/K (Some 1/X)) (Pairof '|3| Any) A))]
|
||||||
|
[else
|
||||||
|
((inst oracle (Pairof '|3| (None (List (∩ 0/K (U '|0| '|1| '|2|)) (∩ 1/K (U '|0| '|1| '|2|))))))
|
||||||
|
(cons '|3| (None (list kx ky))))])))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,101 +1,230 @@
|
||||||
#lang dotlambda/unhygienic type-expander/lang
|
#lang hyper-literate #:꩜ #:no-auto-require (dotlambda/unhygienic
|
||||||
#|hyper-literate #:♦ #:no-auto-require (dotlambda/unhygienic
|
|
||||||
. type-expander/lang)
|
. type-expander/lang)
|
||||||
|
|
||||||
♦chunk[<*>|#
|
꩜title[#:tag "generalized-flex-ctor"]{Generalised constructor functions for
|
||||||
|
flexible structures}
|
||||||
(provide builder-τ
|
|
||||||
None
|
|
||||||
Some
|
|
||||||
Some?
|
|
||||||
Some-f
|
|
||||||
propagate-τ)
|
|
||||||
|
|
||||||
(require racket/require
|
꩜(require hyper-literate/diff1)
|
||||||
(for-syntax (subtract-in racket/base subtemplate/override)
|
꩜(init)
|
||||||
syntax/stx
|
|
||||||
racket/list
|
|
||||||
racket/function
|
|
||||||
subtemplate/override)
|
|
||||||
(for-meta 2 racket/base))
|
|
||||||
|
|
||||||
(struct (T) Some ([f : T]))
|
꩜chunk[<*>
|
||||||
(struct (T) None ([f : T]))
|
(provide builder-τ
|
||||||
|
None
|
||||||
|
Some
|
||||||
|
Some?
|
||||||
|
Some-f
|
||||||
|
propagate-τ)
|
||||||
|
|
||||||
(define-type-expander BinaryTree
|
(require racket/require
|
||||||
(syntax-parser
|
(for-syntax (subtract-in racket/base subtemplate/override)
|
||||||
[(_ leafⱼ …)
|
syntax/stx
|
||||||
;; TODO: implement BinaryTree.
|
racket/list
|
||||||
#'(List leafⱼ …)]))
|
racket/function
|
||||||
|
subtemplate/override)
|
||||||
|
(for-meta 2 racket/base))
|
||||||
|
|
||||||
(define-syntax (def-SomeNone* stx)
|
(struct (T) Some ([f : T]))
|
||||||
(syntax-case stx ()
|
(struct (T) None ([f : T]))
|
||||||
[(_ Some n)
|
|
||||||
(with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i))
|
|
||||||
(range n))])
|
|
||||||
#`(begin
|
|
||||||
(provide Someᵢ …)
|
|
||||||
(struct (T) Someᵢ Some ()) …))]))
|
|
||||||
|
|
||||||
(def-SomeNone* Some 4)
|
(define-type-expander BinaryTree
|
||||||
|
(syntax-parser
|
||||||
|
[(_ leafⱼ …)
|
||||||
|
;; TODO: implement BinaryTree.
|
||||||
|
#'(List leafⱼ …)]))
|
||||||
|
|
||||||
(define-type-expander builder-τ
|
(define-syntax (def-SomeNone* stx)
|
||||||
(syntax-parser
|
(syntax-case stx ()
|
||||||
[(_ n m)
|
[(_ Some n)
|
||||||
#:with (Nᵢ …) (range n)
|
(with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i))
|
||||||
#:with (Mⱼ …) (range m)
|
(range n))])
|
||||||
#:with (Someᵢ …) (map (λ (n) (format-id #'HERE? "Some~a" n)) (Nᵢ …))
|
#`(begin
|
||||||
#:with ((Someᵢⱼ …) …) (map λ.(map (const %) (Mⱼ …)) (#'Someᵢ …))
|
(provide Someᵢ …)
|
||||||
;#:with ((Noneᵢⱼ …) …) (map (const #'(Noneᵢ …)) (Nᵢ …))
|
(struct (T) Someᵢ Some ()) …))]))
|
||||||
#:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …))
|
|
||||||
#:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …))
|
|
||||||
#:with ((Nᵢⱼ …) …) (map (λ (ni) (map (const ni) (Xⱼ …))) (Nᵢ …))
|
|
||||||
#:with ((Nⱼᵢ …) …) (map (const #'(Nᵢ …)) (Mⱼ …))
|
|
||||||
(define Ns (Nᵢ …))
|
|
||||||
(define Ms (Mⱼ …))
|
|
||||||
(define Somes (Someᵢ …))
|
|
||||||
;(define/with-syntax exceptⱼ (remove Mⱼ Ns)) …
|
|
||||||
; (define/with-syntax ((exceptᵢⱼ …) …)
|
|
||||||
; (map (const (exceptⱼ …)) (Nᵢ …)))
|
|
||||||
(define/with-syntax (exceptᵢ …) ((remove Nᵢ Ns) …))
|
|
||||||
(define/with-syntax (((exceptᵢⱼ …) …) …)
|
|
||||||
((map (const (remove Someᵢ Somes)) Ms) …))
|
|
||||||
|
|
||||||
(define/with-syntax result
|
(def-SomeNone* Some 4)
|
||||||
#'(∀ (A (?@ Kⱼ Xⱼ) …)
|
|
||||||
(→ (?@ (∩ Kⱼ (Some Any)) (∩ Kⱼ Xⱼ)) …
|
|
||||||
(BinaryTree
|
|
||||||
(∩ (U (Pairof Nᵢ
|
|
||||||
;; If Kⱼ is Nᵢ, then {∩ Kᵢⱼ {U . exceptᵢⱼ}} will
|
|
||||||
;; Nothing. We multiply the Nothing together by
|
|
||||||
;; building a List out of them (a single occurrence
|
|
||||||
;; of Nothing should collapse the list), so that the
|
|
||||||
;; result should be Nothing only if there is no Kⱼ
|
|
||||||
;; equal to Nᵢ. To force TR to propagate Nothing as
|
|
||||||
;; much as possible, we intersect it with
|
|
||||||
;; (None Any), which should be a no-op, but makes
|
|
||||||
;; sure the simplifier which runs with ∩ kicks in.
|
|
||||||
;; Therefore, the (None whatever) should appear only
|
|
||||||
;; if there is indeed no key provided for that leaf.
|
|
||||||
(None (List {∩ Kᵢⱼ {U (exceptᵢⱼ Any) …}} …)))
|
|
||||||
(∩ Kᵢⱼ (Someᵢⱼ Xᵢⱼ))
|
|
||||||
…)
|
|
||||||
A)
|
|
||||||
…))))
|
|
||||||
(displayln (syntax->datum #'result))
|
|
||||||
#'result]))
|
|
||||||
|
|
||||||
(define-type propagate-τ
|
<builder-τ>
|
||||||
(Pairof Any
|
|
||||||
(U (None (Listof Natural))
|
|
||||||
(Some Any))))
|
|
||||||
|
|
||||||
; ../../../.racket/snapshot/pkgs/typed-racket-lib/typed-racket/types/overlap.rkt
|
<propagate-τ>]
|
||||||
;:40:0: mask-accessor: contract violation
|
|
||||||
; expected: mask?
|
We first define the builder function's type. Since this type is rather
|
||||||
; given: #f
|
complex, we define it using a macro. The type expander takes two arguments.
|
||||||
;(define-type τ-4-2 (builder-τ 4 2))
|
The first argument ꩜racket[n] indicates the total number of fields which
|
||||||
|
appear in the program (i.e. on the number of leaves of the generated tree
|
||||||
|
type), and the second argument ꩜racket[m] indicates how many key/value pairs
|
||||||
|
the function accepts.
|
||||||
|
|
||||||
|
꩜chunk[<builder-τ>
|
||||||
|
(define-type-expander builder-τ
|
||||||
|
(syntax-parser
|
||||||
|
[(_ n m)
|
||||||
|
<builder-τ-with-1>
|
||||||
|
<builder-τ-with-2>
|
||||||
|
<builder-τ-with-3>
|
||||||
|
#'|<builder-function-type''>|]))]
|
||||||
|
|
||||||
|
We start by defining a few syntax pattern variables which will be used in the
|
||||||
|
later definitions. The lists ꩜racket[Nᵢ] and ꩜racket[Mⱼ] range over the field
|
||||||
|
and argument indices, respectively:
|
||||||
|
|
||||||
|
꩜chunk[<builder-τ-with-1>
|
||||||
|
#:with (Nᵢ …) (range n)
|
||||||
|
#:with (Mⱼ …) (range m)]
|
||||||
|
|
||||||
|
The builder function takes a number of keys and values, and builds a (promise
|
||||||
|
for) a binary tree where the leaves corresponding to those keys contain given
|
||||||
|
value, and other leaves contain ꩜racket[None]. We could write (a simplified
|
||||||
|
form of) the builder function type as follows:
|
||||||
|
|
||||||
|
꩜chunk[<builder-function-type>
|
||||||
|
(∀ ({?@ Kⱼ Xⱼ} …)
|
||||||
|
(→ (code:comment "; Keys and values:")
|
||||||
|
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||||
|
;; Result type:
|
||||||
|
(BinaryTree |<Some or None>| …)))]
|
||||||
|
|
||||||
|
We expect each key ꩜racket[Kⱼ] to be a symbol of the shape ꩜racket[|0|],
|
||||||
|
꩜racket[|1|], ꩜racket[|2|] and so on:
|
||||||
|
|
||||||
|
꩜chunk[<builder-τ-with-2>
|
||||||
|
#:with (NSymᵢ …) ((string->symbol (format "~a" Nᵢ)) …)
|
||||||
|
#:with ((NSymⱼᵢ …) …) (map (const (NSymᵢ …)) (Mⱼ …))]
|
||||||
|
|
||||||
|
The type of each leaf of the binary tree should be ꩜racket[(Some Xⱼ)] if a
|
||||||
|
corresponding ꩜racket[Kⱼ] matches the leaf name, and ꩜racket[None] otherwise.
|
||||||
|
|
||||||
|
꩜chunk[|<Some or None>|
|
||||||
|
(U |<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
||||||
|
|<None if ∀ k ∈ Kⱼ, k ≠ NSymᵢ>|)]
|
||||||
|
|
||||||
|
This type-level conditional is achieved via a trick involving intersection
|
||||||
|
types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one
|
||||||
|
of the ꩜racket['NSymᵢ …] symbols. For a given leaf with index ꩜racket[i], if
|
||||||
|
the ꩜racket[Kⱼ] key is the type ꩜racket['NSymᵢ], then the intersection type
|
||||||
|
꩜racket[(∩ Kⱼ 'NSymᵢ)] is ꩜racket['NSymᵢ]. Conversely, if the ꩜racket[Kⱼ] key
|
||||||
|
is not ꩜racket['NSymᵢ], the intersection will be the bottom type
|
||||||
|
꩜racket[Nothing]. No values inhabit the bottom type, and Typed Racket can
|
||||||
|
determine that there is no pair whose first (or second) element has the type
|
||||||
|
꩜racket[Nothing], since no concrete value could be used to construct such a
|
||||||
|
pair.
|
||||||
|
|
||||||
|
꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
||||||
|
(Pairof (∩ Kᵢⱼ 'NSymᵢⱼ)
|
||||||
|
(Some Xᵢⱼ))
|
||||||
|
…]
|
||||||
|
|
||||||
|
where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows:
|
||||||
|
|
||||||
|
꩜chunk[<builder-τ-with-3>
|
||||||
|
#:with ((Kᵢⱼ …) …) (map (const (Kⱼ …)) (Nᵢ …))
|
||||||
|
#:with ((Xᵢⱼ …) …) (map (const (Xⱼ …)) (Nᵢ …))
|
||||||
|
#:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))]
|
||||||
|
|
||||||
|
We use this fact to construct a pair above. Its first element is either
|
||||||
|
꩜racket['NSymᵢ] when ꩜racket[Kⱼ] is ꩜racket['NSymᵢ], and ꩜racket[Nothing]
|
||||||
|
otherwise. The second element of the pair contains our expected
|
||||||
|
꩜racket[(Some Xⱼ)] type, but the whole pair is collapsed to ꩜racket[Nothing]
|
||||||
|
when ꩜racket[Kⱼ] is not ꩜racket['NSymᵢ].
|
||||||
|
|
||||||
|
We use a similar approach to conditionally produce the ꩜racket[None] element,
|
||||||
|
but instead of intersecting ꩜racket[Kⱼ] with ꩜racket['NSymᵢ], we intersect it
|
||||||
|
with the complement of ꩜racket['NSymᵢ]. Typed Racket lacks the possibility to
|
||||||
|
negate a type, so we manually compute the complement of ꩜racket['NSymᵢ] in the
|
||||||
|
set of possible keys (that is, ꩜racket['NSymᵢ …]).
|
||||||
|
|
||||||
|
꩜chunk[<builder-τ-with-3>
|
||||||
|
#:with NSyms (NSymᵢ …)
|
||||||
|
#:with Ms (Mⱼ …)
|
||||||
|
#:with (exceptᵢ …) ((remove NSymᵢ NSyms) …)
|
||||||
|
#:with (((exceptᵢⱼ …) …) …) ((map (const exceptᵢ) Ms) …)]
|
||||||
|
|
||||||
|
If ꩜racket[Kⱼ] is ꩜racket[Nᵢ], then ꩜racket[{∩ Kⱼ {U . exceptᵢ}}] will be
|
||||||
|
꩜racket[Nothing]. We take the Cartesian product of the intersections by
|
||||||
|
building a ꩜racket[List] out of them. A single occurrence of ꩜racket[Nothing]
|
||||||
|
will collapse the whole list to ꩜racket[Nothing], because the Cartesian
|
||||||
|
product of the empty set and any other set will produce the empty set.
|
||||||
|
|
||||||
|
The resulting type should therefore be ꩜racket[Nothing] only if there is no
|
||||||
|
꩜racket[Kⱼ] equal to ꩜racket[Nᵢ], and be the list of symbols
|
||||||
|
꩜racket[(List . exceptᵢ)] otherwise.
|
||||||
|
|
||||||
|
꩜chunk[|<None if ∀ k ∈ Kⱼ, k ≠ NSymᵢ>|
|
||||||
|
(Pairof 'NSymᵢ
|
||||||
|
(None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …)))]
|
||||||
|
|
||||||
|
This approach relies on the fact that occurrences of ꩜racket[Nothing] within
|
||||||
|
structs and pairs containing collapse the entire struct or pair type to
|
||||||
|
꩜racket[Nothing]. Unfortunately, current versions of Typed Racket perform this
|
||||||
|
simplification step in some situations but not others:
|
||||||
|
|
||||||
|
꩜itemlist[
|
||||||
|
꩜item{It simplifies polymorphic types when they are defined;}
|
||||||
|
꩜item{When a polymorphic type is instantiated, the parts which are directly
|
||||||
|
affected by the intersection with a polymorphic type variable are subject to
|
||||||
|
this simplification;}
|
||||||
|
꩜item{However, occurrences of ꩜racket[Nothing] which occur as a result of
|
||||||
|
instantiating the type variable do not propagate outside of the intersection
|
||||||
|
itself. This means that given the following type:
|
||||||
|
꩜racketblock[(define-type (Foo A) (U (Pairof (∩ Integer A) String) Boolean))]
|
||||||
|
its instantiation ꩜racket[(Foo Symbol)] will produce the type
|
||||||
|
꩜racket[(U (Pairof Nothing String) Boolean)], but this type will not be
|
||||||
|
simplified to ꩜racket[(U Nothing Boolean)] or equivalently to
|
||||||
|
꩜racket[Boolean].}]
|
||||||
|
|
||||||
|
To force Typed Racket to propagate ꩜racket[Nothing] outwards as much as
|
||||||
|
we need, we intersect the whole form with a polymorphic type ꩜racket[A]:
|
||||||
|
|
||||||
|
꩜hlite[|<builder-function-type'>|
|
||||||
|
{/(∀(+ _ / _ _)(→ _ _ ooo (bt + (∩ / _ + A) / _)))}
|
||||||
|
(∀ (A {?@ Kⱼ Xⱼ} …)
|
||||||
|
(→ (code:comment "; Keys and values:")
|
||||||
|
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||||
|
;; Result type:
|
||||||
|
(BinaryTree (∩ |<Some or None>| A) …)))]
|
||||||
|
|
||||||
|
The type ꩜racket[propagate-τ] defined below is used to instantiate ꩜racket[A],
|
||||||
|
and is carefully picked so that its intersection will in no way change the
|
||||||
|
result type (i.e. the intersection with ꩜racket[A] will be an identity
|
||||||
|
operation where it is used). In other words, ꩜racket[propagate-τ] has the same
|
||||||
|
shape as the leaves of the binary tree. This intersection however forces the
|
||||||
|
simplification step to be performed on the affected parts once the type is
|
||||||
|
instantiated.
|
||||||
|
|
||||||
|
꩜chunk[<propagate-τ>
|
||||||
|
(define-type propagate-τ
|
||||||
|
(Pairof Any
|
||||||
|
(U (None (Listof Natural))
|
||||||
|
(Some Any))))]
|
||||||
|
|
||||||
|
꩜;Use chunkref instead of ꩜racket[|<Some or None>|] ?
|
||||||
|
|
||||||
|
The implementation of the builder function will need to convert values with
|
||||||
|
the ꩜racket[|<Some or None>|] type to values of type
|
||||||
|
꩜racket[(∩ |<Some or None>| A)]. Since the intersection could, in principle,
|
||||||
|
be any subtype of ꩜racket[|<Some or None>|], we request that the caller
|
||||||
|
supplies a proof that the conversion is possible. This proof takes the form of
|
||||||
|
an ꩜racket[oracle] function, which transforms an element with the type
|
||||||
|
꩜racket[propagate-τ] (which is a supertype of every possible
|
||||||
|
꩜racket[|<Some or None>|] type) into an element with the type
|
||||||
|
꩜racket[(∩ A B)], where ꩜racket[B] is the original type of the value to
|
||||||
|
upgrade.
|
||||||
|
|
||||||
|
꩜chunk[<oracle-type>
|
||||||
|
(∀ (B) (→ (∩ B
|
||||||
|
(Pairof Any (U (Some Any) (None (Listof Any)))))
|
||||||
|
(∩ A B)))]
|
||||||
|
|
||||||
|
The builder function type is updated as follows:
|
||||||
|
|
||||||
|
꩜hlite[|<builder-function-type''>|
|
||||||
|
{/(∀(_ _ _)(→ + _ _ / _ _ ooo _))}
|
||||||
|
(∀ (A {?@ Kⱼ Xⱼ} …)
|
||||||
|
(→ (code:comment "; Oracle:")
|
||||||
|
<oracle-type>
|
||||||
|
(code:comment "; Keys and values:")
|
||||||
|
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||||
|
;; Result type:
|
||||||
|
(BinaryTree (∩ |<Some or None>| A) …)))]
|
||||||
|
|
||||||
|
|
||||||
;]
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -17,4 +17,5 @@ the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document.
|
||||||
@include-section[(submod "../graph-info.hl.rkt" doc)]
|
@include-section[(submod "../graph-info.hl.rkt" doc)]
|
||||||
@include-section[(submod "../graph-type.hl.rkt" doc)]
|
@include-section[(submod "../graph-type.hl.rkt" doc)]
|
||||||
@include-section[(submod "../graph.hl.rkt" doc)]
|
@include-section[(submod "../graph.hl.rkt" doc)]
|
||||||
@include-section[(submod "../main-draft.hl.rkt" doc)]
|
@include-section[(submod "../main-draft.hl.rkt" doc)]
|
||||||
|
@include-section[(submod "../flexible-with-generalized-ctor.hl.rkt" doc)]
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user