deft: gradual typing for Janet

The art of progress is to preserve order amid change, and to preserve change amid order.

—Alfred North Whitehead, Process and Reality

Overview

deft provides a way of adding optional type checks to Janet code at runtime, compile time, or ahead-of-time. The type system uses gradual typing as described by Siek & Taha, and the blame calculus of Wadler & Findler. It enables interoperability between typed and untyped (dynamically typed) forms. Type inference (bidirectional) and checking (static) can be enabled or disabled programatically. It has been designed to support a flexible, exploratory approach to working with types in Janet code.

In typed code, types appear at call boundaries (function call and return, value assignment, etc) and can be introduced (or changed) as needed. Arguments can be checked at function entry (blaming the caller), and return values at exit (blaming the function).

Various features, in no particular order

• Gradual typing with blame (co-existence of static/dynamic typing)
• NQ-Dependent types (types as predicates. Lacking Π or Σ types)
• Compound types (untagged union, intersection, sum, and container types)
• Record types (typed structs)
• Higher-order contracts (typed functions)
• Bidrectional inference (with unification)
• Boundary checks can be enabled or disabled
• Static type checking can be performed manually (e.g. with ‘jpm test’)
• Incompleteness and lack of conceptual rigour

Various features that may be possible, but not yet implemented

• Types as terms (?) dependent types with Π and Σ
• Type classes, kinds, traits (?)
• Multiple (?) dispatch based on type signature (?)
• Matching on supertypes of compound types
• Closer integration into Janet’s core type system

Installation

deft can be installed with jpm

jpm install https://codeberg.org/zzkt/deft

…or added to project.janet

:dependencies ["https://codeberg.com/zzkt/deft"]

…or installed locally

git clone https://codeberg.com/zzkt/deft
cd deft
jpm install

Then import the module (with an optional prefix (or “”))

(import deft :as deft)

There are some deft forms that share names with declarations in the Janet API (notably type, ->, and pp). By importing deft without a prefix, deft forms should take precedence. Note that most examples don’t include a prefix.

(import deft :prefix "")

Defining and using types

I knew that signs also allow others to judge the one who makes them, and that in the course of a galactic year tastes and ideas have time to change, and the way of regarding the earlier ones depends on what comes afterwards.

—Italo Calvino, Cosmicomics.

Type annotations can be used by adding a keyword immediately after a name wherever it’s declared in a deft form, e.g. (define five :number 5). Any of the built-in Janet types can be used, and new types can be created with deftype.

define

that finds the nameform that whets the wits

—James Joyce, Finnegans Wake.

Universal definition dispatcher, define is used to define functions and variables that can be gradually typed. It uses the shape of the definition arguments to exapnd to the appropriate underlying form, and is the recommended way to introduce new bindings in annotated code.

A typed function expects (optional) type declarations after each arg, and (optional) return type.

(define add
        [x :number y :number] :number
        (+ x y))

A docstring can be incdlued before the argument vector of function definitions (same as docstrings in defn)

(define factorial
  "Compute n! recursively."
  [n :number] :number
  (if (<= n 1) 1
    (* n (factorial (- n 1)))))

An untyped (or partially typed) function can be defined where omitted annotations default to the :dynamic type (or can be inferred at run time)

(define flex
  [a :number b c] :string
  (string (+ a b) " " c))

An untyped function without type declarations uses inference to determine arg types (when inference is enabled).

(define greet
  [name]
  (string "Hello, " name "!"))

A typed value guards an expression with a cast, using deftval. The value of any mutable type can be changed using set in the same way as an untyped value, or in a type aware way by using sett

(define phi :number 1.618033988)

An untyped value without type declarations behaves the same as var (mutable by default)

(define x 42)

Immutable typed constants can be declared using the :immutable type. Note that the inverse (using a :mutable type) is not necessarily true, since the :mutable type refers specifically to Janet’s built-in mutable data strutures (i.e. Array, Table and Buffer) by default.

(define phi (:and :number :immutable) 1.618033988)

If any parameter in the arg vector carries a type annotation, all parameters are parsed through parse-flex-args, those without annotations are typed as :dynamic (then inferred). The return type is optional and also defaults to :dynamic when omitted. When no parameters carry annotations, inference attempts to resolve types from the function body and generate casts accordingly.

Typed function bodies are wrapped in arg casts (checking each argument) and a return cast (checking the result). On failure, blame is assigned to the caller (bad argument) or the function (bad return).

The define macro replaces the need to choose between defn, deftfn, deftn, def, and deftval and provides a smooth (gradual) way of moving from untyped to typed code and back.

Shape	Behaviour
(define name [args+types] :ret body...)	Typed function (any or all params annotated)
(define name [args] body...)	Untyped function with inference via deftn
(define name :type value)	Typed value via deftval (cast at definition)
(define name value)	Untyped value via var

Further: Boundary cast semantics [cite:@siek-taha-2006]; Blame assignment [cite:@wadler-findler-2009]

deftype

Define a new type from a predicate. Predicate based type definition rely on the boolean output of a predicate function to determine if a value is of the given type or not. Predicates can be any form that returns a boolean. deftype shold be used for any user defined types.

An exsting predicate can be used to define a type. e.g the even numbers

(deftype :even even?)

Any function can be used as a predicate if it returns true or false. Type predicates should ideally be as simple as possible, side-effect free, and guarateed to return.

(deftype :positive (fn [v] (and (number? v) (> v 0))))
(deftype :negative (fn [v] (and (number? v) (< v 0))))

Type definitions can include types and typed functions.

(deftype :nonzero (or :positive (define [v :number] (< v 0))))

A type can be defined as a logical combination of other types. This technique can be used to define compound types which provide limited approximations of union types, intersection types, sum types, and negation types.

(deftype :nonzero (or :negative :positive))

(isa? -3 :nonzero) # returns true
(isa?  0 :nonzero) # returns false

There are also compound type operators that can be used to declare the element types of containers (i.e. :array, :tuple, :table, and :string types) at runtime. Note: the container types are currently hardcoded to include Janet’s containers and can’t (yet) be extended to user defined containers, however the elements can be of any type.

(deftfn sum-all [xs (:array :number)] :number (reduce + 0 xs))

(deftype :numeric-array (:array :number))

(deftfn sum-all [xs :numeric-array] :number (reduce + 0 xs))

Types defined with deftype can be used anywhere a type annotation is expected.

(deftfn pos-add [a :positive b :positive] :positive
  (+ a b))

(deftfn divide [a :number b :nonzero] :number
  (/ a b))

Using functions to define type predicates enables a limited form of (not quite) dependent typing. A type can be refined with it’s own value, but the declaration can’t access values of other type declarations. An argument value can’t be used in the type predicate of a return value (However, a function contract could provide a suitable way to dynamically manipulate return values if you insist…)

This makes it possible for example, to define the type “an array of 7 prime numbers” but not easily declare a return type that is “an array of numbers twice as long as the first argument to the calling function”.

Further: [cite:@siek-taha-2006] on the consistency relation extended to custom predicates.

Typed functions

deftfn

Define a gradually typed function. Every parameter must be followed by a type spec, the return type comes after the parameter vector. deftfn inserts runtime arg and return checks but does not register a :fn type scheme, so fn-type-of will not work for functions defined with deftfn (use deftn or define if you need to query a function’s type at runtime).

(deftfn add [x :number y :number] :number
  (+ x y))

(deftfn greet [name :string] :string
  (string "Hello, " name "!"))

deftfn-

Like deftfn but defines a private function (c.f defn-)

deftn

Define a function with optional type annotations. Parameters without an explicit type are inferred from usage in the function body (when inference is enabled) or default to :dynamic. The return type is optional and defaults to :dynamic when omitted. deftn registers a :fn type scheme, so fn-type-of can be used to query the function’s type at runtime.

typed and untyped params can be mixed

(deftn flex [a :number b c :string] :string
  (string (+ a b) " " c))

…and without annotations behaves the same as unaugmented defn

(deftn plain [x y]
  (+ x y))

Return type is optional

(deftn greet [name :string]
  (string "Hello, " name "!"))

Typed values

deftval

Define an immutable typed value.

(deftval phi :number 1.618033988)
(deftval name :string "golden ratio")

Can be used with user defined types.

(deftype :positive (fn [v] (and (number? v) (> v 0))))
(deftval three :positive 3)

deftv

Define a mutable typed value (using var rather than def).

(deftv counter :number 0)
(++ counter)

Typed local bindings

lett

Sequentially typed local bindings with type annotations. lett is like let* with optional type checks on each binding, and in every other respect should behave as closely as possible to Janet’s let. Bindings can be expressed as an array of one or more doubles (name value) or triples (name type value) or use a flat array [name type value ...] (all bindings must include a type). Values are cast to the declared type at bind time. In contrast to Janet’s let bindings, names bound with lett are mutable (similar to scheme or CL)

(lett [x :number 1318131
       y :string "Shikamoo"]
  (print x y))

Sequential binding allows later bindings see previous ones (c.f. let*)

(lett [x :number 5
       y :number (* x 2)]
  (print y))  # => 10

Bindings can be nested within a lexical scope

(lett [x :number 3]
  (lett [y :number (* x 3)]
    (print (+ x y))))

Bindings can use a more ‘traditional’ let syntax, with or without annotations.

(lett [(x :number 101)
       (y "nisam upoznat")]
  (print x y))

Composed and structured types

anonymous compound types

Compound type expressions can be used in parameter or return positions without a separate deftype using (:or ...), (:and ...), (:not ...) forms.

(deftype :positive (define [v :number] (> v 0)))
(deftype :negative (define [v :number] (< v 0)))

(define pos-or-neg [x (:or :positive :negative)] :number x)
(define pos-nonzero [x (:and :number :nonzero)] :number x)
(define not-str [x (:not :string)] x)

(pos-or-neg 5)    # returns 5
(pos-or-neg 0)    # type error

deftrecord

Define a named structural record type with typed field declarations. A definition will also generate a constructor, accessors, mutators (if mutable), and an optional :pp pretty-print handler.

Generated functions

Symbol	Purpose
make-{name}	Constructor (validates)
{name}-{field}	Accessor
set-{name}-{field}	Mutator (validates)

A record declaration consists of a keyword (the type) and field clauses. Required fields are declared first, then optional, then keyword pairs.

Field clauses

• (field name type) required positional argument
• (optional name type) optional positional argument (defaults to nil), can also be set via :keyword value
• (guard pred-fn) optional guard predicate (for any extra validation)
• (print handler-fn) optional custom pretty-print handler (for string based output)

(deftrecord :person
   (field name :string)
   (field age :number)
   (optional title :string)
   (optional nickname :string))

Using the constructor to create new records

(def p1 (make-person "Alice" 48)) # only required fields
(def p2 (make-person "Robert');" 19 "Mr." "Little Bobby Tables")) # optional positional
(def p3 (make-person "Frederick" 35 :nickname "Fred")) # keyword
(def p4 (make-person "Diindiisi" 73 "Dr." :nickname "Jay")) # mix

An accessor can be used to return the value of a field.

(person-name p1) # returns "Alice"

If a field is mutable, a mutator can be used to set the value of the field.

(set-person-age p1 49) # returns {:name "Alice" :age 49 :title nil :nickname nil}

A definition can include a guard predicate which has access to the declared fields and shares the lexical scope of the deftrecord. A guard predicate follows the same semantics as a type predicate. A guard can extend the validation of a single field (c.f. type narrowing) and also validate relations between fields. e.g. a guard can be used to check that an end field of type :datetime occurs later than the start field.

(deftrecord :pos-pair
  (field a :number)
  (field b :number)
  (guard (fn [v] (> (* (get v :a) (get v :b)) 0))))

defenum

Three quarks for Muster Mark!

Define an enumeration type from a string to value map. Values can be of any :type. The macro registers a type predicate and generates an accessor for looking up values by key. The macro also creates the functions ‘<name>-extend’ and ‘<name>-remove’ which can be used to modify the enum.

(defenum :colour {"red" 1 "green" 2 "blue" 3})

Generated functions

Symbol	Purpose
{name}	Lookup value by key
{name}-extend	Add or update a key-value pair
{name}-remove	Remove a key and return its value

The accessor function looks up a value in the enumeration table by key and returns the associated value or nil.

(colour "red")    # => 1
(colour "pink")   # => nil

The -extend function adds or updates a key-value pair in the enum table. The key must be a :string and the value must match the declared :type

(colour-extend "orange" 4)   # adds "orange" to 4 mapping
(colour "orange")            # returns 4

The -remove function removes a key from the enum table and returns its previous value (or nil if not found).

(colour-remove "green")      # removes "green", returns 2
(colour "green")             # returns nil

Mutation of the enum table is reflected immediately in the accessor function and the type predicate.

(deftfn colour-code [c :colour] :number
  (in (enum-table :colour) c))

(colour-code "red")          # returns 1
(colour-code "orange")       # returns 4

(colour-extend "pink" 7)
(colour-code "pink")         # returns 7

Type properties, checking and inference

type (extended)

Returns the type of a value. For values tagged with a user defined type it returns that tag, otherwise falls through to Janet’s built-in type.

(deftval three :positive 3)
(type three)       # returns :positive (user-defined tag)
(core-type three)  # returns :number (underlying Janet type)
(type 42)          # returns :number (no tag, core fallback)

:type

The type :type is the type of types. A type whose values are themselves types. Functions can take and return values of type :type (metaprogramming with types if you are into that sort of thing)

Further: [cite:@brady-2017].

(isa? :number :type)    # true
(isa? number? :type)    # true
(isa? 42 :type)         # false

(deftfn identity-type [t :type] :type t)
(identity-type :number)  # returns :number
(identity-type number?)  # returns number?

isa?

Runtime type check. Tests a value directly against a type predicate, bypassing any declared type. A value can match a type without that type being explicitly declared.

(isa? 42 :number)     # true
(isa? "zero" :number) # false
(isa? 5 :positive)    # true
(isa? 0 :positive)    # false
(isa? 5 :nonzero)     # true

type=

Check if a value’s type matches a given type. Uses an extended type that accounts for user-declared types.

(deftval three :positive 3)
(type= three :positive)     # true
(type= three :number)       # false  (tagged :positive)
(type= 42 :number)          # true   (no tag, core fallback)

type-name

Return the keyword name for a type value, or nil for anonymous predicates.

(type-name :number)    # returns :number
(type-name number?)    # returns nil

consistent?

The consistency relation from Siek & Taha 2006. :dynamic is consistent with every type, otherwise requires equality. Used internally as the core relation for gradual type checking.

(consistent? :number :number)  # true
(consistent? :number :string)  # false
(consistent? :number :dynamic) # true
(consistent? :dynamic :string) # true

registered-types

Return the table used for mapping type names to predicates.

(registered-types)  # e.g. @{:positive <fn> :nonzero <fn>}

enable-checking

Enable or disable runtime type checking.

(enable-checking false)  # disable all checks
(enable-checking true)   # enable the checks

enable-inference

Enable or disable bidirectional type inference for unannotated parameters (default: true).

(enable-inference false)  # disable type inference
(enable-inference true)   # enable type inference

When enabled, deftn and define run inference on unannotated parameters using a dual-mode bidirectional system. Known types propagate downward from operator type schemes and declared parameter types (checking mode), while any unknown types are synthesized upward from observing usage patterns (inference mode).

Type variables are resolved through unification with gradual semantics (i.e. :dynamic unifies with anything, and unresolved variables are typed as :dynamic.) The resulting inferred types are used to add runtime casts at the function boundaries, preserving blame semantics of explicit annotations.

When disabled, all unannotated parameters default to :dynamic so no inference or type-variable resolution occurs.

type?

Check if a value is a registered or built-in type. Returns true for e.g. :number, :string, :fn contracts, and user-defined types (via deftype, defenum, deftrecord). Returns false for non-type values.

(type? :number)      # => true
(type? :positive)    # => true
(type? :nonexistent) # => false
(type? 42)           # => false
(type? nil)          # => false

fn-type-of

Retrieve the registered type scheme for a function at runtime. Returns a function contract, or nil for functions declared with defn.

(deftn add [x y] (+ x y))

(fn-type-of 'add)
# => (:fn @[:number :number] :number)

(deftn strung [a :string x]
  (string a x))

(fn-type-of 'strung)
# => (:fn @[:string :dynamic] :string)

deftcheck (static checking)

Macro that wraps one or more deft forms and runs type consistency verification at compile time. Errors print to stderr before the wrapped forms are expanded. Reports mismatches between declared and inferred types, inconsistent argument usage, and flow-sensitive narrowing errors.

(deftcheck
  (define safe-division
    [a :number b :nonzero] :number
     (/ a b)))

(deftcheck
 (deftfn wrong
   [s :string] :number
    s))

# => deftcheck: 1 type error(s)
#      wrong: type mismatch: expected number, cannot unify string and number

See check-form for the equivalent runtime function and its error/return values.

check-form (runtime checking)

Runtime function that checks a single deft form using bidirectional inference. Returns an array of error strings (empty means no errors). Useful for programmatic or REPL driven validation.

(check-form '(deftn add [a b] (+ a b)))                  # => @[]
(check-form '(deftn flex [a :number b] (string a b)))    # => @[]

(check-form '(deftfn bad [s :string] :number s))
 # => @["bad: type mismatch: expected number, got: cannot unify string and number"]

infer-expression (ad-hoc inference)

Return the inferred type of any expression using bidirectional inference with gradual unification. An optional environment table maps symbols to their known types.

(infer-expression '(+ 1 2))                           # => :number
(infer-expression '(string 42 "!"))                   # => :string
(infer-expression '(if true 1 "O"))                   # => :dynamic
(infer-expression '(+ x y) @{:x :number :y :number})  # => :number

infer-expression-full (detailed inference)

Like infer-expression but returns a table with :type containing the inferred type, and :substitution containing the unification substitution after resolution.

(def info (infer-expression-full '(+ x 1) @{:x :number}))

(info :type)          # => :number
(info :substitution)  # => @{}

infer-assert-type (compile-time assertion)

An assert inside a deftn body that ensures the inferred type of an expression matches an expected type. Errors at macroexpansion time if the assertion fails.

(deftn safe-add [x y]
  (infer-assert-type :number (+ x y))
  (+ x y))

# compiles (+ x y) is :number

with-inference-trace (per-form tracing)

Wrap an inference call and print every sub-form with its inferred type to stderr.

(with-inference-trace
  (infer-expression '(+ 1 2)))

# stderr: infer 1 => :number
# stderr: infer 2 => :number
# stderr: infer (+ 1 2) => :number

enable-inference-trace

Toggle persistent tracing to see how types are inferred. Every argument and body form is logged to stderr with inferred and resolved types.

(enable-inference-trace true)
(deftn add [x y] (+ x y))

# stderr: --- infer-defn: add ---
# stderr:   infer  x  =>  :dynamic
# stderr:   infer  y  =>  :dynamic
# stderr:   infer  (+ x y)  =>  :number
# stderr:   resolved args:  [:number :number]  -> ret:  :number

(enable-inference-trace false)

The inference engine follows the approach of Siek & Vachharajani (2008) for gradual typing, extended with bidirectional checking via Dunfield & Krishnaswami (2021).

Further: [cite:@siek-vachharajani-2008] unification-based inference for gradual types; [cite:dunfield-krishnaswami-2021] Comprehensive survey of bidirectional type systems, covering the dual-mode (inference/checking) organisation used in deft; [cite:@miyazaki-2019] dynamic type inference for gradual Hindley–Milner.

Features

Thus the unfacts, did we possess them, are too imprecisely few to warrant our certitude

—James Joyce, Finnegans Wake.

deft implements a gradual typing approach to integrating static and dynamic typing within the same language. It has Features.

Blame

Without Contraries is no progression.

—William Blake, The Marriage of Heaven and Hell

When a cast fails, blame is assigned to either the caller or the function

• Caller blamed. Argument type mismatch (i.e. caller passed a bad value)
• Function blamed. Return type mismatch (i.e. function returned a bad value)

This enables you to locate the source of a type error without using a full static type checker.

Further: [cite:@wadler-findler-2009]; also the higher-order blame semantics in [cite:@siek-garcia-taha-2009].

Consistency

The consistency relation is a core feature of gradual typing. It relies on the relation between types, rather than strict equality or static subtyping. Where a type is unknown, values are assigned the :dynamic type. The type :dynamic is consistent with every type and allows typed and untyped code to coexist. Consistency is symmetric but not transitive.

• :number ~ :dynamic → true
• :dynamic ~ :string → true
• :number ~ :string → false

Further: [cite:@siek-taha-2006] also; [cite:@garcia-2016] for the abstract specification of consistency.

Function Contracts

I had developed a system of my own, to shut him up: ‘Oh, no? And what does it mean then, in your opinion?’ He kept quiet: lacking imagination as he did, when a word began to have one meaning it promptly lost all the others.

—Italo Calvino, Cosmicomics, “A Sign in Space”

Higher-order function types (:fn [:a :b -> :return]) wrap arguments in contracts, each call (re)checks args and return types. A contract can be used to type a function. A contract can also be used as a return type (i.e. function that returns a function) and used to infer the type of values it operates on.

While it may be possible to define value-dependent predicates (e.g. to implement Π and Σ types) it’s currently fragile and error prone.

Note: arrow notation can use either ‘->’ or ‘:->’ as preferred, however this is only syntactic and not a type class, nor first-class arrows.

(deftfn map2
  [f (:fn [:number :number -> :number]) a :number b :number] :number
  (f a b))

(map2 (fn [x y] (+ x y)) 3 4)  # returns 7
(map2 |(+ $0 $1) 3 4)          # returns 7

Further: [cite:@findler-felleisen-2002] higher-order contract system; [cite:@wadler-findler-2009] on blame for higher-order casts; [cite:@siek-garcia-taha-2009] on the design space of higher-order casts.

Occurrence Typing & Narrowing

All that you touch you Change. All that you Change changes you.

—Octavia Butler, Parable of the Sower

At some points of evaluation (e.g. arithmetic operations) and flow control (e.g. if branches) a variable’s type can be treated as more specific (narrowed) based on use and predicate checks (number?, string?, etc.) e.g. in the true branch of (= :keyword x), x is treated as :keyword.

This follows the occurance typing approach as described in Tobin-Hochstadt & Felleisen (2008) and Kent, Kempe & Tobin-Hochstadt (2016).

Further: [cite:@tobin-hochstadt-felleisen-2008] occurrence typing in Typed Scheme, reference for flow-sensitive type narrowing; [cite:@kent-2016] generalisation of occurrence typing modulo external theories.

Local Type Inference

Unannotated parameters in deftn and define are inferred from usage in the function body, e.g. arithmetic operators (+, -, *, /) imply :number, the string function implies :string, etc.

(deftn add [x y] (+ x y))  # x: :number, y: :number, return :number
(deftn greet [a :string x] (string a x))  # x: :dynamic, return :string

See Type properties, checking and inference for the details; infer-expression, infer-expression-full, fn-type-of, infer-assert-type, with-inference-trace, enable-inference-trace, deftcheck, and check-form.

Type schemes

Operators are registered with a :fn type scheme (function contract) which is used for inference.

Operator	Scheme
+, -, *, /	(:fn [:number :number] :number)
string	(:fn [:dynamic] :string)
string/join	(:fn [:array :string] :string)
<, >, =	(:fn [:number :number] :boolean)
not	(:fn [:boolean] :boolean)
length	(:fn [:dynamic] :number)
	etc…

Predicate narrowing

In if branches, the condition can be used to narrow variable types in each branch environment.

(deftn classify [x]
  (if (string? x)
    (string "got string: " x)           # x is narrowed to :string
    (string "got non-string: " x)))

Ways of Working

Nothing is so painful to the human mind as a great and sudden change.

—Mary Shelley, Frankenstein

deft supports several workflows depending on where you are in a project’s lifecycle. Gradual typing should ensure that adding type annotations never breaks working code.

Adding types to existing code

Start by converting a defn declaration to a define, annotate any hot paths or API surfaces first, leaving internals dynamic. Run the code to validate behaviour, then add annotations as your understanding develops.

Start with an unannotated function

(define process
  [data threshold]
  (filter |(> $ threshold) data))

Type the boundary, leave internals dynamic

(define process
  [data :array threshold :number]
  (filter |(> $ threshold) data))

Tighten return type once internal behaviour is stable

(define process
  [data :array threshold :number] :array
  (filter |(> $ threshold) data))

Cast failure (blame) can tell you where any mismatch occurs; caller-blamed means the caller passed a mismatched value, function-blamed means the function returned one. Use this to locate any source of inconsistencies without requiring a full static check.

Further: [cite:@siek-2015] the gradual guarantee that adding types never breaks working code.

Writing new exploratory code

Use define without return type annotations while prototyping. Any parameters that lack a type will default to :dynamic (equivalent to using defn), add annotations when any parameters require a specific type.

prototype without type annotations

(define analyse
  [data]
  (define helper [x] (+ 1 x))
  (map helper data))

As the shape solidifies, add meaningful annotations

(define analyse
  [data :array] :array
  (define helper [x :number] :number (+ 1 x))
  (map helper data))

The consistency relation guarantees that every step is backwards-compatible, annotations constrain but never break existing call sites.

Further reading: [cite:@siek-taha-2006] The consistency relation as the foundation of backwards-compatible annotation; [cite:@siek-2015] The gradual guarantee formalised.

Static analysis for correctness

Wrap deft forms in deftcheck to run compile-time type consistency verification. Errors are reported at compile time rather than at runtime.

deftcheck passes when all types are consistent

(deftcheck
  (deftfn safe-div [a :number b :nonzero] :number (/ a b))
  (deftfn greet [name :string] :string (string "Hello, " name)))

typed. catches return value declared as :string when expression yields :number

(check-form '(deftfn bad-ret [x :number] :string (+ x 1)))

typed. catches arg declared as :string but used in arithmetic

(check-form '(deftfn bad-add [s :string] :number (+ 3 s)))

untyped. no annotations, nothing to check (passes)

(check-form '(defn fine [s] (+ 3 s)))

The checker identifies

• Return type mismatches between declared and inferred types
• Arithmetic misuse (e.g. declared :string used in +, -, etc.)
• Function type violations (e.g. wrong number of args, or incorrect types)
• Flow-sensitive narrowing conflicts (e.g. predicate contradicts declared type)

Further: [cite:@rastogi-2015] ahead-of-time checking for hybrid type systems; [cite:@siek-taha-2006] the consistency relation checked at compile time.

Blame-driven debugging

Everything is real and not real, both real and not real, neither real nor not real.

—Nagarjuna, Mūlamadhyamakakārikā 18:8

When a cast fails at runtime, the blame error tells you which boundary to fix. This can be used in combination with deftcheck to catch as much as possible statically.

entry blame. caller passes wrong type

(define greet [n :string] :string
  (string "Hello, " n))

(greet "world")          # "Hello, world"
(greet 42)               # cast error: argument n expected :string, got :number
                         #   → blame: caller

return blame. function returns wrong type

(define broken
  [x :number] :string
  (+ x 1))               # (+ x 1) yields :number, declared :string

(broken 5)               # cast error: return expected :string, got :number
                         #   → blame: function

Errors can be bisected by disabling & enabling type checking. Turn off all runtime checks, run the test suite, re-enable checks one function at a time (or bisect) to isolate where an annotation carries a false assumption.

Further: [cite:@wadler-findler-2009] for blame calculus; [cite:@findler-felleisen-2002] for the contract system and blame tags.

Progressive typing by module boundary

The Hive is an idea that shapes reality.

—Ada Palmer, Too Like the Lightning

Following the Typed Racket model, add types one module at a time. Untyped modules are assumed to produce :dynamic values at their exports, and typed modules insert casts at the boundary.

untyped module. imports deft but doesn’t use annotations

(import deft)
(define parse-json [s] (json/decode s))

typed module. expects correctly typed input and output

(import deft)
(define parse-json
  [s :string] :json
  (json/decode s))

This lets you migrate a codebase module by module with the guarantee that existing code continues to work as expected.

Further: [cite:@tobin-hochstadt-felleisen-2008] the Typed Scheme module-system approach to gradual migration; [cite:@siek-2015] refinement of the gradual guarantee for inter-module typing.

Inference and refinement

Write untyped define or deftn forms and watch type inference deduce the types from usage. Use the inferred types as a guide, then add explicit annotations that match, or narrow them as needed. Types are assigned to argument bindings based on their usage in the function body.

An untyped function (where x,y =:number and z =:string is inferred)

(define process [x y z]
  (def sum (+ x y))
  (string sum " " z))

caller is blamed when wrong type is used…

(process 2 3 "items")    # returns "5 items" as a :string
(process "x" 2 "items")  # → Type error (process:x): expected :number, got "x"
(process 1 2 3)          # → Type error (process:z): expected :string, got 3

Add annotations from correct inference. Any type errors should provide information about how to correctly type the boundaries. Since all symbols passed directly to (string ...) are inferred as :string (or as types that can be cast to :string) and arithmetic operations infer :number these annotations can be added.

(define process
  [x :number y :number z :string]
  (def sum (+ x y))
  (string sum z))

Add a suitable type for the expected return value

(deftn process
  [x :number y :number z :string] :string
  (def sum (+ x y))
  (string sum z))

The return type can be computed directly by using the type function

(type (process 2 3 "items")) # returns :string

To help with adding annotations, you can query the inferred types using fn-type-of

(fn-type-of 'process)  # => (:fn @[:number :number :string] :string)

…or test individual expressions with infer-expression

(infer-expression '(+ x y) @{:x :number :y :number}) # => :number

(infer-expression '(string sum z) @{:sum :number :z :string})  # => :string

If unexpected type errors appear, add tests to ensure correct behaviour with expected args, or that the arg types haven’t been narrowed too tightly.

Further: [cite:@siek-vachharajani-2008]

Static verification

Use check-form to statically verify any form without executing it

(check-form '(deftn add [a b] (+ a b)))

# returns @[] i.e. no errors

(check-form '(deftn wrong [s :string n] (+ s n)))

# returns @["wrong: arg 's' declared string but used in arithmetic"]

Further: [cite:@siek-vachharajani-2008] on inference-first refinement; [cite:@siek-2015] on the gradual guarantee.

Contract escalation

Start with simple type annotations, escalate to higher-order :fn contracts for critical boundaries that need per-call argument and return-value checks. [cite:@findler-felleisen-2002]

References and reading

A comprehensive overview of gradual typing research can be found in the Gradual Typing Bibliography.

• Gradual Typing for Functional Languages, Siek & Taha 2006. [cite:@siek-taha-2006] Foundations of the consistency relation and typing with :dynamic. Scheme and Functional Programming Workshop 2006
• Refined Criteria for Gradual Typing, Siek et al. 2015. [cite:@siek-2015] Formalises the gradual guarantee: adding type annotations to a term never breaks existing well-typed programs under the same (or more permissive) typing context. 10.4230/LIPIcs.SNAPL.2015.274
• Contracts for Higher-Order Functions, Findler & Felleisen 2002. [cite:@findler-felleisen-2002] Function contract boundaries and higher-order contracts. 10.1145/581478.581484
• Abstracting Gradual Typing, Garcia et al. 2016. [cite:@garcia-2016] Provides an abstract-specification framework for gradual type systems via the abstracting discipline, unifying the design space of consistency, predicates, and the gradual guarantee. 10.1145/2837614.2837670
• Occurrence Typing Modulo Theories, Kent, Kempe & Tobin-Hochstadt 2016. [cite:@kent-2016] Generalisation of occurrence typing to work with external predicate theories, narrowing variable types under arbitrary compound predicates. 10.1145/2908080.2908091
• Dynamic Type Inference for Gradual Hindley–Milner, Miyazaki, Sekiyama & Igarashi 2019. [cite:@miyazaki-2019] Extension of gradual inference to a Hindley–Milner style. 10.1145/3290331
• The Safe TypeScript Type System, Rastogi et al. 2015. [cite:@rastogi-2015] Ahead-of-time static verification for hybrid typed-untyped programs. 10.1145/2676726.2676971
• Exploring the Design Space of Higher-Order Casts, Siek, Garcia & Taha 2009. [cite:@siek-garcia-taha-2009] 10.1007/978-3-642-00590-9_2
• Gradual Typing with Unification-Based Inference, Siek & Vachharajani 2008. [cite:@siek-vachharajani-2008] Local type inference for unannotated parameters. 10.1145/1408681.1408688
• The Design and Implementation of Typed Scheme, Tobin-Hochstadt & Felleisen 2008. [cite:@tobin-hochstadt-felleisen-2008] Occurrence typing, flow-sensitive type narrowing based on predicate checks. The module boundary approach for progressive typing. 10.1145/1328438.1328486
• Well-Typed Programs Can’t Be Blamed, Wadler & Findler 2009. [cite:@wadler-findler-2009] Blame assignment for runtime casts. 10.1007/978-3-642-00590-9_1
• Type-Driven Development with Idris, Edwin Brady 2017. [cite:@brady-2017] Practical introduction to type-driven development using dependent types. ISBN 9781617293023