Changeset 36679 in project

Timestamp:

10/05/18 18:10:26 (10 days ago)

Author:

megane

Message:

Add some docs for scrutinizer

File:

• wiki/scrutinizer (modified) (1 diff)

wiki/scrutinizer

@@ +1 @@
+[[toc:]]
+[[tags: internals]]
+
+== 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:
+
+<enscript highlight="scheme">
+(let ((x (the (list-of symbol))))
+  (if (pair? x) <branch-c> <branch-a>))
+</enscript>
+
+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:
+
+<enscript highlight="scheme">
+(let ((x (foo)))
+  (length x))
+</enscript>
+
+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 *)}}.
+
+* Ideally if {{t2}} is a subtype of {{t1}} (t2 <= t1 and {{(match-types t1 t2)}}
+returns true) refine-types should return {{t2}}.
+
+Simple case: {{(refine-types '(or symbol number) 'symbol) -> 'symbol}}.
+
+=== TODO
+* how function calls are checked
+* enabling debug output
+
+=== possible topics
+* what is type
+* subtype relation
+* typeenv / forall / type variables
+* how match-types works