Changeset 36679 in project


Ignore:
Timestamp:
10/05/18 18:10:26 (10 days ago)
Author:
megane
Message:

Add some docs for scrutinizer

File:
1 edited

Legend:

Unmodified
Added
Removed
  • wiki/scrutinizer

    r36678 r36679  
     1[[toc:]]
     2[[tags: internals]]
     3
     4== Scrutinizer
     5Scrutinizer is the CHICKEN's type checker.
     6
     7It checks type agreement in 2 situations: at function call sites and
     8at assignments (set!).
     9
     10In addition to type checking, scrutinizer does optimizations by doing
     11tree re-writes for function calls using specializations and
     12special-cases ({{define-special-case}} in scrutinizer).
     13
     14=== Type environment
     15This is the big greek gamma letter one can see in the literature.
     16
     17It's basically just a mapping from variable identifiers to types.
     18Things are added to and removed from it while the node tree is walked
     19and variables enter and leave the current scope.
     20
     21It consists of three things:
     22
     23; type database : This is populated from the .types files before the
     24walking starts.
     25; e : The second argument to {{walk}}. id -> type alist
     26; blist : ("branch list"), when walking {{if}} nodes the variable
     27types are updated only in the current {{if}} (tree) branch.
     28
     29New mappings are added to {{e}} when walking {{let}} nodes (only?).
     30
     31=== Some functions
     32==== {{(match-types t1 t2 #!optional (typeenv (type-typeenv `(or ,t1 ,t2))) all)}}
     33The heart of the scrutinizer. Basically returns {{#t}} iff {{t2}} is a
     34subtype of (or of equal type to) {{t1}}.
     35
     36In addition, mutates typeenv if unification happens.
     37
     38==== scrutinize -> (walk n e loc dest tail flow ctags)
     39; {{n}} : the canonicalized node (tree)
     40; {{e}} : one part of "type environment". An alist from identifiers to
     41type types.
     42; {{flow}} and {{ctags}} : related to blist
     43
     44Returns {{*}} for unknown number of return values, or {{(type ...)}} for
     45known number of return values.
     46
     47For example walking {{(begin)}} would return {{*}}. Walking {{(cons 'a 'b)}} would
     48return {{((pair symbol symbol))}}.
     49
     50==== (refine-types t1 t2)
     51Given a variable has type {{t1}} and it's learned that it also has type
     52{{t2}} this function returns a hopefully more detailed type for the
     53variable.
     54
     55There are two cases when this function is used:
     56
     57Refining variable's type for if's branches when the if's test was a
     58predicate:
     59
     60<enscript highlight="scheme">
     61(let ((x (the (list-of symbol))))
     62  (if (pair? x) <branch-c> <branch-a>))
     63</enscript>
     64
     65Here {{pair?}} is a predicate for {{pair}}.
     66
     67In {{<branch-c>}} we know {{x}}'s type is {{pair}} in addition to
     68{{'(list-of symbol)}}. The variable's type will be updated, in {{blist}},
     69to:
     70{{(refine-types '(list-of symbol) 'pair)}} which would ideally return
     71{{(pair symbol (list-of symbol))}}.
     72
     73For {{<branch-a>}} {{x}}'s type will be:
     74
     75{{(refine-types '(list-of symbol) '(not pair))}} which would ideally
     76return {{null}}.
     77
     78This kind of reasoning is called {{occurence typing}} in the
     79literature.
     80
     81In {{tests/scrutinizer-tests.scm}} the last case could be asserted
     82with this: {{(test (~> (list-of symbol) (not pair) null))}}
     83
     84Second place refine-type will be used is when calling functions with
     85{{enforce-argument-types}} declaration:
     86
     87<enscript highlight="scheme">
     88(let ((x (foo)))
     89  (length x))
     90</enscript>
     91
     92This will cause a {{x}}'s type to be set (in blist) to {{(refine-types
     93'* 'list)}}, which should be {{list}}. {{list}} is an alias for
     94{{(list-of *)}}.
     95
     96* Ideally if {{t2}} is a subtype of {{t1}} (t2 <= t1 and {{(match-types t1 t2)}}
     97returns true) refine-types should return {{t2}}.
     98
     99Simple case: {{(refine-types '(or symbol number) 'symbol) -> 'symbol}}.
     100
     101=== TODO
     102* how function calls are checked
     103* enabling debug output
     104
     105=== possible topics
     106* what is type
     107* subtype relation
     108* typeenv / forall / type variables
     109* how match-types works
Note: See TracChangeset for help on using the changeset viewer.