From 26256a09b94a4e29e31fa2db6321fee4e068b087 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Tue, 15 Mar 2016 00:55:04 +0100 Subject: [PATCH] WIP on FB case 128 --- graph-lib/graph/__DEBUG_constructor.rkt | 5 + graph-lib/graph/adt.lp2.rkt | 108 ++++++++ graph-lib/graph/constructor.lp2.rkt | 256 ++++++++++++++++++ graph-lib/graph/define-adt.lp2.rkt | 102 ++++++++ graph-lib/graph/remember.rkt | 101 ++++---- graph-lib/graph/structure.lp2.rkt | 21 +- graph-lib/graph/tagged.lp2.rkt | 155 +++++++++++ graph-lib/graph/variant.lp2.rkt | 328 +----------------------- graph-lib/graph/variant2.lp2.rkt | 158 ++++++++++++ graph-lib/lib/low/todo.rkt | 15 ++ 10 files changed, 870 insertions(+), 379 deletions(-) create mode 100644 graph-lib/graph/__DEBUG_constructor.rkt create mode 100644 graph-lib/graph/adt.lp2.rkt create mode 100644 graph-lib/graph/constructor.lp2.rkt create mode 100644 graph-lib/graph/define-adt.lp2.rkt create mode 100644 graph-lib/graph/tagged.lp2.rkt create mode 100644 graph-lib/graph/variant2.lp2.rkt create mode 100644 graph-lib/lib/low/todo.rkt diff --git a/graph-lib/graph/__DEBUG_constructor.rkt b/graph-lib/graph/__DEBUG_constructor.rkt new file mode 100644 index 0000000..4fab3b0 --- /dev/null +++ b/graph-lib/graph/__DEBUG_constructor.rkt @@ -0,0 +1,5 @@ +#lang racket +(require syntax/parse + syntax/parse/experimental/template) +(require (for-template "../type-expander/type-expander.lp2.rkt")) +(require (submod "../lib/low.rkt" untyped)) \ No newline at end of file diff --git a/graph-lib/graph/adt.lp2.rkt b/graph-lib/graph/adt.lp2.rkt new file mode 100644 index 0000000..ffe6df2 --- /dev/null +++ b/graph-lib/graph/adt.lp2.rkt @@ -0,0 +1,108 @@ +#lang scribble/lp2 +@(require "../lib/doc.rkt") +@doc-lib-setup + +@title[#:style manual-doc-style]{Algebaraic Data Types: Constructor} + +@(table-of-contents) + +@section[#:tag "ADT|introduction"]{Introduction} + +We define variants (tagged unions), with the following constraints: + +@itemlist[ + @item{Unions are anonymous: two different unions can contain the same tag, and + there's no way to distinguish these two occurrences of the tag} + @item{Callers can require an uninterned tag which inherits the interned tag, so + that @racket[(constructor #:uninterned tag Number)] is a subtype of + @racket[(constructor #:uninterned tag Number)], but not the reverse} + @item{The tag can be followed by zero or more “fields”} + @item{An instance of a variant only @racket[match]es with its constructor and + the same number of fields, with exact matching on the tag for uninterned + tags}] + +See @url{https://github.com/andmkent/datatype/} for an existing module providing +Algebraic Data Types. The main difference with our library is that a given tag +(i.e. constructor) cannot be shared by multiple unions, as can be seen in the +example below where the second @tc[define-datatype] throws an error: + +@chunk[ + (require datatype) + + (define-datatype Expr + [Var (Symbol)] + [Lambda (Symbol Expr)] + [App (Expr Expr)]) + + ;; define-datatype: variant type # already bound + ;; in: Simple-Expr + (define-datatype Simple-Expr + [Var (Symbol)] + [Lambda (Symbol Expr)])] + +@section{Constructors, tagged, variants and structures} + +We first define @tc[structure] and @tc[constructor], the +primitives allowing us to build instance, match against them +and express the type itself. + +@chunk[ + (require "structure.lp2.rkt") + (require "constructor.lp2.rkt")] + +We then define @tc[tagged], which is a shorthand for +manipulating constructors which single value is a promise +for a structure. + +@chunk[ + (require "tagged.lp2.rkt")] + +For convenience, we write a @tc[variant] form, which is a +thin wrapper against @tc[(U (~or constructor tagged) …)]. + +@chunk[ + (require "variant2.lp2.rkt")] + +The @tc[define-tagged] and @tc[define-constructor] forms +also allow the @tc[#:uninterned] and @tc[#:private] +keywords, to create uninterned constructors and tagged +structures as described in @secref{ADT|introduction}. + +@chunk[ + (require "define-adt.lp2.rkt")] + +Finally, we define a @tc[uniform-get] form, which can +operate on @tc[tagged] structures. We also wrap the plain +@tc[structure] form so that it instead returns a tagged +structure, using a common tag for all plain structures. This +allows us to rely on the invariant that @tc[uniform-get] +always operates on data with the same shape (a constructor +which single value is a promise for a structure)@note{This + avoids the risk of combinatorial explosion for the intput + type of @racket[uniform-get], when accessing a deeply nested + field: allowing + @racket[(U structure + (constructor structure) + (constructor (Promise structure)))] + would result in a type of size @${n⁴}, with ${n} then depth + of the accessed field.} + +@chunk[ + (void)] @;(require "uniform-get.lp2.rkt") + +@chunk[<*> + (void) + #;(begin + (module main typed/racket + + (provide constructor + define-constructor + tagged + define-tagged + variant + define-variant + (rename-out [wrapped-structure structure]) + uniform-get)) + + (require 'main) + (provide (all-from-out 'main)))] \ No newline at end of file diff --git a/graph-lib/graph/constructor.lp2.rkt b/graph-lib/graph/constructor.lp2.rkt new file mode 100644 index 0000000..eabeadc --- /dev/null +++ b/graph-lib/graph/constructor.lp2.rkt @@ -0,0 +1,256 @@ +#lang scribble/lp2 +@(require "../lib/doc.rkt") +@doc-lib-setup + +@title[#:style manual-doc-style]{Algebaraic Data Types: Constructor} + +@(table-of-contents) + +@section{Introduction} + +This file defines @tc[constructor], a form which allows +tagging values, so that two otherwise identical values can +be distinguished by the constructors used to wrapp them. + +@section[#:tag "variant|supertype"]{The @racket[ConstructorTop] supertype} + +We define variants as instances of subtypes of the @tc[Tagged] structure: + +@chunk[ + (struct (T) ConstructorTop ([values : T]) #:transparent) + (define-type ConstructorTopType ConstructorTop)] + +Other options would include defining the variant as a @tc[list], with the tag +symbol in the first element. We couldn't use a @tc[vector], because these are +mutable in @tc[typed/racket] (for now), and occurrence typing can't work +properly on mutable data structures. Using a @tc[list] has the drawback that +other data can easily take the same shape, meaning that it is impossible to +define a reliable predicate for a tagged instance that also works well with* +@tc[typed/racket]'s occurrence typing. + +@section{Declaring a new constructor} + +The constructor type will be a @tc[struct] inheriting from +@tc[ConstructorTop], without adding any field. By default, the +constructor's name is "interned" (not in racket's interned +symbols sense), so that two uses of the same constructor +name in different files refer to the same constructor type. + +For this, we use the @tc[remember] library: + +@chunk[ + (require (for-syntax "remember-lib.rkt"))] + +We pre-declare here in this file all the remembered constructors: + +@CHUNK[ + (struct (T) + constructor-name/struct + #,(syntax-local-introduce #'ConstructorTop) + () + #:transparent) + …] + +We define an associative list which maps the constructor +name to the structure identifier (with the same scopes as +the one declared just above): + +@CHUNK[ + (define-syntax (declare-all-constructors stx) + (define/with-syntax (constructor-name …) + constructor-names-no-duplicates) + (define/with-syntax alist + (syntax-local-introduce #'constructor-name→stx-name/alist)) + (define-temp-ids "~a/struct" (constructor-name …)) + #`(begin + + + (define-for-syntax alist + (stx-map (λ (x y) (cons (syntax->datum x) y)) + #'(constructor-name …) + #'(constructor-name/struct …)))))] + +We call this macro once, to define the structs in the +template meta-level, and the +@tc[constructor-name→stx-name/alist] in the transformer +meta-level. + +@CHUNK[ + (declare-all-constructors)] + +The list of constructor names, @tc[constructor-names-no-duplicates], is the one +remembered by “@code{remember-lib.rkt}” with duplicate entries removed: + +@CHUNK[ + (define-for-syntax constructor-names-no-duplicates + (remove-duplicates (get-remembered 'constructor)))] + +Finally, we define @tc[with-constructor-name→stx-name], a +helper macro which accesses the structure identifier for a +given constructor name, checking whether the constructor +name has been remembered already (and throwing an error +otherwise): + +@chunk[ + (begin-for-syntax + (define-syntax (with-constructor-name→stx-name stx) + (syntax-case stx () + [(_ (stx-name with-struct constructor-name fallback error-stx) + . body) + #`])))] + +@chunk[ + (if #,(syntax/loc #'with-struct (attribute with-struct)) + (with-syntax ([stx-name #'with-struct]) + . body) + (if (check-remember-all 'constructor constructor-name) + (with-syntax + ([stx-name (cdr + (assoc (syntax->datum + (datum->syntax #f constructor-name)) + constructor-name→stx-name/alist))]) + . body) + (remember-all-errors2 fallback constructor-name)))] + +@section{@racket[constructor]} + +We define the @tc[constructor] macro which acts as a type, a +match expander, and a procedure returning a constructor +instance: + +@chunk[ + (define-multi-id constructor + #:type-expander + #:match-expander + #:call )] + +@chunk[ + (check-equal?: (constructor-values + (ann (constructor a 1 "x") + ;; TODO: Make a (ConstructorTop …) type expander. + (ConstructorTop (List Number String)))) + (list 1 "x")) + (check-equal?: (constructor-values + (ann (constructor a 1 "x") + (ConstructorTop Any))) + (list 1 "x")) + (check-equal?: (constructor-values + (ann (constructor a 1 "x") + (constructor a Number String))) + (list 1 "x")) ;; TODO: test that the tag is 'a + (check-equal?: (constructor-values + (ann (constructor b) + (constructor b))) + (list)) ;; TODO: test that the tag is 'b + (check-equal?: (constructor-values + (ann (constructor c 'd) + (constructor c Symbol))) + 'd) ;; TODO: test that the tag is 'c + (check-equal?: (ann (constructor c 2 "y") + (constructor c Number String)) + (constructor c 2 "y")) + (check-not-equal?: (constructor d 2 "y") + (constructor d 2 "y" 'z)) + (check-not-equal?: (constructor e 2 "y") + (constructor F 2 "y"))] + +@subsection{Type-expander} + +@CHUNK[ + (λ/syntax-parse (_ constructor-name:id + (~maybe #:with-struct with-struct) + . (~or (T₀:expr) (Tᵢ:expr …))) + (with-constructor-name→stx-name + (stx-name with-struct #'constructor-name #'please-recompile stx) + (template + (stx-name (?? T₀ (List Tᵢ …))))))] + +@subsection{Predicate} + +@CHUNK[ + (define-syntax (Constructor-predicate? stx) + (syntax-parse stx + [(_ constructor-name (~maybe #:with-struct with-struct) v) + (quasisyntax/loc stx + (#,(syntax/loc stx + (Constructor-predicate? constructor-name + (?? (?@ #:with-struct with-struct)))) + v))] + [(_ constructor-name (~maybe #:with-struct with-struct)) + ;; make-predicate works for polymorphic structs when + ;; instantiating them with Any. + (with-constructor-name→stx-name + (stx-name with-struct + #'constructor-name + (syntax/loc #'constructor-name please-recompile) + stx) + (syntax/loc stx (make-predicate (stx-name Any))))] + [(_) + (syntax/loc stx (make-predicate (ConstructorTop Any)))]))] + +@subsection{Match-expander} + +@chunk[ + (λ/syntax-parse (_ constructor-name:id (~maybe #:with-struct with-struct) + . (~or (pat₀:expr) (patᵢ:expr …))) + (template + (? (Constructor-predicate? constructor-name + (?? (?@ #:with-struct with-struct))) + (app ConstructorTop-values (?? pat₀ (list patᵢ …))))))] + +@subsection{Instance creation} + +@CHUNK[ + (λ/syntax-parse (_ constructor-name:id + (~maybe #:with-struct with-struct) + value:expr …) + (define/with-syntax (arg …) (generate-temporaries #'(value …))) + (define/syntax-parse (~or (arg₀) (argᵢ …)) #'(arg …)) + (define/with-syntax (T …) (generate-temporaries #'(value …))) + (with-constructor-name→stx-name + (stx-name with-struct + #'constructor-name + (syntax/loc #'constructor-name please-recompile) + stx) + (template + ((λ #:∀ (T …) ([arg : T] …) + : (constructor constructor-name T …) + (stx-name (?? arg₀ (list argᵢ …)))) + value …))))] + +@chunk[<*> + (begin + (module main typed/racket + (require (for-syntax racket/list + syntax/parse + syntax/parse/experimental/template + racket/syntax + (submod "../lib/low.rkt" untyped)) + (for-meta 2 racket/base) + "../lib/low.rkt" + "../type-expander/multi-id.lp2.rkt" + "../type-expander/type-expander.lp2.rkt") + + (provide constructor + (rename-out [Constructor-predicate? constructor?]) + (rename-out [ConstructorTopType ConstructorTop]) + ConstructorTop? + (rename-out [ConstructorTop-values constructor-values])) + + + + + + + + + ) + + (require 'main) + (provide (all-from-out 'main)) + + (module* test typed/racket + (require (submod "..") + "../lib/low.rkt" + "../type-expander/type-expander.lp2.rkt") + ))] \ No newline at end of file diff --git a/graph-lib/graph/define-adt.lp2.rkt b/graph-lib/graph/define-adt.lp2.rkt new file mode 100644 index 0000000..86f4ad4 --- /dev/null +++ b/graph-lib/graph/define-adt.lp2.rkt @@ -0,0 +1,102 @@ +#lang scribble/lp2 +@(require "../lib/doc.rkt") +@doc-lib-setup + +@title[#:style manual-doc-style]{Algebaraic Data Types: + @racket[define-constructor] and @racket[define-tagged]} + +@(table-of-contents) + +@section{Introduction} + +@section{@racket{define-constructor}} + +@chunk[ + (define-syntax/parse + (define-constructor constructor-name:id + (~maybe #:with-struct with-struct) + (~maybe #:? name?) + type …) + + (define/with-syntax default-name? (format-id #'name "~a?" #'name)) + (define-temp-ids "pat" (type …)) + (define-temp-ids "value" (type …)) + (template + (begin + (define-multi-id constructor-name + #:type-expand-once + (constructor constructor-name + (?? (?@ #:with-struct with-struct)) + type …) + #:match-expander + (λ/syntax-parse (_ pat …) + #'(constructor constructor-name + (?? (?@ #:with-struct with-struct)) + pat …)) + #:call + (λ/syntax-parse (_ value …) + #'(constructor constructor-name + (?? (?@ #:with-struct with-struct)) + value …))) + (define-multi-id (?? name? default-name?) + #:else + #'(constructor? constructor-name + (?? (?@ #:with-struct with-struct)))))))] + +@chunk[ + (define-syntax/parse (define-tagged tag:id + (~maybe #:with-struct with-struct) + (~maybe #:? name?) + [field type] …) + (define/with-syntax default-name? (format-id #'name "~a?" #'name)) + (define-temp-ids "pat" (type …)) + (define-temp-ids "value" (type …)) + (template + (begin + (define-multi-id tag + #:type-expand-once + (tagged tag + (?? (?@ #:with-struct with-struct)) + [field type] …) + #:match-expander + (λ/syntax-parse (_ pat …) + #'(tagged tag + (?? (?@ #:with-struct with-struct)) + [field pat] …)) + #:call + (λ/syntax-parse (_ value …) + #'(tagged #:instance + tag + (?? (?@ #:with-struct with-struct)) + value …))) + (define-multi-id (?? name? default-name?) + #:else + #'(tagged? tag + (?? (?@ #:with-struct with-struct)) + field …)))))] + +@section{Conclusion} + +@chunk[<*> + (begin + (module main typed/racket + (require (for-syntax racket/list + syntax/parse + syntax/parse/experimental/template + racket/syntax + (submod "../lib/low.rkt" untyped)) + (for-meta 2 racket/base) + "../lib/low.rkt" + "../type-expander/multi-id.lp2.rkt" + "../type-expander/type-expander.lp2.rkt") + + + ) + + (require 'main) + (provide (all-from-out 'main)) + + (module* test typed/racket + (require (submod "..") + "../lib/low.rkt" + "../type-expander/type-expander.lp2.rkt")))] \ No newline at end of file diff --git a/graph-lib/graph/remember.rkt b/graph-lib/graph/remember.rkt index d5453d3..eeeefe7 100644 --- a/graph-lib/graph/remember.rkt +++ b/graph-lib/graph/remember.rkt @@ -100,58 +100,63 @@ (structure foo) (structure foo) (structure foo) -(variant . x) -(variant . y) -(variant . z) -(variant . tagged-s1) -(variant . tagged-s2) -(variant . tagged-s3) -(variant . tagged-s4) -(variant . a) -(variant . b) -(variant . c) -(variant . c) -(variant . d) -(variant . e) -(variant . dd) -(variant . ddd) -(variant . dde) -(variant . ddf) -(variant . ddg) -(variant . ddh) -(variant . ddi) -(variant . ddj) -(variant . ddk) -(variant . ddl) -(variant . F) -(variant . w) -(variant . foo) -(variant . foo) -(variant . foo) -(variant . de1) -(variant . de2) -(variant . de3) -(variant . df3) -(variant . df1) -(variant . df2) +(constructor . x) +(constructor . y) +(constructor . z) +(constructor . tagged-s1) +(constructor . tagged-s2) +(constructor . tagged-s3) +(constructor . tagged-s4) +(constructor . a) +(constructor . b) +(constructor . c) +(constructor . c) +(constructor . d) +(constructor . e) +(constructor . dd) +(constructor . ddd) +(constructor . dde) +(constructor . ddf) +(constructor . ddg) +(constructor . ddh) +(constructor . ddi) +(constructor . ddj) +(constructor . ddk) +(constructor . ddl) +(constructor . F) +(constructor . w) +(constructor . foo) +(constructor . foo) +(constructor . foo) +(constructor . de1) +(constructor . de2) +(constructor . de3) +(constructor . df3) +(constructor . df1) +(constructor . df2) (structure Number String) (structure Number String) (structure Number String) -(variant . dg1) -(variant . dh1) -(variant . dh1) -(variant . dh1) -(variant . di2) -(variant . dj1) -(variant . dk1) -(variant . dl1) +(constructor . dg1) +(constructor . dh1) +(constructor . dh1) +(constructor . dh1) +(constructor . di2) +(constructor . dj1) +(constructor . dk1) +(constructor . dl1) (structure x y) -(variant . txyz) -(variant . City89/with-promises-tag) -(variant . Street90/with-promises-tag) -(variant . House91/with-promises-tag) -(variant . Person92/with-promises-tag) +(constructor . txyz) +(constructor . City89/with-promises-tag) +(constructor . Street90/with-promises-tag) +(constructor . House91/with-promises-tag) +(constructor . Person92/with-promises-tag) (structure n) (structure water) (structure water) -(variant . cxyz) +(constructor . cxyz) +(constructor . v) +(constructor . t1) +(constructor . Number) +(constructor . String) +(constructor . Number) diff --git a/graph-lib/graph/structure.lp2.rkt b/graph-lib/graph/structure.lp2.rkt index e61713b..5b474e2 100644 --- a/graph-lib/graph/structure.lp2.rkt +++ b/graph-lib/graph/structure.lp2.rkt @@ -232,7 +232,8 @@ field part of the structure. @CHUNK[ (define-syntax/parse (declare-all-structs fields→stx-name-alist:id (name field ...) ...) - #'(begin + (define-temp-ids "~a/T" ((field …) …)) + #`(begin (define-for-syntax fields→stx-name-alist @@ -283,10 +284,18 @@ associative list. The struct declarations are rather standard. We use @tc[#:transparent], so that @tc[equal?] compares instances memberwise. +@chunk[ + (struct StructureTop ()) + (define-type StructureTopType StructureTop)] + @; TODO: write “field : Tfield”, it's cleaner. @CHUNK[ - (struct (field ...) name ([field : field] ...) #:transparent) - ...] + (struct (field/T …) + name + #,(syntax-local-introduce #'StructureTop) + ([field : field/T] …) + #:transparent) + …] @section{Constructor} @@ -561,10 +570,14 @@ its arguments across compilations, and adds them to the file structure structure-supertype structure-supertype* - structure?) + structure? + (rename-out [StructureTopType StructureTop]) + StructureTop?) (begin-for-syntax (provide structure-args-stx-class)) + + diff --git a/graph-lib/graph/tagged.lp2.rkt b/graph-lib/graph/tagged.lp2.rkt new file mode 100644 index 0000000..907afa7 --- /dev/null +++ b/graph-lib/graph/tagged.lp2.rkt @@ -0,0 +1,155 @@ +#lang scribble/lp2 +@(require "../lib/doc.rkt") +@doc-lib-setup + +@title[#:style manual-doc-style]{Algebaraic Data Types: Tagged} + +@(table-of-contents) + +@section{Introduction} + +We define @tc[tagged], which is a shorthand for +manipulating constructors which single value is a promise +for a structure. + +@section{@racket[tagged]} + +@chunk[ + (define-multi-id tagged + #:type-expander + #:match-expander + #:call )] + +@subsection{@racket[TaggedTop]} + +@chunk[ + (define-type TaggedTop (ConstructorTop (Promise StructureTop)))] + +@subsection{@racket[type-expander]} + +@chunk[ + (λ/syntax-parse (_ tag:id (~maybe #:with-struct with-struct) + . structure-type) + (quasitemplate + (constructor tag (?? (?@ #:with-struct with-struct)) + #,(syntax/loc #'structure-type + (structure . structure-type)))))] + +@subsection{@racket[match-expander]} + +@chunk[ + (λ/syntax-parse (_ tag:id (~maybe #:with-struct with-struct) + . structure-pat) + (quasitemplate + (constructor tag (?? (?@ #:with-struct with-struct)) + #,(syntax/loc #'structure-pat + (structure . structure-pat)))))] + +@subsection{@racket[instance creation]} + +@; TODO: clean this up a bit, and explain it. +@chunk[ + (λ/syntax-parse + (~and (_ (~and (~seq disambiguate …) + (~or (~seq #:instance) + (~seq #:make-instance) + (~seq))) + tag:id (~maybe #:with-struct with-struct) + . fields) + (~parse (sa:structure-args-stx-class) + #'(disambiguate … . fields))) + (define-temp-ids "~a/TTemp" (sa.field …)) + (define-temp-ids "~a/arg" (sa.field …)) + (define/with-syntax c + (if (attribute sa.type) + (quasitemplate + (λ ([sa.field/arg : sa.type] …) + : (constructor tag (?? (?@ #:with-struct with-struct)) + #,(syntax/loc #'fields + (structure [sa.field sa.type] …))) + (constructor tag (?? (?@ #:with-struct with-struct)) + #,(syntax/loc #'fields + (structure #:instance + [sa.field : sa.type sa.field/arg] + …))))) + (quasitemplate + (λ #:∀ (sa.field/TTemp …) ([sa.field/arg : sa.field/TTemp] …) + : (constructor tag (?? (?@ #:with-struct with-struct)) + #,(syntax/loc #'fields + (structure [sa.field sa.field/TTemp] …))) + (constructor tag (?? (?@ #:with-struct with-struct)) + #,(syntax/loc #'fields + (structure #:instance + [sa.field sa.field/arg] …))))))) + (if (attribute sa.value) + #'(c sa.value …) + #'c))] + +@subsection{@racket[predicate]} + +@CHUNK[ + (define-multi-id TaggedTop? + #:else #'(λ (v) (and (ConstructorTop? v) + (promise? (constructor-values v)) + (StructureTop? (force (constructor-values v))))))] + +@CHUNK[ + (define-syntax/parse (tagged? tag (~maybe #:with-struct with-struct) + field …) + #'(λ (v) (and (constructor? tag (?? (?@ #:with-struct with-struct)) v) + (promise? (constructor-values v)) + ((structure? field …) + (force (constructor-values v))))))] + +@section{Tests} + +@chunk[ + (check-equal?: (match (ann (tagged t1 [x 1] [y "b"]) + (tagged t1 [x : Number] [y : String])) + [(tagged t1 [x a] [y b]) (list 'ok b a)] + [_ #f]) + '(ok "b" 1))] + +@chunk[ + (check-equal?: (match (ann (tagged foo [x "o"] [y 3] [z 'z]) + (tagged foo + [x String] + [z 'z] + [y Fixnum])) + [(tagged foo z x y) (list z y x)]) + '(z 3 "o"))] + +@section{Conclusion} + +@chunk[<*> + (begin + (module main typed/racket + (require (for-syntax racket/list + syntax/parse + syntax/parse/experimental/template + racket/syntax + (submod "../lib/low.rkt" untyped)) + "../lib/low.rkt" + "../type-expander/multi-id.lp2.rkt" + "../type-expander/type-expander.lp2.rkt" + "constructor.lp2.rkt" + "structure.lp2.rkt") + + (provide tagged + tagged? + TaggedTop + TaggedTop?) + + + + + ) + + (require 'main) + (provide (all-from-out 'main)) + + (module* test typed/racket + (require (submod "..") + "../lib/low.rkt" + "../type-expander/type-expander.lp2.rkt") + ))] \ No newline at end of file diff --git a/graph-lib/graph/variant.lp2.rkt b/graph-lib/graph/variant.lp2.rkt index f35144a..69deb19 100644 --- a/graph-lib/graph/variant.lp2.rkt +++ b/graph-lib/graph/variant.lp2.rkt @@ -6,331 +6,8 @@ @(table-of-contents) -@section{Introduction} - -We define variants (tagged unions), with the following constraints: - -@itemlist[ - @item{Unions are anonymous: two different unions can contain the same tag, and - there's no way to distinguish these two occurrences of the tag} - @item{Callers can require an uninterned tag which inherits the interned tag, so - that @racket[(tagged #:uninterned tag Number)] is a subtype of - @racket[(tagged #:uninterned tag Number)], but not the reverse} - @item{The tag can be followed by zero or more “fields”} - @item{An instance of a variant only @racket[match]es with its constructor and - the same number of fields, with exact matching for uninterned tags}] - -See @url{https://github.com/andmkent/datatype/} for an existing module providing -Algebraic Data Types. The main difference with our library is that a given tag -(i.e. constructor) cannot be shared by multiple unions, as can be seen in the -example below where the second @tc[define-datatype] throws an error: - -@chunk[ - (require datatype) - - (define-datatype Expr - [Var (Symbol)] - [Lambda (Symbol Expr)] - [App (Expr Expr)]) - - ;; define-datatype: variant type # already bound - ;; in: Simple-Expr - (define-datatype Simple-Expr - [Var (Symbol)] - [Lambda (Symbol Expr)])] - -@section[#:tag "variant|supertype"]{The @racket[Variant] supertype} - -We define variants as instances of subtypes of the @tc[Tagged] structure: - -@chunk[ - (struct (T) Tagged ([value : T]) #:transparent) - (define-type Tagged-type Tagged)] - -Other options would include defining the variant as a @tc[list], with the tag -symbol in the first element. We couldn't use a @tc[vector], because these are -mutable in @tc[typed/racket] (for now), and occurrence typing can't work -properly on mutable data structures. Using a @tc[list] has the drawback that -other data can easily take the same shape, meaning that it is impossible to -define a reliable predicate for a tagged instance that is also understood by -@tc[typed/racket]. - -@section{Declaring a new tag} - -The tag type will be a @tc[struct] inheriting from -@tc[Tagged], without adding any field. By default, the tag -is "interned" (not in racket's interned symbols sense), so -that two uses of the same tag name in different files refer -to the same tag type. - -For this, we use the @tc[remember] library: - -@chunk[ - (require (for-syntax "remember-lib.rkt"))] - -We pre-declare here in this file all the remembered tags: - -@CHUNK[ - (struct (T) tag-name/struct Tagged () #:transparent) - …] - -We define an associative list which maps tag names to the -structure identifier (with the same scopes as the one -declared just above): - -@CHUNK[ - (define-syntax/parse (declare-all-tags tag-name→stx-name/alist:id - tag-name …) - (define-temp-ids "~a/struct" (tag-name …)) - #'(begin - - - (define-for-syntax tag-name→stx-name/alist - (stx-map (λ (x y) (cons (syntax->datum x) y)) - #'(tag-name …) - #'(tag-name/struct …)))))] - -This macro should be called only once, and given as parameters the whole -remembered list of tag names: - -@CHUNK[ - (define-syntax/parse (call-declare-all-tags tag-name→stx-name/alist:id) - #`(declare-all-tags tag-name→stx-name/alist - #,@tag-names-no-duplicates)) - - (call-declare-all-tags tag-name→stx-name/alist)] - -This list of tag names is the one remembered by -“@code{remember-lib.rkt}” with duplicate entries removed: - -@CHUNK[ - (define-for-syntax tag-names-no-duplicates - (remove-duplicates (get-remembered 'variant)))] - -Finally, we define @tc[with-tag-name→stx-name], a helper -macro which accesses the structure identifier for a given -tag name, checking whether the tag name has been remembered -already: - -@chunk[ - (begin-for-syntax - (define-syntax-rule (with-tag-name→stx-name - (stx-name tag-name fallback error-stx) - . body) - (if (check-remember-all 'variant tag-name) - (with-syntax ([stx-name (cdr (assoc (syntax->datum - (datum->syntax #f tag-name)) - tag-name→stx-name/alist))]) - . body) - (remember-all-errors2 fallback tag-name))))] - -@section{@racket[constructor]} - -We define the @tc[constructor] macro which acts as a type, -a match expander, and a procedure returning a tagged -instance: - -@chunk[ - (define-multi-id constructor - #:type-expander - #:match-expander - #:call )] - -@chunk[ - (check-equal?: (Tagged-value - (ann (constructor a 1 "x") - (constructor a Number String))) - (list 1 "x")) ;; TODO: test that the tag is 'a - (check-equal?: (Tagged-value - (ann (constructor b) - (constructor b))) - (list)) ;; TODO: test that the tag is 'b - (check-equal?: (Tagged-value - (ann (constructor c 'd) - (constructor c Symbol))) - 'd) ;; TODO: test that the tag is 'c - (check-equal?: (ann (constructor c 2 "y") - (constructor c Number String)) - (constructor c 2 "y")) - (check-not-equal?: (constructor d 2 "y") - (constructor d 2 "y" 'z)) - (check-not-equal?: (constructor e 2 "y") - (constructor F 2 "y"))] - -@subsection{Type-expander} - -@CHUNK[ - (λ/syntax-parse (_ tag:id . (~or (T₀:expr) (Tᵢ:expr …))) - (with-tag-name→stx-name (stx-name #'tag #'please-recompile stx) - (quasitemplate - (stx-name (?? T₀ (List Tᵢ …))))))] - -@subsection{Predicate} - -@CHUNK[ - (define-syntax (Tagged-predicate? stx) - (syntax-case stx () - [(_ tag v) - #'((Tagged-predicate? tag) v)] - [(_ tag) - ;; make-predicate works for polymorphic structs when - ;; instantiating them with Any. - (with-tag-name→stx-name - (stx-name #'tag (syntax/loc #'tag please-recompile) stx) - #`(make-predicate (stx-name Any)))] - [(_) - #'(make-predicate (Tagged Any))]))] - -@subsection{Match-expander} - -@chunk[ - (λ/syntax-parse (_ tag:id . (~or (pat₀:expr) (patᵢ:expr …))) - (template - (and (? (Tagged-predicate? tag)) - (app Tagged-value (?? pat₀ (list patᵢ …))))))] - -@subsection{Actual constructor} - -@CHUNK[ - (λ/syntax-parse (_ tag:id value:expr …) - (define/with-syntax (arg …) (generate-temporaries #'(value …))) - (define/syntax-parse (~or (arg₀) (argᵢ …)) #'(arg …)) - (define/with-syntax (T …) (generate-temporaries #'(value …))) - (with-tag-name→stx-name - (stx-name #'tag (syntax/loc #'tag please-recompile) stx) - (template - ((λ #:∀ (T …) ([arg : T] …) - : (constructor tag T …) - (stx-name (?? arg₀ (list argᵢ …)))) - value …))))] - -@section{@racket[define-variant]} - -In @tc[define-variant], we only define the type (which is the union of all the -possible constructors. We don't define the constructors, for two reasons: the -same @tc[constructor]s could appear in several variants, so we would define them -twice, and it is likely that a constructor will have the same identifier as an -existing variable or function. - -@CHUNK[ - (define-syntax/parse (define-variant name [tag:id type:expr …] … - (~maybe #:? name?)) - (define/with-syntax default-name? (format-id #'name "~a?" #'name)) - (define-temp-ids "pat" ((type …) …)) - (if (andmap (λ (t) (check-remember-all 'variant t)) - (syntax->list #'(tag …))) - (let () - (define/with-syntax (stx-name …) - (stx-map (λ (t) - (cdr (assoc (syntax->datum (datum->syntax #f t)) - tag-name→stx-name/alist))) - #'(tag …))) - (quasitemplate - (begin - (define-type name (U (constructor tag type …) …)) - (: (?? name? default-name?) - (→ Any Boolean : - #:+ (or (stx-name Any) …) - #:- (and (! (stx-name Any)) …))) - (define ((?? name? default-name?) x) - (or (Tagged-predicate? tag x) …))))) - (stx-map (λ (t) - (remember-all-errors2 (syntax/loc t #'please-recompile) - t)) - #'(tag …))))] - -@chunk[ - (define-variant v1 [x Number String] [y String Number] [z Number String]) - (check-equal?: (ann (constructor x 1 "a") - (U [constructor w Number String] - [constructor x Number String] - [constructor y String Number])) - (constructor x 1 "a")) - (check-equal?: (constructor x 1 "a") - (constructor x 1 "a")) - (check-equal?: (ann (constructor x 1 "a") v1) - (constructor x 1 "a")) - (check-equal?: (ann (constructor x 1 "a") v1) - (ann (constructor x 1 "a") v1)) - (check-not-equal?: (ann (constructor x 2 "b") v1) - (ann (constructor y "b" 2) v1)) - (check-not-equal?: (ann (constructor x 3 "c") v1) - (ann (constructor z 3 "c") v1))] - -This makes pattern-matching more verbose, though, since we have to specify -@tc[(variant tag pat …)] each time, instead of just @tc[(tag pat …)]. I -don't really know how to solve that. It should be noted that constructors are -likely to have names starting with a capital letter, so maybe this reduces the -number of name collisions. - @section{@racket[tagged]} -@CHUNK[ - (define-multi-id tagged - #:type-expander - (λ/syntax-parse (_ tag:id . structure-type) - #`(constructor tag #,(syntax/loc #'structure-type - (structure . structure-type)))) - #:match-expander - (λ/syntax-parse (_ tag:id . structure-pat) - #`(constructor tag #,(syntax/loc #'structure-pat - (structure . structure-pat)))) - #:call ;; TODO: clean this up a bit, and explain it. - (λ/syntax-parse - (~and (_ (~and (~seq disambiguate …) (~or (~seq #:instance) - (~seq #:constructor) - (~seq))) - tag:id . fields) - (~parse (sa:structure-args-stx-class) - #'(disambiguate … . fields))) - (define-temp-ids "~a/TTemp" (sa.field …)) - (define-temp-ids "~a/arg" (sa.field …)) - (define/with-syntax c - (if (attribute sa.type) - #`(λ ([sa.field/arg : sa.type] …) - : (constructor tag #,(syntax/loc #'fields - (structure [sa.field sa.type] …))) - (constructor tag - #,(syntax/loc #'fields - (structure #:instance - [sa.field : sa.type - sa.field/arg] - …)))) - #`(λ #:∀ (sa.field/TTemp …) ([sa.field/arg : sa.field/TTemp] …) - : (constructor tag #,(syntax/loc #'fields - (structure [sa.field sa.field/TTemp] - …))) - (constructor tag - #,(syntax/loc #'fields - (structure #:instance - [sa.field sa.field/arg] …)))))) - (if (attribute sa.value) - #'(c sa.value …) - #'c)))] - -@CHUNK[ - (define-multi-id any-tagged - #:type-expander - (λ/syntax-parse (_ . structure-type) - #'(Tagged (structure . structure-type))) - ;; This would require each tag struct to contain a field with its - ;; tag name. We'll implement it if we need that kind of reflection. - #| - #:match-expander - (λ/syntax-parse (_ tag-pat:id . structure-pat) - #`(any-constructor (? symbol? tag-pat:id) - #,(syntax/loc #'structure-pat - (structure . structure-pat))))|#)] - -@chunk[ - (check-equal?: (match (ann (tagged foo [x "o"] [y 3] [z 'z]) - (tagged foo - [x String] - [z 'z] - [y Fixnum])) - [(tagged foo z x y) (list z y x)]) - '(z 3 "o"))] - @section{@racket[define-tagged]} @chunk[ @@ -615,11 +292,8 @@ the uninterned @tc[tag] either). Tagged-value constructor define-variant - tagged - define-tagged define-private-tagged - define-private-constructor - any-tagged) + define-private-constructor) diff --git a/graph-lib/graph/variant2.lp2.rkt b/graph-lib/graph/variant2.lp2.rkt new file mode 100644 index 0000000..15f509b --- /dev/null +++ b/graph-lib/graph/variant2.lp2.rkt @@ -0,0 +1,158 @@ +#lang scribble/lp2 +@(require "../lib/doc.rkt") +@doc-lib-setup + +@title[#:style manual-doc-style]{Algebaraic Data Types: Variant} + +@(table-of-contents) + +@section{Introduction} + +For convenience, we write a @tc[variant] form, which is a +thin wrapper against @tc[(U (~or constructor tagged) …)]. + +@section{@racket[variant]} + +In @tc[define-variant], we only define the type (which is +the union of all the possible constructors. We do not bind +identifiers for the constructors, for two reasons: the same +@tc[constructor]s could appear in several variants, so we +would define them twice, and it is likely that a constructor +will have the same identifier as an existing variable or +function. + +@chunk[ + (begin-for-syntax + (define-syntax-class constructor-or-tagged + (pattern [constructor-name:id . (~or ([field:id C:colon type:expr] …) + (type:expr …))])))] + +@chunk[ + (define-type-expander (variant stx) + (syntax-parse stx + [(_ :constructor-or-tagged …) + (template + (U (?? (tagged constructor-name [field C type] …) + (constructor constructor-name type …)) + …))]))] + +@section{Predicate} + +@chunk[ + (define-syntax/parse (variant? :constructor-or-tagged …) + (template + (λ (v) (or (?? ((tagged? constructor-name field …) v) + (constructor? constructor-name v)) + …))))] + +@section{@racket[define-variant]} + +@chunk[ + (define-syntax/parse + (define-variant variant-name + (~optkw #:debug) + (~maybe #:? name?) + (~maybe #:match variant-match) + (~and constructor-or-tagged :constructor-or-tagged) …) + (define/with-syntax default-name? (format-id #'name "~a?" #'name)) + (define/with-syntax default-match (format-id #'name "~a-match" #'name)) + (define-temp-ids "pat" ((type …) …)) + (define-temp-ids "match-body" (constructor-name …)) + (template/debug debug + (begin + (define-type variant-name + (variant [constructor-name (?? (?@ [field C type] …) + (?@ type …))] + …)) + (define-syntax (?? variant-match default-match) + (syntax-rules (constructor-name … (?? (?@ field …)) …) + [(_ v + [(constructor-name (?? (?@ [field pat] …) + (pat …))) + . match-body] + …) + (match v + (?? [(tagged constructor-name [field pat] …) . match-body] + [(constructor constructor-name pat …) . match-body]) + …)])) + (define-multi-id (?? name? default-name?) + #:else + #'(variant? constructor-or-tagged …)))) + #| + (if (andmap (λ (t) (check-remember-all 'variant t)) + (syntax->list #'(tag …))) + (let () + (define/with-syntax (stx-name …) + (stx-map (λ (t) + (cdr (assoc (syntax->datum (datum->syntax #f t)) + tag-name→stx-name/alist))) + #'(tag …))) + (quasitemplate + (begin + (define-type name (U (constructor tag type …) …)) + (: (?? name? default-name?) + (→ Any Boolean : + #:+ (or (stx-name Any) …) + #:- (and (! (stx-name Any)) …))) + (define ((?? name? default-name?) x) + (or (Tagged-predicate? tag x) …))))) + (stx-map (λ (t) + (remember-all-errors2 (syntax/loc t #'please-recompile) + t)) + #'(tag …)))|#)] + +@section{Tests} + +@chunk[ + (define-variant v1 [x Number String] [y String Number] [z Number String]) + (check-equal?: (ann (constructor x 1 "a") + (U [constructor w Number String] + [constructor x Number String] + [constructor y String Number])) + (constructor x 1 "a")) + (check-equal?: (constructor x 1 "a") + (constructor x 1 "a")) + (check-equal?: (ann (constructor x 1 "a") v1) + (constructor x 1 "a")) + (check-equal?: (ann (constructor x 1 "a") v1) + (ann (constructor x 1 "a") v1)) + (check-not-equal?: (ann (constructor x 2 "b") v1) + (ann (constructor y "b" 2) v1)) + (check-not-equal?: (ann (constructor x 3 "c") v1) + (ann (constructor z 3 "c") v1))] + +@section{Conclusion} + +@chunk[<*> + (begin + (module main typed/racket + (require (for-syntax racket/list + syntax/parse + syntax/parse/experimental/template + racket/syntax + (submod "../lib/low.rkt" untyped)) + "../lib/low.rkt" + "../type-expander/multi-id.lp2.rkt" + "../type-expander/type-expander.lp2.rkt" + "constructor.lp2.rkt" + "structure.lp2.rkt") + + (provide variant + variant? + define-variant) + + + + + ) + + (require 'main) + (provide (all-from-out 'main)) + + (module* test typed/racket + (require (submod "..") + "constructor.lp2.rkt" + "../lib/low.rkt" + "../type-expander/type-expander.lp2.rkt") + + ))] diff --git a/graph-lib/lib/low/todo.rkt b/graph-lib/lib/low/todo.rkt new file mode 100644 index 0000000..080967b --- /dev/null +++ b/graph-lib/lib/low/todo.rkt @@ -0,0 +1,15 @@ +#lang racket + +(module m racket + (require syntax/parse + syntax/parse/experimental/template) + (provide (rename-out [template syntax] + [quasitemplate quasisyntax]) + (all-from-out syntax/parse + syntax/parse/experimental/template))) + +(require 'm) + +(syntax-parse #'(a b) + [(x (~optional y) z) + #'(x (?? y 1) z)]) \ No newline at end of file