Uploaded image for project: 'core.typed'
  1. CTYP-299

Add per-namespace flag to check annotations at runtime

    Details

    • Type: Improvement
    • Status: Closed
    • Priority: Minor
    • Resolution: Completed
    • Affects versions: None
    • Fix versions: 0.3.19
    • Components: None
    • Labels:
      None

      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.

      (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

        Attachments

          Activity

            People

            • Assignee:
              ambrosebs Ambrose BS
              Reporter:
              ambrosebs Ambrose BS
            • Votes:
              0 Vote for this issue
              Watchers:
              0 Start watching this issue

              Dates

              • Created:
                Updated:
                Resolved: