git @ Cat's Eye Technologies Robin / 7b53df2
Add "Detecting Errors in Robin" document. Chris Pressey 1 year, 5 months ago
3 changed file(s) with 173 addition(s) and 49 deletion(s). Raw diff Collapse all Expand all
1111
1212 It would just be a fexpr that evaluates (in the calling
1313 environment) what the body evaluates to.
14
15 For static analysis (see below), it could also annotate
16 the value with a version whose return value does not get
17 evaluated. This annotation "expand-macro" could be used
18 by static analyzers to expand the macro to a form which
19 they can then continue to analyze.
20
21 Static analysis of fexprs
22 -------------------------
23
24 It has been noted many times that fexprs are hard to statically
25 analyze. "Hard" isn't even the right word: they have a trivial
26 equational theory. In less formal terms, if I'm a static
27 analyzer and you give me a fexpr I'm like, what can I say about
28 this? This thing could be doing literally _anything_ with its
29 arguments...
30
31 The idea so far is to be able to decorate operator values with
32 some metadata which describes the equational theory that should
33 apply to them.
34
35 So, any operator defined with `fun` will come with some metadata
36 that says "This operator takes _n_ arguments and evaluates all
37 of them".
38
39 A static analyzer is passed an environment, containing that value
40 and its metadata; when it sees the name that maps to that value
41 in the environment, it looks at the metadata and knows a bit more
42 how to analyze the arguments it sees.
43
44 This metadata would also be a good place for such an analyzer to
45 store information it deduces, such as types.
46
47 How exactly that information should be represented in the metadata
48 is an open question. In some sense it is very similar to early
49 Lisps associating a property list with each symbol. But I think
50 ultimately it could be far more general, e.g. the metadata for an
51 operator could faithfully capture the complete axiomatic or
52 algebraic semantics of that operator, which could be used in a
53 proof. But that's a long way off.
5414
5515 Disjointness of types
5616 ---------------------
9555
9656 `lispish` lib, that just gives you all the old jargon-y names
9757 as aliases.
98
99 Static analysis lib. This is its own bucket of worms. It should
100 expose an operator that can be wrapped around an arbitrary standard
101 Robin program _p_ and, if static analysis of _p_ is successful,
102 simply evaluates to whatever _p_ evaluates to. And if not
103 successful, produces an abort. Should probably start small --
104 statically check the arity of every application, for instance.
105 Note that this relies on the assumption that all standard symbols
106 have their standard meanings.
10758
10859 TopLevel
10960 --------
0 Detecting Errors in Robin
1 =========================
2
3 This is a somewhat philosophical write-up that overlaps with the
4 [Design Goals and Rationale](Rationale.md) document to some degree.
5
6 A Sea of Parentheses
7 --------------------
8
9 The thing about lispoids is that all those parentheses _do_ make things hard to read and hard to edit.
10 Take these two Scheme expressions, for instance:
11
12 (list (+ 1 2) 3)
13
14 versus
15
16 (list (+ 1 2 3))
17
18 They're both syntactically correct, but they have rather different meanings, and the
19 difference is subtle. Deep in a sea of parentheses, the shifted parentheses might be
20 hard to spot. Your only clue might be a error message from somewhere higher up in
21 the code, that an attempt to apply `car` failed. Hunting it down to this shifted
22 parenthesis can be taxing.
23
24 This problem is a particularly bad problem in Robin, for the following reasons.
25
26 Robin has, as an ideal, that there should be as little done statically as possible. The static
27 phase is: parse an S-expression, get it into a data structure. That's all. The rest is up
28 to evaluating that data structure.
29
30 There aren't even any "special forms". The data structure you get might not be well-formed.
31 You might get `(bind a)`. You can have "syntax errors" at runtime.
32
33 Even worse, Robin has, as an ideal, not to do much extra work at runtime either. Meaning
34 that, some syntax oddities aren't checked for, they're just ignored.
35
36 In particular, maybe you call a fexpr with more arguments than it can understand. Say,
37
38 (bind a 1 (foo a) z)
39
40 In this case the `z` is ignored.
41
42 This is compounded by, maybe you said
43
44 (bar (bind a 1 (foo a) z))
45
46 but maybe you meant
47
48 (bar (bind a 1 (foo a)) z)
49
50 and maybe `bar` doesn't complain when you only give it one argument either. Maybe its
51 second argument is optional and giving it just changes the behaviour slightly.
52
53 Deep in a sea of parentheses these differences can be hard to find.
54
55 Addressing the problem
56 ----------------------
57
58 How do we approach this problem?
59
60 First, we recognize it. That's why I'm writing this.
61
62 Second, we accept it as the price we have to pay for having a set of rules that are
63 this simple.
64
65 Third, we consider whether we want to pay that price, or if there is some other way
66 to achieve those ends, and if we want to pay that price instead.
67
68 To that end we might want to examine why Robin has the ideals that it does.
69
70 It's been said that Lisp isn't a programming language, it's a building material.
71 Under that view, Robin isn't trying to be a better programming language; it's
72 trying to be a more building-material-like building material.
73
74 As little as possible is done statically because we want to give the programmer the
75 choice of what static checking is or is not done. By default, as little as possible
76 is done, and the programmer can add to that, by writing their own static analyzers,
77 if they like.
78
79 And we want to not do much extra work at runtime for essentially the same reason:
80 we want to give the programmer the choice of what checking is or is not done.
81 By default, as little as possible is done, and the programmer can add to it by,
82 for example, defining and using argument-checking wrappers, if they like.
83
84 Each of these goals by itself is fine. It's that putting them together doesn't
85 work very well.
86
87 In order to live with them together we need to start giving the Robin programmer
88 tools to do this checking that we're leaving up to them.
89
90 But that is *also* a particularly difficult problem, because Robin is based on
91 fexprs.
92
93 Static analysis of fexprs
94 -------------------------
95
96 It has been noted many times that fexprs are hard to statically
97 analyze. "Hard" isn't even the right word: they have a trivial
98 equational theory. In less formal terms, if I'm a static
99 analyzer and you give me a fexpr, then I'm like, what do I do
100 with this? I can't even tell which arguments are going to get
101 evaluated and which ones aren't, so how do I analyze what's in
102 the arguments?
103
104 Robin's approach to addressing this, which may or may not be a good one,
105 is to annotate operator values with some metadata which describes
106 what happens to the arguments, so that there is some chance of analyzing it.
107
108 Robin uses fexprs in a _definitional_, rather than _implementational_,
109 way. It is expected that most fexprs will be defined in the standard
110 library. So at the very least we can advertise behaviour like,
111 "this operator is the same as `bind` in the standard library, so
112 if you're an analyzer, you should treat it like that".
113
114 But not just specific operators in the standard library:
115 any operator defined with `fun` will come with some metadata
116 that says "This operator takes _n_ arguments and evaluates all
117 of them".
118
119 In a sense, we are supplanting the trivial equational theory of
120 fexprs, with our own non-trivial home-cooked equational theory that a
121 static analyzer can make use of.
122
123 A static analyzer is passed an environment, containing that value
124 and its metadata; when it sees the name that maps to that value
125 in the environment, it looks at the metadata and knows a bit more
126 how to analyze the arguments it sees.
127
128 This metadata would also be a good place for such an analyzer to
129 store information it deduces, such as types.
130
131 How exactly that information should be represented in the metadata
132 is still an open question. In some sense it is very similar to early
133 Lisps associating a property list with each symbol. But I think
134 ultimately it could be far more general, e.g. the metadata for an
135 operator could faithfully capture the complete axiomatic or
136 algebraic semantics of that operator, which could be used in a
137 proof. But that's a long way off.
138
139 The paper "Special Forms in Lisp" advocates removing fexprs from
140 the Lisp language and using macros instead.
141
142 In Robin, a macro can be defined as a kind of fexpr whose return value
143 does not get evaluated. This is easier for a static analyzer to
144 analyzer: it just expands the macro and analyzes that.
145
146 Because it is defined as a kind of fexpr in Robin, and that fexpr will
147 evaluate the value the macro returns (because to execute it, something
148 needs to), to support static analysis, the macro will need to produce
149 an annotation that only expands the macro, without evaluating the
150 result of the expansion. Such "expand-macro" annotation could also
151 be used by compilers or other tools which do not need to immediately
152 evaluate the macro, but rather want to know how it transforms the code.
153
154 Static analysis as a library
155 ----------------------------
156
157 Because Robin lets you write fexprs, it lets you write fexprs which
158 take a piece of code, check that piece of code, and if the code passes
159 the check, evaluates that piece of code, or otherwise evaluates to
160 an abort value.
161
162 In other words, you can write static analyzers as fexprs.
163
164 Such static analyzer fexprs should be available in the standard
165 library, i.e. there should be standard static analyses available.
166
167 The first such analyzer should simply check the arity of all the
168 applied operators in an expression.
169
170 That would begin to address the problem of shifted parentheses that was
171 brought up at the beginning of this document.
33 * [Robin Tutorial](Tutorial.md)
44 * [Robin Specification](Robin.md)
55 * [Design Goals and Rationale](Rationale.md)
6 * [Detecting Errors in Robin](Errors.md)
67
78 For normative definitions of the symbols in the standard library,
89 see the definition files in the [stdlib directory](../stdlib/).