From bf9d5b2328c7d52c7ea1bed6c4b906ae35f73d65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Thu, 18 May 2017 15:10:33 +0200 Subject: [PATCH] Cleaned up flexible structures implementation. The problem is that compiling the definitions is rather slow (~4 minutes for 10/128 fields), although those can be pre-compiled in advance, and using the functions is rather slow to typecheck (about 0.4s to use a 10/32 constructor), which is more of a problem. --- binarytree.hl.rkt | 12 ++++++ flexible-with-generalized-ctor-test.rkt | 31 ++++++++++---- flexible-with-generalized-ctor.hl.rkt | 56 +++++++++++-------------- 3 files changed, 60 insertions(+), 39 deletions(-) create mode 100644 binarytree.hl.rkt diff --git a/binarytree.hl.rkt b/binarytree.hl.rkt new file mode 100644 index 0000000..d8abb2c --- /dev/null +++ b/binarytree.hl.rkt @@ -0,0 +1,12 @@ +#lang type-expander + +(provide BinaryTree) + +(require (for-syntax syntax/parse + phc-toolkit/aliases)) + +(define-type-expander BinaryTree + (syntax-parser + [(_ leafⱼ …) + ;; TODO: implement BinaryTree. + #'(List leafⱼ …)])) \ No newline at end of file diff --git a/flexible-with-generalized-ctor-test.rkt b/flexible-with-generalized-ctor-test.rkt index 0b0176c..b7961b2 100644 --- a/flexible-with-generalized-ctor-test.rkt +++ b/flexible-with-generalized-ctor-test.rkt @@ -1,13 +1,28 @@ #lang type-expander -(require (lib "phc-graph/flexible-with-generalized-ctor.hl.rkt")) -(provide f g) +(require "flexible-with-generalized-ctor.hl.rkt" + "binarytree.hl.rkt") +(provide f-4-2 f-8-3) -(builder-f f 4 2) +(builder-f f-4-2 4 2) -#;((inst f propagate-τ '|1| Number '|3| String) - oracle '|1| 100 '|3| "bee") +(ann ((inst f-4-2 propagate-τ '|1| Number '|3| String) + oracle '|1| 100 '|3| "bee") + (BinaryTree + (Promise (Pairof #f Any)) + (Promise (Pairof '|1| Number)) + (Promise (Pairof #f Any)) + (Promise (Pairof '|3| String)))) -(builder-f g 8 3) +(builder-f f-8-3 8 3) -#;((inst g propagate-τ '|1| Number '|3| String '|7| Symbol) - oracle '|1| 100 '|3| "bee" '|7| 'buzz) \ No newline at end of file +(ann ((inst f-8-3 propagate-τ '|1| Number '|3| String '|7| Symbol) + oracle '|1| 100 '|3| "bee" '|7| 'buzz) + (BinaryTree + (Promise (Pairof #f Any)) + (Promise (Pairof '|1| Number)) + (Promise (Pairof #f Any)) + (Promise (Pairof '|3| String)) + (Promise (Pairof #f Any)) + (Promise (Pairof #f Any)) + (Promise (Pairof #f Any)) + (Promise (Pairof '|7| Symbol)))) \ No newline at end of file diff --git a/flexible-with-generalized-ctor.hl.rkt b/flexible-with-generalized-ctor.hl.rkt index ab8dd78..93e9c5b 100644 --- a/flexible-with-generalized-ctor.hl.rkt +++ b/flexible-with-generalized-ctor.hl.rkt @@ -9,7 +9,6 @@ ꩜chunk[<*> (provide builder-τ - None propagate-τ oracle builder-f) @@ -20,15 +19,8 @@ racket/list racket/function subtemplate/override) - (for-meta 2 racket/base)) - - (struct (T) None ([f : (Promise T)])) - - (define-type-expander BinaryTree - (syntax-parser - [(_ leafⱼ …) - ;; TODO: implement BinaryTree. - #'(List leafⱼ …)])) + (for-meta 2 racket/base) + "binarytree.hl.rkt") @@ -70,7 +62,7 @@ form of) the builder function type as follows: (→ (code:comment "; Keys and values:") {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … ;; Result type: - (BinaryTree || …)))] + (BinaryTree (Promise ||) …)))] We expect each key ꩜racket[Kⱼ] to be a symbol of the shape ꩜racket[|0|], ꩜racket[|1|], ꩜racket[|2|] and so on: @@ -115,11 +107,12 @@ 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ᵢ …]). +We use a similar approach to conditionally produce the ꩜racket[None] element +(which we represent as ꩜racket[#f]), 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[ #:with NSyms (NSymᵢ …) @@ -138,7 +131,7 @@ The resulting type should therefore be ꩜racket[Nothing] only if there is no ꩜racket[(List . exceptᵢ)] otherwise. ꩜chunk[|| - (None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …))] + (Pairof #f (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 @@ -163,12 +156,12 @@ 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[|| - {/(∀(+ _ / _ _)(→ _ _ ooo (bt + (∩ / _ + A) / _)))} + {/(∀(+ _ / _ _)(→ _ _ ooo (bt (p + (∩ / _ + A)) / ooo)))} (∀ (A {?@ Kⱼ Xⱼ} …) (→ (code:comment "; Keys and values:") {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … ;; Result type: - (BinaryTree (∩ || A) …)))] + (BinaryTree (Promise (∩ || 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 @@ -180,8 +173,8 @@ instantiated. ꩜chunk[ (define-type propagate-τ - (U (Pairof Any Any) - (None (Listof Any))))] + (U (Pairof Symbol Any) + (Pairof #f (Listof Symbol))))] ꩜;Use chunkref instead of ꩜racket[||] ? @@ -199,8 +192,8 @@ upgrade. ꩜chunk[ (define-type (oracle-τ A) (∀ (B) (→ (∩ B - (U (Pairof Any Any) - (None (Listof Any)))) + (U (Pairof Symbol Any) + (Pairof #f (Listof Symbol)))) (∩ A B))))] The oracle does nothing more than return its argument unchanged: @@ -220,7 +213,7 @@ oracle: (code:comment "; Keys and values:") {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … ;; Result type: - (BinaryTree (∩ || A) …)))] + (BinaryTree (Promise (∩ || A)) …)))] @@ -243,11 +236,12 @@ oracle: ꩜chunk[ (: name || #;(builder-τ n m)) (define (name oracle {?@ kⱼ xⱼ} …) - (list (cond - [((make-predicate 'NSymᵢⱼ) kᵢⱼ) - ((inst oracle (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) Xᵢⱼ)) (cons kᵢⱼ xᵢⱼ))] - … - [else - ((inst oracle (None (List (∩ Kᵢⱼ (U 'exceptᵢⱼ …)) …))) - (None (delay (list kᵢⱼ …))))]) + (list (delay + (cond + [((make-predicate 'NSymᵢⱼ) kᵢⱼ) + ((inst oracle (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) Xᵢⱼ)) (cons kᵢⱼ xᵢⱼ))] + … + [else + ((inst oracle (Pairof #f (List (∩ Kᵢⱼ (U 'exceptᵢⱼ …)) …))) + (cons #f (list kᵢⱼ …)))])) …))] \ No newline at end of file