You are looking at historical revision 36679 of this page. It may differ significantly from its current revision.

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. Basically returns #t iff t2 is a subtype of (or of equal type to) t1.

In addition, mutates typeenv 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