deft

Following the semantics of of Janet's fn, arguments to define can include keywords and optional arguments.

Optional arguments are declared with &opt, default to nil and should work as expected with the default macro

(define opt [a b c &opt d e f]
  (default d 10)
  (default e 11)
  (default f 12)
  (+ a b c d e f))

(opt 1 2 3)         # => 39
(opt 1 2 3 4 5 6)   # => 21

Keyword arguments are declared with &keys and bind named :keyword parameters in function scope.

(define greet
  [name :string &keys {:greeting :string}]
  (string greeting ", " name "!"))

(greet "World" :greeting "Hello")  # => "Hello, World!"

(deftn draw
  [x :number &opt y :number &keys {:color :string}]
  (default y 0)
  (string color ": " (+ x y)))

(draw 1 2 :color "red")  # => "red: 3"

Variadic functions can be defined by including the & symbol for rest args. The rest tuple is untyped (i.e. :dynamic) by default.

(define sum
  [& xs :number]
  (var total 0)
  (each n xs (+= total n))
  total)
(sum 1 2 3)  # => 6

(define mix
  [x :number &opt y :number & tail :number]
  (default y 0)
  (+ x y (length tail)))

Adding a type annotation after the rest name types all the rest elements.

(define long
  [x :number & xs :number] :number
  (+ x (length xs)))

(long 1 2 3 4)  # => 4

It is also possible to ignore extra arguments using an unnamed & at the end of the argument list.

(deftfn ignore-extra
  [x :number &] :number
  (+ x 11))

(ignore-extra 1 2 3 4 5)  # => 12

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)

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

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

(lett [x :number 10
       y :string "hello"]
  (print x y))

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

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

(lett [(x :number 10)
       (y "hello")]
  (print x y))

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

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

Generated functions

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 [default]) — positional argument; required unless a default is given
• (optional name type [default]) — optional positional argument (defaults to nil or a given default), which can also be set via :keyword value
• (guard predicate-function) — optional guard predicate (for any extra validation)
• (=print handler-function) — optional custom pretty-print handler (for string based output)

Consider a :person, for example

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

A generated constructor can be used to create new records

(def p1 (make-person "Alice" 48)) # with 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")) # mixed

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 31) # returns {:name "Alice" :age 31 :title nil :nickname nil}

Adding a default value to a field or optional declaratoion provides an instantiation value if the argument is not provided. Any field with a default value therefore becomes optional at creation.

(deftrecord :settings
   (field host :string "localhost")
   (field port :number)
   (optional user :string "nobody"))

(make-settings 9999) # => @{:host "localhost" :port 9999 :user "nobody"}

A definition can include a guard predicate which has access to the declared fields. 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 :timeframe
  (field start :datetime)
  (field end :datetime)
  (guard (fn [v] (> (get v :end) (get v :start)))))

(make-timeframe  "2026-01-01T22:23:46" "2025-W17")

# => error: Type error (make-timeframe): guard predicate failed. fields may be incorrect.

Three quarks for Muster Mark!

—James Joyce, Finnegans Wake.

Use defenum to define an enumeration type using a string to value map. Values can be of any :type. defenum registers a type predicate and generates an accessor for looking up values by key. The functions <name>-extend and <name>-remove are also generated and can be used to modify the enum.

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

Generated functions

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 <name>-extend function adds or updates a key-value pair in the enumeration. 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 <name>-remove function removes a key from the enumeration and returns its previous value (or nil if not found).

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

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

(define 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

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)

Conditional forms for type driven flow control. A typecase matches clauses with isa? (which will match if the value satifies the given type's predicate or guard), while typecase-strict matches with type= (explicit type equality). In both forms, the value is evaluated exactly once. The result is nil when no clause matches.

(typecase value
  :number "n"
  :string "str")

(typecase 5 :posint "pos")   # => "pos"
(typecase -5 :posint "pos")  # => nil (guard rejects)
(typecase 42 :number "n")    # => "n"
(typecase true :number "n")  # => nil (no match, default finaliser)
(typecase-strict -5 :posint "pos") # => nil (raw type, no :posint clause)

A finaliser may be supplied as the final argument. When no clause matches, the finalser function is called with the value.

(typecase value
  :number "n"
  :string "str"
  (fn [x] (string "no match: " x)))

(typecase true
  :number "n"
  :string "str"
  (fn [x] (string "no match: " x)))   # => "no match: true"

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

(define identity-type [t :type] :type t)

(identity-type :number)  # returns :number
(identity-type number?)  # returns number?

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

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

Check if a value's type matches a given type. Uses the extended type to include user-declared types.

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

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

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

The consistency relation from Siek & Taha 2006. The type :dynamic is consistent with every type, otherwise it 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

Return the table used for mapping type names to predicates.

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

Enable or disable runtime type checking.

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

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 unknown types are synthesized upward from usage patterns (inference mode).

Type variables are resolved through unification with gradual semantics (i.e. :dynamic unifies with anything) and unresolved variables default to :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.

(enable-inference false)  # disable: untyped params become :dynamic
(enable-inference true)   # re-enable

Check if a value is a registered or built-in type. Returns true for e.g. :number, :string, function 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

Retrieve the registered type scheme (function contract) for a function at runtime. Returns a function contract, or nil for plain defn functions.

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

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

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

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

The &opt, &keys and rest-argument slots are folded into the function scheme as trailing argument types. An untyped rest slot is :dynamic and a typed rest slot records its element type.

Optional arguments

(deftn opt [x :number &opt y :number]
  (default y 0)
  (+ x y))
(fn-type-of 'opt)
# => (:fn @[:number :number] :dynamic)

Untyped variadic function

(deftn variadic [x :number & xs] :number
  (+ x (length xs)))
(fn-type-of 'variadic)
# => (:fn @[:number :dynamic] :number)

Typed variadic function

(deftn sum [& nums :number] :number
  (length nums))
(fn-type-of 'sum)
# => (:fn @[:number] :number)

Keyword arguments

(deftn greet2 [name :string &keys {:greeting :string}] :string
  (string greeting ", " name "!"))
(fn-type-of 'greet2)
# => (:fn @[:string :string] :string)

Positional, optional, and typed rest arguments

(deftn mix [x :number &opt y :number & tail :number] :number
  (default y 0)
  (+ x y (length tail)))
(fn-type-of 'mix)
# => (:fn @[:number :number :number] :number)

Ignored extra arguments

(deftn ignore-extra [x :number &] :number
  (+ x 1))
(fn-type-of 'ignore-extra)
# => (:fn @[:number :dynamic] :number)

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

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

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

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

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

Runtime function that checks a single deft form using bidirectional inference. Returns an array of error strings (the array is empty when there are 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"]

Return the inferred type of any s-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 "x"))                   # => :dynamic
(infer-expression '(+ x y) @{:x :number :y :number})  # => :number

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

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

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

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

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

# compiles (+ x y) is :number

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

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.