1. Scrutinizer
    1. Type environment
    2. Some functions
      1. (match-types t1 t2 #!optional (typeenv (type-typeenv `(or ,t1 ,t2))) all)
      2. scrutinize -> (walk n e loc dest tail flow ctags)
      3. (refine-types t1 t2)
    3. TODO
    4. possible topics

Scrutinizer

Scrutinizer is the CHICKEN's type checker.

It checks type agreement in 2 situations: at function call sites and at assignments (set!).

In addition to type checking, scrutinizer does optimizations by doing tree re-writes for function calls using specializations and special-cases (define-special-case in scrutinizer).

Type environment

This is the big greek gamma letter one can see in the literature.

It's basically just a mapping from variable identifiers to types. Things are added to and removed from it while the node tree is walked and variables enter and leave the current scope.

It consists of three things:

type database
This is populated from the .types files before the walking starts.
e
The second argument to walk. id -> type alist
blist
("branch list"), when walking if nodes the variable types are updated only in the current if (tree) branch.

New mappings are added to e when walking let nodes (only?).

Some functions

(match-types t1 t2 #!optional (typeenv (type-typeenv `(or ,t1 ,t2))) all)

The heart of the scrutinizer.

Let V_(t) denote the set of runtime values the type t stands for. Examples:

V_(boolean) = {#t, #f}

V_(integer) = {0, 1, -1, 2, -2, ...}

V_((or boolean integer)) = {#t, #f, 0, 1, -1, 2, -2, ...}

When all is true match-types returns #t iff V_(t2) is a subset of V_(t1).

When all is false match-types returns #t iff the sets V_(t2) and V_(t1) intersect.

If all is true and match-types is true then it's safe to specialize.

If all is false and match-types if false it's safe to issue warning without risking a false positive.

In addition, this function mutates typeenv and the trail if unification happens.

scrutinize -> (walk n e loc dest tail flow ctags)
n
the canonicalized node (tree)
e
one part of "type environment". An alist from identifiers to type types.
flow and ctags
related to blist

Returns * for unknown number of return values, or (type ...) for known number of return values.

For example walking (begin) would return *. Walking (cons 'a 'b) would return ((pair symbol symbol)).

(refine-types t1 t2)

Given a variable has type t1 and it's learned that it also has type t2 this function returns a hopefully more detailed type for the variable.

There are two cases when this function is used:

Refining variable's type for if's branches when the if's test was a predicate:

(let ((x (the (list-of symbol))))
  (if (pair? x) <branch-c> <branch-a>))

Here pair? is a predicate for pair.

In <branch-c> we know x's type is pair in addition to '(list-of symbol). The variable's type will be updated, in blist, to (refine-types '(list-of symbol) 'pair) which would ideally return (pair symbol (list-of symbol)).

For <branch-a> x's type will be (refine-types '(list-of symbol) '(not pair)) which would ideally return null.

This kind of reasoning is called occurence typing in the literature.

In tests/scrutinizer-tests.scm the last case could be asserted with this: (test (~> (list-of symbol) (not pair) null))

Second place refine-type will be used is when calling functions with enforce-argument-types declaration:

(let ((x (foo)))
  (length x))

This will cause a x's type to be set (in blist) to (refine-types '* 'list), which should be list. list is an alias for (list-of *).

Simple case: (refine-types '(or symbol number) 'symbol) -> 'symbol.

TODO

possible topics