Skeptic

Skeptic is a Leiningen plugin that statically type-checks Clojure projects based on Plumatic Schema annotations.

Experimental support for Malli is in development.

What Skeptic checks

• Call sites where inferred argument types do not fit the declared input schema:

  (s/defn inc-int :- s/Int
    [x :- s/Int]
    (+ x 1))
  
  (inc-int "1")  ; String flows into an s/Int parameter
  

• Return values where the inferred result does not fit the declared output schema:

  (s/defn as-int :- s/Int
    [x :- s/Int]
    (str x))  ; body returns String, not s/Int
  

• Nilability and structural mismatches that flow into declared schemas:

  (s/defn inc-int :- s/Int
    [x :- s/Int]
    (+ x 1))
  
  (s/defn caller
    [m :- {:n (s/maybe s/Int)}]
    (inc-int (:n m)))  ; (:n m) is (maybe s/Int); nil case flows into s/Int
  

Installation

Add the plugin to the :plugins vector in your project.clj:

:plugins [[org.clojars.nomicflux/lein-skeptic "0.8.0"]]

Or for the snapshot version:

:plugins [[org.clojars.nomicflux/lein-skeptic "0.8.1-SNAPSHOT"]]

Running it

From the project you want to check:

lein skeptic

lein skeptic exits with status 0 when no inconsistencies are found and status 1 when it reports inconsistencies.

Options:

• -n, --namespace NAMESPACE: only check one namespace.
• -c, --show-context: print local-variable and reference context for each result.
• -v, --verbose: print extra progress and debugging output.
• -a, --analyzer: print the analyzer forms for the namespace being checked.
• -k, --keep-empty: include analyzed expressions even when they produced no mismatches.
• --explain-full: show fully expanded structural forms in type-mismatch output instead of compact declared names.
• -p, --porcelain: emit machine-readable JSONL (one JSON object per line) instead of the default human-readable output. See Output below.
• --profile: profile the run (CPU, memory, wall-clock time). Long-only.
• -o, --output OUTPUT_FILE: write Skeptic's output to this file instead of stdout, so lein/JVM messages stay on stdout. Works with text and -p JSONL output.

Output

Text (default)

The default output is a human-readable, ANSI-coloured report, one block per inconsistency, grouped by namespace. Findings include the source of the reported type, such as Schema, Malli, a built-in/native declaration, a type override, or inference.

---------
Namespace: 		skeptic.showcase
Location: 		/Users/demouser/Code/skeptic/skeptic/src/skeptic/showcase.clj:10:3 [source: native]
Blame: 			context( value )
---
(str x)

has an output mismatch against the declared return type.

Declared return type expects:

Int

Problem fields:

	- Str but expected Int

---------
Namespace: 		skeptic.showcase
Location: 		/Users/demouser/Code/skeptic/skeptic/src/skeptic/showcase.clj:14:3 [source: schema]
Blame: 			context( value )
---
(:n m)

	in

(inc-int (:n m))

has inferred type incompatible with the expected type:

Problems:

	- a nullable value was provided where the type requires a non-null value

Per-namespace inconsistencies:
  skeptic.showcase: 2

When the run finds inconsistencies, the report ends with a per-namespace summary listing each affected namespace and its error count, sorted with the worst-offending namespace first.

JSONL (-p / --porcelain)

lein skeptic -p switches stdout to newline-delimited JSON. One object per line, in this order:

{"kind": "ns-discovery-warning", "path": "src/foo/broken.clj", "message": "..."}

{
  "kind": "finding",
  "ns": "foo.bar",
  "report_kind": "input",
  "location": {
    "file": "src/foo/bar.clj",
    "line": 42,
    "column": 3,
    "source": "schema"
  },
  "blame": "(+ 1 :x)",
  "blame_side": "term",
  "blame_polarity": "positive",
  "rule": "ground-mismatch",
  "actual_type":   {"t": "ground", "name": "Keyword"},
  "expected_type": {"t": "ground", "name": "Int"},
  "actual_type_str":   "Keyword",
  "expected_type_str": "Int",
  "focuses":             ["x"],
  "enclosing_form":      "(defn f [x] (+ 1 x))",
  "expanded_expression": "(clojure.core/+ 1 x)",
  "messages":            ["Keyword is not compatible with Int at ..."]
}

{
  "kind": "exception",
  "ns": "foo.bar",
  "phase": "declaration",
  "location": {
    "file": "src/foo/bar.clj",
    "line": 99,
    "source": "schema"
  },
  "blame": "my-fn",
  "exception_class": "java.lang.RuntimeException",
  "exception_message": "could not resolve schema",
  "messages": ["Skeptic hit an exception while checking declared schema for my-fn ..."]
}

{
  "kind": "namespace-error-summary",
  "counts": {
    "foo.bar": 5,
    "foo.baz": 2
  }
}

{
  "kind": "run-summary",
  "errored": true,
  "finding_count": 7,
  "exception_count": 1,
  "namespace_count": 12,
  "namespaces_with_findings": 3
}

Exit code matches text mode (0 clean, 1 otherwise).

See docs/jsonl-output.md for the full per-kind field spec and the structured type-tag reference.

Configuration

Skeptic reads optional project-level configuration from .skeptic/config.edn at the project root. The file is EDN and every key is optional.

{:exclude-files ["src/fixtures/*.clj"
                 "test/**/*_examples.clj"]
 :type-overrides {clojure.tools.logging/infof {:output (s/eq nil)}}}

:exclude-files

Vector of glob patterns matched against each file's path relative to the project root. Matched files are skipped entirely. Patterns use the platform's java.nio.file.PathMatcher glob syntax (*, **, ?, character classes).

:type-overrides

Map from fully-qualified symbol to an override map with any of :schema, :output, :arglists. Values are Plumatic Schema expressions evaluated with [schema.core :as s] in scope, so you can write (s/eq nil), s/Int, etc. Overrides replace whatever Skeptic would otherwise infer or collect for that symbol at call sites.

{:type-overrides {clojure.tools.logging/infof {:output (s/eq nil)}}}

After this, call sites of infof are checked as returning nil.

Experimental Malli support

Skeptic can read simple Malli function declarations from :malli/schema var metadata:

(defn takes-int
  {:malli/schema [:=> [:cat :int] :string]}
  [x]
  (str x))

Currently parsed forms include [:=> [:cat ...] out], primitive leaves such as :int, :string, :keyword, :boolean, and :any, plus :maybe, :or, :enum, and bare predicate symbols that Skeptic recognizes.

Broader Malli forms are still experimental. Unsupported forms are admitted when Malli accepts them; their Skeptic type is currently dynamic.

Suppressing checks

Skeptic provides three opt-out mechanisms for when its inference is wrong or too dynamic.

Ignoring a function body

Use :skeptic/ignore-body in a function's attribute map to skip checks inside the function body. The declared schema still applies to all callers:

(s/defn my-fn :- s/Int
  {:skeptic/ignore-body true}
  [x :- s/Int]
  (int-add nil x))

The body's internal mismatch (passing nil to int-add) is suppressed. Callers are still checked against the declared :- s/Int schema.

Treating a function as a black box

Use :skeptic/opaque in a function's attribute map to exclude both the function body and its schema from checking. Callers see the function as accepting and returning s/Any:

(s/defn my-fn :- s/Int
  {:skeptic/opaque true}
  [x :- s/Int]
  "not-an-int")

The body is not checked, and callers can pass any type and expect any type back.

Overriding an expression's type

Use ^{:skeptic/type T} metadata on an expression to pin its inferred type to schema T:

(let [y ^{:skeptic/type s/Int} (some-call-that-returns-any)]
  (int-add y 1))

The expression's type is treated as s/Int for subsequent checks. Clojure does not allow metadata on bare literal values (numbers, strings, keywords); wrap them in a form if needed:

^{:skeptic/type s/Int} (identity 42)

How it works

Skeptic loads the namespaces in your project, collects the Plumatic Schema annotations you've written on vars and functions, infers a type for each expression in your code, and compares the inferred types against the declared schemas on function inputs and outputs. Each mismatch is reported with a source location, the inferred type, and the expected type.

During lein skeptic, the checker runs with Plumatic Schema function validation disabled around the analysis pass. Projects that enable runtime Schema validation still keep that behavior for their own code; Skeptic simply avoids paying that validation cost while it is inspecting the project.

Attribution

Skeptic's cast semantics — how directional checks between inferred and declared types assign responsibility for a mismatch — are informed by the polymorphic blame calculus and runtime cast algorithm from:

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for All. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Austin, TX, USA, January 2011. ACM. https://doi.org/10.1145/1926385.1926409

The key takeaway is that Any is not treated as some sort of Top or Object type. Any (and internally, Dyn) is treated as a Dynamic type that should be treated as typechecking anything, until a more precise form can be inferred. This is what lets Skeptic work with dynamic code without requiring users to add in a library of type hints: proveable inconsistencies are flagged without required proof of consistency.

Building from source

To run an unreleased version of the plugin from a local checkout:

1. Running script/install-local.sh we delete old versions in you .m2 cache, install the Skeptic library, then install the lein-skeptic plugin. This will insure a clean run, but careful if you are running multiple versions.
2. Otherwise, run lein install in the skeptic/ directory first to install the core library, then again in the lein-skeptic/ directory to install the plugin.

License

The MIT License (MIT)