From 41f7dc0f508ff0b25df3e3d6b8444933f14b8c35 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Thu, 27 Apr 2017 22:54:34 +0200 Subject: [PATCH] Squashed commits. --- .gitignore | 6 + .gitmodules | 0 .travis.yml | 69 + LICENSE | 27 + README.md | 66 + base.rkt | 11 + base/lang/reader.rkt | 2 + dbg.rkt | 8 + expander.rkt | 11 + identifiers.rkt | 58 + info.rkt | 25 + lang.rkt | 1 + lang/main.rkt | 11 + lang/reader.rkt | 2 + licenses/bsd.txt | 19 + licenses/lgpl-3.0--license.txt | 165 ++ main.rkt | 7 + more-expanders.hl.rkt | 262 +++ parameterize-lexical-context.rkt | 146 ++ scribblings/deprecated-colon.scrbl | 23 + .../type-expander-implementation.scrbl | 12 + scribblings/type-expander.scrbl | 844 +++++++ test/base-lang-test-1.rkt | 5 + test/base-lang-test-2.rkt | 7 + test/base-lang-test-3.rkt | 5 + test/lang-test-1.rkt | 5 + test/lang-test-2.rkt | 7 + test/lang-test-3.rkt | 5 + test/readme.rkt | 20 + test/type-expander-test.rkt | 746 +++++++ type-expander.hl.rkt | 1977 +++++++++++++++++ utils.rkt | 13 + 32 files changed, 4565 insertions(+) create mode 100644 .gitignore create mode 100644 .gitmodules create mode 100644 .travis.yml create mode 100644 LICENSE create mode 100644 README.md create mode 100644 base.rkt create mode 100644 base/lang/reader.rkt create mode 100644 dbg.rkt create mode 100644 expander.rkt create mode 100644 identifiers.rkt create mode 100644 info.rkt create mode 120000 lang.rkt create mode 100644 lang/main.rkt create mode 100644 lang/reader.rkt create mode 100644 licenses/bsd.txt create mode 100644 licenses/lgpl-3.0--license.txt create mode 100644 main.rkt create mode 100644 more-expanders.hl.rkt create mode 100644 parameterize-lexical-context.rkt create mode 100644 scribblings/deprecated-colon.scrbl create mode 100644 scribblings/type-expander-implementation.scrbl create mode 100644 scribblings/type-expander.scrbl create mode 100644 test/base-lang-test-1.rkt create mode 100644 test/base-lang-test-2.rkt create mode 100644 test/base-lang-test-3.rkt create mode 100644 test/lang-test-1.rkt create mode 100644 test/lang-test-2.rkt create mode 100644 test/lang-test-3.rkt create mode 100644 test/readme.rkt create mode 100644 test/type-expander-test.rkt create mode 100644 type-expander.hl.rkt create mode 100644 utils.rkt diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..adfb974 --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +*~ +\#* +.\#* +.DS_Store +compiled +/doc/ \ No newline at end of file diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..e69de29 diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000..7664612 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,69 @@ +language: c + +# Based from: https://github.com/greghendershott/travis-racket + +# Optional: Remove to use Travis CI's older infrastructure. +sudo: false + +env: + global: + # Supply a global RACKET_DIR environment variable. This is where + # Racket will be installed. A good idea is to use ~/racket because + # that doesn't require sudo to install and is therefore compatible + # with Travis CI's newer container infrastructure. + - RACKET_DIR=~/racket + matrix: + # Supply at least one RACKET_VERSION environment variable. This is + # used by the install-racket.sh script (run at before_install, + # below) to select the version of Racket to download and install. + # + # Supply more than one RACKET_VERSION (as in the example below) to + # create a Travis-CI build matrix to test against multiple Racket + # versions. + #- RACKET_VERSION=6.0 + #- RACKET_VERSION=6.1 + #- RACKET_VERSION=6.1.1 + # Dependency "custom-load" does not work with 6.2 and 6.3 + #- RACKET_VERSION=6.2 + # Collection scribble/example is not available yet in 6.3 + #- RACKET_VERSION=6.3 + # Scribble bug in 6.4 which got fixed in 6.5 + #- RACKET_VERSION=6.4 + - RACKET_VERSION=6.5 + - RACKET_VERSION=6.6 + - RACKET_VERSION=HEAD + +matrix: + allow_failures: + # No support for https://github.com/user/repo.git#commit-hash in info.rkt "deps" + - env: RACKET_VERSION=6.0 + - env: RACKET_VERSION=6.1 + - env: RACKET_VERSION=6.1.1 + - env: RACKET_VERSION=6.2 + - env: RACKET_VERSION=6.3 + fast_finish: true + +before_install: +- git clone https://github.com/greghendershott/travis-racket.git ~/travis-racket +- cat ~/travis-racket/install-racket.sh | bash # pipe to bash not sh! +- export PATH="${RACKET_DIR}/bin:${PATH}" #install-racket.sh can't set for us + +install: +- raco pkg install -j 1 --deps search-auto + +before_script: + +# Here supply steps such as raco make, raco test, etc. You can run +# `raco pkg install --deps search-auto type-expander` to install any required +# packages without it getting stuck on a confirmation prompt. +script: + - raco test -p type-expander + - raco setup --check-pkg-deps --no-zo --no-launcher --no-install --no-post-install --no-docs --pkgs type-expander + - raco pkg install --deps search-auto doc-coverage + - if $RACKET_VERSION != "6.5" -a $RACKET_VERSION != "6.6"; then raco doc-coverage type-expander; fi + +after_success: + - raco pkg install --deps search-auto cover cover-coveralls + - raco pkg install --deps search-auto + # TODO: raco cover doesn't support having a "-s " option, to run the entire module in addition to the specified submodules + - raco cover -b -s doc -s test -s main -f coveralls -d $TRAVIS_BUILD_DIR/coverage . diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..158d173 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +This software was initially written as part of a project at Cortus, S.A.S. which +can be reached at 97 Rue de Freyr, 34000 Montpellier, France. + +This software may contain a few pieces of code copied from typed/racket +https://github.com/racket/typed-racket (mostly the syntax-parse syntax classes +for the various overloaded forms) and is therefore licensed under the +GNU Lesser General Public License (LGPL). + + +This package is distributed under the GNU Lesser General Public +License (LGPL). This means that you can link this package into proprietary +applications, provided you follow the rules stated in the LGPL. You +can also modify this package; if you distribute a modified version, +you must distribute it under the terms of the LGPL, which in +particular means that you must release the source code for the +modified software. See http://www.gnu.org/copyleft/lesser.html +for more information. + +under the BSD license, at your option. Both licenses can be found in the +`licenses/` folder. + +This double-licensing has been chosen in order to make it possible to integrate +the type-expander library with Typed/Racket +(https://github.com/racket/typed-racket) and/or Racket +(https://github.com/racket/racket), which are both under the LGPL license, as +well as integrate the graph library with the Nanopass Compiler Framework +(https://github.com/akeep/nanopass-framework), which is under the BSD license. \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..9614f67 --- /dev/null +++ b/README.md @@ -0,0 +1,66 @@ +[![Build Status,](https://img.shields.io/travis/jsmaniac/type-expander/master.svg)](https://travis-ci.org/jsmaniac/type-expander) +[![Coverage Status,](https://img.shields.io/coveralls/jsmaniac/type-expander/master.svg)](https://coveralls.io/github/jsmaniac/type-expander) +[![Build Stats,](https://img.shields.io/badge/build-stats-blue.svg)](http://jsmaniac.github.io/travis-stats/#jsmaniac/type-expander) +[![Online Documentation,](https://img.shields.io/badge/docs-online-blue.svg)](http://docs.racket-lang.org/type-expander/) +[![Maintained as of 2017.](https://img.shields.io/maintenance/yes/2017.svg)](https://github.com/jsmaniac/type-expander/issues) + +Type-expander +============= + +This project is written for +[Typed/Racket](https://docs.racket-lang.org/ts-guide/) using Literate +Programming. See the “[Implementation of the type expander +library](http://docs.racket-lang.org/type-expander/)” part of the [online +documentation](http://docs.racket-lang.org/type-expander/) if you want to dig +into the source. + +This library enhances typed/racket with type expanders, which are special +macros that can appear where a type would normally be expected, and must +expand to a type. Type expanders are to types what match expanders are to +match patterns. It is based on Asumu Takikawa's [type +expanders](https://github.com/racket/racket/compare/master...takikawa:tr-type-expander) +(see also his [original pull request +here](https://github.com/racket/racket/pull/604)). Asumu Takikawa's work +attempted to integrate type expanders directly into Typed/Racket. This +project instead implements type expanders as a library and works without any +modification of the core Typed/Racket codebase. This shows the extensibility +of Typed/Racket thanks to macros, and could serve as the basis for other +projects which need to alter the manner in which Typed/Racket handles types. + +Installation +============ + +``` +raco pkg install --deps search-auto type-expander +``` + +Usage example +============= + +The `type-expander` is enabled by simply requiring the `type-expander` module +in a `typed/racket` program. + + #lang typed/racket + (require type-expander) + +For example, one can write the `(HomogeneousList n t)` type-expander, which +expands to the type for a list of `n` elements of type `t`: + + (require (for-syntax syntax/parse racket/list)) + (define-type-expander (HomogeneousList stx) + (syntax-parse stx + [(_ t:expr n:nat) + #`(List #,@(map (λ (x) #'t) + (range (syntax-e #'n))))])) + +It can then be used wherever a regular type is usually expected: + + (: five-strings (→ String (HomogeneousList String 5))) + (define (five-strings x) + (list x "a" "b" "c" "d")) + + (five-strings "hello") + ;; => '("hello" "a" "b" "c" "d") + + (ann (five-strings "moon") (HomogeneousList String 5)) + ;; => '("moon" "a" "b" "c" "d") diff --git a/base.rkt b/base.rkt new file mode 100644 index 0000000..46908f7 --- /dev/null +++ b/base.rkt @@ -0,0 +1,11 @@ +#lang racket/base + +(require racket/require + (subtract-in typed/racket/base type-expander) + type-expander) + +(provide (all-from-out typed/racket/base + type-expander)) + +(module reader syntax/module-reader + type-expander/lang/main) \ No newline at end of file diff --git a/base/lang/reader.rkt b/base/lang/reader.rkt new file mode 100644 index 0000000..2e6216d --- /dev/null +++ b/base/lang/reader.rkt @@ -0,0 +1,2 @@ +(module reader syntax/module-reader + type-expander/base) \ No newline at end of file diff --git a/dbg.rkt b/dbg.rkt new file mode 100644 index 0000000..3cc5c17 --- /dev/null +++ b/dbg.rkt @@ -0,0 +1,8 @@ +#lang typed/racket +(require type-expander + (for-syntax racket/list) + (for-syntax type-expander/expander + typed/rackunit + debug-scopes)) + +(debug-type-expander #t) diff --git a/expander.rkt b/expander.rkt new file mode 100644 index 0000000..d418d74 --- /dev/null +++ b/expander.rkt @@ -0,0 +1,11 @@ +#lang racket +(require (submod "type-expander.hl.rkt" expander) + (for-template (submod "type-expander.hl.rkt" main)) + syntax/parse) +(provide prop:type-expander + expand-type + apply-type-expander + type + stx-type/c + type-expand! + colon) diff --git a/identifiers.rkt b/identifiers.rkt new file mode 100644 index 0000000..23a767f --- /dev/null +++ b/identifiers.rkt @@ -0,0 +1,58 @@ +#lang typed/racket + +(require (for-syntax racket/syntax)) + +(define-syntax-rule (provide-id id) + (begin + (define-syntax (id stx) + (raise-syntax-error 'id + (format "Type expander form “~a” cannot be used as an expression" + 'id) + stx)) + (provide id))) + +(define-syntax-rule (provide-ids id ...) (begin (provide-id id) ...)) + +(provide-ids Let Letrec Λ ...* No-Expand) + +;; Define a mutable implementation for new-:, circumvent the fact that +;; typed/racket wraps macros with a contract. +;; +;; Technique from: +;; +;; https://github.com/racket/typed-racket/issues/329#issuecomment-205060192 + +(define-syntax (provide-mutable-id stx) + (syntax-case stx () + [(_ short-id) + (with-syntax ([id (format-id #'short-id "new-~a" #'short-id)] + [id-set-impl (format-id #'short-id + "set-~a-impl!" + #'short-id)]) + #'(begin + (provide id id-set-impl) + + (define-for-syntax (id-impl-orig stx) + (raise-syntax-error ': + (format "Implementation for ~a was not loaded!" + 'short-id) + stx)) + + (define-for-syntax id-impl (box id-impl-orig)) + + (define-syntax (id stx) + ((unbox id-impl) stx)) + + (define-syntax-rule (id-set-impl impl) + (begin-for-syntax + (when (eq? (unbox id-impl) id-impl-orig) + (set-box! id-impl impl))))))])) + +(define-syntax-rule (provide-mutable-ids id ...) + (begin (provide-mutable-id id) ...)) + +(provide-mutable-ids : + ;; The class-related IDs need to also work as types. + ;field + ;super-new + ) \ No newline at end of file diff --git a/info.rkt b/info.rkt new file mode 100644 index 0000000..48504a2 --- /dev/null +++ b/info.rkt @@ -0,0 +1,25 @@ +#lang info +(define collection "type-expander") +(define deps '("base" + "rackunit-lib" + "scribble-lib" + "typed-racket-lib" + "typed-racket-more" + "hyper-literate" + "auto-syntax-e" + "debug-scopes")) +(define build-deps '("scribble-lib" + "racket-doc" + "typed-racket-more" + "typed-racket-doc" + "scribble-enhanced" + ;; Just for a link to the library inside the documentation. + ;; Can be removed and change the link + ;; in type-expander.hl.rkt to + ;; http://docs.racket-lang.org/mutable-match-lambda/ + "mutable-match-lambda")) +(define scribblings '(("scribblings/type-expander.scrbl" () ("typed-racket")) + ("scribblings/type-expander-implementation.scrbl" (multi-page) ("typed-racket")))) +(define pkg-desc "Description Here") +(define version "1.0") +(define pkg-authors '(|Georges Dupéron|)) diff --git a/lang.rkt b/lang.rkt new file mode 120000 index 0000000..cb5b5a7 --- /dev/null +++ b/lang.rkt @@ -0,0 +1 @@ +lang/main.rkt \ No newline at end of file diff --git a/lang/main.rkt b/lang/main.rkt new file mode 100644 index 0000000..8449d6d --- /dev/null +++ b/lang/main.rkt @@ -0,0 +1,11 @@ +#lang racket/base + +(require racket/require + (subtract-in typed/racket type-expander) + type-expander) + +(provide (all-from-out typed/racket + type-expander)) + +(module reader syntax/module-reader + type-expander/lang/main) \ No newline at end of file diff --git a/lang/reader.rkt b/lang/reader.rkt new file mode 100644 index 0000000..54bdc2b --- /dev/null +++ b/lang/reader.rkt @@ -0,0 +1,2 @@ +(module reader syntax/module-reader + type-expander/lang) \ No newline at end of file diff --git a/licenses/bsd.txt b/licenses/bsd.txt new file mode 100644 index 0000000..21a8f5c --- /dev/null +++ b/licenses/bsd.txt @@ -0,0 +1,19 @@ +Copyright (c) 2000-2015 Dipanwita Sarkar, Andrew W. Keep, R. Kent Dybvig, Oscar Waddell + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the "Software"), +to deal in the Software without restriction, including without limitation +the rights to use, copy, modify, merge, publish, distribute, sublicense, +and/or sell copies of the Software, and to permit persons to whom the +Software is furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL +THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +DEALINGS IN THE SOFTWARE. \ No newline at end of file diff --git a/licenses/lgpl-3.0--license.txt b/licenses/lgpl-3.0--license.txt new file mode 100644 index 0000000..65c5ca8 --- /dev/null +++ b/licenses/lgpl-3.0--license.txt @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/main.rkt b/main.rkt new file mode 100644 index 0000000..ea5c83b --- /dev/null +++ b/main.rkt @@ -0,0 +1,7 @@ +#lang typed/racket +(require "type-expander.hl.rkt" + "more-expanders.hl.rkt" + (for-syntax "expander.rkt")) +(provide (all-from-out "type-expander.hl.rkt") + (all-from-out "more-expanders.hl.rkt") + (for-syntax colon)) \ No newline at end of file diff --git a/more-expanders.hl.rkt b/more-expanders.hl.rkt new file mode 100644 index 0000000..1251dd4 --- /dev/null +++ b/more-expanders.hl.rkt @@ -0,0 +1,262 @@ +#lang hyper-literate typed/racket/base #:no-require-lang #:no-auto-require +@; The #:no-require-lang above is needed because type-expander requires +@; from 'main some identifiers (e.g. λ) which conflict with the re-required +@; racket/base. With this option, we loose arrows in DrRacket for the +@; built-ins in this file, and have otherwise no adverse effects. +@(require scribble-enhanced/doc) +@doc-lib-setup + +@(module orig-ids racket/base + (require scribble/manual + (for-label typed/racket/base)) + (provide (all-defined-out)) + (define orig:: (racket :)) + (define orig:let (racket let)) + (define orig:→AnyBoolean:Integer (racket (→ Any Boolean : Integer)))) +@(require 'orig-ids) + +@(unless-preexpanding + (require racket/require + (for-label "type-expander.hl.rkt" + (submod "type-expander.hl.rkt" expander) + (subtract-in typed/racket/base + "type-expander.hl.rkt") + (subtract-in racket + typed/racket/base + "type-expander.hl.rkt") + typed/racket/unsafe + racket/format + racket/syntax + syntax/stx + syntax/parse + syntax/parse/experimental/template + syntax/id-table))) + +@title[#:style manual-doc-style + #:tag "ty-xp-more" + #:tag-prefix "type-expander/ty-xp-more"]{Some example type expanders} + +@(chunks-toc-prefix + '("(lib type-expander/scribblings/type-expander-implementation.scrbl)" + "type-expander/ty-xp-more")) + +@section{Example type expanders: quasiquote and quasisyntax} + +We define type expanders for @racket[quote], @racket[quasiquote], +@racket[syntax] and @racket[quasisyntax]: + +The next four special forms are implemented as type expanders with +@tc[patch-type-expander] because redefining their name (@tc[quote], +@tc[quasiquote], @tc[syntax] and @tc[quasisyntax]) would conflict with +existing identifiers. @racket[patch-type-expander] uses a global persistant +(across modules) for-syntax mutable table, which associates identifiers to +type-expanders. @note{ @racketmodname[typed/racket] works in that way by + associating data (their type) to existing identifiers. The + @racketmodname[mutable-match-lambda] library on the other hand allows adding + behaviour to an identifier after it is defined, but relies on some level of + cooperation from that identifier, which may be less practical for built-in + identifiers like @racket[quote].} Relying on an external data structure to +associate information with identifiers makes it possible to overload the +meaning of @tc[quote] or @tc[curry] when used as a type expander, without +having to alter their original definition. Another option would be to provide +overloaded versions of these identifiers, to shadow those imported by the +@litchar{#lang} module. This would however cause conflicts for @tc[curry] when +@tc[racket/function] is explicitly required (instead of being required +implicitly by @racket[#,hash-lang #,(racketmodname racket)], for example. + +@chunk[ + (patch-type-expander quote + (λ (stx) + (syntax-case stx () + [(_ T) + (expand-quasiquote 'quote 1 #'T)])))] + +@chunk[ + (patch-type-expander quasiquote + (λ (stx) + (syntax-case stx () + [(_ T) + (expand-quasiquote 'quasiquote 1 #'T)])))] + +@chunk[ + (patch-type-expander syntax + (λ (stx) + (syntax-case stx () + [(_ T) + (expand-quasiquote 'syntax 1 #'T)])))] + +@chunk[ + (patch-type-expander quasisyntax + (λ (stx) + (syntax-case stx () + [(_ T) + (expand-quasiquote 'quasisyntax 1 #'T)])))] + +Their implementation is factored out into the @tc[expand-quasiquote] +for-syntax function. It is a reasonably complex showcase of this library's +functionality. @racketmodname[typed/racket] allows the use of @tc[quote] to +describe a type which contains a single inhabitant, the quoted datum. For +example, @tc[(define-type foo '(a b (1 2 3) c))] declares a type @tc[foo] +which is equivalent to @tc[(List 'a 'b (List 1 2 3) 'c)]. + +We build upon that idea to allow the use of @tc[syntax], +@tc[quasiquote] and @tc[quasisyntax]. Both @tc[syntax] and +@tc[quasisyntax] wrap each s-expression within the quoted +datum with @tc[Syntaxof], which avoids the otherwise tedious +declaration of the type for a piece of syntax. Both +@tc[quasiquote] and @tc[quasisyntax] allow escaping the +quoted datum (using @tc[unquote] and @tc[unsyntax], +respectively). A later version of this library could +support @tc[unquote-splicing] and @tc[unsyntax-splicing]. + +Using this type-expander, one can write +@racketblock[(define-type bar `(a ,Symbol (1 ,(U Number String) 3) c))] +The above declaration gets expanded to: +@racketblock[(define-type bar (List 'a Symbol (List 1 (U Number String) 3) 'c))] + +The implementation of @tc[expand-quasiquote] recursively +traverses the type expression. The @tc[mode] argument +can be one of @tc['quote], @tc['quasiquote], @tc['syntax] or +@tc['quasisyntax]. It is used to determine whether to wrap +parts of the type with @tc[Syntaxof] or not, and to know +which identifier escapes the quoting (@tc[unquote] or +@tc[unsyntax]). The @tc[depth] argument keeps track of the +quoting depth: in Racket @tc[`(foo `(bar ,baz))] is +equivalent to +@tc[(list 'foo (list 'quasiquote (list 'bar (list 'unquote 'baz))))] +(two levels of @tc[unquote] are required to escape the two +levels of @tc[quasiquote]), so we want the type to be +@tc[(List 'foo (List 'quasiquote (List 'bar (List 'unquote 'baz))))]. + +@CHUNK[ + (define (list*->list l) + (if (pair? l) + (cons (car l) (list*->list (cdr l))) + (list l))) + (define (expand-quasiquote mode depth stx) + (define (wrap t) + (if (or (eq? mode 'syntax) (eq? mode 'quasisyntax)) + #`(Syntaxof #,t) + t)) + (define (wrap-quote t) + (if (or (eq? mode 'syntax) (eq? mode 'quasisyntax)) + #`(Syntaxof (No-Expand (quote #,t))) + #`(No-Expand (quote #,t)))) + (define expand-quasiquote-rec (curry expand-quasiquote mode depth)) + (syntax-parse stx + [((~literal quote) T) + (wrap #`(List #,(wrap-quote #'quote) + #,(expand-quasiquote-rec #'T)))] + [((~literal quasiquote) T) + (wrap #`(List #,(wrap-quote #'quasiquote) + #,(if (eq? mode 'quasiquote) + (expand-quasiquote mode (+ depth 1) #'T) + (expand-quasiquote-rec #'T))))] + [((~literal unquote) T) + (if (eq? mode 'quasiquote) + (if (= depth 1) + (expand-type #'T) ;; TODO: applicable? !!!!!!!!!!!!!!!!!!!!!!!!!!!! + (wrap #`(List #,(wrap-quote #'unquote) + #,(expand-quasiquote mode (- depth 1) #'T)))) + (wrap #`(List #,(wrap-quote #'unquote) + #,(expand-quasiquote-rec #'T))))] + [((~literal syntax) T) + (wrap #`(List #,(wrap-quote #'quote) + #,(expand-quasiquote-rec #'T)))] + [((~literal quasisyntax) T) + (wrap #`(List #,(wrap-quote #'quasisyntax) + #,(if (eq? mode 'quasisyntax) + (expand-quasiquote mode (+ depth 1) #'T) + (expand-quasiquote-rec #'T))))] + [((~literal unsyntax) T) + (if (eq? mode 'quasisyntax) + (if (= depth 1) + (expand-type #'T) ;; TODO: applicable? !!!!!!!!!!!!!!!!!!!!!!!!!!!! + (wrap #`(List #,(wrap-quote #'unsyntax) + #,(expand-quasiquote mode (- depth 1) #'T)))) + (wrap #`(List #,(wrap-quote #'unsyntax) + #,(expand-quasiquote-rec #'T))))] + ;; TODO For lists, we should consider the cases where syntax-e gives + ;; a pair vs the cases where it gives a list. + [(T . U) + #:when (syntax? (cdr (syntax-e stx))) + (wrap #`(Pairof #,(expand-quasiquote-rec #'T) + #,(expand-quasiquote-rec #'U)))] + [() (wrap #'Null)] + [(T ...) + #:when (list? (syntax-e stx)) + (wrap #`(List #,@(stx-map expand-quasiquote-rec #'(T ...))))] + [whole + #:when (pair? (syntax-e #'whole)) + #:with (T ... S) (list*->list (syntax-e #'whole)) + (wrap #`(List* #,@(stx-map expand-quasiquote-rec #'(T ... S))))] + [#(T ...) + (wrap #`(Vector #,@(stx-map expand-quasiquote-rec #'(T ...))))] + [#&T (wrap #`(Boxof #,(expand-quasiquote-rec #'T)))] + ; TODO: Prefab with #s(prefab-struct-key type ...) + [T:id (wrap #'(No-Expand (quote T)))] + [T #:when (string? (syntax-e #'T)) (wrap #'T)] + [T:number (wrap #'T)] + [T:keyword (wrap #'(No-Expand (quote T)))] + [T:char (wrap #'T)] + [#t (wrap #'True)] + [#t (wrap #'False)] + [_ (raise-syntax-error 'expand-quasiquoste + (format "Unknown quasiquote contents: ~a" stx) + stx)]))] + +@section{Implementation of the @racket[Let*] special type expander form} + +The @racket[Let*] special form is implemented in terms of @racket[Let], +binding each variable in turn: + +@chunk[ + (define-type-expander (Let* stx) + (syntax-case stx () + [(me ([var val] . rest) τ) + (with-syntax ([L (datum->syntax #'here 'Let #'me #'me)] + [L* (datum->syntax #'here 'Let* #'me #'me)]) + #'(L ([var val]) + (L* rest + τ)))] + [(_ () τ) #'τ]))] + +@section{curry} + +The @tc[curry] special form takes a type expander (or a polymorphic type) and +some arguments. The whole form should appear in the first position of its +containing form, which contains more arguments, or be bound with a +@racket[Let] or @racket[Letrec]. @tc[curry] appends the arguments in the outer +form to the whole inner form, and expands the result. This really should be +implemented as a type expander so that the partially-applied expander or +polymorphic type can be bound using @tc[Let], for example, but for now it is +hardcoded here. + +@chunk[ + (patch-type-expander curry + (λ (stx) + (syntax-case stx () + [(_ T Arg1 ...) + #'(Λ (_ . Args2) #'(T Arg1 ... . Args2))])))] + +@section{Putting it all together} + +@chunk[<*> + (require "type-expander.hl.rkt" + "identifiers.rkt" + racket/function + (for-syntax racket/base + (only-in racket/base [... …]) + (submod "type-expander.hl.rkt" expander) + syntax/parse + syntax/stx + racket/function + racket/match)) + (provide Let*) + + + + (begin-for-syntax ) + + + ] \ No newline at end of file diff --git a/parameterize-lexical-context.rkt b/parameterize-lexical-context.rkt new file mode 100644 index 0000000..ecb8730 --- /dev/null +++ b/parameterize-lexical-context.rkt @@ -0,0 +1,146 @@ +#lang racket + +(require (for-template racket/base) + syntax/parse + syntax/id-table + (for-syntax syntax/parse + racket/syntax + syntax/parse/experimental/template) + debug-scopes) + +(provide with-bindings + with-rec-bindings + tl-redirections + start-tl-redirections + f-start-tl-redirections + binding-table-find-best + binding-table-set! + make-binding-table) + +(struct binding-table-struct (val)) + +(define/contract tl-redirections + (parameter/c (or/c binding-table-struct? #f)) + (make-parameter #f)) + +(define (make-binding-table) + (-> binding-table-struct?) + (binding-table-struct (make-hasheq))) + +(define/contract (binding-table-set! table id value) + (-> binding-table-struct? identifier? any/c void?) + (let ([group (hash-ref! (binding-table-struct-val table) + (syntax-e id) + (make-bound-id-table))]) + (when (dict-has-key? group id) + (raise-syntax-error + 'type-expander + "Attempted to re-bind the same identifier with the same scopes" + id)) + (bound-id-table-set! group id value))) + +(define (binding-table-find-best table id fallback) + (-> binding-table-struct? identifier? (or/c procedure? any/c) void?) + (define (scopes-of i) + (list->set (map (λ (v) (vector-ref v 0)) + (hash-ref (syntax-debug-info i) 'context)))) + (define scopes-of-id (scopes-of id)) + (let* ([group (hash-ref (binding-table-struct-val table) + (syntax-e id) + (λ () (make-bound-id-table)))] + [candidates (filter (λ (other) + (subset? (car other) scopes-of-id)) + (bound-id-table-map group + (λ (a b) + (list (scopes-of a) a b))))]) + (if (= 0 (length candidates)) + (if (procedure? fallback) + (fallback) + fallback) + (let* ([best-candidate (argmax (λ (c) (set-count (car c))) + candidates)]) + (for ([c candidates]) + (unless (subset? (car c) (car best-candidate)) + (raise-syntax-error 'type-expander + (format "Ambiguous bindings: ~a" + (map (λ (c) (list (cadr c) (car c))) + candidates))))) + (caddr best-candidate))))) + +(define-syntax-rule (start-tl-redirections . rest) + (parameterize ([tl-redirections (or (tl-redirections) + (make-binding-table))]) + . rest)) + +(define-syntax-rule (f-start-tl-redirections f) + (λ l (start-tl-redirections (apply f l)))) + + +(define-syntax with-bindings + (syntax-parser + [(_ [{~or v1:id (v* {~and ooo {~literal ...}})} e/es] x code ...+) + #:with vs (if (attribute ooo) #'(v* ooo) #'(v1)) + #:with es (if (attribute ooo) #'e/es #'(list e/es)) + (template + (let () + (define ctx (make-syntax-introducer)) + (invariant-assertion (λ (ll) (and (list? ll) + (andmap identifier? ll))) + (syntax->list #'vs)) + (for ([binding (in-syntax #'vs)] + [value es]) + (binding-table-set! (tl-redirections) (ctx binding) value)) + (with-syntax ([(vs x) + (ctx #'(vs x))]) + code ...)))])) + +(define-syntax with-rec-bindings + (syntax-parser + [(_ [{~or v1:id (v* {~and ooo {~literal ...}})} func e/es] x code ...+) + #:with vs (if (attribute ooo) #'(v* ooo) #'(v1)) + #:with es (if (attribute ooo) #'(e/es ooo) #'(e/es)) + (template + (let () + (define ctx (make-syntax-introducer)) + (define ctx2 (make-syntax-introducer #t)) + (invariant-assertion (λ (ll) (and (list? ll) + (andmap identifier? ll))) + (syntax->list #'vs)) + (for ([binding (in-syntax #'vs)] + [stx-value (in-syntax #'es)]) + (let ([vvv (func (ctx stx-value))]) + (binding-table-set! (tl-redirections) + (ctx binding) + vvv))) + (with-syntax ([(vs x) + (ctx2 (ctx #'(vs x)))]) + code ...)))])) + +(provide trampoline-eval) +(define trampoline-result (make-parameter #f)) +(define (trampoline-eval code) + (define result 'not-yet-result) + (parameterize ([trampoline-result (λ (v) (set! result v))]) + (local-expand (syntax-local-introduce + #`(let-syntax ([tr ((trampoline-result) #,code)]) + (void))) + 'expression + '())) + result) + + +(module+ test + (require rackunit) + (check-equal? (let () + (define tbl (make-binding-table)) + (define id #'id) + (binding-table-set! tbl id 123) + (define ctx (make-syntax-introducer)) + (binding-table-set! tbl (ctx id) 456) + (define ctx2 (make-syntax-introducer)) + (list (binding-table-find-best tbl id #f) + (binding-table-find-best tbl (ctx id) #f) + (binding-table-find-best tbl (ctx2 id) #f) + (binding-table-find-best tbl (ctx2 (ctx id)) #f) + (binding-table-find-best tbl (ctx (ctx2 id)) #f))) + '(123 456 123 456 456))) \ No newline at end of file diff --git a/scribblings/deprecated-colon.scrbl b/scribblings/deprecated-colon.scrbl new file mode 100644 index 0000000..d96f400 --- /dev/null +++ b/scribblings/deprecated-colon.scrbl @@ -0,0 +1,23 @@ +#lang scribble/manual + +@require[@for-label[type-expander]] + +@(module m racket/base + (require scribble/manual) + (provide e:colon) + (require (for-label type-expander/expander)) + (define e:colon (racket colon))) +@(require 'm) + +@title{Deprecated export of @racket[colon] via @racketmodname[type-expander]} + +@declare-exporting[type-expander] + +@defidform[colon]{ + @deprecated[ + #:what "reprovide" + @list{@e:colon from @racketmodname[type-expander/expander]} + @list{The @e:colon identifier is re-exported for-syntax as @racket[colon] by + @racketmodname[type-expander]. Prefer instead explicitly using + @racket[(require (for-syntax #,(racketmodname type-expander/expander)))], as + the re-export will be removed in future versions.}]} \ No newline at end of file diff --git a/scribblings/type-expander-implementation.scrbl b/scribblings/type-expander-implementation.scrbl new file mode 100644 index 0000000..fdd9854 --- /dev/null +++ b/scribblings/type-expander-implementation.scrbl @@ -0,0 +1,12 @@ +#lang scribble/manual + +@title{Type expander: Implementation} +@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]] + +This library is implemented using literate programming. The implementation +details are presented in the following sections. The user documentation is in +the @other-doc['(lib "type-expander/scribblings/type-expander.scrbl")] document. + +@(table-of-contents) +@include-section[(submod "../type-expander.hl.rkt" doc)] +@include-section[(submod "../more-expanders.hl.rkt" doc)] diff --git a/scribblings/type-expander.scrbl b/scribblings/type-expander.scrbl new file mode 100644 index 0000000..c330fea --- /dev/null +++ b/scribblings/type-expander.scrbl @@ -0,0 +1,844 @@ +#lang scribble/manual + +@title{Type expander library} +@author{@author+email["Georges Dupéron" "georges.duperon@gmail.com"]} + +@defmodule[type-expander + #:use-sources [(lib "type-expander/type-expander.hl.rkt") + (lib "type-expander/more-expanders.hl.rkt")]] + +@require[racket/require + scribble/example + @for-syntax[racket/base] + @for-label[type-expander + type-expander/expander + (subtract-in typed/racket/base + type-expander + type-expander/expander) + (only-in racket/base [... …]) + (prefix-in racket/base: racket/base) + syntax/stx + racket/list + syntax/parse + syntax/parse/experimental/template + auto-syntax-e + debug-scopes]] + +@(require (for-syntax syntax/strip-context + syntax/stx + racket/syntax)) +@(define-syntax (orig stx) + (syntax-case stx () + [(_ name ...) + (with-syntax ([(prefixed ...) + (stx-map (λ (id) (format-id id "orig:~a" id)) + #'(name ...))]) + #`(begin + (module #,(syntax-local-introduce #'orig-module) . + #,(strip-context + #'(racket/base + (require (for-label (only-meta-in 0 (only-in typed/racket + name ...)))) + (require scribble/manual) + (define prefixed @racket[name]) ... + (provide prefixed ...)))) + (require #,(syntax-local-introduce #''orig-module))))])) + +@(orig + class + ;; + define-type + ;; TODO: add all-defined-out in prims.rkt + ;; top-interaction.rkt + :type + :print-type + :query-type/args + :query-type/result + ;; case-lambda.rkt + case-lambda + case-lambda: + pcase-lambda: + ;; (submod "prims-contract.rkt" forms) + require/opaque-type + ;require-typed-struct-legacy + require-typed-struct + ;require/typed-legacy + require/typed + require/typed/provide + require-typed-struct/provide + cast + make-predicate + define-predicate + ;; prims.rkt + define-type-alias + define-new-subtype + define-typed-struct + define-typed-struct/exec + ann + inst + : + define-struct: + define-struct + struct + struct: + λ: + lambda: + lambda + λ + define + let + let* + letrec + let-values + letrec-values + let/cc + let/ec + let: + let*: + letrec: + let-values: + letrec-values: + let/cc: + let/ec: + for + for/list + for/vector + for/hash + for/hasheq + for/hasheqv + for/and + for/or + for/sum + for/product + for/lists + for/first + for/last + for/fold + for* + for*/list + for*/lists + for*/vector + for*/hash + for*/hasheq + for*/hasheqv + for*/and + for*/or + for*/sum + for*/product + for*/first + for*/last + for*/fold + for/set + for*/set + do + do: + with-handlers + define-struct/exec: + define-struct/exec) + +@(define eval-factory + (make-eval-factory (list 'typed/racket 'type-expander))) + +This library is implemented using literate programming. The +implementation details are presented in the +@other-doc['(lib + "type-expander/scribblings/type-expander-implementation.scrbl")] +document. + +It enhances @racketmodname[typed/racket] with +@deftech[#:key "type expander"]{type expanders}, which are +special macros that can appear wherever a regular type is +usually expected, and must expand to a type. Type expanders +are to types what +@tech[#:doc '(lib "scribblings/reference/reference.scrbl") + #:key "match expander"]{ + match expanders} are to @racket[match] patterns. + +It is based on +@hyperlink[(string-append "https://github.com/racket/racket/compare/" + "master...takikawa:tr-type-expander")]{ + Asumu Takikawa's type expanders} (see also his +@hyperlink["https://github.com/racket/racket/pull/604"]{original pull request}). +Asumu Takikawa's work attempted to integrate type expanders +directly into Typed/Racket. This project instead implements +type expanders as a library, which does not need any changes +to the core Typed/Racket codebase. This shows the +extensibility of Typed/Racket thanks to macros, and could +serve as the basis for other projects which need to alter +how Typed/Racket handles types. + +The input for a type expander is the syntax used to call +it, just as the input to a macro is the syntax used to call +it. The output should be a type, which can itself contain +type expanders. + +This library works by shadowing the definitions of +@orig::, @orig:define, @orig:lambda @etc from +@racketmodname[typed/racket] with versions which support +type expanders. + +@section{@(hash-lang) and module languages based on + @racketmodname[type-expander]} + +@subsection{@(hash-lang) combining @racketmodname[type-expander] and + @racketmodname[typed/racket]} + +@defmodulelang[type-expander + #:link-target? #f]{ + The @racket[#,(hash-lang) #,(racketmodname type-expander)] language works like + @racket[#,(hash-lang) #,(racketmodname typed/racket)], but it initially imports + the forms overridden by @racketmodname[type-expander], instead of importing + the original identifiers defined by @racket[typed/racket]. + + This language cannot be used as a module language, instead use + @racketmodname[type-expander/lang] which provides the same bindings.} + +@subsection{Module language combining @racketmodname[type-expander] and + @racketmodname[typed/racket]} + +@defmodulelang[type-expander/lang]{ + This language is equivalent to + @racket[#,(hash-lang) #,(racketmodname type-expander)], but can also be used as + a module language.} + +@subsection{@(hash-lang) and module language combining + @racketmodname[type-expander] and @racketmodname[typed/racket/base]} + +@defmodulelang[type-expander/base]{ + This language is similar to @racketmodname[type-expander/lang], but it + exports the identifiers from @racketmodname[typed/racket/base] instead of + @racket[typed/racket].} + + +@section{Defining new type expanders} + +@defform*[((define-type-expander (name stx) . body) + (define-type-expander name transformer-function)) + #:grammar ([name Identifier] + [stx Identifier] + [transformer-function (expr/c (-> syntax? syntax?))])]{ + The @racket[define-type-expander] form binds + @racket[_name] to a type expander, which can be used in + places where a type would normally be expected. + + For example, one could define the @racket[HomogeneousList] + type expander, which accepts a type @racket[_t] and an + integer @racket[_n], and produces a @racket[List] type with + @racket[_n] elements, each of type @racket[_t]: + + @racketblock[ + (define-type-expander (HomogeneousList stx) + (syntax-case stx () + [(_ t n) + (number? (syntax-e #'n)) + (with-syntax ([(tᵢ ...) (stx-map (const #'t) + (range (syntax-e #'n)))]) + #'(List tᵢ ...))]))]} + +@subsection{Attaching type expanders to existing identifiers} + +@defform[(patch-type-expander name transformer-function) + #:grammar ([name Identifier] + [transformer-function (expr/c (-> syntax? syntax?))])]{ + This macro records in a global table that @racket[name] should behave + according to the given @racket[transformer-function], when used as a type. + + It allows attaching type expanders to existing identifiers, without shadowing + them. It is used for example to attach the type expanders for @racket[quote], + @racket[quasiquote], @racket[syntax] and @racket[quasisyntax] which are + described below, and also for the @racket[curry] type expander.} + +@section{Using a type expander} + +The @racket[HomogeneousList] type expander defined above could be +used in many of @racketmodname[typed/racket]'s forms. + +@racketblock[ + (define-type three-ints (HomogeneousList 3 Integer)) + (define (incr3 [x : three-ints]) : HomogeneousList + (map add1 x)) + (ann (incr3 '(1 2 3)) HomogeneousList)] + +Type expanders can produce types which may contain other +uses of type expanders, much in the same way as macros can +expand to code calling other macros. The type expander can +also produce directly a call to another type expander, just +as a macro can expand to a call to another macro, without +any extra surrounding syntax. + +@; TODO: examples + +Contrarily to macros, if a call to a type expander is in the +first position of more arguments, then the nested call is +first expanded, and can produce the name of a second +expander which will use the outer arguments, or can simply +produce a polymorphic type which will be applied to the +arguments. More than two levels of nesting are possible. + +@; TODO: examples with two levels and more. + +@section{Debugging type expanders} + +@defform*[[(debug-type-expander #t) + (debug-type-expander #f)]]{ + The first form enables printing of debugging information while expanding + types, and the second form disables that behaviour. Debugging information is + not printed by default. + + Currently, when debugging information is enabled, the type expander prints at + each step a human-readable representation of the syntax object it is about to + expand, and once an expansion step finishes, it prints the original syntax + object as well as its expanded form. The identifiers are adorned with + superscripts indicating the scopes present on them. See the documentation for + the debugging tool @racket[+scopes] for more details.} + +@section{Compile-time aspects of type expanders} + +@defmodule[type-expander/expander + #:use-sources + [(submod (lib "type-expander/type-expander.hl.rkt") expander) + (submod (lib "type-expander/type-expander.hl.rkt") main)]] + +@defproc[(expand-type [stx Type]) PlainType]{ + Fully expands the type @racket[stx], which may contain any + number of calls to type expanders. If those calls result in + more type expanders, those are expanded too.} + +@defproc[(apply-type-expander [type-expander-stx Identifier] [stx Syntax]) + Type]{ + Produces the result of applying the type expander bound to + @racket[type-expander-stx] to the syntax @racket[stx]. + Normally, the syntax @racket[stx] would be of the form + @racket[(type-expander-stx arg …)] (similar to a macro + call) or simply @racket[type-expander-stx] (similar to an + @tech[#:doc '(lib + "scribblings/guide/guide.scrbl")]{identifier + macro}). It is however possible to pass arbitrary syntax + to the type expander, just as it is possible for macros + (for example @racket[set!] calls + @tech[#:doc '(lib "scribblings/reference/reference.scrbl")]{ + assignment transformer} macros with the syntax + @racket[(set! macro-name arg …)] as an argument).} + +@defthing[prop:type-expander struct-type-property?]{ + A + @tech[#:doc '(lib "scribblings/reference/reference.scrbl")]{ + structure type property} to identify structure types that + act as @tech[#:key "type expander"]{type expanders} like + the ones created by @racket[define-type-expander]. + + The property value must be a procedure of arity 1 or an + @racket[exact-nonnegative-integer?] designating a field + index within the structure which contains such a + procedure. + + The procedure serves as a syntax transformer when + expanding the use of a type expander. If the type expander + was in the first position of a syntax list (i.e. it looks + like a macro or function call), then the whole syntax list + is passed as an argument. Otherwise, just the identifier is + passed as an argument, exactly as what would be done when + calling an + @tech[#:doc '(lib + "scribblings/guide/guide.scrbl")]{identifier macro}. The + procedure can support other use patterns if desired, so + that it would be possible in principle to implement special + type forms that behave in a way similar to + @secref["set__Transformers" #:doc '(lib "scribblings/guide/guide.scrbl")].} + +@subsection{Syntax class for @racketid[:]} + +@defidform[#:kind "syntax-parse syntax class" + colon]{ + This library shadows the @orig:: identifier from + @racketmodname[typed/racket] with a new definition + @racket[:], adjusted to handle type expanders. Programs + using the @racketmodname[type-expander] library will + therefore use our version of @racket[:]. The @racket[:] + identifier provided by this library is not + @racket[free-identifier=?] with the original @orig:: from + @racketmodname[typed/racket]. This has an impact when + writing patterns for the @racketmodname[syntax/parse] + library, as the two identifiers @racket[:] and @orig:: are + not the same from the point of view of the + @racket[~literal] pattern. + + The @racket[colon] syntax class is provided + @racket[for-syntax] by this library, and can be used in + @racket[syntax-parse] patterns, using @racket[c:colon] for + example. It matches both the original @orig:: and the new + @racket[:], but not other @racketid[:] identifiers. + + It can be used to write macros which expect either + @racketid[:] identifier.} + +@subsection{Syntax classes for types} + +@defidform[#:kind "syntax-parse syntax class" + type]{ + Matches a type. For now, this is just an alias for @racket[expr], because types + can contain arbitrary syntax thanks to type expanders.} + +@defthing[stx-type/c flat-contract?]{ + Flat contract which recognises syntax objects representing types. For now, + this is just an alias for @racket[syntax?], because types can contain + arbitrary syntax thanks to type expanders. + + Future versions may implement this as a non-flat contract, in order to be + able to check that in a macro's result, the syntax for a type is not used as + an expression, and vice versa.} + +@defidform[#:kind "syntax-parse syntax class" + type-expand!]{ + Matches a type @racket[_t], and provides an attribute named @racket[expanded] + which contains the result of @racket[(expand-type #'_t)]. For now, + @racket[type-expand] does not perform any check other than verifying that + @racket[_t] is an @racket[expr], because types can contain arbitrary syntax + thanks to type expanders.} + +@section{multi-id} + +@; TODO: separate multi-id or type-expander into two packages, so that we can +@; write @racketmodname[multi-id] without causing a circular dependency: +Type expanders are supported by the multi-id library. It is +therefore easy to define an identifier which acts as a type +expander and match expander as well as a regular racket +macro and/or +@tech[#:doc '(lib + "scribblings/guide/guide.scrbl")]{identifier macro}. This +can be useful to define feature-rich data structures, which +need to provide all of the above features. + +@section{Expansion model for type expanders} + +The expansion model for type expanders is similar to the expansion model for +macros. There are a few differences, however, which are presented below. + +@itemlist[ + @item{When a form like @racket[(f args ... . rest)] is encountered, if its + first element, @racket[f], is a type expander, the type expander is applied to + the whole form. If @racket[f] is a special identifier (e.g. like @racket[Let] + or @racket[Rec]), then the form is handled according to the special + identifier's rules. Otherwise, the @racket[f] form is expanded, and the result + @racket[(e args ... . rest)] is expanded once again (@racket[e] being the + result of the expansion of @racket[f]). + + In comparison, the ``official'' macro expander for Racket would, in the last + case, expand @racket[f] on its own, and then expand the arguments one by one + without re-considering the form as a whole. + + + With the type expander, during the second expansion pass for the form, if the + @racket[e] identifier is a type expander it is applied to the whole form. If + @racket[e] is a special identifier, the form is processed following that + identifier's rules. Otherwise, the @racket[e] form is left intact, and the + arguments @racket[args ...] and @racket[rest] are expanded each in turn. + + In comparison, the ``official'' macro expander would have fully expanded + @racket[e] in isolation (e.g. as an identifier macro), without letting it take + over the arguments.} + @item{With the ``official'' macro expander, all forms at the same lexical + scoping level are expanded before expanding the contents of @racket[let] + forms. + + In contrast, the type expander expands the contents of @racket[Let] forms in + the same order as other forms. It further replaces the @racket[Let] forms by + their contents, so that the following type: + + @racketblock[((Let ([Foo Pairof]) Foo) Number String)] + + gets expanded by replacing @racket[(Let ([Foo Pairof]) Foo)] by its contents + (i.e. the @racket[Foo] identifier in this case): + + @racketblock[(Foo Number String)] + + The @racket[Foo] identifier is still bound to @racket[Pairof], so this new + type expression gets expanded to: + + @racketblock[(Pairof Number String)] + + This means that identifiers bound by @racket[Let] forms can escape their + scope, but are still attached to their defining scope.} + @item{With the current implementation of the type expander, + @racket[syntax-local-value] ignores types bound by @racket[Let] forms. A + future version of this library will (hopefully) either fix this problem, or + provide an alternative @racket[syntax-local-type-value] which takes those + bindings into account.}] + +@section{Built-in type expanders} + +There are several built-in expanders. Some are documented +here, while others are listed in +@secref["Cases_handled_by_expand-type" + #:doc '(lib "type-expander/type-expander.hl.rkt")]. +Their API should be considered unstable, and may change in +the future. + +@subsection{Let} + +@defform[#:kind "type expander" + (Let ([Vᵢ Eᵢ] …) τ) + #:grammar + ([Vᵢ Identifier] + [Eᵢ Type] + [τ Type])]{ + The @racket[Let] form binds each type expression + @racket[Eᵢ] (which may contain uses of type expanders bound + outside of the @racket[Let] form) to the identifier @racket[Vᵢ]. + The type @racket[τ] can contain type expanders and can + refer to occurrences of the bound @racket[Vᵢ] identifiers, + which will expand to @racket[Eᵢ]. The @racket[Let] form therefore + behaves is a way similar to @racket[let-syntax]. + + @examples[#:eval (eval-factory) + (ann '(1 2 3) + (Let ([Foo Number]) + (Listof Foo))) + (eval:error (ann '(1 2 3) + (Listof Foo)))] + + @examples[#:eval (eval-factory) + (ann '([1 . "a"] [2 . b] [3 . 2.71]) + (Let ([Foo (Λ (_ T) + #'(Pairof Number T))]) + (List (Foo String) + (Foo Symbol) + (Foo Float))))] + +@examples[#:eval (eval-factory) + (ann '(a b c) + (Let ([Foo Number]) + (Let ([Foo String]) + (Let ([Foo Symbol]) + (Listof Foo))))) + (ann '(a b c) + (Let ([Foo Number]) + (Listof (Let ([Foo String]) + (Let ([Foo Symbol]) + Foo)))))]} + +@subsection{Letrec} + +@defform[#:kind "type expander" + (Letrec ([Vᵢ Eᵢ] …) τ)]{ + Like @racket[Let], but all the @racket[Vᵢ] identifiers are bound within all + the @racket[Eᵢ] type expressions. This means the type expression within an + @racket[Eᵢ] can refer to any @racket[Vᵢ] of the same @racket[Letrec].} + + +@subsection{Let*} + +@defform[#:kind "type expander" + (Let* ([Vᵢ Eᵢ] …) τ)]{ + Like @racket[Let], but all the preceding @racket[Vᵢ] identifiers are bound + each @racket[Eᵢ] type expression. This means the type expression within an + @racket[Eᵢ] can refer to any @racket[Vᵢ] already bound above it, but not to + the @racket[Vᵢ] it is being bound to, nor to the following @racket[Vᵢ].} + +@subsection{Λ} + +@defform[#:kind "type expander" + (Λ formals . body) + #:grammar + ([stx Identifier])]{ + + The @racket[Λ] form (a capital @racketid[λ]) can be used to construct an + anonymous type expander. It is equivalent to replacing the whole + @racket[(Λ formals . body)] form with @racket[_generated-id], where + @racket[_generated-id] is defined as a named type expander as follows: + + @racketblock[(define-type-expander (_gen-id _gen-stx-id) + (auto-syntax-case _gen-stx-id () + [formals (let () . body)]))] + + where @racket[_id] and @racket[_gen-stx-id] are fresh unique identifiers. + + Since @racket[Λ] relies on @racket[auto-syntax-case], the syntax pattern + variables bound by @racket[formals] can also be used outside of syntax + templates, in which case they evaluate to @racket[(syntax->datum #'pvar)]. + + @examples[#:eval (eval-factory) + #:escape UNSYNTAX + (eval:no-prompt (require (for-syntax racket/list racket/function))) + (ann '(1 2 3 4) + ((Λ (_ T n) + #`(List #,@(map (const #'T) (range n)))) + Number 4))]} + +@subsection{Quasiquote} + +The type expander library also adds support for +quasiquoting in types: The type @racket[`(a (1 b) ,String)] +is expanded to @racket[(List 'a (List 1 'b) String)]. + +@examples[#:eval (eval-factory) + (ann '(a (1 b) "foo") + `(a (1 b) ,String))] + +The @racket[quote], @racket[quasiquote], @racket[syntax] and +@racket[quasisyntax] identifiers are interpreted specially within type +expressions. The @racket[quote] identifier can be used to describe a type +matching containing only the quoted value. Similarly, @racket[syntax] can be +used to describe the type of the quoted syntax object, without the need to +insert @racket[Syntaxof] by hand around each part of the type. Note that the +type @racket[#'(a b c)] will match the syntax object @racket[#'(a b c)], but +not the syntax object @tt{#'(a b . (c))}, i.e. the generated type is +sensitive to the distinction between syntax pairs and syntax lists. It is +possible that a future version of this library provides another type expander +which accepts both. The @racket[quasiquote] and @racket[quasisyntax] forms +allow the use of @racket[unquote] and @racket[unsyntax], respectively. + +@subsection{Currying type expanders} + +The @racket[curry] special type-expander form can be used to curry in some +arguments to a type expander. + +@examples[#:eval (eval-factory) + (ann '([a . 1] [a . b] [a . "c"]) + (Let ([PA (curry Pairof 'a)]) + (List (PA 1) (PA 'b) (PA "c"))))] + +@section{Common issues (FAQ)} + +@(require (only-in scribble/eval interaction)) +@itemlist[ + @item{Explicitly requiring @racketmodname[typed/racket] + causes an error: + @(let ([errmsg (string-append "module: identifier already imported from" + " a different source in:" "\n" + " λ:" "\n" + " type-expander" "\n" + " typed/racket" "\n")]) + @interaction[(eval:alts (require typed/racket type-expander) + (eval:result "" + "" + errmsg))]) + A required module can shadow the definitions provided by + the @litchar{#lang} language, but it cannot shadow the + definitions provided by other explicitly required + modules. + + The solution is to avoid explicitly requiring + @racketmodname[typed/racket], or to subtract from it the + identifiers that would otherwise be shadowed anyway: + + @racketblock[ + (require racket/require + (subtract-in typed/racket type-expander) + type-expander)]} + @item{An error complains that a type expander is unbound: + @(let ([errmsg (string-append "Type Checker: parse error in type;\n" + " type name `foo' is unbound")]) + @interaction[(eval:alts (module main typed/racket + (module m type-expander/lang + (provide foo) + (define-type-expander (foo stx) #'Void)) + (require 'm) + (: v foo) + (define v (void))) + (eval:result "" + "" + errmsg))]) + + This error will be raised if the @racketmodname[type-expander] library is not + @racket[require]d. It is best to double-check that a + @racket[(require type-expander)] form is present, and that it is present at + the appropriate meta-level (it should be loaded at the same meta-level as the + use of @racket[(: var type)], @racket[(define var : type value)]). + + In the example above, the problem is that the module @racketid[main] requires + @racket['m], but does not require @racketmodname[type-expander]. The @orig:: + in @racket[(#,orig:: #,(racketid v) #,(racketid foo))] therefore comes from + @racketmodname[typed/racket], and does not know how to use the @racketid[foo] + type expander.} + @item{@bold{Q:} Can I write a recursive type-level + function? + + @bold{A:} Yes, but be sure that it is not infinitely + recursive, as the expansion would never terminate, unlike + @racketmodname[typed/racket]'s @racket[Rec], which allows + truly recursive types. + + Furthermore, it is best to ponder the risk of + combinatorial explosion, for example in + @racketmodname[typed/racket], + @racket[((∀ (X) (List X X)) Number)] expands internally to + the type @racket[(List Number Number)]. Nesting this + pattern a few times will produce a type having an + in-memory representation whose size is exponential in the + size of the original type declaration. A type expander can + easily produce a very large type, which will bring the + type checker to a crawl and/or crash it.}] + +@section{Overloaded @racketmodname[typed/racket] primitives} + + +@defform[(unsafe-cast value type)]{ + We define an @racket[unsafe-cast] form which is not (yet) provided by + Typed/Racket. It works like @racket[cast], but does not generate a predicate + to check that the value is indeed of the given type. It can therefore be used + to cast values to types for which @racket[cast] would fail at compile-time + when trying to generate the predicate, for example function types, or any type + which translates to a + @tech[#:doc '(lib "scribblings/reference/reference.scrbl")]{chaperone} + contract.} + +@defform[(unsafe-cast/no-expand value type)]{ + Like @racket[unsafe-cast], but does not expand the type. Can be useful for + types which are not completely handled by @racketmodname[type-expander], for + example function types with filters.} + +@(require (for-syntax racket/function racket/struct racket/vector)) +@(define-for-syntax (strip-loc e) + (cond [(syntax? e) (datum->syntax e (strip-loc (syntax-e e)) #f)] + [(pair? e) (cons (strip-loc (car e)) (strip-loc (cdr e)))] + [(vector? e) (vector-map strip-loc e)] + [(box? e) (box (strip-loc (unbox e)))] + [(prefab-struct-key e) + => (λ (k) (apply make-prefab-struct + k + (strip-loc (struct->list e))))] + [else e])) + +@(define-syntax (ovl stx) + (syntax-case stx () + [(_ name ...) + (with-syntax ([(prefixed ...) + (stx-map (λ (id) (format-id id "orig:~a" id)) + #'(name ...))] + [(stripped-name ...) + (stx-map strip-loc + #'(name ...))] + [(stripped-ooo ...) + (stx-map (compose strip-loc stx-car stx-cdr) + #'([name (... ...)] ...))]) + #'(list + @defform[(stripped-name stripped-ooo)]{ + Overloaded version of @|prefixed| from + @racketmodname[typed/racket].} + ...))])) + +@ovl[ + : + :type + :print-type + :query-type/args + :query-type/result + define-type + define + lambda + λ + case-lambda + case-lambda: + struct + define-struct/exec + ann + cast + inst + let + let* + let-values + make-predicate + ;; + class] + +@defidform[...*]{ + Overloaded version of @racketid[...*], which is interpreted specially by + @racketmodname[typed/racket]. It seems to be equivalent to @racket[*] for + indicating the type of a rest argument within a typed @orig:λ form.} + +@section{Unimplemented @racketmodname[typed/racket] + primitives (will be overloaded in later versions).} + +@(define-syntax (ovl-todo stx) + (syntax-case stx () + [(_ name ...) + (with-syntax ([(prefixed ...) + (stx-map (λ (id) (format-id id "orig:~a" id)) + #'(name ...))] + [(stripped-name ...) + (stx-map strip-loc + #'(name ...))] + [(stripped-ooo ...) + (stx-map (compose strip-loc stx-car stx-cdr) + #'([name (... ...)] ...))]) + #'(list + @defform[(stripped-name stripped-ooo)]{ + Overloaded version of @|prefixed| from + @racketmodname[typed/racket] (not implemented for the + @racketmodname[type-expander] library yet, just throws an + error).} + ...))])) + +@ovl-todo[ + ;; TODO: add all-defined-out in prims.rkt + ;; top-interaction.rkt + ;; case-lambda.rkt + pcase-lambda: + ;; (submod "prims-contract.rkt" forms) + require/opaque-type + ;require-typed-struct-legacy + require-typed-struct + ;require/typed-legacy + require/typed + require/typed/provide + require-typed-struct/provide + ;cast + define-predicate + ;; prims.rkt + define-type-alias + define-new-subtype + define-typed-struct + define-typed-struct/exec + define-struct: + define-struct + struct: + λ: + lambda: + letrec + letrec-values + let/cc + let/ec + let: + let*: + letrec: + let-values: + letrec-values: + let/cc: + let/ec: + for + for/list + for/vector + for/hash + for/hasheq + for/hasheqv + for/and + for/or + for/sum + for/product + for/lists + for/first + for/last + for/fold + for* + for*/list + for*/lists + for*/vector + for*/hash + for*/hasheq + for*/hasheqv + for*/and + for*/or + for*/sum + for*/product + for*/first + for*/last + for*/fold + for/set + for*/set + do + do: + with-handlers + define-struct/exec:] + +@include-section{deprecated-colon.scrbl} diff --git a/test/base-lang-test-1.rkt b/test/base-lang-test-1.rkt new file mode 100644 index 0000000..95d0276 --- /dev/null +++ b/test/base-lang-test-1.rkt @@ -0,0 +1,5 @@ +#lang type-expander/base +(require typed/rackunit) +(check-equal? (ann (add1 1) + (Let ([T Number]) T)) + 2) \ No newline at end of file diff --git a/test/base-lang-test-2.rkt b/test/base-lang-test-2.rkt new file mode 100644 index 0000000..4b4bc17 --- /dev/null +++ b/test/base-lang-test-2.rkt @@ -0,0 +1,7 @@ +#lang racket + +(module m type-expander/base + (require typed/rackunit) + (check-equal? (ann (add1 1) + (Let ([T Number]) T)) + 2)) \ No newline at end of file diff --git a/test/base-lang-test-3.rkt b/test/base-lang-test-3.rkt new file mode 100644 index 0000000..95d0276 --- /dev/null +++ b/test/base-lang-test-3.rkt @@ -0,0 +1,5 @@ +#lang type-expander/base +(require typed/rackunit) +(check-equal? (ann (add1 1) + (Let ([T Number]) T)) + 2) \ No newline at end of file diff --git a/test/lang-test-1.rkt b/test/lang-test-1.rkt new file mode 100644 index 0000000..d09a308 --- /dev/null +++ b/test/lang-test-1.rkt @@ -0,0 +1,5 @@ +#lang type-expander +(require typed/rackunit) +(check-equal? (ann (add1 1) + (Let ([T Number]) T)) + 2) \ No newline at end of file diff --git a/test/lang-test-2.rkt b/test/lang-test-2.rkt new file mode 100644 index 0000000..9c544d2 --- /dev/null +++ b/test/lang-test-2.rkt @@ -0,0 +1,7 @@ +#lang racket + +(module m type-expander/lang + (require typed/rackunit) + (check-equal? (ann (add1 1) + (Let ([T Number]) T)) + 2)) \ No newline at end of file diff --git a/test/lang-test-3.rkt b/test/lang-test-3.rkt new file mode 100644 index 0000000..0f652ab --- /dev/null +++ b/test/lang-test-3.rkt @@ -0,0 +1,5 @@ +#lang type-expander/lang +(require typed/rackunit) +(check-equal? (ann (add1 1) + (Let ([T Number]) T)) + 2) \ No newline at end of file diff --git a/test/readme.rkt b/test/readme.rkt new file mode 100644 index 0000000..ece9eab --- /dev/null +++ b/test/readme.rkt @@ -0,0 +1,20 @@ +#lang typed/racket +(require type-expander + typed/rackunit + (for-syntax racket/list)) + +(define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) + #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + +(: five-strings (→ String (Repeat String 5))) +(define (five-strings x) + (list x "a" "b" "c" "d")) + +(check-equal? (five-strings "hello") + '("hello" "a" "b" "c" "d")) + +(check-equal? (ann (five-strings "moon") (Repeat String 5)) + '("moon" "a" "b" "c" "d")) diff --git a/test/type-expander-test.rkt b/test/type-expander-test.rkt new file mode 100644 index 0000000..e68a3b7 --- /dev/null +++ b/test/type-expander-test.rkt @@ -0,0 +1,746 @@ +#lang typed/racket + +(require type-expander + typed/rackunit + (for-syntax type-expander/expander + racket/list + version/utils + rackunit + syntax/parse)) + +; Tests for expand-type +(begin + ;; Test harness: + (begin + (define-syntax (test-expander stx) + (syntax-parse stx + [(_ type expanded-type) + (let ([actual (syntax->datum (expand-type #'type))] + [expected (syntax->datum #'expanded-type)]) + (unless (equal? actual expected) + (raise-syntax-error + 'test-expander + (format "test-expander failed: expected ~a, got ~a" + expected + actual) + stx + #'type)) + #`(check-equal? '#,actual + '#,expected))]))) + + ; Simple identity expander test, with a different case when used as a + ; simple identifier. + + (begin + (define-type-expander (id stx) + (syntax-case stx () + [(_ t) #'t] + [x #'(∀ (A) (→ A A))])) + + (test-expander (id Number) Number) + (test-expander id (∀ (A) (→ A A)))) + + (begin + (define-type-expander (double stx) + (syntax-case stx () + [(_ t) #'(id (Pairof (id t) t))])) + + (test-expander (∀ (A) (→ A (id (double (id A))))) + (∀ (A) (→ A (Pairof A A)))) + + (test-expander (→ Any Boolean : (double (id A))) + (→ Any Boolean : (Pairof A A)))) + + ;; Curry expander arguments: + (begin + (define-type-expander (CPairof stx) + (syntax-case stx () + [(_ a) #'(curry Pairof a)] + [(_ a b) #'(Pairof a b)])) + + (test-expander (CPairof Number String) + (Pairof Number String)) + + (test-expander ((CPairof Number) String) + (Pairof Number String)) + + (check-equal? (ann (ann '(1 . "b") (CPairof Number String)) + (Pairof Number String)) + '(1 . "b")) + + (check-equal? (ann (ann '(1 . "c") ((CPairof Number) String)) + (Pairof Number String)) + '(1 . "c"))) + + ;; Shadowing with ∀ variables: + (begin + (test-expander (∀ (id) (→ id)) + (∀ (id) (→ id))) + (test-expander (∀ (id2) (→ id)) + (∀ (id2) (→ (∀ (A) (→ A A)))))) + + (begin + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + + (test-expander (Repeat Number 5) + (List Number Number Number Number Number))) + + (begin + (: count-five-more (→ Number (Repeat Number 5))) + (define (count-five-more x) + (list (+ x 1) (+ x 2) (+ x 3) (+ x 4) (+ x 5))) + + (check-equal? (count-five-more 3) + '(4 5 6 7 8)) + (check-equal? (ann (count-five-more 15) (Repeat Number 5)) + '(16 17 18 19 20))) + + ;; Shadowing with Rec variables: + + (begin + (: repeat-shadow (→ Number (Rec Repeat (U Null (List Number Repeat))))) + (define (repeat-shadow n) + (if (= n 0) + '() + (list n (repeat-shadow (sub1 n))))) + (check-equal? (repeat-shadow 5) + '(5 (4 (3 (2 (1 ())))))) + (test-expander (→ Number (Rec Repeat (U Null (List Number Repeat)))) + (→ Number (Rec Repeat (U Null (List Number Repeat)))))) + + ;; Shadowing with Let: + + (begin + (let () + (define-type-expander (exp stx) + #'(List 1 2 3)) + + (define-type e String) + (: x (List e (Let ([e exp]) e))) + (define x (list "e1" (list 1 2 3))) + (check-equal? x '("e1" (1 2 3))) + (test-expander (List e (Let ([e exp]) e)) + (List e (List 1 2 3))) + + (: y (List e)) + (define y (list "e2")) + (check-equal? y '("e2")) + (test-expander (List e) + (List e)) + (void))) + + ;; Let, Λ and ∀ + (begin + (let () + (define-type-expander Str1 (λ (_) #'String)) + + (test-expander (Let ([Number Str1]) Number) + String) + (test-expander (Let ([Number (Λ stx #'String)]) (Number)) + String) + (test-expander (Let ([Number (Λ stx #'Str1)]) (Number)) + String) + (test-expander (Let ([Number (Λ stx #'String)]) Number) + String) + + (test-expander ((∀ (A) (Pairof A A)) Number) + (Pairof Number Number)) + (test-expander (Let ([String (∀ (A) (Pairof A A))]) + (String Number)) + (Pairof Number Number)) + + (test-expander (Let ([Poly-Repeat + (Λ (_ n) + #`(∀ (A) + (List #,@(map (λ (_) #'A) + (range (syntax-e #'n))))))] + [Number String]) + ((Poly-Repeat 5) Number)) + (List String String String String String)) + + (test-expander (Let ([Poly-Repeat + (Λ (_ n) + #`(∀ (A) + (List #,@(map (λ (_) #'A) + ;; like above, but also works + ;; without the syntax-e here: + (range n)))))] + [Number String]) + ((Poly-Repeat 5) Number)) + (List String String String String String)) + + (ann '(1 . "b") ((Let ([Foo String]) + (∀ (ty) + (Pairof ty Foo))) + Integer)) + + (test-expander ((∀ (A1) + (Let () + (Let () + (Let () + (Let () + A1))))) + Number) + Number) + + (void))) + + ;; Let*, Letrec + (let () + (test-expander + (Letrec ([Poly-Repeat + (Λ (_ n) + (if (= 0 n) + #'(∀ (A) Null) + #`(∀ (A) + (Pairof A + ((Poly-Repeat #,(sub1 n)) A)))))] + [Number String]) + ((Poly-Repeat 5) Number)) + (Pairof String + (Pairof String + (Pairof String + (Pairof String + (Pairof String Null)))))) + + #;(test-expander (Let* ([String Number] + [Number String]) + (List Number String)) + (List Number Number)) + (void))) + +;; Test ":" +(begin + (: c0 `(2 "abc" #,,(Pairof (U 'x 'y) (U 'y 'z)) #(1 "b" x) d)) + (define c0 '(2 "abc" #,(x . z) #(1 "b" x) d)) + + (let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + + (: x (→ (Repeat Number 5))) + (define (x) (list 1 2 3 4 5)) + (check-equal? (x) '(1 2 3 4 5)))) + +;; Test define-type +(let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + + (define-type R5 (Repeat Number 5)) + (check-equal? (ann '(1 2 3 4 5) R5) '(1 2 3 4 5))) + +;; Test define +(begin + (define d0 + : `(2 "abc" #,,(Pairof (U 'x 'y) (U 'y 'z)) #(1 "b" x) d) + '(2 "abc" #,(x . z) #(1 "b" x) d)) + (check-equal? (ann d0 (List 2 + "abc" + (List 'unsyntax + (Pairof (U 'x 'y) (U 'y 'z))) + (Vector 1 "b" 'x) 'd)) + '(2 "abc" (unsyntax (x . z)) #(1 "b" x) d)) + + (: d1 (→ Number (→ Number Number))) + (define ((d1 [x : Number]) [y : Number]) : Number (+ x y)) + (check-equal? (ann ((d1 2) 3) Number) 5) + + (: d2 (→ Number (→ Number Number))) + (define ((d2 [x : Number]) [y : Number]) (+ x y)) + (check-equal? (ann ((d2 3) 4) Number) 7) + + (define #:∀ (T) ((d3 [x : T]) [y : T]) : (Pairof T T) (cons x y)) + (check-equal? (ann ((d3 'x) 'y) (Pairof Symbol Symbol)) '(x . y))) + +;; Test lambda +(begin + (check-equal? ((ann (lambda ([x : Number]) : Number (* x 2)) + (→ Number Number)) + 3) + 6) + (check-equal? ((ann (λ ([x : Number]) : Number (* x 2)) + (→ Number Number)) + 3) + 6) + (check-equal? ((λ x x) 1 2 3) '(1 2 3)) + (check-equal? ((λ #:∀ (A) [x : A ...*] : (Listof A) x) 1 2 3) '(1 2 3)) + (check-equal? ((λ [x : Number ...*] : (Listof Number) x) 1 2 3) '(1 2 3)) + (check-not-exn (λ () + (ann (λ #:∀ (A) [x : A ...*] : (Listof A) x) + (∀ (A) (→ A * (Listof A)))))) + (check-not-exn (λ () + (ann (λ #:∀ (A) [x : A *] : (Listof A) x) + (∀ (A) (→ A * (Listof A)))))) + (check-not-exn (λ () + (ann (λ #:∀ (A ...) ([l : (List A ... A)]) : (List A ... A) + l) + (∀ (A ...) (→ (List A ... A) (List A ... A)))))) + (check-not-exn (λ () + (ann (λ #:∀ (A ...) [l : (List A ... A) *] + : (Listof (List A ... A)) + l) + (∀ (A ...) (→ (List A ... A) * + (Listof (List A ... A))))))) + (check-not-exn (λ () + (ann (λ #:∀ (A ...) [l : (List A ... A) ...*] + : (Listof (List A ... A)) + l) + (∀ (A ...) (→ (List A ... A) * + (Listof (List A ... A)))))))) + +;; Test struct +(begin + (struct s0 ()) + (struct s1 ([x : Number])) + (struct s2 ([x : Number] [y : Number])) + (struct s3 ([x : Number] [y : Number]) #:transparent) + (struct s4 () #:transparent) + (struct (A B) s5 ([x : A] [y : B]) #:transparent) + (struct (A B) s6 () #:transparent) + (struct s7 s2 ([z : String]) #:transparent) + (struct (A) s8 s3 ([z : A]) #:transparent) + (struct (A B C) s9 s5 ([z : C]) #:transparent) + (struct (A B C) s10 s2 ([z : C]) #:transparent) + (struct (A B C) s11 s5 ([z : C])) + + (check (λ (a b) (not (equal? a b))) (s0) (s0)) + (check-equal? (s1-x (s1 123)) 123) + (check-equal? (s2-x (s2 2 3)) 2) + (check-equal? (s2-y (s2 2 3)) 3) + (check-equal? (s3-x (s3 4 5)) 4) + (check-equal? (s3-y (s3 4 5)) 5) + (check-equal? (s4) (s4)) + (check-equal? (s5-x (s5 6 7)) 6) + (check-equal? (s5-y (s5 6 7)) 7) + (check-equal? (s5 6 7) (s5 6 7)) + (check-equal? ((inst s5 Number String) 6 "g") (s5 6 "g")) + (check-equal? (s6) (s6)) + (check-equal? ((inst s6 Number String)) (s6)) + + ;(check-equal? (s7-x (s7 -1 -2 "c") -1)) + ;(check-equal? (s7-y (s7 -1 -2 "c") -2)) + (check-equal? (s7-z (s7 -1 -2 "c")) "c") + (check-equal? (s2-x (s7 -1 -2 "c")) -1) + (check-equal? (s2-y (s7 -1 -2 "c")) -2) + (check-not-equal? (s7 -1 -2 "c") (s7 -1 -2 "c")) + (check-not-exn (λ () (ann (s7 -1 -2 "c") s2))) + (check-true (s2? (s7 -1 -2 "c"))) + + ;(check-equal? (s8-x (s8 -1 -2 "c") -1)) + ;(check-equal? (s8-y (s8 -1 -2 "c") -2)) + (check-equal? (s8-z (s8 -1 -2 "c")) "c") + (check-equal? (s3-x (s8 -1 -2 "c")) -1) + (check-equal? (s3-y (s8 -1 -2 "c")) -2) + (check-equal? (s8 -1 -2 "c") (s8 -1 -2 "c")) + (check-equal? ((inst s8 String) -1 -2 "c") (s8 -1 -2 "c")) + (check-not-exn (λ () (ann ((inst s8 String) -1 -2 "c") s3))) + (check-true (s3? ((inst s8 String) -1 -2 "c"))) + + ;(check-equal? (s9-x (s9 8 9 10)) 8) + ;(check-equal? (s9-y (s9 8 9 10)) 9) + (check-equal? (s9-z (s9 8 9 10)) 10) + (check-equal? (s5-x (s9 8 9 10)) 8) + (check-equal? (s5-y (s9 8 9 10)) 9) + (check-equal? (s9 8 9 10) (s9 8 9 10)) + ;; Bug https://github.com/racket/typed-racket/issues/451 + ;(check-not-exn (λ () (ann ((inst s9 Number Symbol String) 8 'i "j") + ; (Struct s5)))) + (check-not-exn (λ () (ann ((inst s9 Number Symbol String) 8 'i "j") + (Struct (s5 Number Symbol))))) + (check-not-exn (λ () (ann ((inst s9 Number Symbol String) 8 'i "j") + (s5 Number Symbol)))) + (check-not-exn (λ () (ann ((inst s9 Number Symbol String) 8 'i "j") + (s5 Any Any)))) + (check-true (s5? ((inst s9 Number Symbol String) -1 'i "j"))) + (check-not-equal? (s10 11 12 13) (s10 11 12 13)) + (check-not-equal? (s11 14 15 16) (s11 14 15 16))) + +;; Test define-struct/exec +(begin + (define-struct/exec se0 () + ;[(λ (self v) (cons self v)) : (∀ (A) (→ se0 A (Pairof se0 A)))]) + [(λ (self v) (cons self v)) : (→ se0 Any (Pairof se0 Any))]) + (define-struct/exec se1 ([x : Number]) + ;[(λ (self v) (cons self v)) : (∀ (A) (→ se0 A (Pairof se0 A)))]) + [(λ (self v) (cons self v)) : (→ se1 Any (Pairof se1 Any))]) + (define-struct/exec se2 ([x : Number] [y : Number]) + [(λ (self v) (cons self v)) : (→ se2 Any (Pairof se2 Any))]) + (define-struct/exec (se3 se2) ([z : String]) + [(λ (self v w) (list self v w)) + ;: (∀ (A B) (→ se3 A B (List se2 A B)))]) + : (→ se3 Any Any (List se2 Any Any))]) + (define-struct/exec (se4 se2) ([z : String]) + [(λ (self v w) (list self v w)) + ;: (∀ (A B) (→ se4 A B (List se2 A B)))]) + : (→ se4 Any (→ Number Number) (List se2 Any (→ Number Number)))]) + + (check (λ (a b) (not (equal? a b))) (se0) (se0)) + (check-equal? (cdr ((se0) 'a)) 'a) + (check-not-exn (λ () (ann (car ((se0) 'a)) se0))) + (check-true (se0? (car ((se0) 'a)))) + + (check (λ (a b) (not (equal? a b))) (se1 123) (se1 123)) + (check-equal? (se1-x (se1 123)) 123) + (check-equal? (se1-x (car ((se1 123) 'b))) 123) + (check-equal? (cdr ((se1 123) 'b)) 'b) + (check-not-exn (λ () (ann (car ((se1 123) 'b)) se1))) + (check-true (se1? (car ((se1 123) 'b)))) + + (check (λ (a b) (not (equal? a b))) (se2 2 3) (se2 2 3)) + (check-equal? (se2-x (se2 2 3)) 2) + (check-equal? (se2-y (se2 2 3)) 3) + (check-equal? (se2-x (car ((se2 2 3) 'c))) 2) + (check-equal? (se2-y (car ((se2 2 3) 'c))) 3) + (check-equal? (cdr ((se2 2 3) 'c)) 'c) + (check-not-exn (λ () (ann (car ((se2 2 3) 'c)) se2))) + (check-true (se2? (car ((se2 2 3) 'c)))) + + (check (λ (a b) (not (equal? a b))) (se3 4 5 "f") (se3 4 5 "f")) + (check-equal? (se2-x (se3 4 5 "f")) 4) + (check-equal? (se2-y (se3 4 5 "f")) 5) + (check-equal? (se3-z (se3 4 5 "f")) "f") + (check-equal? (se2-x (car ((se3 4 5 "f") 'd 'e))) 4) + (check-equal? (se2-y (car ((se3 4 5 "f") 'd 'e))) 5) + (check-equal? (let ([ret : Any (car ((se3 4 5 "f") 'd 'e))]) + (if (se3? ret) + (se3-z ret) + "wrong type!")) + "f") + (check-equal? (cadr ((se3 4 5 "f") 'd 'e)) 'd) + (check-equal? (caddr ((se3 4 5 "f") 'd 'e)) 'e) + (check-equal? ((caddr ((se4 4 5 "f") 'd (λ ([x : Number]) (* x 2)))) 12) + 24) + (check-not-exn (λ () (ann (car ((se3 4 5 "f") 'd 'e)) se2))) + (check-true (se2? (car ((se3 4 5 "f") 'd 'e)))) + (check-true (se3? (car ((se3 4 5 "f") 'd 'e))))) + +;; Test ann +(let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + (check-equal? (ann (ann '(1 2 3) + (Repeat Number 3)) + (List Number Number Number)) + '(1 2 3))) + +;; Test inst +(let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + + (: f (∀ (A B C D) (→ (Pairof A B) (Pairof C D) (List A C B D)))) + (define (f x y) (list (car x) (car y) (cdr x) (cdr y))) + + (check-equal? ((inst f + (Repeat Number 3) + (Repeat String 2) + (Repeat 'x 1) + (Repeat undefined-type 0)) + '((1 2 3) . ("a" "b")) + '((x) . ())) + '((1 2 3) (x) ("a" "b") ()))) + +;; Test let +(begin + (check-equal? (ann (let loop-id ([x 1]) + (if (equal? x 2) + x + (loop-id 2))) + Any) + 2) + (check-equal? (let () 'x) 'x) + (check-equal? (ann (let #:∀ (T) ([a : T 3] + [b : (Pairof T T) '(5 . 7)]) + (cons a b)) + (Pairof Number (Pairof Number Number))) + '(3 5 . 7))) + +;; Test let* +(let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + + (check-equal? (let* ([x* : (Repeat Number 3) '(1 2 3)] + [y* : (Repeat Number 3) x*]) + y*) + '(1 2 3))) + +;; Test let-values +(let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + + (check-equal? (ann (let-values + ([([x : (Repeat Number 3)]) + (list 1 2 3)]) + (cdr x)) + (List Number Number)) + '(2 3)) + + (check-equal? (ann (let-values + ([([x : (Repeat Number 3)] [y : Number]) + (values (list 1 2 3) 4)]) + (cons y x)) + (Pairof Number (List Number Number Number))) + '(4 . (1 2 3))) + + (check-equal? (ann (let-values + ([(x y) + (values (list 1 2 3) 4)]) + (cons y x)) + (Pairof Number (List Number Number Number))) + '(4 . (1 2 3)))) + +;; Test make-predicate +(let () + (define-type-expander (Repeat stx) + (syntax-case stx () + [(_ t n) #`(List #,@(map (λ (x) #'t) + (range (syntax->datum #'n))))])) + (check-equal? ((make-predicate (Repeat Number 3)) '(1 2 3)) #t) + (check-equal? ((make-predicate (Repeat Number 3)) '(1 "b" 3)) #f)) + +;; row-inst +(let-syntax ([when-row-inst-is-defined + (λ (stx) + (syntax-case stx () + [(_ body) + (if (or (identifier-binding #'row-inst) + (version<=? "6.7" (version))) + #'body + #'(void))]))]) + (when-row-inst-is-defined + (let () + ;; Example taken from the docs + (: id (All (r #:row) + (-> (Class #:row-var r) (Class #:row-var r)))) + (define (id cls) cls) + (define result ((row-inst id (Row (field [x Integer]))) + (class object% (super-new) (field [x : Integer 0])))) + (ann result (Class (field (x Integer)))) + (void)))) + +;; Tests written while debugging +(begin + (let () + (define-type-expander flob + (λ (stx) #'(All (abc) (List abc)))) + + (ann '(a) ((flob) Symbol)) + + (ann '(42) ((Let ([flob (Λ (_ arg) + #'((∀ (abc) + (List abc)) arg))]) + flob) + Integer)) + + (ann '(1 2 3) ((∀ (abc) + (Listof abc)) + Integer)) + + (ann '(1 2 3) ((Let () + (∀ (abc) + (Listof abc))) + Integer)) + (void)) + + (let () + (test-expander + ((Let () (∀ (A1) (Let () A1))) Number) + Number)) + + (let () + (ann '(1 2 3) (Listof Integer)) + + (define-type (poly1 ty) + (Listof ty)) + + (ann '(1 2 3) (poly1 Integer)) + + (define-type poly2 + (∀ (ty) + (Listof ty))) + + (ann '(1 2 3) (poly2 Integer)) + + (ann '(1 2 3) ((∀ (ty) + (Listof ty)) + Integer)) + + (ann '(1 2 3) ((Let () + (∀ (ty) + (Listof ty))) + Integer)) + + (void)) + + (define-for-syntax (test-use/def stx def expected-use expected-def) + (let ([actual-use (syntax->datum + (apply-type-expander (datum->syntax stx 'Quux) + (datum->syntax stx 'Quux)))] + [actual-def (syntax->datum + (apply-type-expander def def))]) + (check-equal? actual-use expected-use) + (check-equal? actual-def expected-def))) + + (let () + (define-type-expander (Foo stx) #'Integer) + (define-type-expander (Bar stx) #'Integer) + (define-type-expander (Quux stx) #'Integer) + + (define-type mytype1 + (Let ([Foo (Λ (_ T) + (test-use/def #'T #'Quux 'Integer 'Integer) + #'T)]) + (Foo Quux))) + + (define-type mytype23 + (Let ([Quux String]) + (Let ([Foo (Λ (_ T) + (test-use/def #'T #'Quux 'String 'String) + #'T)]) + (Foo (∀ (A) + (Let ([Bar (Λ (_ T) + (test-use/def #'T #'Quux 'String 'String) + #'T)]) + (Bar (Listof A)))))))) + + (define-type mytype45 + (Let ([Foo (Λ (_ T) + (test-use/def #'T #'Quux 'String 'Integer) + #'T)]) + (Let ([Quux String]) + (Foo (∀ (A) + (Let ([Bar (Λ (_ T) + (test-use/def #'T #'Quux 'String 'String) + #'T)]) + (Bar (Listof A)))))))) + + (define-type mytype67 + (Let ([Foo (Λ (_ T) + (test-use/def #'T #'Quux 'Integer 'Integer) + #'T)]) + (Foo (Let ([Quux String]) + (∀ (A) + (Let ([Bar (Λ (_ T) + (test-use/def #'T #'Quux 'String 'String) + #'T)]) + (Bar (Listof A)))))))) + + (define-type mytype89 + (Let ([Foo (Λ (_ T) + (test-use/def #'T #'Quux 'Integer 'Integer) + #'T)]) + (Foo (∀ (A) + (Let ([Quux String]) + (Let ([Bar (Λ (_ T) + (test-use/def #'T #'Quux 'String 'String) + #'T)]) + (Bar (Listof A)))))))) + + (void)) + + (let () + (test-expander ((Let ([F (Λ (_ T) #'T)]) F) String) + String) + (test-expander ((Let ([F (Λ (_ T) #'(List T))]) F) String) + (List String))) + + ;; Please don't ever do that in practice :) ! + (let () + (test-expander (Let ([Loot Number]) + ((Let ([Loot Let]) Loot) ([AAA Number]) + AAA)) + Number) + (test-expander (Let ([Loot Number]) + ((Let ([Loot Let]) Loot) ([Let Loot]) + Let)) + Number) + (test-expander (Let ([Loot Number]) + ((Let ([Loot Let]) Loot) ([Loot String]) + Loot)) + String))) + +;; more tests +(begin + (test-expander ((∀ (A) ((∀ (A) ((∀ (A) ((∀ (A) A) A)) A)) A)) Number) + Number) + (test-expander (Let ([A Number]) + (Let ([A A]) + (Let ([A A]) + (Let ([A A]) + A)))) + Number) + (test-expander (Let* ([A Number] + [A A] + [A A] + [A A] + [A A]) + A) + Number) + (test-expander (Let* ([A Number] + [A (List A)] + [A (Pairof A A)] + [A (Vector A)] + [A (Set A)]) + A) + (Set (Vector (Pairof (List Number) (List Number))))) + + ;; Adjusted from http://www.cs.utah.edu/~mflatt/scope-sets/ + ;; #%28part._.Macro_.Definitions_in_a_.Recursive_.Scope%29 + (test-expander (Letrec ([Identity (Λ (_ misc-id) + #'(∀ (X) + (Let ([misc-id String]) + X)))]) + ((Identity X) Number)) + Number) + (test-expander (Letrec ([Identity (Λ (_ misc-id) + #'(∀ (misc-id) + (Let ([X String]) + misc-id)))]) + ((Identity X) Number)) + Number) + (test-expander (Letrec ([GetY (Λ (_ misc-id) + (datum->syntax #'misc-id 'Y))]) + (Let ([Y Number]) (GetY X))) + Number) + (test-expander (Letrec ([GetY (Λ (_ misc-id) + (datum->syntax #'misc-id 'Y))]) + ((∀ (Y) (GetY X)) Number)) + Number)) + +;; Tests for Syntax +(let () + (test-expander #'a (Syntaxof 'a)) + (test-expander #'(a) (Syntaxof (List (Syntaxof 'a)))) + (test-expander #'(a . b) (Syntaxof (Pairof (Syntaxof 'a) (Syntaxof 'b)))) + (test-expander #'(a . (b)) + (Syntaxof (Pairof (Syntaxof 'a) + (Syntaxof (List (Syntaxof 'b)))))) + (test-expander #'(a b) (Syntaxof (List (Syntaxof 'a) (Syntaxof 'b)))) + (test-expander #'(a b . c) + (Syntaxof (List* (Syntaxof 'a) (Syntaxof 'b) (Syntaxof 'c)))) + (test-expander #'(a b . (c)) + (Syntaxof (List* (Syntaxof 'a) + (Syntaxof 'b) + (Syntaxof (List (Syntaxof 'c))))))) + +;; Small typo +(let () + (test-expander ((No-Expand List) 'a 'b) (List 'a 'b))) \ No newline at end of file diff --git a/type-expander.hl.rkt b/type-expander.hl.rkt new file mode 100644 index 0000000..b692771 --- /dev/null +++ b/type-expander.hl.rkt @@ -0,0 +1,1977 @@ +#lang hyper-literate racket/base #:no-require-lang +@; The #:no-require-lang above is needed because type-expander requires +@; from 'main some identifiers (e.g. λ) which conflict with the re-required +@; racket/base. With this option, we loose arrows in DrRacket for the +@; built-ins in this file, and have otherwise no adverse effects. +@(require scribble-enhanced/doc) +@doc-lib-setup + +@(module orig-ids racket/base + (require scribble/manual + (for-label typed/racket/base)) + (provide (all-defined-out)) + (define orig:: (racket :)) + (define orig:let (racket let)) + (define orig:→AnyBoolean:Integer (racket (→ Any Boolean : Integer)))) +@(require 'orig-ids) + +@(unless-preexpanding + (require racket/require + (for-label (submod "..") + (only-in (submod ".." main) colon) + (subtract-in typed/racket/base (submod "..")) + (subtract-in racket typed/racket/base (submod "..")) + racket/require-syntax + racket/provide-syntax + typed/racket/unsafe + racket/format + racket/syntax + syntax/stx + syntax/parse + syntax/parse/experimental/template + syntax/id-table + auto-syntax-e + #;(subtract-in typed-racket/base-env/annotate-classes + (submod ".."))))) + +@title[#:style manual-doc-style + #:tag "ty-xp-impl" + #:tag-prefix "type-expander/ty-xp-impl" + ]{Implementation of the type expander library} + +@(chunks-toc-prefix + '("(lib type-expander/scribblings/type-expander-implementation.scrbl)" + "type-expander/ty-xp-impl")) + +This document describes the implementation of the +@racketmodname[type-expander] library, using literate +programming. For the library's documentation, see the +@other-doc['(lib "type-expander/scribblings/type-expander.scrbl")] +document instead. + +@section{Introduction} + +Extensible types would be a nice feature for typed/racket. Unlike +@racket[require] and @racket[provide], which come with +@tc[define-require-syntax] and @tc[define-provide-syntax], and unlike +@tc[match], which comes with @tc[define-match-expander], @tc[typed/racket] +doesn't provide a way to define type expanders. The +@racketmodname[type-expander] library extends @racketmodname[typed/racket] +with the ability to define type expanders, i.e. type-level macros. + +The @secref["ty-xp-more" #:tag-prefixes '("type-expander/ty-xp-more")] section +presents a small library of type expanders built upon the mechanism implemented +here. + +We redefine the forms @tc[:], @tc[define], @tc[lambda] and so on to +equivalents that support type expanders. Type expanders are defined via the +@tc[define-type-expander] macro. Ideally, this would be handled directly by +@tc[typed/racket], which would directly expand uses of type expanders. + +@(table-of-contents) + +@section{Expansion model for type expanders} + +Type expanders are expanded similarly to macros, with two minor differences: +@itemlist[ + @item{A form whose first element is a type expander, e.g. + @racket[(F . args₁)], can expand to the identifier of another type expander + @racket[G]. If the form itself appears as the first element of an outer form, + e.g. @racket[((F . args₁) . args₂)], the first expansion step will result in + @racket[(G . args₂)]. The official macro expander for Racket would then expand + @racket[G] on its own, as an + @tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier macro}, without + passing the @racket[args₂] to it. In contrast, the type expander will expand + the whole @racket[(G . args₂)] form, letting @racket[G] manipulate the + @racket[args₂] arguments.} + @item{It is possible to write anonymous macros, + + The @racket[Λ] form can be used to create anonymous type expanders. Anonymous + type expanders are to type expanders what anonymous functions are to function + definitions. The following table presents the expression-level and type-level + function and macro forms. Note that @racket[Let] serves as a type-level + equivalent to both @racket[let] and @racket[let-syntax], as anonymous macros + can be used in conjunction with @racket[Let] to obtain the equivalent of + @racket[let-syntax]. + + @tabular[#:style 'boxed + #:sep (hspace 1) + #:column-properties '((right-border right) left) + #:row-properties '((bottom-border baseline) (baseline)) + (list (list "" + @bold{Definitions} + @bold{Local binding} + @bold{Anonymous functions}) + (list @bold{Functions} + @racket[define] + @racket[let] + @racket[λ]) + (list @bold{Macros} + @racket[define-syntax] + @racket[let-syntax] + @emph{N/A}) + (list @bold{Type‑level functions@superscript{a}} + @racket[define-type] + @racket[Let] + @racket[∀]) + (list @bold{Type‑level macros} + @racket[define-type-expander] + @racket[Let] + @racket[Λ]))] + + @superscript{a}: The type-level functions are simple substitution functions, + and cannot perform any kind of computation. They are, in a sense, closer to + pattern macros defined with @racket[define-syntax-rule] than to actual + functions.}] + +Combined, these features allow some form of "curried" application of type +expanders: The @racket[F] type expander could expand to an anonymous +@racket[Λ] type expander which captures the @racket[args₁] arguments. In the +second expansion step, the @racket[Λ] anonymous type expander would then +consume the @racket[args₂] arguments, allowing @racket[F] to effectively +rewrite the two nested forms, instead of being constrained to the innermost +form. + +@subsection{Comparison with TeX's macro expansion model} + +For long-time TeX or LaTeX users, this may raise some concerns. TeX programs +are parsed as a stream of tokens. A TeX commands is a macro. When a TeX macro +occurs in the stream of tokens, it takes its arguments by consuming a certain +number of tokens following it. After consuming these arguments, a TeX macro +may expand to another TeX macro, which in turn consumes more arguments. This +feature is commonly used in TeX to implement macros which consume a variable +number arguments: the macro will initially consume a single argument. +Depending on the value of that argument, it will then expand to a macro taking +@racket[_n] arguments, or another macro taking @racket[_m] arguments. This +pattern, omnipresent in any sufficiently large TeX program, opens the door to +an undesirable class of bugs: when a TeX macro invocation appears in the +source code, it is not clear syntactically how many arguments it will +eventually consume. An incorrect parameter value can easily cause it to +consume more arguments than expected. This makes it possible for the macro to +consume the end markers of surrounding environments, for example in the code: + +@verbatim|{ + \begin{someEnvironment} + \someMacro{arg1}{arg2} + \end{someEnvironment} + }| + +the @literal|{someMacro}| command may actually expect three arguments, in +which case it will consume the @literal|{\end}| token, but leave the +@literal|{{someEnvironment}}| token in the stream. This will result in a badly +broken TeX program, which will most likely throw an error complaining that the +environment @literal|{\begin{someEnvironment}}| is not properly closed. The +error may however occur in a completely different location, and may easily +cause a cascade of errors (the missing @literal|{\end{someEnvironment}}| may +cause later TeX commands to be interpreted in a different way, causing them to +misinterpret their arguments, which in turn may cause further errors. The end +result is a series of mysterious error messages somewhat unrelated to the +initial problem. + +This problem with TeX macros can be summed up as follows: the number of tokens +following a TeX macro invocation that will be consumed by the macro is +unbounded, and cannot be easily guessed by looking at the raw source code, +despite the presence of programmer-friendly looking syntactic hints, like +wrapping arguments with @literal|{{…}}|. + +We argue that the expansion model for type expanders is less prone to this +class of problems, for several reasons: +@itemlist[ + @item{Firstly, macros can only consume outer forms if they appear as the + leftmost leaf of the outer form, i.e. while the @racket[F] macro in the + expression + + @racketblock[((F . args₁) . args₂)] + + may access the @racket[args₂] arguments, it will be constrained within the + @racket[(F . args₁)] in the following code: + + @racketblock[(H leading-args₂ (F . args₁) . more-args₂)] + + The first case occurs much more rarely than the second, so is less likely to + happen} + @item{Secondly, all TeX macros will consume an arbitrary number of arguments + in a linear fashion until the end of the enclosing group or a paragraph + separation. In contrast, most type expanders will consume all the arguments + within their enclosing application form, and no more. ``Curried'' type + expanders, which expand to a lone macro identifier, will likely only represent + a small subset of all type expanders. For comparison, consider the following + TeX code: + + @verbatim|{\CommandOne{argA}\CommandTwo{argB}}| + + The @literal|{\CommandOne}| TeX macro might consume zero, one, two three or + more arguments. If it consumes zero arguments, @literal|{{argA}}| will not be + interpreted as an argument, but instead will represent a scoped expression, + similar to @racket[(let () argA)]. If @literal|{\CommandOne}| consumes two or + more arguments, @literal|{\CommandTwo}| will be passed as an argument, + unevaluated, and may be discarded or applied to other arguments than the + seemingly obvious @literal|{{argB}}| argument. The TeX code above could + therefore be equivalent to any the following Racket programs: + + @racketblock[ + (CommandOne) + (let () argA) + (CommandTwo) + (let () argB)] + + @racketblock[ + (CommandOne argA) + (CommandTwo) + (let () argB)] + + @racketblock[ + (CommandOne) + (let () argA) + (CommandTwo argB)] + + @racketblock[ + (CommandOne argA) + (CommandTwo argB)] + + @racketblock[ + (CommandOne argA CommandTwo) + (let () argB)] + + @racketblock[ + (CommandOne argA CommandTwo argB)] + + In contrast, the obvious interpretation at a first glance of the TeX program + would be written as follows in Racket: + + @racketblock[ + (CommandOne argA) + (CommandTwo argB)] + + If these appear as ``arguments'' of a larger expression, then their meaning + is unambiguous (unless the larger expression is itself a macro): + + @racketblock[ + (+ (CommandOne argA) + (CommandTwo argB))] + + If however the @racket[(CommandOne argA)] is the first element in its form, + then, if it is a curried macro, it may consume the the + @racket[(CommandTwo argB)] form too: + + + @racketblock[ + ((CommandOne argA) + (CommandTwo argB))] + + As stated earlier, this case will likely be less common, and it is clearer + that the intent of the programmer to pass @racket[(CommandTwo argB)] as + arguments to the result of @racket[(CommandOne argA)], either as a macro + application or as a regular run-time function application.} + @item{Finally, Racket macros (and type expanders) usually perform a somewhat + thorough check of their arguments, using @racket[syntax-parse] or + @racket[syntax-case] patterns. Arguments to macros and type expanders which do + not have the correct shape will trigger an error early, thereby limiting the + risk of causing errors in cascade.}] + +@subsection{Interactions between type expanders and scopes} + +Our expansion model for type expanders therefore allows a type expander to +escape the scope in which it was defined before it is actually expanded. For +example, the following type: + +@RACKETBLOCK[ + (Let ([A Number]) + ((Let ([F (Λ (self T) + #`(Pairof #,(datum->syntax #'self 'A) + T))]) + (Let ([A String]) + F)) + A))] + +first expands to: + +@RACKETBLOCK[ + (F + A)] + +and then expands to: + +@RACKETBLOCK[ + (Pairof String A)] + +and finally expands to: + +@RACKETBLOCK[ + (Pairof String A)] + +Effectively, @racket[F] captures the scope where its name appears (inside all +three @racket[Let] forms), but is expanded in a different context (outside of +the two innermost @racket[Let] forms). + +Using Matthew Flatt's notation to indicate the scopes present on an +identifier, we can more explicitly show the expansion steps: + +@RACKETBLOCK[ + (Let ([A Number]) + ((Let ([F (Λ (self T) + #`(Pairof #,(datum->syntax #'self 'A) + T))]) + (Let ([A String]) + F)) + A))] + +The first @racket[Let] form annotates the identifier it binds with a fresh +scope, numbered @racket[1] here, and adds this scope to all identifiers within +its body. It stores the binding in the @racket[(tl-redirections)] binding +table, as shown by the comment above the code + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + ((Let¹ ([F¹ (Λ¹ (self¹ T¹) + #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹) + T¹))]) + (Let¹ ([A¹ String¹]) + F¹)) + A¹)] + +The second @racket[Let] form then binds the @racket[F] identifier, adding a +fresh scope as before: + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + (code:comment "F¹² := (Λ¹ (self¹ T¹)") + (code:comment " #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹)") + (code:comment " T¹))") + ((Let¹² ([A¹² String¹²]) + F¹²) + A¹)] + +The third @racket[Let] form then binds @racket[A] within its body, leaving the +outer @racket[A] unchanged: + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + (code:comment "F¹² := (Λ¹ (self¹ T¹)") + (code:comment " #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹)") + (code:comment " T¹))") + (code:comment "A¹²³ := String¹²") + (F¹²³ + A¹)] + +The @racket[F¹²³] macro is then expanded, passing as an argument the syntax +object @racket[#'(F¹²³ A¹)]. A fresh scope is added to the identifiers +generated by the macro, in order to enforce macro hygiene. The @racket[A¹] +identifier is passed as an input to the macro, so it is left unchanged, and +@racket[A¹²³] is derived from @racket[F¹²³], via @racket[datum->syntax], and +therefore has the same scopes (@racket[F¹²³] is also a macro input, so it is +not tagged with the fresh scope). The @racket[Pairof¹] identifier, generated by +the macro, is however flagged with the fresh scope @racket[4]. The result of +the application of @racket[F] to this syntax object is: + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + (code:comment "F¹² := (Λ¹ (self¹ T¹)") + (code:comment " #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹)") + (code:comment " T¹))") + (code:comment "A¹²³ := String¹²") + (Pairof¹⁴ A¹²³ A¹)] + +The @racket[Pairof¹⁴] type is resolved to the primitive type constructor +@racket[Pairof]: + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + (code:comment "F¹² := (Λ¹ (self¹ T¹)") + (code:comment " #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹)") + (code:comment " T¹))") + (code:comment "A¹²³ := String¹²") + (Pairof A¹²³ A¹)] + +The type @racket[A¹²³] is then resolved to @racket[String¹²], which in turn is +resolved to the @racket[String] built-in type: + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + (code:comment "F¹² := (Λ¹ (self¹ T¹)") + (code:comment " #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹)") + (code:comment " T¹))") + (code:comment "A¹²³ := String¹²") + (Pairof String A¹)] + +And the type @racket[A¹] is resolved to @racket[Number]: + +@RACKETBLOCK[ + (code:comment "A¹ := Number") + (code:comment "F¹² := (Λ¹ (self¹ T¹)") + (code:comment " #`(Pairof¹ #,(datum->syntax¹ #'self¹ 'A¹)") + (code:comment " T¹))") + (code:comment "A¹²³ := String¹²") + (Pairof String Number)] + +The @racket[syntax-local-value] function does not support querying the +transformer binding of identifiers outside of the lexical scope in which they +are bound. In our case, however, we need to access the transformer binding of +@racket[F¹²³] outside of the scope of the @racket[Let] binding it, and +similarly for @racket[A¹²³]. + +@section{The @racket[prop:type-expander] structure type property} + +Type expanders are identified by the @tc[prop:type-expander] +@tech[#:doc '(lib "scribblings/reference/reference.scrbl")]{structure type + property}. Structure type properties allow the same identifier to act as a +rename transformer, a match expander and a type expander, for example. Such an +identifier would have to implement the @tc[prop:rename-transformer], +@tc[prop:match-expander] and @tc[prop:type-expander] properties, respectively. + +@chunk[ + (define-values (prop:type-expander + has-prop:type-expander? + get-prop:type-expander-value) + (make-struct-type-property 'type-expander prop-guard))] + +The value of the @tc[prop:type-expander] property should either be a +transformer procedure which will be called when expanding the type, or the +index of a field containing such a procedure. + +@chunk[ + (define (prop-guard val struct-type-info-list) + (cond + + ))] + +If the value is a field index, it should be within bounds. The +@tc[make-struct-field-accessor] function performs this check, and also returns +an accessor. The accessor expects an instance of the struct, and returns the +field's value. + +@chunk[ + [(exact-nonnegative-integer? val) + (let* ([make-struct-accessor (cadddr struct-type-info-list)] + [accessor (make-struct-field-accessor make-struct-accessor val)]) + (λ (instance) + (let ([type-expander (accessor instance)]) + )))]] + +The expander procedure will take one argument: the piece of syntax +corresponding to the use of the expander. If the property's value is a +procedure, we therefore check that its arity includes 1. + +@chunk[ + (if (and (procedure? type-expander) + (arity-includes? (procedure-arity type-expander) 1)) + type-expander + (raise-argument-error 'prop:type-expander-guard + (~a "the value of the " val "-th field should" + " be a procedure whose arity includes 1") + type-expander))] + +In the first case, when the property value is a field index, we return an +accessor function. The accessor function expects a struct instance, performs +some checks and returns the actual type expander procedure. + +When the property's value is directly a type expander procedure, we follow the +same convention. We therefore return a function which, given a struct +instance, returns the type expander procedure (ignoring the @racket[_] +argument). + +@chunk[ + [(procedure? val) + (if (arity-includes? (procedure-arity val) 1) + (λ (_) val) + (raise-argument-error 'prop:type-expander-guard + "a procedure whose arity includes 1" + val))]] + +When the value of the @racket[prop:type-expander] property is neither a +positive field index nor a procedure, an error is raised: + +@chunk[ + [else + (raise-argument-error + 'prop:type-expander-guard + (~a "a procedure whose arity includes 1, or an exact " + "non-negative integer designating a field index within " + "the structure that should contain a procedure whose " + "arity includes 1.") + val)]] + +@subsection{The @racket[type-expander] struct} + +We make a simple struct that implements @tc[prop:type-expander] and nothing +else. It has a single field, @racket[expander-proc], which contains the type +expander transformer procedure. + +@chunk[ + (struct type-expander (expander-proc) #:transparent + #:extra-constructor-name make-type-expander + #:property prop:type-expander (struct-field-index expander-proc))] + +@section{Associating type expanders to identifiers} + +@subsection{The @racket[type-expander] syntax class} + +The @tc[type-expander] syntax class recognises identifiers +which are bound to type expanders. These fall into three cases: +@itemlist[ + @item{The identifier's @racket[syntax-local-value] is an instance of a struct + implementing @racket[prop:type-expander]} + @item{The identifier has been bound by a type-level local binding form like + @racket[Let] or @racket[∀], and therefore are registered in the + @racket[(tl-redirections)] binding table.} + @item{The identifier has been patched via @racket[patch-type-expander], i.e. + a type expander has been globally attached to an existing identifier, in which + case the type expander is stored within the @racket[patched] free identifier + table.}] + +@chunk[ + (define-syntax-class type-expander + (pattern local-expander:id + #:when (let ([b (binding-table-find-best (tl-redirections) + #'local-expander + #f)]) + (and b (has-prop:type-expander? b))) + #:with code #'local-expander) + (pattern (~var expander + (static has-prop:type-expander? "a type expander")) + #:when (not (binding-table-find-best (tl-redirections) + #'expander + #f)) + #:with code #'expander) + (pattern patched-expander:id + #:when (let ([p (free-id-table-ref patched + #'patched-expander + #f)]) + (and p (has-prop:type-expander? p))) + #:when (not (binding-table-find-best (tl-redirections) + #'expander + #f)) + #:with code #'patched-expander))] + +We also define a syntax class which matches types. Since types can bear many +complex cases, and can call type expanders which may accept arbitrary syntax, +we simply define the @tc[type] syntax class as @tc[expr]. Invalid syntax will +be eventually caught while expanding the type, and doing a thorough check +before any processing would only make the type expander slower, with little +actual benefits. The @tc[type] syntax class is however used in syntax patterns +as a form of documentation, to clarify the distinction between types and +run-time or compile-time expressions. + +@CHUNK[ + (define-syntax-class type + (pattern :expr))] + +@chunk[ + (define stx-type/c syntax?)] + +Finally, we define a convenience syntax class which expands the matched type: + +@chunk[ + (define-syntax-class type-expand! + #:attributes (expanded) + (pattern t:expr + #:with expanded (expand-type #'t #f)))] + +@subsection{Calling type expanders} + +The @tc[apply-type-expander] function applies the syntax expander transformer +function associated to @tc[type-expander-id]. It passes @tc[stx] as the single +argument to the transformer function. Usually, @tc[stx] will be the syntax +used to call the type expander, like @tc[#'(te arg ...)] or just @tc[#'te] if +the type expander is not in the first position of a form. + +The identifier @tc[type-expander-id] should be bound to a type expander, in +one of the three possible ways described above. + +@chunk[ + (define/contract (apply-type-expander type-expander-id stx) + (-> identifier? syntax? syntax?) + (let ([val (or (binding-table-find-best (tl-redirections) + type-expander-id + #f) + (let ([slv (syntax-local-value type-expander-id + (λ () #f))]) + (and (has-prop:type-expander? slv) slv)) + (free-id-table-ref patched type-expander-id #f))] + [ctxx (make-syntax-introducer)]) + + (ctxx (((get-prop:type-expander-value val) val) (ctxx stx)))))] + +The @racket[apply-type-expander] function checks that its +@racket[type-expander-id] argument is indeed a type expander before attempting +to apply it: + +@chunk[ + (unless val + (raise-syntax-error 'apply-type-expander + (format "Can't apply ~a, it is not a type expander" + type-expander-id) + stx + type-expander-id))] + +@subsection{Associating type expanders to already existing identifiers} + +As explained above, existing identifiers which are provided by other libraries +can be ``patched'' so that they behave like type expanders, using a global +table associating existing identifiers to the corresponding expander code: + +@chunk[ + (define patched (make-free-id-table))] + +@CHUNK[ + (define-syntax patch-type-expander + (syntax-parser + [(_ id:id expander-expr:expr) + #`(begin + (begin-for-syntax + (free-id-table-set! patched + #'id + (type-expander #,(syntax/loc this-syntax + expander-expr)))))]))] + +@subsection{Defining new type expanders} + +The @tc[define-type-expander] macro binds @tc[_name] to a +type expander which uses @tc[(λ (_arg) . _body)] as the +transformer procedure. To achieve this, we create a +transformer binding (with @tc[define-syntax]), from +@tc[_name] to an instance of the @tc[type-expander] +structure. + +@CHUNK[ + (define-syntax define-type-expander + (syntax-parser + [(_ (name:id arg:id) . body) + #`(define-syntax name + (type-expander #,(syntax/loc this-syntax (λ (arg) . body))))] + [(_ name:id fn:expr) + #`(define-syntax name + (type-expander #,(syntax/loc this-syntax fn)))]))] + +@subsection[#:tag "shadow"]{Locally binding type expanders} + +Some features of the type expander need to locally bind new type expanders: + +@itemlist[ + @item{The @racket[(Let ([_id _expr] …) . _body)] special form binds the + identifiers @racket[_id …] to the type expanders @racket[_expr …] in its + @racket[_body].} + @item{When expanding the body of a @racket[(∀ (Tᵢ …) body)] form, the + @racket[Tᵢ] bound by the @racket[∀] may shadow some type expanders with the + same name. If the @racket[∀] form is directly applied to arguments, each + @racket[Tᵢ] is instead bound to the corresponding argument.} + @item{When expanding the body of a @racket[(Rec T body)] form, the @racket[T] + bound by the @racket[Rec] may shadow a type expander with the same name.}] + +We use @racket[with-bindings] (defined in another file) to achieve this. The +code + +@racketblock[(with-bindings [_bound-ids _transformer-values] + _rebind-stx + _transformer-body)] + +evaluates @racket[_transformer-body] in the transformer environment. It +creates a fresh scope, which it applies to the @racket[_bound-ids] and the +@racket[_rebind-stx]. It associates each modified @racket[_bound-id] with the +corresponding @racket[_transformer-value] in the @racket[(tl-redirections)] +binding table. The @racket[with-bindings] form does not mutate the syntax +objects, instead it shadows the syntax pattern variables mentioned in +@racket[_bound-ids] and @racket[_rebind-stx] with versions pointing to the +same syntax objects, but with the fresh scope flipped on them. + +The code + +@racketblock[(with-rec-bindings [_bound-ids _generate-transformer-values _rhs] + _rebind-stx + _transformer-body)] + +works in the same way, but it also flips the fresh scope on each element of +@racket[_rhs]. The @racket[_generate-transformer-values] is expected to be a +transformer expression which, given an element of @racket[_rhs] with the +flipped scope, produces the transformer value to bind to the corresponding +@racket[_bound-id]. + + +The implementation of @racket[with-bindings] unfortunately does not play well +with @racket[syntax-local-value], so the binding table has to be queried +directly instead of using @racket[syntax-local-value]. To our knowledge, the +only ways to make new bindings recognised by @racket[syntax-local-value] are: +@itemlist[ + @item{To expand to a @racket[define-syntax] form, followed with a macro + performing the remaining work} + @item{Equivalently, to expand to a @racket[let-syntax] form, whose body is a + macro performing the remaining work} + @item{To call @racket[local-expand] with an internal definition context which + contains the desired bindings} + @item{To explicitly call @racket[syntax-local-value] with an internal + definition context argument}] + +It is not practical in our case to use the first solution involving +@racket[define-syntax], as the type expander may be called while expanding an +expression (e.g. @racket[ann]). The next two solutions assume that +@racket[syntax-local-value] will be called in a well-scoped fashion (in the +sense of the official expander): in the second solution, +@racket[syntax-local-value] must be called by expansion-time code located +within the scope of the @racket[let-syntax] form, and in the third solution, +@racket[syntax-local-value] must be called within the dynamic extent of +@racket[local-expand]. The last solution works, but requires that the user +explicitly passes the appropriate internal definition context. + +The second and third solutions cannot be applied in our case, because type +expanders can be expanded outside of the scope in which they were defined and +used, as explained the +@secref["Interactions_between_type_expanders_and_scopes"] section. + +The current version of the type expander does not support a reliable +alternative to @racket[syntax-local-value] which takes into account local +binding forms for types (@racket[Let], @racket[∀] and @racket[Rec]), but one +could be implemented, either by using some tricks to make the first solution +work, or by providing an equivalent to @racket[syntax-local-value] which +consults the @racket[(tl-redirections)] binding table. + +@section{Expanding types} + +The @tc[expand-type] function fully expands the type +@tc[stx]. As explained in +@secref["shadow"], shadowing would be better handled using +scopes. The @tc[expand-type] function starts by defining +some syntax classes, then parses @tc[stx], which can fall in +many different cases. + +@CHUNK[ + (define (expand-type stx [applicable? #f]) + (start-tl-redirections + + (define (expand-type-process stx first-pass?) + + ((λ (result) ) + (parameterize () + + (syntax-parse stx + + + + + + + + + + + + + + + (code:comment "Must be after other special application cases") + + + )))) + (expand-type-process stx #t)))] + +@subsection{Cases handled by @racket[expand-type]} + +The cases described below which expand a use of a type expander re-expand the +result, by calling @tc[expand-type] once more. This process is repeated until +no more expansion can be performed. This allows type expanders to produce +calls to other type expanders, exactly like macros can produce calls to other +macros. + +We distinguish the expansion of types which will appear as the first element +of their parent form from types which will appear in other places. When the +@racket[applicable?] argument to @racket[expand-type] is @racket[#true], it +indicates that the current type, once expanded, will occur as the first +element of its enclosing form. If the expanded type is the name of a type +expander, or a @racket[∀] or @racket[Λ] form, it will be directly applied to +the given arguments by the type expander. When @racket[applicable?] is +@racket[#false], it indicates that the current type, once expanded, will +@emph{not} appear as the first element of its enclosing form (it will appear +in another position, or it is at the top of the syntax tree representing the +type). + +When @racket[applicable?] is @racket[#true], if the type is the name of a type +expander, or a @racket[∀] or @racket[Λ] form, it is not expanded immediately. +Instead, the outer form will expand it with the arguments. Otherwise, these +forms are expanded without arguments, like +@tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier macros} would be. + +@subsection{Applying type expanders} + +When a type expander is found in a non-applicable position, it is called, +passing the identifier itself to the expander. An +@tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier macro} would be +called in the same way. + +@CHUNK[ + [expander:type-expander + #:when (not applicable?) + (rule id-expander/not-applicable + (let ([ctxx (make-syntax-introducer)]) + (expand-type (ctxx (apply-type-expander #'expander.code + (ctxx #'expander))) + applicable?)))]] + +When a type expander is found in an applicable position, it is returned +without modification, so that the containing application form may expand it +with arguments. When the expander @racket[e] appears as @racket[(e . args)], +it is applicable. It is also applicable when it appears as +@racket[((Let (bindings…) e) . args)], for example, because @racket[Let] +propagates its @racket[applicable?] status. + +@CHUNK[ + [expander:type-expander + #:when applicable? + (rule id-expander/applicable + #'expander)]] + +When a form contains a type expander in its first element, the type expander +is called. The result is re-expanded, so that a type expander can expand to a +use of another type expander. + +@CHUNK[ + [(~and expander-call-stx (expander:type-expander . _)) + (rule app-expander + (let ([ctxx (make-syntax-introducer)]) + (expand-type (ctxx (apply-type-expander #'expander.code + (ctxx #'expander-call-stx))) + applicable?)))]] + +When a form of the shape @racket[(_f . _args)] is encountered, and the +@racket[_f] element is not a type expander, the @racket[_f] form is expanded, +and the whole form (with @racket[_f] replaced by its expansion) is expanded a +second time. The @racket[applicable?] parameter is set to @racket[#true] while +expanding @racket[_f], so that if @racket[_f] produces a type expander (e.g. +@racket[_f] has the shape @racket[(Let (…) _some-type-expander)]), the type +expander can be applied to the @racket[_args] arguments. + +@CHUNK[ + [(~and whole (f . args)) + #:when first-pass? + (rule app-other + (expand-type-process + (datum->syntax #'whole + (cons (expand-type #'f #true) #'args) + #'whole + #'whole) + #f))]] + +@subsubsection{Polymorphic types with @racket[∀]} + +When the @tc[∀] or @tc[All] special forms from @racketmodname[typed/racket] +are used, the bound type variables may shadow some type expanders. The type +expanders used in the body @tc[T] which have the same identifier as a bound +variable will be affected by this (they will not act as a type-expander +anymore). The body of the @tc[∀] or @tc[All] form is expanded with the +modified environment. The result is wrapped again with +@tc[(∀ (TVar …) expanded-T)], in order to conserve the behaviour from +@racketmodname[typed/racket]'s @tc[∀]. + +@CHUNK[ + [({~and ∀ {~literal ∀}} (tvar:id …) T:type) + #:when (not applicable?) + (rule just-∀/not-applicable + (with-syntax ([(tvar-vars-only …) (remove-ddd #'(tvar …))]) + (with-bindings [(tvar-vars-only …) (stx-map + #'(tvar-vars-only …))] + (T tvar …) + #`(∀ (tvar …) + #,(expand-type #'T #f)))))]] + +Where @racket[] is used to bind the type variables @racket[tvarᵢ] to +@racket[(No-Expand tvarᵢ)], so that their occurrences are left intact by the +type expander: + +@CHUNK[ + (λ (__τ) + (make-type-expander + (λ (stx) + (syntax-case stx () + [self (identifier? #'self) #'(No-Expand self)] + [(self . args) #'((No-Expand self) . args)]))))] + +When a @racket[∀] polymorphic type is found in an applicable position, it is +returned without modification, so that the containing application form may +expand it, binding the type parameters to their effective arguments. + +@CHUNK[ + [(~and whole ({~literal ∀} (tvar:id …) T:type)) + #:when applicable? + (rule just-∀/applicable + #'whole)]] + +When a @racket[∀] polymorphic type is immediately applied to arguments, the +type expander attempts to bind the type parameters to the effective arguments. +It currently lacks any support for types under ellipses, and therefore that +case is currently handled by the @racket[] case +described later. + +@chunk[ + [(({~literal ∀} ({~and tvar:id {~not {~literal …}}} …) τ) arg …) + (unless (= (length (syntax->list #'(tvar …))) + (length (syntax->list #'(arg …)))) + ) + (rule app-∀ + (with-bindings [(tvar …) (stx-map (λ (a) (make-type-expander (λ (_) a))) + #'(arg …))] + τ + (expand-type #'τ applicable?)))]] + +If the given number of arguments does not match the expected number of +arguments, an error is raised immediately: + +@chunk[ + (raise-syntax-error + 'type-expander + (format (string-append "Wrong number of arguments to " + "polymorphic type: ~a\n" + " expected: ~a\n" + " given: ~a" + " arguments were...:\n") + (syntax->datum #'f) + (length (syntax->list #'(tvar …))) + (length (syntax->list #'(arg …))) + (string-join + (stx-map (λ (a) + (format "~a" (syntax->datum a))) + #'(arg …)) + "\n")) + #'whole + #'∀ + (syntax->list #'(arg …)))] + +@subsubsection{Recursive types with @racket[Rec]} + +Similarly, the @tc[Rec] special form will cause the bound +variable @tc[R] to shadow type expanders with the same name, +within the extent of the body @tc[T]. The result is wrapped +again with @tc[(Rec R expanded-T)], in order to conserve the +behaviour from @racketmodname[typed/racket]'s @tc[Rec]. + +@CHUNK[ + [((~literal Rec) R:id T:type) + (rule Rec + #`(Rec R #,(with-bindings [R ( #'R)] + T + (expand-type #'T #f))))]] + +@subsubsection{Local bindings with @racket[Let] and @racket[Letrec]} + +The @tc[Let] special form binds the given identifiers to the corresponding +type expanders. We use @racket[with-bindings], as explained above in +@secref["shadow" #:doc '(lib "type-expander/type-expander.hl.rkt")], to bind +the @racket[Vᵢ …] identifiers to their corresponding @racket[Eᵢ] while +expanding @racket[T]. + +@CHUNK[ + [((~commit (~literal Let)) ([Vᵢ:id Eᵢ] …) T:type) + (rule Let + (with-bindings [(Vᵢ …) + (stx-map (λ (Eᵢ) + (make-type-expander + (λ (stx) + (syntax-case stx () + [self (identifier? #'self) Eᵢ] + [(self . argz) #`(#,Eᵢ . argz)])))) + #'(Eᵢ …))] + T + (expand-type #'T applicable?)))]] + +The @tc[Letrec] special form behaves in a similar way, but uses +@racket[with-rec-bindings], so that the right-hand-side expressions +@racket[Eᵢ] appear to be within the scope of all the @racket[Vᵢ] bindings. + +@CHUNK[ + [((~commit (~literal Letrec)) ([Vᵢ:id Eᵢ] …) T:type) + (rule Letrec + (with-rec-bindings [(Vᵢ …) + (λ (Eᵢ) + (make-type-expander + (λ (stx) + (syntax-case stx () + [self (identifier? #'self) Eᵢ] + [(self . args444) #`(#,Eᵢ . args444)])))) + Eᵢ] + T + (expand-type #'T applicable?)))]] + +@subsubsection{Anonymous types with @racket[Λ]} + +When an anonymous type expander appears as the first element of its enclosing +form, it is applied to the given arguments. We use the +@racket[trampoline-eval] function defined in another file, which evaluates the +given quoted transformer expression, while limiting the issues related to +scopes. The ``official'' @racket[eval] function from +@racketmodname[racket/base] removes one of the module scopes which are +normally present on the expression to evaluate. In our case, we are evaluating +an anonymous type expander, i.e. a transformer function. When using +@racket[eval], identifiers generated by the transformer function may not have +the expected bindings. The alternative @racket[trampoline-eval] seems to solve +this problem. + +The @racket[auto-syntax-case] form is used, so that an anonymous type expander +@racket[(Λ (_ a b) …)] can either use @racket[a] and @racket[b] as pattern +variables in quoted syntax objects, or as regular values (i.e +@racket[syntax->datum] is automatically applied on the syntax pattern +variables when they are used outside of syntax templates, instead of throwing +an error). + +@chunk[ + (trampoline-eval + #'(λ (stx) + (define ctxx (make-syntax-introducer)) + (ctxx (auto-syntax-case (ctxx (stx-cdr stx)) () + [formals (let () . body)]))))] + +This case works by locally binding a fresh identifier @racket[tmp] to a type +expander, and then applying that type expander. It would also be possible to +immediately invoke the type expander function. + +@chunk[ + [{~and whole (({~literal Λ} formals . body) . __args)} + ;; TODO: use the same code as for the not-applicable case, to avoid ≠ + (rule app-Λ + (with-syntax* ([tmp (gensym '#%Λ-app-)] + [call-stx #'(tmp . whole)]) + (with-bindings [tmp (make-type-expander + )] + call-stx + (expand-type #'call-stx applicable?))))]] + +When a @racket[Λ] anonymous type expander appears on its own, in a +non-applicable position, it is expanded like an +@tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier macro} would +be. + +This case is implemented like the @racket[] case, i.e. +by locally binding a fresh identifier @racket[tmp] to a type expander, and +then applying that type expander. The difference is that in the +@tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier macro} case, +the syntax object given as an argument to the type expander contains only the +generated @racket[tmp] identifier. This allows the type expander to easily +recognise the @tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier + macro} case, where the whole syntax form is an identifier, from regular +applications, where the whole syntax form is a syntax pair. The whole original +syntax is attached @racket[cons]ed onto a syntax property named +@racket['original-Λ-syntax], in (unlikely) case the type expander needs to +access the original @racket[Λ] syntax used to call it (this is an experimental +feature, and may change without notice in later versions). + +@CHUNK[ + [{~and whole ({~literal Λ} formals . body)} + #:when (not applicable?) + (rule just-Λ/not-applicable + (with-syntax* ([tmp (syntax-property + (datum->syntax #'whole + (gensym '#%Λ-id-macro-) + #'whole + #'whole) + 'original-Λ-syntax + (cons #'whole + (or (syntax-property #'whole + 'original-Λ-syntax) + null)))] + [call-stx #'(tmp . tmp)]) + (with-bindings [tmp (make-type-expander + )] + call-stx + ;; applicable? should be #f here, otherwise it would have been + ;; caught by other cases. + (expand-type #'call-stx applicable?))))]] + +When a @racket[Λ] anonymous type expander appears on its own, in an applicable +position, it is returned without modification, so that the containing +application form may expand it with arguments (instead of expanding it like an +@tech[#:doc '(lib "scribblings/guide/guide.scrbl")]{identifier macro} would +be). + +@CHUNK[ + [(~and whole ({~literal Λ} formals . body)) + #:when applicable? + (rule just-Λ/applicable + #'whole)]] + +@subsubsection{Preventing the expansion of types with @racket[No-Expand]} + +The @racket[No-Expand] special form prevents the type expander from +re-expanding the result. This is useful for example for the implementation of +the fancy @racket[quote] expander, which relies on the built-in @racket[quote] +expander. It is also used to implement shadowing: type variables bound by +@racket[∀] in non-applicable positions and type variables bound by +@racket[Rec] are re-bound to type expanders returning +@racket[(No-Expand original-tvar)]. + +@CHUNK[ + [((~literal No-Expand) T) + (rule just-No-Expand + #'T)] + [(((~literal No-Expand) T) arg ...) + (rule app-No-Expand + #`(T #,@(stx-map (λ (τ) (expand-type τ #f)) #'(arg ...))))]] + +@subsubsection{The overloaded @racket[:] identifier} + +This case handles the colon identifiers @tc[:] (overloaded by this +library) and @|orig::| (provided by @racketmodname[typed/racket]). Wherever +the new overloaded @tc[:] identifier appears in a type, we want to convert it +back to the original @orig:: from @racketmodname[typed/racket]. The goal is +that a type of the form @racket[(→ Any Boolean : Integer)], using the new +@tc[:], will get translated to @orig:→AnyBoolean:Integer, using the old +@orig:: so that it gets properly interpreted by @racketmodname[typed/racket]'s +parser. + +@chunk[ + [(~and c (~literal new-:)) + (rule (datum->syntax #'here ': #'c #'c) + ':)]] + +@subsubsection{Last resort cases: leaving the type unchanged} + +If the type expression to expand was not matched by any of the above cases, +then it can still be an application of a polymorphic type @tc[T]. The +arguments @tc[TArg …] can contain uses of type expanders. We therefore expand +each separately, and combine the results. + +@CHUNK[ + [{~and whole (T TArg …)} + (rule app-fallback + (quasisyntax/loc #'whole + (T #,@(stx-map (λ (a) (expand-type a #f)) #'(TArg ...)))))]] + +As a last resort, we consider that the type @tc[T] (which +would most likely be an identifier) is either a built-in +type provided by @tc[typed/racket], or a user-declared type +introduced by @tc[define-type]. In both cases, we just leave +the type as-is. + +@CHUNK[ + [T + (rule just-fallback + #'T)]] + +@subsection{Debugging type expanders} + +In order to facilitate writing type expanders, it is possible to print the +inputs, steps and outputs of the expander using +@racket[(debug-type-expander #t)], which sets the value of +@racket[debug-type-expander?]. This can then be undone using +@racket[(debug-type-expander #f)]. + +@chunk[ + (define debug-type-expander? (box #f))] + +@chunk[ + (define-syntax (debug-type-expander stx) + (syntax-case stx () + [(_ #t) (set-box! debug-type-expander? #t) #'(void)] + [(_ #f) (set-box! debug-type-expander? #f) #'(void)]))] + +For better readability, each level of recursion indents the debugging +information: + +@chunk[ + (define indent (make-parameter 0))] + +@chunk[ + [indent (+ (indent) 3)]] + +Before expanding a term, it is printed: + +@chunk[ + (when (unbox debug-type-expander?) + (printf "~a~a ~a" + (make-string (indent) #\ ) + applicable? + (+scopes stx)))] + +Once the term has been expanded, the original term and the expanded term are +printed: + +@chunk[ + (when (unbox debug-type-expander?) + (printf "~a~a ~a\n~a=> ~a (case: ~a)\n" + (make-string (indent) #\ ) + applicable? + (+scopes stx) + (make-string (indent) #\ ) + (+scopes (car result)) + (cdr result)) + (when (= (indent) 0) + (print-full-scopes))) + (car result)] + +Finally, each rule for the type expander is wrapped with the @racket[rule] +macro, which prints the name of the rule, and returns a pair containing the +result and the rule's name, so that the debugging information indicates the +rule applied at each step. + +@chunk[ + (define-syntax-rule (rule name e) + (begin (when (unbox debug-type-expander?) + (printf "(case:~a)\n" + 'name)) + (cons e 'name)))] + +@section{Overloading @racket[typed/racket] forms} + +Throughout this section, we provide alternative definitions of the +@tc[typed/racket] forms @tc[:], @tc[lambda], @tc[define], @tc[struct], @tc[ann], +@tc[inst]… . We write these definitions with @tc[syntax-parse], using the syntax +classes defined in section @secref{type-expander|syntax-classes}. + +Most of the time, we will use the experimental @tc[template] macro from +@tc[syntax/parse/experimental/template] which allows more concise code than the +usual @code{#'()} and @code{#`()}. + +@subsection[#:tag "type-expander|syntax-classes"]{syntax classes} + +The syntax classes from +@tc[typed-racket/base-env/annotate-classes] match against +the @orig:: literal. Since we provide a new definition for +it, these syntax classes do not match code using our +definition of @tc[:]. We therefore cannot use the original +implementations of @tc[curried-formals] and +@tc[lambda-formals], and instead have to roll out our own +versions. + +We take that as an opportunity to expand the types directly from the syntax +classes using @tc[#:with], instead of doing that inside the macros that use +them. + +The @tc[colon] syntax class records the identifier it matches as a "disappeared +use", which means that DrRacket will draw an arrow from the library importing it +(either @racketmodname[typed/racket] or @racketmodname[type-expander]) to the +identifier. Unfortunately, this effect is not (yet) undone by +@racketmodname[syntax/parse]'s backtracking. See +@url{https://groups.google.com/forum/#!topic/racket-users/Nc1klmsj9ag} for more +details about this. + +@chunk[ + (define (remove-ddd stx) + (remove #'(... ...) (syntax->list stx) free-identifier=?))] + +@CHUNK[ + (define-syntax-class colon + #:attributes () + (pattern (~and {~or {~literal new-:} {~literal :}} + C + {~do (record-disappeared-uses (list #'C))}))) + + (define-splicing-syntax-class new-maybe-kw-type-vars + #:attributes ([vars 1] maybe) + (pattern kw+vars:lambda-type-vars + #:with (vars …) (remove-ddd #'kw+vars.type-vars) + #:with maybe #'kw+vars) + (pattern (~seq) + #:with (vars …) #'() + #:attr maybe #f)) + + (define-splicing-syntax-class new-maybe-type-vars + #:attributes ([vars 1] maybe) + (pattern v:type-variables + #:with (vars …) (remove-ddd #'v) + #:with maybe #'v) + (pattern (~seq) + #:with (vars …) #'() + #:attr maybe #f)) + + (define-splicing-syntax-class new-kw-formal + #:attributes ([expanded 1]) + (pattern (~seq kw:keyword id:id) + #:with (expanded ...) #'(kw id)) + (pattern (~seq kw:keyword [id:id + (~optional (~seq :colon type:type-expand!)) + (~optional default:expr)]) + #:with (expanded ...) + (template (kw [id (?@ : type.expanded) + (?? default)])))) + + (define-splicing-syntax-class new-mand-formal + #:attributes ([expanded 1]) + (pattern id:id + #:with (expanded ...) #'(id)) + (pattern [id:id :colon type:type-expand!] + #:with (expanded ...) + (template ([id : type.expanded]))) + (pattern kw:new-kw-formal + #:with (expanded ...) #'(kw.expanded ...))) + + (define-splicing-syntax-class new-opt-formal + #:attributes ([expanded 1]) + (pattern [id:id + (~optional (~seq :colon type:type-expand!)) + default:expr] + #:with (expanded ...) + (template ([id (?? (?@ : type.expanded)) + default]))) + (pattern kw:new-kw-formal + #:with (expanded ...) #'(kw.expanded ...))) + + (define-syntax-class new-rest-arg + #:attributes ([expanded 0]) + (pattern rest:id + #:with expanded #'rest) + (pattern (rest:id + :colon type:type-expand! + (~or (~and x* (~describe "*" (~or (~literal *) + (~literal ...*)))) + (~seq (~literal ...) bound:type-expand!))) + #:with expanded + (template (rest : type.expanded + (?? x* + (?@ (... ...) bound.expanded)))))) + + (define-syntax-class new-lambda-formals + (pattern (~or (mand:new-mand-formal ... + opt:new-opt-formal ... + . rest:new-rest-arg) + (mand:new-mand-formal ... + opt:new-opt-formal ...)) + ;; TODO: once template supports ?? in tail position, use it. + #:with expanded #`(mand.expanded ... + ... + opt.expanded ... + ... + . #,(if (attribute rest) + #'rest.expanded + #'())))) + + (define-syntax-class (new-curried-formals def-id) + (pattern (f:id . args:new-lambda-formals) + #:with expanded #`(#,def-id . args.expanded)) + (pattern ((~var lhs (new-curried-formals def-id)) + . args:new-lambda-formals) + #:with expanded #'(lhs.expanded . args.expanded))) + + (define-syntax-class new-curried-formals-id + (pattern (id:id . _)) + (pattern (lhs:new-curried-formals-id . _) + #:with id #'lhs.id)) + + (define-splicing-syntax-class new-optionally-annotated-name + (pattern (~seq name:id (~optional (~seq :colon type:type-expand!))) + #:with expanded + (template (name + (?? (?@ : type.expanded)))))) + + (define-syntax-class new-name-or-parenthesised-annotated-name + (pattern name:id + #:with expanded #'name) + (pattern [id:id :colon type:type-expand!] + #:with expanded + (template [id : type.expanded])))] + +@subsection{Overview of the overloaded primitives} + +The following sections merely define overloads for the +@racketmodname[typed/racket] primitives. The process is +similar each time: a new primitive is defined, e.g. +@tc[new-:] for @|orig::|. The new primitive calls the old one, +after having expanded (using @tc[expand-type]) all parts of +the syntax which contain types. Aside from heavy usage of +@tc[syntax-parse], there is not much to say concerning these +definitions. + +@subsection{@racket[:]} + +@CHUNK[<:> + (set-:-impl! (syntax-parser + [(_ x:id t:expr) + #`(: x #,(expand-type #'t #f))]))] + +@subsection{@racket[define-type]} + +@chunk[ + (define-syntax new-define-type + (syntax-parser + [(_ (~or name:id (name:id maybe-tvar …)) . whole-rest) + #:with (tvar …) (if (attribute maybe-tvar) #'(maybe-tvar …) #'()) + #:with (tvar-not-ooo …) (filter (λ (tv) (not (free-identifier=? tv #'(… …)))) + (syntax->list #'(tvar …))) + (start-tl-redirections + (with-bindings [(tvar-not-ooo …) (stx-map + #'(tvar-not-ooo …))] + whole-rest + (syntax-parse #'whole-rest + [(type:type-expand! . rest) + (template + (define-type (?? (name tvar …) name) + type.expanded + . rest))])))]))] + +@subsection{@racket[define]} + +@chunk[ + (define-syntax new-define + (f-start-tl-redirections + (syntax-parser + [(_ {~and (~seq _:new-maybe-kw-type-vars + (~or v:id + formals-id:new-curried-formals-id) + _ …) + (~with-tvars (tvars new-maybe-kw-type-vars) + (~or _:id + (~var formals (new-curried-formals + #'formals-id.id))) + (~optional (~seq :colon type:type-expand!)) + e ...)}) + (template + (define (?? (?@ . tvars.maybe)) (?? v formals.expanded) + (?? (?@ : type.expanded)) + e ...))])))] + +@subsection{@racket[lambda]} + +@CHUNK[ + (define-syntax new-lambda + (f-start-tl-redirections + (syntax-parser + [(_ {~with-tvars (tvars new-maybe-kw-type-vars) + args:new-lambda-formals + (~optional (~seq :colon ret-type:type-expand!)) + e …}) + (template (lambda (?? (?@ . tvars.maybe)) args.expanded + (?? (?@ : ret-type.expanded)) + e ...))])))] + +@subsection{@racket[case-lambda]} + +@CHUNK[ + (define-syntax new-case-lambda + (f-start-tl-redirections + (syntax-parser + [(_ {~with-tvars (tvars new-maybe-kw-type-vars) + [args:new-lambda-formals + (~optional (~seq :colon ret-type:type-expand!)) + e …] + …}) + (template (case-lambda + (?? (?@ #:∀ tvars.maybe)) + [args.expanded + (?? (ann (let () e …) ret-type.expanded) + (?@ e …))] + …))])))] + +@subsection{@racket[struct]} + +The name must be captured outside of the @racket[~with-tvars], as +@racket[~with-tvars] introduces everything in a new lexical context. + +@chunk[ + (define-syntax new-struct + (f-start-tl-redirections + (syntax-parser + [(_ (~and + (~seq _:new-maybe-type-vars + (~and (~seq name+parent …) + (~or (~seq name:id) + (~seq name:id parent:id))) + _ …) + {~with-tvars (tvars new-maybe-type-vars) + (~or (~seq _:id) + (~seq _:id _:id)) + ([field:id :colon type:type-expand!] ...) + rest …})) + (template (struct (?? tvars.maybe) name (?? parent) + ([field : type.expanded] ...) + rest …))])))] + +@subsection{@racket[define-struct/exec]} + +@chunk[ + (define-syntax (new-define-struct/exec stx) + (syntax-parse stx + [(_ (~and name+parent (~or name:id [name:id parent:id])) + ([field:id (~optional (~seq :colon type:type-expand!))] ...) + [proc :colon proc-type:type-expand!]) + (template (define-struct/exec name+parent + ([field (?? (?@ : type.expanded))] ...) + [proc : proc-type.expanded]))]))] + +@subsection{@racket[ann]} + +@chunk[ + (define-syntax/parse (new-ann value:expr + (~optional :colon) type:type-expand!) + (template (ann value type.expanded)))] + +@subsection{@racket[cast]} + +@chunk[ + (define-syntax/parse (new-cast value:expr type:type-expand!) + (template (cast value type.expanded)))] + +@subsection{@racket[unsafe-cast]} + +We additionally define an @racket[unsafe-cast] macro, which Typed/Racket does +not provide yet, but can easily be defined using @racket[unsafe-require/typed] +and a polymorphic function. + +@chunk[ + (module m-unsafe-cast typed/racket + (provide unsafe-cast-function) + (define (unsafe-cast-function [v : Any]) v)) + + (require (only-in typed/racket/unsafe unsafe-require/typed)) + (unsafe-require/typed 'm-unsafe-cast + [unsafe-cast-function (∀ (A) (→ Any A))]) + + (define-syntax-rule (unsafe-cast/no-expand v t) + ((inst unsafe-cast-function t) v)) + + (define-syntax/parse (unsafe-cast value:expr type:type-expand!) + (template (unsafe-cast/no-expand value type.expanded)))] + +@subsection{@racket[inst]} + +@chunk[ + (define-syntax new-inst + (syntax-parser + [(_ v (~optional :colon) t:type-expand! ... + last:type-expand! (~literal ...) b:id) + (template (inst v + t.expanded ... + last.expanded (... ...) b))] + [(_ v (~optional :colon) t:type-expand! ...) + (template (inst v t.expanded ...))]))] + +@subsection{@racket[row-inst]} + +@chunk[ + (define-syntax/parse (new-inst e row:type-expand!) + (template (row-inst e row.expanded)))] + +@subsection{@racket[let]} + +@chunk[ + (define-syntax new-let + (f-start-tl-redirections + (syntax-parser + [(_ (~optional (~seq loop:id + (~optional + (~seq :colon return-type:type-expand!)))) + (~with-tvars (tvars new-maybe-kw-type-vars) + ([name:new-optionally-annotated-name e:expr] ...) + rest ...)) + (template + (let (?? (?@ loop (?? (?@ : return-type.expanded)))) + (?@ . tvars) + ([(?@ . name.expanded) e] ...) + rest ...))])))] + +@subsection{@racket[let*]} + +@chunk[ + (define-syntax/parse + (new-let* + ([name:new-optionally-annotated-name e:expr] ...) + . rest) + (template + (let* ([(?@ . name.expanded) e] ...) . rest)))] + +@subsection{@racket[let-values]} + +@chunk[ + (define-syntax/parse + (new-let-values + ([(name:new-name-or-parenthesised-annotated-name ...) e:expr] ...) + . rest) + (template + (let-values ([(name.expanded ...) e] ...) + . rest)))] + +@subsection{@racket[make-predicate]} + +@chunk[ + (define-simple-macro (new-make-predicate type:type-expand!) + (make-predicate type.expanded))] + +@subsection{@racket[:type], @racket[:print-type], @racket[:query-type/args], + @racket[:query-type/result]} + +@chunk[<:type> + (define-syntax/parse (new-:type (~optional (~and verbose #:verbose)) + type:type-expand!) + (template (eval #'(#%top-interaction + . (:type (?? verbose) type.expanded)))))] + +@chunk[<:print-type> + (define-syntax/parse (new-:print-type e:expr) + #'(:print-type e) + #'(eval #'(#%top-interaction + . (:print-type e))))] + +@chunk[<:query-type/args> + (define-syntax/parse (new-:query-type/args f type:type-expand! …) + #'(eval #'(#%top-interaction + . (:query-type/args f type.expanded …))))] + +@chunk[<:query-type/result> + (define-syntax/parse (new-:query-type/result f type:type-expand!) + #'(eval #'(#%top-interaction + . (:query-type/result f type.expanded))))] + +@subsection{Type expanders for the typed classes} + +Not all forms are supported for now. + +@chunk[ + (define-syntax-class field-decl + (pattern id:id #:with expanded #'(field id)) + (pattern (maybe-renamed {~optional {~seq :colon type:type-expand!}} + {~optional default-value-expr}) + #:with expanded + (template (maybe-renamed (?? (?@ : type.expanded)) + (?? default-value-expr)))))] + +@chunk[ + (define-syntax-class field-clause + #:literals (field) + (pattern (field field-decl:field-decl …) + #:with expanded (template (field field-decl.expanded …))))] + +@chunk[ + (define-syntax-class super-new-clause + #:literals (super-new) + (pattern (super-new . rest) + #:with expanded (template (super-new . rest))))] + +@;{ + @chunk[ + (set-field-impl! + (syntax-parser [clause:field-clause #'clause.expanded]))] + + @chunk[ + (set-super-new-impl! + (syntax-parser [clause:super-new-clause #'clause.expanded]))]} + + +@chunk[ + (define-syntax-class class-clause + #:attributes (expanded) + (pattern :field-clause) + (pattern :super-new-clause))] + +@chunk[ + (define-syntax new-class + (f-start-tl-redirections + (syntax-parser + [(_ superclass-expr + {~with-tvars (tvars new-maybe-kw-type-vars) + clause:class-clause ...}) + (template (class superclass-expr + (?? (?@ . tvars.maybe)) + clause.expanded ...))])))] + +@subsection[#:tag "type-expander|other-forms"]{Other @racket[typed/racket] + forms} + +The other @tc[typed/racket] forms below do not have an alternative definition +yet. + +@chunk[ + (define-syntax (missing-forms stx) + (syntax-parse stx + [(_ name ...) + (define/with-syntax (tmp ...) (generate-temporaries #'(name ...))) + #'(begin + (begin + (define-syntax (tmp stx) + (raise-syntax-error + 'name + (format "~a not implemented yet for type-expander" 'name) + stx)) + (provide (rename-out [tmp name]))) + ...)])) + + (missing-forms + (code:comment ";TODO: add all-defined-out in prims.rkt") + (code:comment "; top-interaction.rkt") + (code:comment ":type") + (code:comment ":print-type") + (code:comment ":query-type/args") + (code:comment ":query-type/result") + (code:comment "; case-lambda.rkt") + (code:comment "case-lambda") + (code:comment "case-lambda:") + pcase-lambda: + (code:comment "; (submod \"prims-contract.rkt\" forms)") + require/opaque-type + (code:comment "require-typed-struct-legacy") + require-typed-struct + (code:comment "require/typed-legacy") + require/typed + require/typed/provide + require-typed-struct/provide + (code:comment "cast") + (code:comment "make-predicate") + define-predicate + (code:comment "; prims.rkt") + define-type-alias + define-new-subtype + define-typed-struct + define-typed-struct/exec + (code:comment "ann") + (code:comment "inst") + (code:comment ":") + define-struct: + define-struct + (code:comment "struct") + struct: + λ: + lambda: + (code:comment "lambda") + (code:comment "λ") + (code:comment "define") + (code:comment "let") + (code:comment "let*") + letrec + (code:comment "let-values") + letrec-values + let/cc + let/ec + let: + let*: + letrec: + let-values: + letrec-values: + let/cc: + let/ec: + for + for/list + for/vector + for/hash + for/hasheq + for/hasheqv + for/and + for/or + for/sum + for/product + for/lists + for/first + for/last + for/fold + for* + for*/list + for*/lists + for*/vector + for*/hash + for*/hasheq + for*/hasheqv + for*/and + for*/or + for*/sum + for*/product + for*/first + for*/last + for*/fold + for/set + for*/set + do + do: + with-handlers + define-struct/exec: + (code:comment "define-struct/exec"))] + +@section{Future work} + +We have not implemented alternative type-expanding definitions for all the +@tc[typed/racket] forms, as noted in @secref{type-expander|other-forms}. + +Integrating the type expander directly into typed/racket +would avoid the need to provide such definitions, and allow +using type expanders in vanilla @tc[typed/racket], instead +of having to @racket[require] this library. However, the +code wrapping the @tc[typed/racket] forms could be re-used +by other libraries that alter the way @tc[typed/racket] +works, so implementing the remaining forms could still be +useful. + +Also, we would need to provide a @tc[syntax-local-type-introduce] function, +similar to the @tc[syntax-local-match-introduce] function provided by @tc[match] +for example. + +@section{Conclusion} + +When an identifier is @racket[require]d from another module, +it is not the same as the one visible within the defining +module. This is a problem for @tc[:], because we match +against it in our syntax classes, using @tc[(~literal :)], +but when it is written in another module, for example +@tc[(define foo : Number 42)], it is not the same identifier +as the one used by original definition of @tc[:], and +therefore the @tc[(~literal :)] won't match. I suspect that +issue to be due to contract wrappers added by +@tc[typed/racket]. + +To get around that problem, we define @tc[:] in a separate module, and +@racket[require] it in the module containing the syntax classes: + +Since our @tc[new-:] macro needs to call the +@tc[type-expander], and the other forms too, we cannot +define @tc[type-expander] in the same module as these forms, +it needs to be either in the same module as @tc[new-:], or +in a separate module. Additionally, @tc[expand-type] needs +to be required @tc[for-syntax] by the forms, but needs to be +@tc[provide]d too, so it is much easier if it is defined in +a separate module (that will be used only by macros, so it +will be written in @tc[racket], not @tc[typed/racket]). + +@chunk[ + (module expander racket + (require (for-template typed/racket + "identifiers.rkt") + racket + (only-in racket/base [... …]) + syntax/parse + racket/format + racket/syntax + syntax/id-table + syntax/stx + auto-syntax-e + "parameterize-lexical-context.rkt" + debug-scopes) + ;; TODO: move this in a separate chunk and explain it + + (provide prop:type-expander + type-expander + apply-type-expander + ;bind-type-vars + expand-type + type + stx-type/c + type-expand! + debug-type-expander? + patched + make-type-expander) + + + + + + + + + + + ; + + + + + )] + +We can finally define the overloaded forms, as well as the +@tc[] form. + +@chunk[ + (module main typed/racket + (require (only-in typed/racket/base [... …]) + typed/racket/class + (for-syntax racket + (only-in racket/base [... …]) + racket/syntax + syntax/parse + syntax/parse/experimental/template + syntax/id-table + "parameterize-lexical-context.rkt" + syntax/stx) + (for-meta 2 racket/base syntax/parse) + "utils.rkt" + syntax/parse/define + "identifiers.rkt") + + (require (submod ".." expander)) + (require (for-syntax (submod ".." expander))) + (require (for-syntax typed-racket/base-env/annotate-classes)) + + (provide prop:type-expander + expand-type + define-type-expander + patch-type-expander + Let + Letrec + Λ + ...* + No-Expand + unsafe-cast/no-expand + unsafe-cast + debug-type-expander + (rename-out [new-: :] + [new-define-type define-type] + [new-define define] + [new-lambda lambda] + [new-lambda λ] + [new-case-lambda case-lambda] + [new-case-lambda case-lambda:] + [new-struct struct] + [new-define-struct/exec define-struct/exec] + [new-ann ann] + [new-cast cast] + [new-inst inst] + [new-let let] + [new-let* let*] + [new-let-values let-values] + [new-make-predicate make-predicate] + [new-:type :type] + [new-:print-type :print-type] + [new-:query-type/args :query-type/args] + [new-:query-type/result :query-type/result] + ;[new-field field] + ;[new-super-new super-new] + [new-class class])) + + (begin-for-syntax + (define-syntax ~with-tvars + (pattern-expander + (syntax-parser + [(_ (tv tv-stxclass) pat ...) + #'{~seq {~var tmp-tv tv-stxclass} + {~seq whole-rest (... ...)} + {~parse (({~var tv tv-stxclass}) pat ...) + ;; rebind tvars: + (with-bindings [(tmp-tv.vars (... ...)) + (stx-map + #'(tmp-tv.vars (... ...)))] + ;; rebind occurrences of the tvars within: + (tmp-tv whole-rest (... ...)) + ;; to (re-)parse: + #'(tmp-tv whole-rest (... ...)))}}])))) + + + + <:> + + + + + (begin-for-syntax + + + + (provide colon)) + + + + + + + + + + + + + + + + <:type> + <:print-type> + <:query-type/args> + <:query-type/result> + ; + + ; + )] + +We can now assemble the modules in this order: + +@chunk[<*> + + + + (require 'main) + (provide (except-out (all-from-out 'main) (for-syntax colon)))] diff --git a/utils.rkt b/utils.rkt new file mode 100644 index 0000000..78861b1 --- /dev/null +++ b/utils.rkt @@ -0,0 +1,13 @@ +#lang typed/racket + +(require (for-syntax syntax/parse)) + +(provide define-syntax/parse) + +;; Copied from phc-toolkit, but does not bind "stx". Use this-syntax +;; instead, from syntax/parse. +(define-syntax-rule (define-syntax/parse (name . args) body0 . body) + (define-syntax (name stx2) + ;(with-backtrace (syntax->datum stx2) + (syntax-parse stx2 + [(_ . args) body0 . body]))) \ No newline at end of file