Changeset 36679 in project
- Timestamp:
- 10/05/18 18:10:26 (5 months ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
wiki/scrutinizer
r36678 r36679 1 [[toc:]] 2 [[tags: internals]] 3 4 == Scrutinizer 5 Scrutinizer is the CHICKEN's type checker. 6 7 It checks type agreement in 2 situations: at function call sites and 8 at assignments (set!). 9 10 In addition to type checking, scrutinizer does optimizations by doing 11 tree re-writes for function calls using specializations and 12 special-cases ({{define-special-case}} in scrutinizer). 13 14 === Type environment 15 This is the big greek gamma letter one can see in the literature. 16 17 It's basically just a mapping from variable identifiers to types. 18 Things are added to and removed from it while the node tree is walked 19 and variables enter and leave the current scope. 20 21 It consists of three things: 22 23 ; type database : This is populated from the .types files before the 24 walking starts. 25 ; e : The second argument to {{walk}}. id -> type alist 26 ; blist : ("branch list"), when walking {{if}} nodes the variable 27 types are updated only in the current {{if}} (tree) branch. 28 29 New 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)}} 33 The heart of the scrutinizer. Basically returns {{#t}} iff {{t2}} is a 34 subtype of (or of equal type to) {{t1}}. 35 36 In 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 41 type types. 42 ; {{flow}} and {{ctags}} : related to blist 43 44 Returns {{*}} for unknown number of return values, or {{(type ...)}} for 45 known number of return values. 46 47 For example walking {{(begin)}} would return {{*}}. Walking {{(cons 'a 'b)}} would 48 return {{((pair symbol symbol))}}. 49 50 ==== (refine-types t1 t2) 51 Given 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 53 variable. 54 55 There are two cases when this function is used: 56 57 Refining variable's type for if's branches when the if's test was a 58 predicate: 59 60 <enscript highlight="scheme"> 61 (let ((x (the (list-of symbol)))) 62 (if (pair? x) <branch-c> <branch-a>)) 63 </enscript> 64 65 Here {{pair?}} is a predicate for {{pair}}. 66 67 In {{<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}}, 69 to: 70 {{(refine-types '(list-of symbol) 'pair)}} which would ideally return 71 {{(pair symbol (list-of symbol))}}. 72 73 For {{<branch-a>}} {{x}}'s type will be: 74 75 {{(refine-types '(list-of symbol) '(not pair))}} which would ideally 76 return {{null}}. 77 78 This kind of reasoning is called {{occurence typing}} in the 79 literature. 80 81 In {{tests/scrutinizer-tests.scm}} the last case could be asserted 82 with this: {{(test (~> (list-of symbol) (not pair) null))}} 83 84 Second 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 92 This 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)}} 97 returns true) refine-types should return {{t2}}. 98 99 Simple 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.