Trivial: type-tailored library functions
| (require trivial) | package: trivial |
The trivial module exports tailored versions of standard library functions.
1 What is Tailoring?
has the same specification and behavior as some library function f
but can catch runtime errors during expansion
and may typecheck a little smoother in Typed Racket.
1.1 Examples of Tailoring
For example, make a new Racket module with a malformed call to format:
#lang racket/base (format "batman and ~a")
This file will compile no problem (raco make file.rkt), but will raise a runtime error (racket file.rkt). If you add the line (require trivial), the file no longer compiles, but instead gives a helpful error message.
Here’s another example. Save the following (correct) Racket module:
#lang racket/base (define (get-sidekick str) (cond [(regexp-match #rx"^([a-z]+) and ([a-z]+)$" str) => caddr] [else "???"])) (get-sidekick "batman and alfred")
It should compile and run, returning "alfred". Great. Now try converting it to Typed Racket:
#lang typed/racket/base (define (get-sidekick (str : String)) : String (cond [(regexp-match #rx"^([a-z]+) and ([a-z]+)$" str) => caddr] [else "???"])) (get-sidekick "batman and alfred")
The file doesn’t compile anymore. Adding (require trivial) to the top of the file removes the error.
1.2 Technical Description
A tailored function f+ is really a macro that examines its call site and attempts to combine knowledge about the behavior of f with static properties of its arguments.
If all goes well, the tailoring will either (1) identify an error or (2) transform the call site into an equivalent—
In general, the static properties could be the result of any static analysis. But this library is limited to properties that other macros can establish through local analysis and propagate via syntax properties. See Defining new Tailorings for more details.
2 Using Tailorings
The following tailorings are all provided by the trivial module. Note that these tailorings have the same name as their Racket and Typed Racket equivalents to make this library a drop-in replacement for existing code.
The descriptions below assume familiarity with the Racket reference and describe only the new behavior of the tailored function or form. Click the name of any tailoring to see its definition in the Racket reference.
2.1 Built-in Tailorings
2.1.1 Definitions
| (require trivial/define) | package: trivial |
WARNING the static analysis implemented by trivial/define is unsound in the presence of set!. Do not set! in a module that uses trivial/define.
syntax
(define id expr)
syntax
(define (head args) expr)
2.1.2 Format Strings
| (require trivial/format) | package: trivial |
2.1.3 Functions
| (require trivial/function) | package: trivial |
syntax
(curry f)
When the arity of the procedure f is available during expansion, expands to a curried version of f. In other words, if f is a function of N arguments then (curry f) is a chain of N one-argument functions.
2.1.4 Integer Arithmetic
| (require trivial/integer) | package: trivial |
2.1.5 List Operations
| (require trivial/list) | package: trivial |
procedure
(make-list k v) → list?
k : exact-nonnegative-integer? v : any/c
procedure
(build-list k proc) → list?
k : exact-nonnegative-integer? proc : (-> exact-nonnegative-integer? any/c)
procedure
a : any/c d : any/c
procedure
p : pair?
procedure
p : pair?
procedure
v : any/c
procedure
(length lst) → exact-nonnegative-integer?
lst : list?
procedure
lst : pair? pos : exact-nonnegative-integer?
procedure
lst : pair? pos : exact-nonnegative-integer?
procedure
lst : list?
procedure
lst : list?
procedure
proc : procedure? lst : list?
procedure
lst : list? less-than? : (-> any/c any/c any/c)
Higher-order list functions check the arity of their functional argument; in particular, map includes a static check that the arity of its first argument includes the number of lists supplied at the call-site.
These Typed Racket examples demonstrate terms that would not typecheck without the trivial library.
> (ann (- (length '(1 2 3)) 3) Zero) - : Integer [more precisely: Zero]
0
> (ann (list-ref (make-list 5 0) 2) Zero) - : Integer [more precisely: Zero]
0
> (ann (list-ref (list-ref '((A)) 0) 0) 'A) - : 'A
'A
2.1.6 Regular Expressions
| (require trivial/regexp) | package: trivial |
procedure
str : string?
procedure
str : string?
procedure
(byte-regexp byt) → byte-regexp?
byt : bytes?
procedure
(byte-pregexp byt) → byte-pregexp?
byt : bytes?
procedure
(regexp-match pattern input)
→
(if (and (or (string? pattern) (regexp? pattern)) (or (string? input) (path? input))) (or/c #f (cons/c string? (listof (or/c string? #f)))) (or/c #f (cons/c bytes? (listof (or/c bytes? #f))))) pattern : (or/c string? bytes? regexp? byte-regexp?) input : (or/c string? bytes? path? input-port?)
This example is adapted from scribble/html-render
> (: parse-font-size : String -> (List String String (U #f String) String))
> (define (parse-font-size str) (or (regexp-match #rx"^([0-9]*\\.?([0-9]+)?)(em|ex|pt|%|)$" str) (error 'malformed-input)))
2.1.7 String Operations
| (require trivial/string) | package: trivial |
procedure
str : string?
procedure
(string-ref str k) → char?
str : string? k : exact-nonnegative-integer?
procedure
str : string? start : exact-nonnegative-integer? end : exact-nonnegative-integer? = (string-length str)
procedure
(string-append str ...) → string?
str : string?
procedure
(bytes-length bstr) → exact-nonnegative-integer?
bstr : bytes?
procedure
bstr : bytes? k : exact-nonnegative-integer?
procedure
bstr : bytes? start : exact-nonnegative-integer? end : exact-nonnegative-integer? = (bytes-length bstr)
procedure
(bytes-append bstr ...) → bytes?
bstr : bytes?
> (regexp-match (string-append "(" "a*" ")") "aaa") - : (U (List String String) False)
'("aaa" "aaa")
2.1.8 Vector Operations
| (require trivial/vector) | package: trivial |
procedure
v : any/c
procedure
(make-vector k v) → vector?
k : exact-nonnegative-integer? v : any/c
procedure
(build-vector k proc) → vector?
k : exact-nonnegative-integer? proc : (-> exact-nonnegative-integer? any/c)
procedure
(vector-append vec ...) → vector?
vec : vector?
procedure
(vector-ref vec pos) → any/c
vec : vector? pos : exact-nonnegative-integer?
procedure
vec : vector?
procedure
(vector-set! vec pos v) → vector?
vec : vector? pos : exact-nonnegative-integer? v : any/c
procedure
(vector-map proc vec ...) → vector?
proc : procedure? vec : vector?
procedure
(vector-map! proc vec ...) → void?
proc : procedure? vec : vector?
procedure
(vector->list vec) → list?
vec : vector?
procedure
(vector->immutable-vector vec) → vector?
vec : vector?
procedure
(vector-fill! vec v) → void?
vec : vector? v : any/c
procedure
(vector-take vec pos) → vector?
vec : vector? pos : exact-nonnegative-integer?
procedure
(vector-take-right vec pos) → vector?
vec : vector? pos : exact-nonnegative-integer?
procedure
(vector-drop vec pos) → vector?
vec : vector? pos : exact-nonnegative-integer?
procedure
(vector-drop-right vec pos) → vector?
vec : vector? pos : exact-nonnegative-integer?
2.2 Typed / Untyped Interaction
The macros provided by trivial and related submodules are all untyped, but should work with no problems in Typed Racket modules. Under the hood, these macros keep two copies of every tailored identifier and use syntax-local-typed-context? to choose the appropriate identifiers and whether to expand to type-annotated code.
3 Defining new Tailorings
| (require trivial/tailoring) | package: trivial |
The bindings documented in this section are not provided by the trivial module.
identify a property of Racket expressions,
define when & how to infer this property from #%datum literals,
define a set of tailorings that infer, propagate, and use the property
For example, here is a tailoring for add1. If the value of its argument is known during expansion, it expands to an integer.
#lang racket/base (require trivial/tailoring (for-syntax racket/base) (only-in racket/base [add1 λ-add1]) (only-in typed/racket/base [add1 τ-add1])) (define-tailoring (-add1 [e ~> e+ (φ [integer-domain ↦ i])]) #:with +add1 (τλ #'τ-add1 #'λ-add1) #:= (⊥? integer-domain i) (+add1 e+) #:+ #t '#,(+ i 1) #:φ (φ-set (φ-init) integer-domain (reduce integer-domain + i 1)))
-add1 is a macro expecting one argument, named e. (If -add1 is called with zero or +2 arguments, it expands to Racket’s add1.)
Note: the key integer-domain describes the relationship between e and i. In short, if tailorings that interact with integer-domain are implemented correctly, then expanding e yields and expression e+ with value i associated with the key integer-domain if and only if all run-time values for e are integers with value i.
-add1 expands its argument e to the term e+ and retrieves a dictionary φ of tailoring properties (see Tailoring Properties) associated with e+. It furthermore pattern-matches the dictionary φ to get the integer value i of the expression e+.- -add1 conditionally produces one of two syntax objects.
Any syntax object produced by expanding a call to -add1 with one argument has a new dictionary of tailoring properties (#:φ). The dictionary has one key, integer-domain. The corresponding value is "the indeterminate integer" when the value of i is indeterminate and (+ i 1) otherwise.
Here is the general form of define-tailoring:
syntax
(define-tailoring (tailored-id arg-pattern ...) guard ... defn ... #:= test-expr template #:+ then-expr template #:- then-expr expr #:φ prop-expr)
arg-pattern = (e-id elab-> e+-id (φ-id [key-id map-> val-id] ...)) guard = #:with expr expr | #:when expr | #:fail-unless expr expr defn = (define . expr) test-expr = expr prop-expr = expr elab-> = ~> | ⇝ map-> = -> | ↦
The arg-pattern clauses describe the shape of arguments to tailored-id. These say: expand e-id to e+-id, retrieve the tailoring properties φ-id associated with e+-id, and finally retrieve the values val-id associated with the given key-id.
If an arg-pattern is followed by a literal ..., then the tailoring accepts any number of arguments and matches each against arg-pattern. See the example for map below.
The guard expressions are a subset of the guards recognized by syntax-parse. Guards are most useful for defining variables based on the context in which the macro is expanding; see for example the #:with guard in -add1.
The defn expressions introduce local bindings.
The reason for #:+ etc. is so that define-tailoring can (1) log 'info messages for successful (#:+) and unsuccessful (#:=) tailorings (2) wrap each template in a syntax/loc based on use-sites of the tailoring.
#:= test-expr template uses test-expr to check whether the tailoring does not have enough information to transform the program. The template should implement "the standard Racket behavior" for tailored-id.
#:+ test-expr template determines when the tailoring can transform the program. The template may use unsafe operations, additional type annotations, or partial evaluation.
#:- test-expr expr detects errors statically and invokes expr to raise an exception. This clause is optional; when omitted, raises an internal exn:fail? about the inexhaustive tailoring.
Finally, prop-expr describes the result with a new dictionary of tailoring properties.
Note if any val-id is bound to a "top element" of the domain key-id, then define-tailoring raises an error message. See Property Domains for further intuition.
These examples contain free variables, but should convey the main ideas of define-tailoring. See the library implementation for working versions.
(define-tailoring (-vector-length [e ~> e+ (φ [vector-domain v])]) #:with +vl (τλ #'τ-vector-length #'λ-vector-length) (define n (vector-domain-length v)) #:= (⊥? V-dom v) (+vl e+) #:+ #t '#,n #:φ (φ-set (φ-init) integer-domain n))
(define-tailoring (-vector-ref [e1 ~> e1+ (φ1 [vector-domain ↦ v])] [e2 ~> e2+ (φ2 [integer-domain ↦ i])]) #:with +vector-ref (τλ #'τ-vector-ref #'λ-vector-ref) #:with +unsafe-vector-ref (τλ #'τ-unsafe-vector-ref #'λ-unsafe-vector-ref) (define n (vector-domain-length v)) #:= (or (⊥? vector-domain v) (⊥? integer-domain i)) (+vector-ref e1+ e2+) #:+ (and (<= 0 i) (< i n)) (+unsafe-vector-ref e1+ e2+) #:- #t (format-bounds-error #'e1+ i) #:φ (vector-domain-ref v i))
(define-tailoring (-map [f ~> f+ (φ1 [A-dom a])] [e* ~> e+* (φ* [L-dom l*])] ...) #:with +map (τλ #'τ-map #'λ-map) (define expected-arity (length l*)) (define arity-ok? (or (⊥? A-dom a) (= (length a) expected-arity))) (define n* (map L->I l*)) #:= (and (⊥? I-dom (⊓* I-dom n*)) arity-ok?) (+map f+ e+* ...) #:+ arity-ok? (+map f+ e+* ...) #:- #t (format-arity-error #'f+ expected-arity) #:φ (φ-set (φ-init) L-dom (I->L (⊓* I-dom n*))))
3.1 Property Domains
Every tailoring extracts and asserts properties about program expressions. For example, tailorings in trivial/vector assert properties about the size and contents of vector values. Tailorings in trivial/format assert properties about the formatting escapes in string values. The "properties of vectors" and "properties of format strings" are two examples of property domains.
A distinguished bottom element (⊥ D).
Interpretation: unknown property.
A (family of) top element(s) (⊤ D message).
Interpretation: contradictory property, because message.
A family of elements.
A partial order <=? relating elements to one another, and to the top and bottom element. For any element e and any string message, both (<=? (⊥ D) e) and (<=? e (⊤ D message)) hold.
syntax
(make-property-domain sym #:leq order clause ...)
sym : symbol?
order : (-> any/c any/c any/c)
generates symbols to represent the top and bottom elements,
lifts order to account for these top and bottom elements,
creates a syntax-parser from clause ...,
registers the new syntax parser with trivial/define.
The default order does not relate any elements to one another. It is (λ (x y) #false).
> (define integer-domain (make-property-domain Z #:leq <= [i:integer (syntax-e #'i)]))
> (define flat-integer-domain (make-property-domain flat-Z [i:integer (syntax-e #'i)]))
procedure
(property-domain? v) → boolean?
v : any/c
procedure
(in-domain? D) → (-> any/c boolean?)
D : property-domain?
procedure
(⊥ D) → (in-domain? D)
D : property-domain?
procedure
(⊤ D str) → (in-domain? D)
D : property-domain? str : string?
> (define bad-rx "foo ( bar") > (regexp-match bad-rx "any string") ~>: [1:0] Invalid regexp pattern (unmatched '(' at index 4)
in "foo ( bar"
procedure
D : property-domain? v : any/c
procedure
D : property-domain? v : any/c
procedure
(glb D v ...) → (in-domain? D)
D : property-domain? v : (in-domain? D)
procedure
(⊓ D v ...) → (in-domain? D)
D : property-domain? v : (in-domain? D)
procedure
(glb* D lst) → (in-domain? D)
D : property-domain? lst : (listof (in-domain? D))
procedure
(⊓* D lst) → (in-domain? D)
D : property-domain? lst : (listof (in-domain? D))
> (glb integer-domain 1 2 -3 0) -3
> (⊥? integer-domain (glb integer-domain 1 2 (⊥ integer-domain))) #t
procedure
(lub D v ...) → (in-domain? D)
D : property-domain? v : (in-domain? D)
procedure
(⊔ D v ...) → (in-domain? D)
D : property-domain? v : (in-domain? D)
procedure
(lub* D lst) → (in-domain? D)
D : property-domain? lst : (listof (in-domain? D))
procedure
(⊔* D lst) → (in-domain? D)
D : property-domain? lst : (listof (in-domain? D))
> (lub* integer-domain '(4 5 6)) 6
> (lub integer-domain 1 2 (⊥ integer-domain)) 2
procedure
(reduce D f init v ...) → (in-domain? D)
D : property-domain? f : (-> any/c any/c any/c) init : any/c v : (in-domain? D)
procedure
(reduce* D f init lst) → (in-domain? D)
D : property-domain? f : (-> any/c any/c any/c) init : any/c lst : (listof (in-domain? D))
> (reduce integer-domain + 8 6 7 5 3 0 9) 38
> (reduce flat-integer-domain + 0 2 2) 4
3.1.1 Built-in Property Domains
The following property domains are provided by the trivial/tailoring module.
value
(λ (x y z) x)
(x y z)
(listof (or/c Char Exact-Number))
value
value
(list #true #false)
#rx"(a*)(b)*"
value
The list-domain and vector-domain have additional operations. These are ⊥-propagating versions of their racket/list and racket/vector equivalents. (And there is probably a better or more-general way to lift these computations.)
procedure
v : (in-domain? vector-domain)
procedure
l : (in-domain? list-domain)
procedure
(list-domain->integer-domain l) → (in-domain? integer-domain)
l : (in-domain? list-domain)
procedure
(vector-domain->integer-domain v) → (in-domain? integer-domain)
v : (in-domain? vector-domain)
procedure
i : (in-domain? integer-domain)
procedure
(integer-domain->vector-domain i) → (in-domain? vector-domain)
i : (in-domain? integer-domain)
procedure
(list-domain-append* lst*) → (in-domain? list-domain)
lst* : (listof (in-domain? list-domain))
procedure
(list-domain-cons prop lst) → (in-domain? list-domain)
prop : φ? lst : (in-domain? list-domain)
procedure
(list-domain-car lst) → φ?
lst : (in-domain? list-domain)
procedure
(list-domain-cdr lst) → (in-domain? list-domain)
lst : (in-domain? list-domain)
procedure
(list-domain-length lst) → (in-domain? integer-domain)
lst : (in-domain? list-domain)
procedure
(list-domain-ref lst pos) → φ?
lst : (in-domain? list-domain) pos : (in-domain? integer-domain)
procedure
(list-domain-reverse lst) → (in-domain? list-domain)
lst : (in-domain? list-domain)
procedure
(list-domain-set lst pos prop) → (in-domain? list-domain)
lst : (in-domain? list-domain) pos : (in-domain? integer-domain) prop : φ?
procedure
(list-domain-slice lst lo hi) → (in-domain? list-domain)
lst : (in-domain? list-domain) lo : (in-domain? integer-domain) hi : (in-domain? integer-domain)
procedure
(vector-domain-append* lst*) → (in-domain? vector-domain)
lst* : (vectorof (in-domain? vector-domain))
procedure
(vector-domain-length lst) → (in-domain? integer-domain)
lst : (in-domain? vector-domain)
procedure
(vector-domain-ref lst pos) → φ?
lst : (in-domain? vector-domain) pos : (in-domain? integer-domain)
procedure
(vector-domain-set lst pos prop) → (in-domain? vector-domain)
lst : (in-domain? vector-domain) pos : (in-domain? integer-domain) prop : φ?
procedure
(vector-domain-slice lst lo hi) → (in-domain? vector-domain)
lst : (in-domain? vector-domain) lo : (in-domain? integer-domain) hi : (in-domain? integer-domain)
3.2 Tailoring Properties
Tailorings associate static properties to expressions using finite maps φ. Each map relates property domains to values in the domain (or the bottom element of the domain).
procedure
(φ-ref prop D) → (in-domain? D)
prop : φ? D : property-domain?
procedure
prop : φ? D : property-domain? v : (in-domain? d)
3.3 Miscellaneous
syntax
(τλ typed-id untyped-id)
value