Trivial: type-tailored library functions🔗 i

• 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.

• 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

• -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.

  • In the neutral case (#:=), when i is an indeterminate value, the result is a call to Racket’s (or Typed Racket’s) add1 .

  • In the positive case (#:+), when i is known during expansion, the result is the integer (+ i1)

• 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 (+ i1) otherwise.

syntax

( define-tailoring (tailored-idarg-pattern...)

guard...

defn...

#:=test-exprtemplate

#:+then-exprtemplate

#:-then-exprexpr

#:φprop-expr)

arg-pattern = (e-idelab->e+-id(φ-id[key-idmap->val-id]...))

guard = #:withexprexpr

| #:whenexpr

| #:fail-unlessexprexpr

defn = (define. expr)

test-expr = expr

prop-expr = expr

elab-> = ~>

| ⇝

map-> = ->

| ↦

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-exprtemplate 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-exprtemplate determines when the tailoring can transform the program. The template may use unsafe operations, additional type annotations, or partial evaluation.

• #:-test-exprexpr 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.

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-domv)

(+vle+)

#:+#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-refe1+e2+)

#:+(and (<= 0i)(< in))

(+unsafe-vector-refe1+e2+)

#:-#t

(format-bounds-error#' e1+i)

#:φ(vector-domain-ref vi))

(define-tailoring (-map[f~>f+(φ1[A-doma])]

[e*~>e+*(φ*[L-doml*])]... )

#:with+map(τλ #' τ-map#' λ-map)

(define expected-arity(length l*))

(define arity-ok?(or (⊥? A-doma)(= (length a)expected-arity)))

(define n*(map L->Il*))

#:=(and (⊥? I-dom(⊓* I-domn*))arity-ok?)

(+mapf+e+*... )

#:+arity-ok?

(+mapf+e+*... )

#:-#t

(format-arity-error#' f+expected-arity)

#:φ(φ-set (φ-init )L-dom(I->L(⊓* I-domn*))))