Add per-namespace flag to check annotations at runtime

Description

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 type t 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 to fact2 or fact3? define/contract in racket does the latter, while racket/contract does the former.

Pull request: 84
Commit: 868a4ff

Environment

None
Completed
Your pinned fields
Click on the next to a field label to start pinning.

Assignee

Ambrose Bonnaire-Sergeant

Reporter

Ambrose Bonnaire-Sergeant