1 USING: help.syntax help.markup kernel sequences words io
2 effects classes math combinators
6 stack-checker.transforms
11 ARTICLE: "inference-simple" "Straight-line stack effects"
12 "The simplest case is when a piece of code does not have any branches or recursion, and just pushes literals and calls words."
14 "Pushing a literal has stack effect " { $snippet "( -- object )" } ". The stack effect of a most words is always known statically from the declaration. Stack effects of " { $link POSTPONE: inline } " words and " { $link "macros" } ", may depend on literals pushed on the stack prior to the call, and this case is discussed in " { $link "inference-combinators" } "."
16 "The stack effect of each element in a code snippet is composed. The result is then the stack effect of the snippet."
19 { $example "[ 1 2 3 ] infer." "( -- object object object )" }
21 { $example "[ 2 + ] infer." "( object -- object )" } ;
23 ARTICLE: "inference-combinators" "Combinator stack effects"
24 "If a word, call it " { $snippet "W" } ", calls a combinator, one of the following two conditions must hold:"
26 { "The combinator may be called with a quotation that is either a literal, or built from literals, " { $link curry } " and " { $link compose } "." }
27 { "The combinator must be called on an input parameter, or be built from input parameters, literals, " { $link curry } " and " { $link compose } ", " { $strong "if" } " the word " { $snippet "W" } " must be declared " { $link POSTPONE: inline } ". Then " { $snippet "W" } " is itself considered to be a combinator, and its callers must satisfy one of these two conditions." }
29 "If neither condition holds, the stack checker throws a " { $link literal-expected } " error, and an escape hatch such as " { $link POSTPONE: call( } " must be used instead. See " { $link "inference-escape" } " for details. An inline combinator can be called with an unknown quotation by currying the quotation onto a literal quotation that uses " { $link POSTPONE: call( } "."
30 { $heading "Examples" }
31 { $subheading "Calling a combinator" }
32 "The following usage of " { $link map } " passes the stack checker, because the quotation is the result of " { $link curry } ":"
33 { $example "[ [ + ] curry map ] infer." "( object object -- object )" }
34 { $subheading "Defining an inline combinator" }
35 "The following word calls a quotation twice; the word is declared " { $link POSTPONE: inline } ", since it invokes " { $link call } " on the result of " { $link compose } " on an input parameter:"
36 { $code ": twice ( value quot -- result ) dup compose call ; inline" }
37 "The following code now passes the stack checker; it would fail were " { $snippet "twice" } " not declared " { $link POSTPONE: inline } ":"
38 { $unchecked-example "USE: math.functions" "[ [ sqrt ] twice ] infer." "( object -- object )" }
39 { $subheading "Defining a combinator for unknown quotations" }
40 "In the next example, " { $link POSTPONE: call( } " must be used because the quotation the result of calling a runtime accessor, and the compiler cannot make any static assumptions about this quotation at all:"
42 "TUPLE: action name quot ;"
43 ": perform ( value action -- result ) quot>> call( value -- result ) ;"
45 { $subheading "Passing an unknown quotation to an inline combinator" }
46 "Suppose we want to write :"
47 { $code ": perform ( values action -- results ) quot>> map ;" }
48 "However this fails to pass the stack checker since there is no guarantee the quotation has the right stack effect for " { $link map } ". It can be wrapped in a new quotation with a declaration:"
49 { $code ": perform ( values action -- results )" " quot>> [ call( value -- result ) ] curry map ;" }
50 { $heading "Explanation" }
51 "This restriction exists because without further information, one cannot say what the stack effect of " { $link call } " is; it depends on the given quotation. If the stack checker encounters a " { $link call } " without further information, a " { $link literal-expected } " error is raised."
53 "On the other hand, the stack effect of applying " { $link call } " to a literal quotation or a " { $link curry } " of a literal quotation is easy to compute; it behaves as if the quotation was substituted at that point."
54 { $heading "Limitations" }
55 "Passing a literal quotation on the data stack through an inlined recursive combinator nullifies its literal status. For example, the following will not infer:"
57 "[ [ reverse ] swap [ reverse ] map swap call ] infer." "Got a computed value where a literal quotation was expected\n\nType :help for debugging help."
59 "To make this work, pass the quotation on the retain stack instead:"
61 "[ [ reverse ] [ [ reverse ] map ] dip call ] infer." "( object -- object )"
64 ARTICLE: "inference-branches" "Branch stack effects"
65 "Conditionals such as " { $link if } " and combinators built on top have the same restrictions as " { $link POSTPONE: inline } " combinators (see " { $link "inference-combinators" } ") with the additional requirement that all branches leave the stack at the same height. If this is not the case, the stack checker throws a " { $link unbalanced-branches-error } "."
67 "If all branches leave the stack at the same height, then the stack effect of the conditional is just the maximum of the stack effect of each branch. For example,"
68 { $example "[ [ + ] [ drop ] if ] infer." "( object object object -- object )" }
69 "The call to " { $link if } " takes one value from the stack, a generalized boolean. The first branch " { $snippet "[ + ]" } " has stack effect " { $snippet "( x x -- x )" } " and the second has stack effect " { $snippet "( x -- )" } ". Since both branches decrease the height of the stack by one, we say that the stack effect of the two branches is " { $snippet "( x x -- x )" } ", and together with the boolean popped off the stack by " { $link if } ", this gives a total stack effect of " { $snippet "( x x x -- x )" } "." ;
71 ARTICLE: "inference-recursive-combinators" "Recursive combinator stack effects"
72 "Most combinators do not call themselves recursively directly; instead, they are implemented in terms of existing combinators, for example " { $link while } ", " { $link map } ", and the " { $link "compositional-combinators" } ". In these cases, the rules outlined in " { $link "inference-combinators" } " apply."
74 "Combinators which are recursive require additional care. In addition to being declared " { $link POSTPONE: inline } ", they must be declared " { $link POSTPONE: recursive } ". There are three restrictions that only apply to combinators with this declaration:"
75 { $heading "Input quotation declaration" }
76 "Input parameters which are quotations must be annotated as much in the stack effect. For example, the following will not infer:"
77 { $example ": bad ( quot -- ) [ call ] keep bad ; inline recursive" "[ [ ] bad ] infer." "Got a computed value where a literal quotation was expected\n\nType :help for debugging help." }
78 "The following is correct:"
79 { $example ": good ( quot: ( -- ) -- ) [ call ] keep good ; inline recursive" "[ [ ] good ] infer." "( -- )" }
80 "The effect of the nested quotation itself is only present for documentation purposes; the mere presence of a nested effect is sufficient to mark that value as a quotation parameter."
81 { $heading "Data flow restrictions" }
82 "The stack checker does not trace data flow in two instances."
84 "An inline recursive word cannot pass a quotation on the data stack through the recursive call. For example, the following will not infer:"
85 { $example ": bad ( ? quot: ( ? -- ) -- ) 2dup [ not ] dip bad call ; inline recursive" "[ [ drop ] bad ] infer." "Got a computed value where a literal quotation was expected\n\nType :help for debugging help." }
86 "However a small change can be made:"
87 { $example ": good ( ? quot: ( ? -- ) -- ) [ good ] 2keep [ not ] dip call ; inline recursive" "[ [ drop ] good ] infer." "( object -- )" }
88 "An inline recursive word must have a fixed stack effect in its base case. The following will not infer:"
90 ": foo ( quot ? -- ) [ f foo ] [ call ] if ; inline"
91 "[ [ 5 ] t foo ] infer."
94 ARTICLE: "tools.inference" "Stack effect tools"
95 { $link "inference" } " can be used interactively to print stack effects of quotations without running them. It can also be used from " { $link "combinators.smart" } "."
100 "There are also some words for working with " { $link effect } " instances. Getting a word's declared stack effect:"
101 { $subsections stack-effect }
102 "Converting a stack effect to a string form:"
103 { $subsections effect>string }
110 "The class of stack effects:"
116 ARTICLE: "inference-escape" "Stack effect checking escape hatches"
117 "In a static checking regime, sometimes it is necessary to step outside the boundaries and run some code which cannot be statically checked; perhaps this code is constructed at run-time. There are two ways to get around the static stack checker."
119 "If the stack effect of a word or quotation is known, but the word or quotation itself is not, " { $link POSTPONE: execute( } " or " { $link POSTPONE: call( } " can be used. See " { $link "call" } " for details."
121 "If the stack effect is not known, the code being called cannot manipulate the datastack directly. Instead, it must reflect the datastack into an array:"
122 { $subsections with-datastack }
123 "The surrounding code has a static stack effect since " { $link with-datastack } " has one. However, the array passed in as input may be transformed arbitrarily by calling this combinator." ;
125 ARTICLE: "inference" "Stack effect checking"
126 "The " { $link "compiler" } " checks the " { $link "effects" } " of words before they can be run. This ensures that words take exactly the number of inputs and outputs that the programmer declares in source."
128 "Words that do not pass the stack checker are rejected and cannot be run, and so essentially this defines a very simple and permissive type system that nevertheless catches some invalid programs and enables compiler optimizations."
130 "If a word's stack effect cannot be inferred, a compile error is reported. See " { $link "compiler-errors" } "."
132 "The following articles describe how different control structures are handled by the stack checker."
135 "inference-combinators"
136 "inference-recursive-combinators"
139 "Stack checking catches several classes of errors."
140 { $subsections "inference-errors" }
141 "Sometimes code with a dynamic stack effect has to be run."
142 { $subsections "inference-escape" }
143 { $see-also "effects" "tools.inference" "tools.errors" } ;
147 HELP: inference-error
148 { $values { "class" class } }
149 { $description "Creates an instance of " { $snippet "class" } ", wraps it in an " { $link inference-error } " and throws the result." }
151 "Thrown by " { $link infer } " when the stack effect of a quotation cannot be inferred."
153 "The " { $snippet "error" } " slot contains one of several possible " { $link "inference-errors" } "."
157 { $values { "quot" "a quotation" } { "effect" "an instance of " { $link effect } } }
158 { $description "Attempts to infer the quotation's stack effect. For interactive testing, the " { $link infer. } " word should be called instead since it presents the output in a nicely formatted manner." }
159 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
162 { $values { "quot" "a quotation" } }
163 { $description "Attempts to infer the quotation's stack effect, and prints this data to " { $link output-stream } "." }
164 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
166 { infer infer. } related-words