Completed
Details
Details
Assignee
Ambrose Bonnaire-Sergeant
Ambrose Bonnaire-SergeantReporter
Ambrose Bonnaire-Sergeant
Ambrose Bonnaire-SergeantFix versions
Priority
Created November 18, 2015 at 1:45 PM
Updated December 3, 2017 at 11:08 PM
Resolved December 3, 2017 at 11:08 PM
Problem
Sometimes (often) static type checking is just too much work to get started with on a new namespace. Contracts, on the other hand, are an easy buy-in: a single contract check can live in complete isolation.
It would be nice to support two situations:
1. Say, we are starting to port a completely untyped namespace to typed. It would take a long time for core.typed to give us any sort of guarantee about our code. Instead, we write static type annotations that get converted into contracts, then gradually get to the point where enough annotations are present to switch to typed mode.
2. Conversely, say we are rapidly developing some typed code, and keeping the file well-typed every iteration is difficult or impossible. Now, we ask core.typed to enforce annotations at runtime instead of completely disabling the static type checker. This way, we have some notion that it will be straightforward to recover well-typedness when the iterations have slowed down, since the contracts keep things in check.
Solution
There are several approaches to generating contracts that are possible.
This is the implemented solution.
Each form is 'collect'ed like usual for type annotations, so annotations are stored as usual.
Then we recur down the AST and look for two things:
1.
:def
Nodes - here, if there is a corresponding annotation of typet
and the :def is not a^:no-check
, we convert the def(def name init)
to(def name (cast t init))
.2.
ann-form
nodes - we perform a similar transformation from(ann-form e t)
to(ann-form (cast e t) t)
.All static type checking is removed, including any tracking of local variable types.
Some remaining questions:
it would be nice to fail silently (or some non-error behaviour, eg. custom or best effort cast) if a contract cannot be generated based on the static type being too complicated.
what kind of function contract do we want to generate? One that checks recursive calls?
eg. Do we transform
fact
tofact2
orfact3
? define/contract in racket does the latter, while racket/contract does the former.(ann fact [Int -> Int]) (defn fact [n] (if (zero? n) 1 (* n (fact n)))) ;; this checks fact2's input at each recursive call. ;; The implementation of fact2 must be internally consistent ;; with the interface it advertises, [Int -> Int]. ;; Also expensive. (def fact2 (cast [Int -> Int] (fn [n] (if (zero? n) 1 (* n (fact2 n)))))) ;; Less expensive, only one check per call, recursive calls don't ;; need to be [Int -> Int]. ;; Difference: fact3 is now a local variable rather than a var dereference, ;; if the semantics of fact3 rely on fact3 being a var, this seems bad. (defn fact3 [n] (letfn [(fact3 [n] (if (zero? n) 1 (* n (fact3 n))))] (cast [Int -> Int] (fact3 n))))
Pull request: 84
Commit: 868a4ff