1 | # Thoughts on Resolver Design # |
---|
2 | |
---|
3 | ## Conversions ## |
---|
4 | C's implicit "usual arithmetic conversions" define a structure among the |
---|
5 | built-in types consisting of _unsafe_ narrowing conversions and a hierarchy of |
---|
6 | _safe_ widening conversions. |
---|
7 | There is also a set of _explicit_ conversions that are only allowed through a |
---|
8 | cast expression. |
---|
9 | Based on Glen's notes on conversions [1], I propose that safe and unsafe |
---|
10 | conversions be expressed as constructor variants, though I make explicit |
---|
11 | (cast) conversions a constructor variant as well rather than a dedicated |
---|
12 | operator. |
---|
13 | Throughout this article, I will use the following operator names for |
---|
14 | constructors and conversion functions from `From` to `To`: |
---|
15 | |
---|
16 | void ?{} ( To*, To ); // copy constructor |
---|
17 | void ?{} ( To*, From ); // explicit constructor |
---|
18 | void ?{explicit} ( To*, From ); // explicit cast conversion |
---|
19 | void ?{safe} ( To*, From ); // implicit safe conversion |
---|
20 | void ?{unsafe} ( To*, From ); // implicit unsafe conversion |
---|
21 | |
---|
22 | [1] http://plg.uwaterloo.ca/~cforall/Conversions/index.html |
---|
23 | |
---|
24 | Glen's design made no distinction between constructors and unsafe implicit |
---|
25 | conversions; this is elegant, but interacts poorly with tuples. |
---|
26 | Essentially, without making this distinction, a constructor like the following |
---|
27 | would add an interpretation of any two `int`s as a `Coord`, needlessly |
---|
28 | multiplying the space of possible interpretations of all functions: |
---|
29 | |
---|
30 | void ?{}( Coord *this, int x, int y ); |
---|
31 | |
---|
32 | That said, it would certainly be possible to make a multiple-argument implicit |
---|
33 | conversion, as below, though the argument above suggests this option should be |
---|
34 | used infrequently: |
---|
35 | |
---|
36 | void ?{unsafe}( Coord *this, int x, int y ); |
---|
37 | |
---|
38 | An alternate possibility would be to only count two-arg constructors |
---|
39 | `void ?{} ( To*, From )` as unsafe conversions; under this semantics, safe and |
---|
40 | explicit conversions should also have a compiler-enforced restriction to |
---|
41 | ensure that they are two-arg functions (this restriction may be valuable |
---|
42 | regardless). |
---|
43 | |
---|
44 | ### Constructor Idiom ### |
---|
45 | Basing our notion of conversions off otherwise normal Cforall functions means |
---|
46 | that we can use the full range of Cforall features for conversions, including |
---|
47 | polymorphism. |
---|
48 | Glen [1] defines a _constructor idiom_ that can be used to create chains of |
---|
49 | safe conversions without duplicating code; given a type `Safe` which members |
---|
50 | of another type `From` can be directly converted to, the constructor idiom |
---|
51 | allows us to write a conversion for any type `To` which `Safe` converts to: |
---|
52 | |
---|
53 | forall(otype To | { void ?{safe}( To*, Safe ) }) |
---|
54 | void ?{safe}( To *this, From that ) { |
---|
55 | Safe tmp = /* some expression involving that */; |
---|
56 | *this = tmp; // uses assertion parameter |
---|
57 | } |
---|
58 | |
---|
59 | This idiom can also be used with only minor variations for a parallel set of |
---|
60 | unsafe conversions. |
---|
61 | |
---|
62 | What selective non-use of the constructor idiom gives us is the ability to |
---|
63 | define a conversion that may only be the *last* conversion in a chain of such. |
---|
64 | Constructing a conversion graph able to unambiguously represent the full |
---|
65 | hierarchy of implicit conversions in C is provably impossible using only |
---|
66 | single-step conversions with no additional information (see Appendix B), but |
---|
67 | this mechanism is sufficiently powerful (see [1], though the design there has |
---|
68 | some minor bugs; the general idea is to use the constructor idiom to define |
---|
69 | two chains of conversions, one among the signed integral types, another among |
---|
70 | the unsigned, and to use monomorphic conversions to allow conversions between |
---|
71 | signed and unsigned integer types). |
---|
72 | |
---|
73 | ### Implementation Details ### |
---|
74 | It is desirable to have a system which can be efficiently implemented, yet |
---|
75 | also to have one which has sufficient power to distinguish between functions |
---|
76 | on all possible axes of polymorphism. |
---|
77 | This ordering may be a partial order, which may complicate implementation |
---|
78 | somewhat; in this case it may be desirable to store the set of implementations |
---|
79 | for a given function as the directed acyclic graph (DAG) representing the |
---|
80 | order. |
---|
81 | |
---|
82 | ## Conversion Costs ## |
---|
83 | Each possible resolution of an expression has a _cost_ consisting of four |
---|
84 | integer components: _unsafe_ conversion cost, _polymorphic_ specialization |
---|
85 | cost, _safe_ conversion cost, and a _count_ of conversions. |
---|
86 | These components form a lexically-ordered tuple which can be summed |
---|
87 | element-wise; summation starts at `(0, 0, 0, 0)`. |
---|
88 | |
---|
89 | ### Lvalue and Qualifier Conversions ### |
---|
90 | C defines the notion of a _lvalue_, essentially an addressable object, as well |
---|
91 | as a number of type _qualifiers_, `const`, `volatile`, and `restrict`. |
---|
92 | As these type qualifiers are generally only meaningful to the type system as |
---|
93 | applied to lvalues, the two concepts are closely related. |
---|
94 | A const lvalue cannot be modified, the compiler cannot assume that a volatile |
---|
95 | lvalue will not be concurrently modified by some other part of the system, and |
---|
96 | a restrict lvalue must have pointer type, and the compiler may assume that no |
---|
97 | other pointer in scope aliases that pointer (this is solely a performance |
---|
98 | optimization, and may be ignored by implementers). |
---|
99 | _Lvalue-to-rvalue conversion_, which takes an lvalue of type `T` and converts |
---|
100 | it to an expression result of type `T` (commonly called an _rvalue_ of type |
---|
101 | `T`) also strips all the qualifiers from the lvalue, as an expression result |
---|
102 | is a value, not an addressable object that can have properties like |
---|
103 | immutability. |
---|
104 | Though lvalue-to-rvalue conversion strips the qualifiers from lvalues, |
---|
105 | derived rvalue types such as pointer types may include qualifiers; |
---|
106 | `const int *` is a distinct type from `int *`, though the latter is safely |
---|
107 | convertable to the former. |
---|
108 | In general, any number of qualifiers can be safely added to the |
---|
109 | pointed-to-type of a pointer type, e.g. `int *` converts safely to |
---|
110 | `const int *` and `volatile int *`, both of which convert safely to |
---|
111 | `const volatile int *`. |
---|
112 | |
---|
113 | Since lvalues are precicely "addressable objects", in C, only lvalues can be |
---|
114 | used as the operand of the `&` address-of operator. |
---|
115 | Similarly, only modifiable lvalues may be used as the assigned-to |
---|
116 | operand of the mutating operators: assignment, compound assignment |
---|
117 | (e.g. `+=`), and increment and decrement; roughly speaking, lvalues without |
---|
118 | the `const` qualifier are modifiable, but lvalues of incomplete types, array |
---|
119 | types, and struct or union types with const members are also not modifiable. |
---|
120 | Lvalues are produced by the following expressions: object identifiers |
---|
121 | (function identifiers are not considered to be lvalues), the result of the `*` |
---|
122 | dereference operator applied to an object pointer, the result of a member |
---|
123 | expression `s.f` if the left argument `s` is an lvalue (note that the |
---|
124 | preceding two rules imply that the result of indirect member expressions |
---|
125 | `s->f` are always lvalues, by desugaring to `(*s).f`), and the result of the |
---|
126 | indexing operator `a[i]` (similarly by its desugaring to `*((a)+(i))`). |
---|
127 | Somewhat less obviously, parenthesized lvalue expressions, string literals, |
---|
128 | and compound literals (e.g. `(struct foo){ 'x', 3.14, 42 }`) are also lvalues. |
---|
129 | |
---|
130 | All of the conversions described above are defined in standard C, but Cforall |
---|
131 | requires further features from its type system. |
---|
132 | In particular, to allow overloading of the `*?` and `?[?]` dereferencing and |
---|
133 | indexing operators, Cforall requires a way to declare that the functions |
---|
134 | defining these operators return lvalues, and since C functions never return |
---|
135 | lvalues and for syntactic reasons we wish to distinguish functions which |
---|
136 | return lvalues from functions which return pointers, this is of necessity an |
---|
137 | extension to standard C. |
---|
138 | In the current design, an `lvalue` qualifier can be added to function return |
---|
139 | types (and only to function return types), the effect of which is to return a |
---|
140 | pointer which is implicitly dereferenced by the caller. |
---|
141 | C++ includes the more general concept of _references_, which are typically |
---|
142 | implemented as implicitly dereferenced pointers as well. |
---|
143 | Another use case which C++ references support is providing a way to pass |
---|
144 | function parameters by reference (rather than by value) with a natural |
---|
145 | syntax; Cforall in its current state has no such mechanism. |
---|
146 | As an example, consider the following (currently typical) copy-constructor |
---|
147 | signature and call: |
---|
148 | |
---|
149 | void ?{}(T *lhs, T rhs); |
---|
150 | |
---|
151 | T x; |
---|
152 | T y = { x }; |
---|
153 | |
---|
154 | Note that the right-hand argument is passed by value, and would in fact be |
---|
155 | copied twice in the course of the constructor call `T y = { x };` (once into |
---|
156 | the parameter by C's standard `memcpy` semantics, once again in the body of |
---|
157 | the copy constructor, though it is possible that return value optimization |
---|
158 | will elide the `memcpy`-style copy). |
---|
159 | However, to pass by reference using the existing pointer syntax, the example |
---|
160 | above would look like this: |
---|
161 | |
---|
162 | void ?{}(T *lhs, const T *rhs); |
---|
163 | |
---|
164 | T x; |
---|
165 | T y = { &x }; |
---|
166 | |
---|
167 | This example is not even as bad as it could be; assuming pass-by-reference is |
---|
168 | the desired semantics for the `?+?` operator, that implies the following |
---|
169 | design today: |
---|
170 | |
---|
171 | T ?+?(const T *lhs, const T *rhs); |
---|
172 | |
---|
173 | T a, b; |
---|
174 | T c = &a + &b, |
---|
175 | |
---|
176 | In addition to `&a + &b` being unsightly and confusing syntax to add `a` and |
---|
177 | `b`, it also introduces a possible ambiguity with pointer arithmetic on `T*` |
---|
178 | which can only be resolved by return-type inference. |
---|
179 | |
---|
180 | Pass-by-reference and marking functions as returning lvalues instead of the |
---|
181 | usual rvalues are actually closely related concepts, as obtaining a reference |
---|
182 | to pass depends on the referenced object being addressable, i.e. an lvalue, |
---|
183 | and lvalue return types are effectively return-by-reference. |
---|
184 | Cforall should also unify the concepts, with a parameterized type for |
---|
185 | "reference to `T`", which I will write `ref T`. |
---|
186 | Syntax bikeshedding can be done later (there are some examples at the bottom |
---|
187 | of this section), but `ref T` is sufficiently distinct from both the existing |
---|
188 | `lvalue T` (which it subsumes) and the closely related C++ `T&` to allow |
---|
189 | independent discussion of its semantics. |
---|
190 | |
---|
191 | Firstly, assignment to a function parameter as part of a function call and |
---|
192 | local variable initialization have almost identical semantics, so should be |
---|
193 | treated similarly for the reference type too; this implies we should be able |
---|
194 | to declare local variables of reference type, as in the following: |
---|
195 | |
---|
196 | int x = 42; |
---|
197 | ref int r = x; // r is now an alias for x |
---|
198 | |
---|
199 | Unlike in C++, we would like to have the capability to re-bind references |
---|
200 | after initialization, as this allows the attractive syntax of references to |
---|
201 | support some further useful code patterns, such as first initializing a |
---|
202 | reference after its declaration. |
---|
203 | Constant references to `T` (`const ref T`) should not be re-bindable. |
---|
204 | |
---|
205 | One option for re-binding references is to use a dedicated operator, as in the |
---|
206 | code example below: |
---|
207 | |
---|
208 | int i = 42, j = 7; |
---|
209 | ref int r = i; // bind r to i |
---|
210 | r = j; // set i (== r) to 7 |
---|
211 | r := j; // rebind r to j using the new := rebind operator |
---|
212 | i = 42; // reset i (!= r) to 42 |
---|
213 | assert( r == 7 ); |
---|
214 | |
---|
215 | The other syntactic option for reference re-bind would be to overload |
---|
216 | assignment and use type inference on the left and right-hand sides to |
---|
217 | determine whether the referred-to variable on the left should be reassigned to |
---|
218 | the value on the right, or if the reference on the left should be aliased to |
---|
219 | the reference on the right. |
---|
220 | This could be disambiguated with casts, as in the following code example: |
---|
221 | |
---|
222 | int i |
---|
223 | int j; |
---|
224 | ref int r = i; // (0a) |
---|
225 | ref int s = i; // (0b) |
---|
226 | |
---|
227 | i = j; // (1) |
---|
228 | i = (int)s; // (2) |
---|
229 | i = s; // (3) |
---|
230 | // --------------------- |
---|
231 | r = s; // (4) |
---|
232 | r = (ref int)j; // (5) |
---|
233 | // --------------------- |
---|
234 | r = j; // (6) |
---|
235 | r = (int)s; // (7) |
---|
236 | |
---|
237 | By the expected aliasing syntax, (0a) and (0b) are initializing `r` and `s` as |
---|
238 | aliases for `i`. |
---|
239 | For C compatibility, (1) has to be assignment; in general, any assignment to a |
---|
240 | non-reference type should be assignment, so (2) and (3) are as well. |
---|
241 | By types, (4) and (5) should have the same semantics, and the semantics of (6) |
---|
242 | and (7) should match as well. |
---|
243 | This suggests that (4) and (5) are reference re-bind, and (6) and (7) are an |
---|
244 | assignment to the referred variable; this makes the syntax to explicitly alias |
---|
245 | a local variable rather ugly (and inconsistent with the initialization |
---|
246 | syntax), as well as making it rather awkward to copy the value stored in one |
---|
247 | reference-type variable into another reference type variable (which is likely |
---|
248 | more painful in functions with by-reference parameters than with local |
---|
249 | variables of reference type). |
---|
250 | |
---|
251 | Because of the aforementioned issues with overloading assignment as reference |
---|
252 | rebind, in addition to the fact that reference rebind should not be a |
---|
253 | user-overloadable operator (unlike assignment), I propose refererence rebind |
---|
254 | should have its own dedicated operator. |
---|
255 | |
---|
256 | The semantics and restrictions of `ref T` are effectively the semantics of an |
---|
257 | lvalue of type `T`, and by this analogy there should be a safe, qualifier |
---|
258 | dropping conversion from `ref const volatile restrict T` (and every other |
---|
259 | qualifier combination on the `T` in `ref T`) to `T`. |
---|
260 | With this conversion, the resolver may type most expressions that C would |
---|
261 | call "lvalue of type `T`" as `ref T`. |
---|
262 | There's also an obvious argument that lvalues of a (possibly-qualified) type |
---|
263 | `T` should be convertable to references of type `T`, where `T` is also |
---|
264 | so-qualified (e.g. lvalue `int` to `ref int`, lvalue `const char` to |
---|
265 | `ref const char`). |
---|
266 | By similar arguments to pointer types, qualifiers should be addable to the |
---|
267 | referred-to type of a reference (e.g. `ref int` to `ref const int`). |
---|
268 | As a note, since pointer arithmetic is explictly not defined on `ref T`, |
---|
269 | `restrict ref T` should be allowable and would have alias-analysis rules that |
---|
270 | are actually comprehensible to mere mortals. |
---|
271 | |
---|
272 | Using pass-by-reference semantics for function calls should not put syntactic |
---|
273 | constraints on how the function is called; particularly, temporary values |
---|
274 | should be able to be passed by reference. |
---|
275 | The mechanism for this pass-by-reference would be to store the value of the |
---|
276 | temporary expression into a new unnamed temporary, and pass the reference of |
---|
277 | that temporary to the function. |
---|
278 | As an example, the following code should all compile and run: |
---|
279 | |
---|
280 | void f(ref int x) { printf("%d\n", x++); } |
---|
281 | |
---|
282 | int i = 7, j = 11; |
---|
283 | const int answer = 42; |
---|
284 | |
---|
285 | f(i); // (1) |
---|
286 | f(42); // (2) |
---|
287 | f(i + j); // (3) |
---|
288 | f(answer); // (4) |
---|
289 | |
---|
290 | The semantics of (1) are just like C++'s, "7" is printed, and `i` has the |
---|
291 | value 8 afterward. |
---|
292 | For (2), "42" is printed, and the increment of the unnamed temporary to 43 is |
---|
293 | not visible to the caller; (3) behaves similarly, printing "19", but not |
---|
294 | changing `i` or `j`. |
---|
295 | (4) is a bit of an interesting case; we want to be able to support named |
---|
296 | constants like `answer` that can be used anywhere the constant expression |
---|
297 | they're replacing (like `42`) could go; in this sense, (4) and (2) should have |
---|
298 | the same semantics. |
---|
299 | However, we don't want the mutation to the `x` parameter to be visible in |
---|
300 | `answer` afterward, because `answer` is a constant, and thus shouldn't change. |
---|
301 | The solution to this is to allow chaining of the two `ref` conversions; |
---|
302 | `answer` has the type `ref const int`, which can be converted to `int` by the |
---|
303 | lvalue-to-rvalue conversion (which drops the qualifiers), then up to `ref int` |
---|
304 | by the temporary-producing rvalue-to-lvalue conversion. |
---|
305 | Thus, an unnamed temporary is inserted, initialized to `answer` (i.e. 42), |
---|
306 | mutated by `f`, then discarded; "42" is printed, just as in case (2), and |
---|
307 | `answer` still equals 42 after the call, because it was the temporary that was |
---|
308 | mutated, not `answer`. |
---|
309 | It may be somewhat surprising to C++ programmers that `f(i)` mutates `i` while |
---|
310 | `f(answer)` does not mutate `answer` (though `f(answer)` would be illegal in |
---|
311 | C++, leading to the dreaded "const hell"), but the behaviour of this rule can |
---|
312 | be determined by examining local scope with the simple rule "non-`const` |
---|
313 | references to `const` variables produce temporaries", which aligns with |
---|
314 | programmer intuition that `const` variables cannot be mutated. |
---|
315 | |
---|
316 | To bikeshed syntax for `ref T`, there are three basic options: language |
---|
317 | keywords (`lvalue T` is already in Cforall), compiler-supported "special" |
---|
318 | generic types (e.g. `ref(T)`), or sigils (`T&` is familiar to C++ |
---|
319 | programmers). |
---|
320 | Keyword or generic based approaches run the risk of name conflicts with |
---|
321 | existing code, while any sigil used would have to be carefully chosen to not |
---|
322 | create parsing conflicts. |
---|
323 | |
---|
324 | **TODO** Consider arguments for move semantics and see if there is a |
---|
325 | compelling case for rvalue references. |
---|
326 | |
---|
327 | ### Conversion Operator Costs ### |
---|
328 | Copy constructors, safe conversions, and unsafe conversions all have an |
---|
329 | associated conversion cost, calculated according to the algorithm below: |
---|
330 | |
---|
331 | 1. Monomorphic copy constructors have a conversion cost of `(0, 0, 0, 0)` |
---|
332 | 2. Monomorphic safe conversions have a conversion cost of `(0, 0, 1, 1)` |
---|
333 | 3. Monomoprhic unsafe conversions have a conversion cost of `(1, 0, 0, 1)` |
---|
334 | 4. Polymorphic conversion operators (or copy constructors) have a conversion |
---|
335 | cost of `(0, 1, 0, 1)` plus the conversion cost of their monomorphic |
---|
336 | equivalent and the sum of the conversion costs of all conversion operators |
---|
337 | passed as assertion parameters, but where the fourth "count" element of the |
---|
338 | cost tuple is fixed to `1`. |
---|
339 | |
---|
340 | **TODO** Polymorphism cost may need to be reconsidered in the light of the |
---|
341 | thoughts on polymorphism below. |
---|
342 | **TODO** You basically just want path-length in the conversion graph implied |
---|
343 | by the set of conversions; the only tricky question is whether or not you can |
---|
344 | account for "mixed" safe and unsafe conversions used to satisfy polymorphic |
---|
345 | constraints, whether a polymorphic conversion should cost more than a |
---|
346 | monomorphic one, and whether to account for non-conversion constraints in the |
---|
347 | polymorphism cost |
---|
348 | |
---|
349 | ### Argument-Parameter Matching ### |
---|
350 | Given a function `f` with an parameter list (after tuple flattening) |
---|
351 | `(T1 t1, T2 t2, ... Tn tn)`, and a function application |
---|
352 | `f(<e1>, <e2>, ... <em>)`, the cost of matching each argument to the |
---|
353 | appropriate parameter is calculated according to the algorithm below: |
---|
354 | |
---|
355 | Given a parameter `t` of type `T` and an expression `<e>` from these lists, |
---|
356 | `<e>` will have a set of interpretations of types `E1, E2, ... Ek` with |
---|
357 | associated costs `(u1, p1, s1, c1), (u2, p2, s2, c2), ... (uk, pk, sk, ck)`. |
---|
358 | (If any `Ei` is a tuple type, replace it with its first flattened element for |
---|
359 | the purposes of this section.) |
---|
360 | |
---|
361 | The cost of matching the interpretation of `<e>` with type `Ei` to `t1` with |
---|
362 | type `T` is the sum of the interpretation cost `(ui, pi, si, ci)` and the |
---|
363 | conversion operator cost from `Ei` to `T`. |
---|
364 | |
---|
365 | ### Object Initialization ### |
---|
366 | The cost to initialize an object is calculated very similarly to |
---|
367 | argument-parameter matching, with a few modifications. |
---|
368 | Firstly, explicit constructors are included in the set of available |
---|
369 | conversions, with conversion cost `(0, 0, 0, 1)` plus associated polymorphic |
---|
370 | conversion costs (if applicable) and the _interpretation cost_ of the |
---|
371 | constructor, the sum of the argument-parameter matching costs for its |
---|
372 | parameters. |
---|
373 | Also, ties in overall cost (interpretation cost plus conversion cost) are |
---|
374 | broken by lowest conversion cost (i.e. of alternatives with the same overall |
---|
375 | cost, copy constructors are preferred to other explicit constructors, |
---|
376 | explicit constructors are preferred to safe conversions, which are preferred |
---|
377 | to unsafe conversions). |
---|
378 | An object initialization is properly typed if it has exactly one min-cost |
---|
379 | interpretation. |
---|
380 | |
---|
381 | ### Explicit Casts ### |
---|
382 | Explicit casts are handled similarly to object initialization. |
---|
383 | Copy constructors and other explicit constructors are not included in the set |
---|
384 | of possible conversions, though interpreting a cast as type ascription |
---|
385 | (`(T)e`, meaning the interpretation of `e` as type `T`) has conversion cost |
---|
386 | `(0, 0, 0, 0)`. |
---|
387 | Explicit conversion operators are also included in the set of possible |
---|
388 | conversions, with cost `(0, 0, 0, 1)` plus whatever polymorphic conversion |
---|
389 | costs are invoked. |
---|
390 | Unlike for explicit constructors and other functions, implicit conversions are |
---|
391 | never applied to the argument or return type of an explicit cast operator, so |
---|
392 | that the cast may be used more effectively as a method for the user programmer |
---|
393 | to guide type resolution. |
---|
394 | |
---|
395 | ## Trait Satisfaction ## |
---|
396 | A _trait_ consists of a list of _type variables_ along with a (possibly empty) |
---|
397 | set of _assertions_ on those variables. |
---|
398 | Assertions can take two forms, _variable assertions_ and the more common |
---|
399 | _function assertions_, as in the following example: |
---|
400 | |
---|
401 | trait a_trait(otype T, otype S) { |
---|
402 | T a_variable_assertion; |
---|
403 | S* another_variable_assertion; |
---|
404 | S a_function_assertion( T* ); |
---|
405 | }; |
---|
406 | |
---|
407 | Variable assertions enforce that a variable with the given name and type |
---|
408 | exists (the type is generally one of the type variables, or derived from one), |
---|
409 | while a function assertion enforces that a function with a |
---|
410 | _compatible signature_ to the provided function exists. |
---|
411 | |
---|
412 | To test if some list of types _satisfy_ the trait, the types are first _bound_ |
---|
413 | to the type variables, and then declarations to satisfy each assertion are |
---|
414 | sought out. |
---|
415 | Variable assertions require an exact match, because they are passed as object |
---|
416 | pointers, and there is no mechanism to employ conversion functions, while |
---|
417 | function assertions only require a function that can be wrapped to a |
---|
418 | compatible type; for example, the declarations below satisfy |
---|
419 | `a_trait(int, short)`: |
---|
420 | |
---|
421 | int a_variable_assertion; |
---|
422 | short* another_variable_assertion; |
---|
423 | char a_function_assertion( void* ); |
---|
424 | // int* may be implicitly converted to void*, and char to short, so the |
---|
425 | // above works |
---|
426 | |
---|
427 | Cforall Polymorphic functions have a _constraining trait_, denoted as follows: |
---|
428 | |
---|
429 | forall(otype A, otype B | some_trait(A, B)) |
---|
430 | |
---|
431 | The trait may be anonymous, with the same syntax as a trait declaration, and |
---|
432 | may be unioned together using `|` or `,`. |
---|
433 | |
---|
434 | **TODO** Consider including field assertions in the list of constraint types, |
---|
435 | also associated types and the appropriate matching type assertion. |
---|
436 | |
---|
437 | ## Polymorphism Costs ## |
---|
438 | The type resolver should prefer functions that are "less polymorphic" to |
---|
439 | functions that are "more polymorphic". |
---|
440 | Determining how to order functions by degree of polymorphism is somewhat less |
---|
441 | straightforward, though, as there are multiple axes of polymorphism and it is |
---|
442 | not always clear how they compose. |
---|
443 | The natural order for degree of polymorphism is a partial order, and this |
---|
444 | section includes some open questions on whether it is desirable or feasible to |
---|
445 | develop a tie-breaking strategy to impose a total order on the degree of |
---|
446 | polymorphism of functions. |
---|
447 | Helpfully, though, the degree of polymorphism is a property of functions |
---|
448 | rather than function calls, so any complicated graph structure or calculation |
---|
449 | representing a (partial) order over function degree of polymorphism can be |
---|
450 | calculated once and cached. |
---|
451 | |
---|
452 | ### Function Parameters ### |
---|
453 | All other things being equal, if a parameter of one function has a concrete |
---|
454 | type and the equivalent parameter of another function has a dynamic type, the |
---|
455 | first function is less polymorphic: |
---|
456 | |
---|
457 | void f( int, int ); // (0) least polymorphic |
---|
458 | forall(otype T) void f( T, int ); // (1a) more polymorphic than (0) |
---|
459 | forall(otype T) void f( int, T ); // (1b) more polymorphic than (0) |
---|
460 | // incomparable with (1a) |
---|
461 | forall(otype T) void f( T, T ); // (2) more polymorphic than (1a/b) |
---|
462 | |
---|
463 | This should extend to parameterized types (pointers and generic types) also: |
---|
464 | |
---|
465 | forall(otype S) struct box { S val; }; |
---|
466 | |
---|
467 | forall(otype T) void f( T, T* ); // (3) less polymorphic than (2) |
---|
468 | forall(otype T) void f( T, T** ); // (4) less polymorphic than (3) |
---|
469 | forall(otype T) void f( T, box(T) ); // (5) less polymorphic than (2) |
---|
470 | // incomparable with (3) |
---|
471 | forall(otype T) void f( T, box(T*) ); // (6) less polymorphic than (5) |
---|
472 | |
---|
473 | Every function in the group above is incomparable with (1a/b), but that's fine |
---|
474 | because an `int` isn't a pointer or a `box`, so the ambiguity shouldn't occur |
---|
475 | much in practice (unless there are safe or unsafe conversions defined between |
---|
476 | the possible argument types). |
---|
477 | |
---|
478 | For degree of polymorphism from arguments, I think we should not distinguish |
---|
479 | between different type parameters, e.g. the following should be considered |
---|
480 | equally polymorphic: |
---|
481 | |
---|
482 | forall(otype T, otype S) void f( T, T, S ); // (7) |
---|
483 | forall(otype T, otype S) void f( S, T, T ); // (8) |
---|
484 | |
---|
485 | However parameter lists are compared, parameters of multi-parameter generic |
---|
486 | types should ideally be treated as a recursive case, e.g. in the example |
---|
487 | below, (9) is less polymorphic than (10), which is less polymorphic than (11): |
---|
488 | |
---|
489 | forall(otype T, otype S) struct pair { T x; S y; }; |
---|
490 | |
---|
491 | void f( pair(int, int) ); // (9) |
---|
492 | forall(otype T) void f( pair(T, int) ); // (10) |
---|
493 | forall(otype T) void f( pair(T, T) ); // (11) |
---|
494 | |
---|
495 | Parameter comparison could possibly be made somewhat cheaper at loss of some |
---|
496 | precision by representing each parameter as a value from the natural numbers |
---|
497 | plus infinity, where infinity represents a monomorphic parameter and a finite |
---|
498 | number counts how many levels deep the shallowest type variable is, e.g. where |
---|
499 | `T` is a type variable, `int` would have value infinity, `T` would have value |
---|
500 | 0, `T*` would have value 1, `box(T)*` would have value 2, etc. |
---|
501 | Under this scheme, higher values represent less polymorphism. |
---|
502 | This makes the partial order on parameters a total order, so that many of the |
---|
503 | incomparable functions above compare equal, though that is perhaps a virtue. |
---|
504 | It also loses the ability to differentiate between some multi-parameter |
---|
505 | generic types, such as the parameters in (10) and (11), which would both be |
---|
506 | valued 1, losing the polymorphism distinction between them. |
---|
507 | |
---|
508 | A variant of the above scheme would be to fix a maximum depth of polymorphic |
---|
509 | type variables (16 seems like a reasonable choice) at which a parameter would |
---|
510 | be considered to be effectively monomorphic, and to subtract the value |
---|
511 | described above from that maximum, clamping the result to a minimum of 0. |
---|
512 | Under this scheme, assuming a maximum value of 4, `int` has value 0, `T` has |
---|
513 | value 4, `T*` has value 3, `box(T)*` has value 2, and `box(T*)**` has value 0, |
---|
514 | the same as `int`. |
---|
515 | This can be quite succinctly represented, and summed without the presence of a |
---|
516 | single monomorphic parameter pushing the result to infinity, but does lose the |
---|
517 | ability to distinguish between very deeply structured polymorphic types. |
---|
518 | |
---|
519 | ### Parameter Lists ### |
---|
520 | A partial order on function parameter lists can be produced by the |
---|
521 | product order of the partial orders on parameters described above. |
---|
522 | In more detail, this means that for two parameter lists with the same arity, |
---|
523 | if any pair of corresponding parameters are incomparable with respect to each |
---|
524 | other, the two parameter lists are incomparable; if in all pairs of |
---|
525 | corresponding parameters one list's parameter is always (less than or) equal |
---|
526 | to the other list's parameter than the first parameter list is (less than or) |
---|
527 | equal to the second parameter list; otherwise the lists are incomparable with |
---|
528 | respect to each other. |
---|
529 | |
---|
530 | How to compare parameter lists of different arity is a somewhat open question. |
---|
531 | A simple, but perhaps somewhat unsatisfying, solution would be just to say |
---|
532 | that such lists are incomparable. |
---|
533 | The simplist approach to make them comparable is to say that, given two lists |
---|
534 | `(T1, T2, ... Tn)` and `(S1, S2, ... Sm)`, where `n <= m`, the parameter lists |
---|
535 | can be compared based on their shared prefix of `n` types. |
---|
536 | This approach breaks the transitivity property of the equivalence relation on |
---|
537 | the partial order, though, as seen below: |
---|
538 | |
---|
539 | forall(otype T) void f( T, int ); // (1a) |
---|
540 | forall(otype T) void f( T, int, int ); // (12) |
---|
541 | forall(otype T) void f( T, int, T ); // (13) |
---|
542 | |
---|
543 | By this rule, (1a) is equally polymorphic to both (12) and (13), so by |
---|
544 | transitivity (12) and (13) should also be equally polymorphic, but that is not |
---|
545 | actually the case. |
---|
546 | |
---|
547 | We can fix the rule by saying that `(T1 ... Tn)` can be compared to |
---|
548 | `(S1 ... Sm)` by _extending_ the list of `T`s to `m` types by inserting |
---|
549 | notional monomorphic parameters. |
---|
550 | In this case, (1a) and (12) are equally polymorphic, because (1a) gets |
---|
551 | extended with a monomorphic type that compares equal to (12)'s third `int` |
---|
552 | parameter, but (1a) is less polymorphic than (13), because its notional |
---|
553 | monomorphic third parameter is less polymorphic than (13)'s `T`. |
---|
554 | Essentially what this rule says is that any parameter list with more |
---|
555 | parameters is no less polymorphic than one with fewer. |
---|
556 | |
---|
557 | We could collapse this parameter list ordering to a succinct total order by |
---|
558 | simply taking the sum of the clamped parameter polymorphism counts, but this |
---|
559 | would again make most incomparable parameter lists compare equal, as well as |
---|
560 | having the potential for some unexpected results based on the (completely |
---|
561 | arbitrary) value chosen for "completely polymorphic". |
---|
562 | For instance, if we set 4 to be the maximum depth of polymorphism (as above), |
---|
563 | the following functions would be equally polymorphic, which is a somewhat |
---|
564 | unexpected result: |
---|
565 | |
---|
566 | forall(otype T) void g( T, T, T, int ); // 4 + 4 + 4 + 0 = 12 |
---|
567 | forall(otype T) void g( T*, T*, T*, T* ); // 3 + 3 + 3 + 3 = 12 |
---|
568 | |
---|
569 | These functions would also be considered equally polymorphic: |
---|
570 | |
---|
571 | forall(otype T) void g( T, int ); // 4 + 0 = 4; |
---|
572 | forall(otype T) void g( T**, T** ); // 2 + 2 = 4; |
---|
573 | |
---|
574 | This issue can be mitigated by choosing a larger maximum depth of |
---|
575 | polymorphism, but this scheme does have the distinct disadvantage of either |
---|
576 | specifying the (completely arbitrary) maximum depth as part of the language or |
---|
577 | allowing the compiler to refuse to accept otherwise well-typed deeply-nested |
---|
578 | polymorphic types. |
---|
579 | |
---|
580 | For purposes of determining polymorphism, the list of return types of a |
---|
581 | function should be treated like another parameter list, and combined with the |
---|
582 | degree of polymorphism from the parameter list in the same way that the |
---|
583 | parameters in the parameter list are combined. |
---|
584 | For instance, in the following, (14) is less polymorphic than (15) which is |
---|
585 | less polymorphic than (16): |
---|
586 | |
---|
587 | forall(otype T) int f( T ); // (14) |
---|
588 | forall(otype T) T* f( T ); // (15) |
---|
589 | forall(otype T) T f( T ); // (16) |
---|
590 | |
---|
591 | ### Type Variables and Bounds ### |
---|
592 | Degree of polymorphism doesn't solely depend on the parameter lists, though. |
---|
593 | Glen's thesis (4.4.4, p.89) gives an example that shows that it also depends |
---|
594 | on the number of type variables as well: |
---|
595 | |
---|
596 | forall(otype T) void f( T, int ); // (1a) polymorphic |
---|
597 | forall(otype T) void f( T, T ); // (2) more polymorphic |
---|
598 | forall(otype T, otype S) void f( T, S ); // (17) most polymorphic |
---|
599 | |
---|
600 | Clearly the `forall` type parameter list needs to factor into calculation of |
---|
601 | degree of polymorphism as well, as it's the only real differentiation between |
---|
602 | (2) and (17). |
---|
603 | The simplest way to include the type parameter list would be to simply count |
---|
604 | the type variables and say that functions with more type variables are more |
---|
605 | polymorphic. |
---|
606 | |
---|
607 | However, it also seems natural that more-constrained type variables should be |
---|
608 | counted as "less polymorphic" than less-constrained type variables. |
---|
609 | This would allow our resolver to pick more specialized (and presumably more |
---|
610 | efficient) implementations of functions where one exists. |
---|
611 | For example: |
---|
612 | |
---|
613 | forall(otype T | { void g(T); }) T f( T ); // (18) less polymorphic |
---|
614 | forall(otype T) T f( T ); // (16) more polymorphic |
---|
615 | |
---|
616 | We could account for this by counting the number of unique constraints and |
---|
617 | saying that functions with more constraints are less polymorphic. |
---|
618 | |
---|
619 | That said, we do model the `forall` constraint list as a (possibly anonymous) |
---|
620 | _trait_, and say that each trait is a set of constraints, so we could |
---|
621 | presumably define a partial order over traits based on subset inclusion, and |
---|
622 | use this partial order instead of the weaker count of constraints to order the |
---|
623 | list of type parameters of a function, as below: |
---|
624 | |
---|
625 | trait has_g(otype T) { void g(T); }; |
---|
626 | trait has_h(otype S) { void h(T); }; |
---|
627 | trait has_gh(otype R | has_g(R) | has_h(R)) {}; |
---|
628 | // has_gh is equivlent to { void g(R); void h(R); } |
---|
629 | |
---|
630 | forall(otype T | has_gh(T)) T f( T ); // (19) least polymorphic |
---|
631 | forall(otype T | has_g(T)) T f( T ); // (18) more polymorphic than (19) |
---|
632 | forall(otype T | has_h(T)) T f( T ); // (18b) more polymorphic than (19) |
---|
633 | // incomparable with (18) |
---|
634 | forall(otype T) T f( T ); // (16) most polymorphic |
---|
635 | |
---|
636 | The tricky bit with this is figuring out how to compare the constraint |
---|
637 | functions for equality up to type variable renaming; I suspect there's a known |
---|
638 | solution, but don't know what it is (perhaps some sort of unification |
---|
639 | calculation, though I hope there's a more lightweight option). |
---|
640 | We also should be able to take advantage of the programmer-provided trait |
---|
641 | subset information (like the constraint on `has_gh` in the example) to more |
---|
642 | efficiently generate the partial-order graph for traits, which should be able |
---|
643 | to be cached for efficiency. |
---|
644 | |
---|
645 | Combining count of type variables with the (partial) order on the trait |
---|
646 | constraining those variables seems like it should be a fairly straightforward |
---|
647 | product ordering to me - one `forall` qualifier is (less than or) equal to |
---|
648 | another if it has both a (less than or) equal number of type variables and a |
---|
649 | (less than or) equal degree of polymorphism from its constraining trait; the |
---|
650 | two qualifiers are incomparable otherwise. |
---|
651 | If an easier-to-calculate total ordering is desired, it might be acceptable to |
---|
652 | use the number of type variables, with ties broken by number of constraints. |
---|
653 | |
---|
654 | Similarly, to combine the (partial) orders on parameter and return lists with |
---|
655 | the (partial) order on `forall` qualifiers, a product ordering seems like the |
---|
656 | reasonable choice, though if we wanted a total order a reasonable choice would |
---|
657 | be to use whatever method we use to combine parameter costs into parameter |
---|
658 | lists to combine the costs for the parameter and return lists, then break ties |
---|
659 | by the order on the `forall` qualifiers. |
---|
660 | |
---|
661 | ## Expression Costs ## |
---|
662 | |
---|
663 | ### Variable Expressions ### |
---|
664 | Variables may be overloaded; that is, there may be multiple distinct variables |
---|
665 | with the same name so long as each variable has a distinct type. |
---|
666 | The variable expression `x` has one zero-cost interpretation as type `T` for |
---|
667 | each variable `T x` in scope. |
---|
668 | |
---|
669 | ### Member Selection Expressions ### |
---|
670 | For every interpretation `I` of `e` which has a struct or union type `S`, |
---|
671 | `e.y` has an interpretation of type `T` for each member `T y` of `S`, with the |
---|
672 | same cost as `I`. |
---|
673 | Note that there may be more than one member of `S` with the same name, as per |
---|
674 | Cforall's usual overloading rules. |
---|
675 | The indirect member expression `e->y` is desugared to `(*e).y` and interpreted |
---|
676 | analogously. |
---|
677 | |
---|
678 | **TODO** Consider allowing `e.y` to be interpreted as `e->y` if no |
---|
679 | interpretations as `e.y` exist. |
---|
680 | |
---|
681 | ### Address Expressions ### |
---|
682 | Address expressions `&e` have an interpretation for each interpretation `I` of |
---|
683 | `e` that is an lvalue of type `T`, with the same cost as `I` and type `T*`. |
---|
684 | Lvalues result from variable expressions, member selection expressions, or |
---|
685 | application of functions returning an lvalue-qualified type. |
---|
686 | Note that the dereference operator is overloadable, so the rules for its |
---|
687 | resolution follow those for function application below. |
---|
688 | |
---|
689 | **TODO** Consider allowing conversion-to-lvalue so that, e.g., `&42` spawns a |
---|
690 | new temporary holding `42` and takes its address. |
---|
691 | |
---|
692 | ### Boolean-context Expressions ### |
---|
693 | C has a number of "boolean contexts", where expressions are assigned a truth |
---|
694 | value; these include both arguments to the short-circuiting `&&` and `||` |
---|
695 | operators, as well as the conditional expressions in `if` and `while` |
---|
696 | statements, the middle expression in `for` statements, and the first argument |
---|
697 | to the `?:` ternary conditional operator. |
---|
698 | In all these contexts, C interprets `0` (which is both an integer and a null |
---|
699 | pointer literal) as false, and all other integer or pointer values as true. |
---|
700 | In this spirit, Cforall allows other types to be considered "truthy" if they |
---|
701 | support the following de-sugaring in a conditional context (see notes on |
---|
702 | interpretation of literal `0` below): |
---|
703 | |
---|
704 | x => ((int)( x != 0 )) |
---|
705 | |
---|
706 | ### Literal Expressions ### |
---|
707 | Literal expressions (e.g. 42, 'c', 3.14, "Hello, world!") have one |
---|
708 | zero-cost interpretation with the same type the expression would have in C, |
---|
709 | with three exceptions: |
---|
710 | |
---|
711 | Character literals like 'x' are typed as `char` in Cforall, not `int` as in C. |
---|
712 | This change breaks very little C code (primarily `sizeof 'x'`; the implicit |
---|
713 | conversion from `int` to `char` and lack of overloading handle most other |
---|
714 | expressions), matches the behaviour of C++, and is more compatible with |
---|
715 | programmer intuition. |
---|
716 | |
---|
717 | The literals `0` and `1` are also treated specially by Cforall, due to their |
---|
718 | potential uses in operator overloading. |
---|
719 | Earlier versions of Cforall allowed `0` and `1` to be variable names, allowing |
---|
720 | multiple interpretations of them according to the existing variable |
---|
721 | overloading rules, with the following declarations in the prelude: |
---|
722 | |
---|
723 | const int 0, 1; |
---|
724 | forall ( dtype DT ) const DT * const 0; |
---|
725 | forall ( ftype FT ) FT * const 0; |
---|
726 | |
---|
727 | This did, however, create some backward-compatibility problems and potential |
---|
728 | performance issues, and works poorly for generic types. To start with, this |
---|
729 | (entirely legal C) code snippet doesn't compile in Cforall: |
---|
730 | |
---|
731 | if ( 0 ) {} |
---|
732 | |
---|
733 | It desugars to `if ( (int)(0 != 0) ) {}`, and since both `int` and |
---|
734 | `forall(dtype DT) DT*` have a != operator which returns `int` the resolver can |
---|
735 | not choose which `0` variable to take, because they're both exact matches. |
---|
736 | |
---|
737 | The general != computation may also be less efficient than a check for a zero |
---|
738 | value; take the following example of a rational type: |
---|
739 | |
---|
740 | struct rational { int32_t num, int32_t den }; |
---|
741 | rational 0 = { 0, 1 }; |
---|
742 | |
---|
743 | int ?!=? (rational a, rational b) { |
---|
744 | return ((int64_t)a.num)*b.den != ((int64_t)b.num)*a.den; |
---|
745 | } |
---|
746 | |
---|
747 | int not_zero (rational a) { return a.num != 0; } |
---|
748 | |
---|
749 | To check if two rationals are equal we need to do a pair of multiplications to |
---|
750 | normalize them (the casts in the example are to prevent overflow), but to |
---|
751 | check if a rational is non-zero we just need to check its numerator, a more |
---|
752 | efficient operation. |
---|
753 | |
---|
754 | Finally, though polymorphic null-pointer variables can be meaningfully |
---|
755 | defined, most other polymorphic variables cannot be, which makes it difficult |
---|
756 | to make generic types "truthy" using the existing system: |
---|
757 | |
---|
758 | forall(otype T) struct pair { T x; T y; }; |
---|
759 | forall(otype T | { T 0; }) pair(T) 0 = { 0, 0 }; |
---|
760 | |
---|
761 | Now, it seems natural enough to want to define the zero for this pair type as |
---|
762 | a pair of the zero values of its element type (if they're defined). |
---|
763 | The declaration of `pair(T) 0` above is actually illegal though, as there is |
---|
764 | no way to represent the zero values of an infinite number of types in the |
---|
765 | single memory location available for this polymorphic variable - the |
---|
766 | polymorphic null-pointer variables defined in the prelude are legal, but that |
---|
767 | is only because all pointers are the same size and the single zero value is a |
---|
768 | legal value of all pointer types simultaneously; null pointer is, however, |
---|
769 | somewhat unique in this respect. |
---|
770 | |
---|
771 | The technical explanation for the problems with polymorphic zero is that `0` |
---|
772 | is really a rvalue, not a lvalue - an expression, not an object. |
---|
773 | Drawing from this, the solution we propose is to give `0` a new built-in type, |
---|
774 | `_zero_t` (name open to bikeshedding), and similarly give `1` the new built-in |
---|
775 | type `_unit_t`. |
---|
776 | If the prelude defines != over `_zero_t` this solves the `if ( 0 )` problem, |
---|
777 | because now the unambiguous best interpretation of `0 != 0` is to read them |
---|
778 | both as `_zero_t` (and say that this expression is false). |
---|
779 | Backwards compatibility with C can be served by defining conversions in the |
---|
780 | prelude from `_zero_t` and `_unit_t` to `int` and the appropriate pointer |
---|
781 | types, as below: |
---|
782 | |
---|
783 | // int 0; |
---|
784 | forall(otype T | { void ?{safe}(T*, int); }) void ?{safe} (T*, _zero_t); |
---|
785 | forall(otype T | { void ?{unsafe}(T*, int); }) void ?{unsafe} (T*, _zero_t); |
---|
786 | |
---|
787 | // int 1; |
---|
788 | forall(otype T | { void ?{safe}(T*, int); }) void ?{safe} (T*, _unit_t); |
---|
789 | forall(otype T | { void ?{unsafe}(T*, int); }) void ?{unsafe} (T*, _unit_t); |
---|
790 | |
---|
791 | // forall(dtype DT) const DT* 0; |
---|
792 | forall(dtype DT) void ?{safe}(const DT**, _zero_t); |
---|
793 | // forall(ftype FT) FT* 0; |
---|
794 | forall(ftype FT) void ?{safe}(FT**, _zero_t); |
---|
795 | |
---|
796 | Further, with this change, instead of making `0` and `1` overloadable |
---|
797 | variables, we can instead allow user-defined constructors (or, more flexibly, |
---|
798 | safe conversions) from `_zero_t`, as below: |
---|
799 | |
---|
800 | // rational 0 = { 0, 1 }; |
---|
801 | void ?{safe} (rational *this, _zero_t) { this->num = 0; this->den = 1; } |
---|
802 | |
---|
803 | Note that we don't need to name the `_zero_t` parameter to this constructor, |
---|
804 | because its only possible value is a literal zero. |
---|
805 | This one line allows `0` to be used anywhere a `rational` is required, as well |
---|
806 | as enabling the same use of rationals in boolean contexts as above (by |
---|
807 | interpreting the `0` in the desguraring to be a rational by this conversion). |
---|
808 | Furthermore, while defining a conversion function from literal zero to |
---|
809 | `rational` makes rational a "truthy" type able to be used in a boolean |
---|
810 | context, we can optionally further optimize the truth decision on rationals as |
---|
811 | follows: |
---|
812 | |
---|
813 | int ?!=? (rational a, _zero_t) { return a.num != 0; } |
---|
814 | |
---|
815 | This comparison function will be chosen in preference to the more general |
---|
816 | rational comparison function for comparisons against literal zero (like in |
---|
817 | boolean contexts) because it doesn't require a conversion on the `0` argument. |
---|
818 | Functions of the form `int ?!=? (T, _zero_t)` can acutally be used in general |
---|
819 | to make a type `T` truthy without making `0` a value which can convert to that |
---|
820 | type, a capability not available in the current design. |
---|
821 | |
---|
822 | This design also solves the problem of polymorphic zero for generic types, as |
---|
823 | in the following example: |
---|
824 | |
---|
825 | // ERROR: forall(otype T | { T 0; }) pair(T) 0 = { 0, 0 }; |
---|
826 | forall(otype T | { T 0; }) void ?{safe} (pair(T) *this, _zero_t) { |
---|
827 | this->x = 0; this->y = 0; |
---|
828 | } |
---|
829 | |
---|
830 | The polymorphic variable declaration didn't work, but this constructor is |
---|
831 | perfectly legal and has the desired semantics. |
---|
832 | |
---|
833 | We can assert that `T` can be used in a boolean context as follows: |
---|
834 | |
---|
835 | `forall(otype T | { int ?!=?(T, _zero_t); })` |
---|
836 | |
---|
837 | Since the C standard (6.5.16.1.1) specifically states that pointers can be |
---|
838 | assigned into `_Bool` variables (and implies that other artithmetic types can |
---|
839 | be assigned into `_Bool` variables), it seems natural to say that assignment |
---|
840 | into a `_Bool` variable effectively constitutes a boolean context. |
---|
841 | To allow this interpretation, I propose including the following function (or |
---|
842 | its effective equivalent) in the prelude: |
---|
843 | |
---|
844 | forall(otype T | { int ?!=?(T, _zero_t); }) |
---|
845 | void ?{safe}( _Bool *this, T that ) { *this = that != 0; } |
---|
846 | |
---|
847 | Note that this conversion is not transitive; that is, for `t` a variable of |
---|
848 | some "truthy" type `T`, `(_Bool)t;` would use this conversion (in the absence |
---|
849 | of a lower-cost one), `(int)t;` would not use this conversion (and in fact |
---|
850 | would not be legal in the absence of another valid way to convert a `T` to an |
---|
851 | `int`), but `(int)(_Bool)t;` could legally use this conversion. |
---|
852 | |
---|
853 | Similarly giving literal `1` the special type `_unit_t` allows for more |
---|
854 | concise and consistent specification of the increment and decrement operators, |
---|
855 | using the following de-sugaring: |
---|
856 | |
---|
857 | ++i => i += 1 |
---|
858 | i++ => (tmp = i, i += 1, tmp) |
---|
859 | --i => i -= 1 |
---|
860 | i-- => (tmp = i, i -= 1, tmp) |
---|
861 | |
---|
862 | In the examples above, `tmp` is a fresh temporary with its type inferred from |
---|
863 | the return type of `i += 1`. |
---|
864 | Under this proposal, defining a conversion from `_unit_t` to `T` and a |
---|
865 | `lvalue T ?+=? (T*, T)` provides both the pre- and post-increment operators |
---|
866 | for free in a consistent fashion (similarly for -= and the decrement |
---|
867 | operators). |
---|
868 | If a meaningful `1` cannot be defined for a type, both increment operators can |
---|
869 | still be defined with the signature `lvalue T ?+=? (T*, _unit_t)`. |
---|
870 | Similarly, if scalar addition can be performed on a type more efficiently than |
---|
871 | by repeated increment, `lvalue T ?+=? (T*, int)` will not only define the |
---|
872 | addition operator, it will simultaneously define consistent implementations of |
---|
873 | both increment operators (this can also be accomplished by defining a |
---|
874 | conversion from `int` to `T` and an addition operator `lvalue T ?+=?(T*, T)`). |
---|
875 | |
---|
876 | To allow functions of the form `lvalue T ?+=? (T*, int)` to satisfy "has an |
---|
877 | increment operator" assertions of the form `lvalue T ?+=? (T*, _unit_t)`, |
---|
878 | we also define a non-transitive unsafe conversion from `_Bool` (allowable |
---|
879 | values `0` and `1`) to `_unit_t` (and `_zero_t`) as follows: |
---|
880 | |
---|
881 | void ?{unsafe} (_unit_t*, _Bool) {} |
---|
882 | |
---|
883 | As a note, the desugaring of post-increment above is possibly even more |
---|
884 | efficient than that of C++ - in C++, the copy to the temporary may be hidden |
---|
885 | in a separately-compiled module where it can't be elided in cases where it is |
---|
886 | not used, whereas this approach for Cforall always gives the compiler the |
---|
887 | opportunity to optimize out the temporary when it is not needed. |
---|
888 | Furthermore, one could imagine a post-increment operator that returned some |
---|
889 | type `T2` that was implicitly convertable to `T` but less work than a full |
---|
890 | copy of `T` to create (this seems like an absurdly niche case) - since the |
---|
891 | type of `tmp` is inferred from the return type of `i += 1`, you could set up |
---|
892 | functions with the following signatures to enable an equivalent pattern in |
---|
893 | Cforall: |
---|
894 | |
---|
895 | lvalue T2 ?+=? (T*, _unit_t); // increment operator returns T2 |
---|
896 | void ?{} (T2*, T); // initialize T2 from T for use in `tmp = i` |
---|
897 | void ?{safe} (T*, T2); // allow T2 to be used as a T when needed to |
---|
898 | // preserve expected semantics of T x = y++; |
---|
899 | |
---|
900 | **TODO** Look in C spec for literal type interprations. |
---|
901 | **TODO** Write up proposal for wider range of literal types, put in appendix |
---|
902 | |
---|
903 | ### Initialization and Cast Expressions ### |
---|
904 | An initialization expression `T x = e` has one interpretation for each |
---|
905 | interpretation `I` of `e` with type `S` which is convertable to `T`. |
---|
906 | The cost of the interpretation is the cost of `I` plus the conversion cost |
---|
907 | from `S` to `T`. |
---|
908 | A cast expression `(T)e` is interpreted as hoisting initialization of a |
---|
909 | temporary variable `T tmp = e` out of the current expression, then replacing |
---|
910 | `(T)e` by the new temporary `tmp`. |
---|
911 | |
---|
912 | ### Assignment Expressions ### |
---|
913 | An assignment expression `e = f` desugars to `(?=?(&e, f), e)`, and is then |
---|
914 | interpreted according to the usual rules for function application and comma |
---|
915 | expressions. |
---|
916 | Operator-assignment expressions like `e += f` desugar similarly as |
---|
917 | `(?+=?(&e, f), e)`. |
---|
918 | |
---|
919 | ### Function Application Expressions ### |
---|
920 | Every _compatible function_ and satisfying interpretation of its arguments and |
---|
921 | polymorphic variable bindings produces one intepretation for the function |
---|
922 | application expression. |
---|
923 | Broadly speaking, the resolution cost of a function application is the sum of |
---|
924 | the cost of the interpretations of all arguments, the cost of all conversions |
---|
925 | to make those argument interpretations match the parameter types, and the |
---|
926 | binding cost of any of the function's polymorphic type parameters. |
---|
927 | |
---|
928 | **TODO** Work out binding cost in more detail. |
---|
929 | **TODO** Address whether "incomparably polymorphic" should be treated as |
---|
930 | "equally polymorphic" and be disambiguated by count of (safe) conversions. |
---|
931 | **TODO** Think about what polymorphic return types mean in terms of late |
---|
932 | binding. |
---|
933 | **TODO** Consider if "f is less polymorphic than g" can mean exactly "f |
---|
934 | specializes g"; if we don't consider the assertion parameters (except perhaps |
---|
935 | by count) and make polymorphic variables bind exactly (rather than after |
---|
936 | implicit conversions) this should actually be pre-computable. |
---|
937 | **TODO** Add "deletable" functions - take Thierry's suggestion that a deleted |
---|
938 | function declaration is costed out by the resolver in the same way that any |
---|
939 | other function declaration is costed; if the deleted declaration is the unique |
---|
940 | min-cost resolution refuse to type the expression, if it is tied for min-cost |
---|
941 | then take the non-deleted alternative, and of two equivalent-cost deleted |
---|
942 | interpretations with the same return type pick one arbitrarily rather than |
---|
943 | producing an ambiguous resolution. This would also be useful for forbidding |
---|
944 | pointer-to-floating-point explicit conversions (C11, 6.5.4.4). |
---|
945 | **TODO** Cover default parameters, maybe named parameters (see "named |
---|
946 | arguments" thread of 11 March 2016) |
---|
947 | |
---|
948 | |
---|
949 | ### Sizeof, Alignof & Offsetof Expressions ### |
---|
950 | `sizeof`, `alignof`, and `offsetof` expressions have at most a single |
---|
951 | interpretation, of type `size_t`. |
---|
952 | `sizeof` and `alignof` expressions take either a type or an expression as a |
---|
953 | an argument; if the argument is a type, it must be a complete type which is |
---|
954 | not a function type, if an expression, the expression must have a single |
---|
955 | interpretation, the type of which conforms to the same rules. |
---|
956 | `offsetof` takes two arguments, a type and a member name; the type must be |
---|
957 | a complete structure or union type, and the second argument must name a member |
---|
958 | of that type. |
---|
959 | |
---|
960 | ### Comma Expressions ### |
---|
961 | A comma expression `x, y` resolves `x` as if it had been cast to `void`, and |
---|
962 | then, if there is a unique interpretation `I` of `x`, has one interpretation |
---|
963 | for each interpretation `J` of `y` with the same type as `J` costing the sum |
---|
964 | of the costs of `I` and `J`. |
---|
965 | |
---|
966 | ### Index Expressions ### |
---|
967 | **TODO** Consider adding polymorphic function in prelude for this, as per |
---|
968 | 6.5.2.1.2 in the C standard: |
---|
969 | |
---|
970 | forall(otype T, otype I, otype R, otype E | { R ?+?(T, I); lvalue E *?(R); }) |
---|
971 | lvalue E ?[?](T a, I i) { return *(a + i); } |
---|
972 | |
---|
973 | I think this isn't actually a good idea, because the cases for it are niche, |
---|
974 | mostly odd tricks like `0[p]` as an alternate syntax for dereferencing a |
---|
975 | pointer `p`, and adding it to the prelude would slow down resolution of |
---|
976 | every index expression just a bit. Our existing prelude includes an indexing |
---|
977 | operator `forall(otype T) lvalue T ?[?](ptrdiff_t, T*)`, plus qualified |
---|
978 | variants, which should satisfy C source-compatibility without propegating this |
---|
979 | silly desugaring further. |
---|
980 | |
---|
981 | #### Compatible Functions #### |
---|
982 | **TODO** This subsection is very much a work in progress and has multiple open |
---|
983 | design questions. |
---|
984 | |
---|
985 | A _compatible function_ for an application expression is a visible function |
---|
986 | declaration with the same name as the application expression and parameter |
---|
987 | types that can be converted to from the argument types. |
---|
988 | Function pointers and variables of types with the `?()` function call operator |
---|
989 | overloaded may also serve as function declarations for purposes of |
---|
990 | compatibility. |
---|
991 | |
---|
992 | For monomorphic parameters of a function declaration, the declaration is a |
---|
993 | compatible function if there is an argument interpretation that is either an |
---|
994 | exact match, or has a safe or unsafe implicit conversion that can be used to |
---|
995 | reach the parameter type; for example: |
---|
996 | |
---|
997 | void f(int); |
---|
998 | |
---|
999 | f(42); // compatible; exact match to int type |
---|
1000 | f('x'); // compatible; safe conversion from char => int |
---|
1001 | f(3.14); // compatible; unsafe conversion from double => int |
---|
1002 | f((void*)0); // not compatible; no implicit conversion from void* => int |
---|
1003 | |
---|
1004 | Per Richard[*], function assertion satisfaction involves recursively searching |
---|
1005 | for compatible functions, not an exact match on the function types (I don't |
---|
1006 | believe the current Cforall resolver handles this properly); to extend the |
---|
1007 | previous example: |
---|
1008 | |
---|
1009 | forall(otype T | { void f(T); }) void g(T); |
---|
1010 | |
---|
1011 | g(42); // binds T = int, takes f(int) by exact match |
---|
1012 | g('x'); // binds T = char, takes f(int) by conversion |
---|
1013 | g(3.14); // binds T = double, takes f(int) by conversion |
---|
1014 | |
---|
1015 | [*] Bilson, s.2.1.3, p.26-27, "Assertion arguments are found by searching the |
---|
1016 | accessible scopes for definitions corresponding to assertion names, and |
---|
1017 | choosing the ones whose types correspond *most closely* to the assertion |
---|
1018 | types." (emphasis mine) |
---|
1019 | |
---|
1020 | There are three approaches we could take to binding type variables: type |
---|
1021 | variables must bind to argument types exactly, each type variable must bind |
---|
1022 | exactly to at least one argument, or type variables may bind to any type which |
---|
1023 | all corresponding arguments can implicitly convert to; I'll provide some |
---|
1024 | possible motivation for each approach. |
---|
1025 | |
---|
1026 | There are two main arguments for the more restrictive binding schemes; the |
---|
1027 | first is that the built-in implicit conversions in C between `void*` and `T*` |
---|
1028 | for any type `T` can lead to unexpectedly type-unsafe behaviour in a more |
---|
1029 | permissive binding scheme, for example: |
---|
1030 | |
---|
1031 | forall(dtype T) T* id(T *p) { return p; } |
---|
1032 | |
---|
1033 | int main() { |
---|
1034 | int *p = 0; |
---|
1035 | char *c = id(p); |
---|
1036 | } |
---|
1037 | |
---|
1038 | This code compiles in CFA today, and it works because the extra function |
---|
1039 | wrapper `id` provides a level of indirection that allows the non-chaining |
---|
1040 | implicit conversions from `int*` => `void*` and `void*` => `char*` to chain. |
---|
1041 | The resolver types the last line with `T` bound to `void` as follows: |
---|
1042 | |
---|
1043 | char *c = (char*)id( (void*)p ); |
---|
1044 | |
---|
1045 | It has been suggested that making the implicit conversions to and from `void*` |
---|
1046 | explicit in Cforall code (as in C++) would solve this particular problem, and |
---|
1047 | provide enough other type-safety benefits to outweigh the source-compatibility |
---|
1048 | break with C; see Appendix D for further details. |
---|
1049 | |
---|
1050 | The second argument for a more constrained binding scheme is performance; |
---|
1051 | trait assertions need to be checked after the type variables are bound, and |
---|
1052 | adding more possible values for the type variables should correspond to a |
---|
1053 | linear increase in runtime of the resolver per type variable. |
---|
1054 | There are 21 built-in arithmetic types in C (ignoring qualifiers), and each of |
---|
1055 | them is implicitly convertable to any other; if we allow unrestricted binding |
---|
1056 | of type variables, a common `int` variable (or literal) used in the position |
---|
1057 | of a polymorphic variable parameter would cause a 20x increase in the amount |
---|
1058 | of time needed to check trait resolution for that interpretation. |
---|
1059 | These numbers have yet to be emprically substantiated, but the theory is |
---|
1060 | reasonable, and given that much of the impetus for re-writing the resolver is |
---|
1061 | due to its poor performance, I think this is a compelling argument. |
---|
1062 | |
---|
1063 | I would also mention that a constrained binding scheme is practical; the most |
---|
1064 | common type of assertion is a function assertion, and, as mentioned above, |
---|
1065 | those assertions should be able to be implicitly converted to to match. |
---|
1066 | Thus, in the example above with `g(T)`, where the assertion is `void f(T)`, |
---|
1067 | we first bind `T = int` or `T = char` or `T = double`, then substitute the |
---|
1068 | binding into the assertion, yielding assertions of `void f(int)`, |
---|
1069 | `void f(char)`, or `void f(double)`, respectively, then attempt to satisfy |
---|
1070 | these assertions to complete the binding. |
---|
1071 | Though in all three cases, the existing function with signature `void f(int)` |
---|
1072 | satisfies this assertion, the checking work cannot easily be re-used between |
---|
1073 | variable bindings, because there may be better or worse matches depending on |
---|
1074 | the specifics of the binding. |
---|
1075 | |
---|
1076 | The main argument for a more flexible binding scheme is that the binding |
---|
1077 | abstraction can actually cause a wrapped function call that would work to |
---|
1078 | cease to resolve, as below: |
---|
1079 | |
---|
1080 | forall(otype T | { T ?+? (T, T) }) |
---|
1081 | T add(T x, T y) { return x + y; } |
---|
1082 | |
---|
1083 | int main() { |
---|
1084 | int i, j = 2; |
---|
1085 | short r, s = 3; |
---|
1086 | i = add(j, s); |
---|
1087 | r = add(s, j); |
---|
1088 | } |
---|
1089 | |
---|
1090 | Now, C's implicit conversions mean that you can call `j + s` or `s + j`, and |
---|
1091 | in both cases the short `s` is promoted to `int` to match `j`. |
---|
1092 | If, on the other hand, we demand that variables exactly match type variables, |
---|
1093 | neither call to `add` will compile, because it is impossible to simultaneously |
---|
1094 | bind `T` to both `int` and `short` (C++ has a similar restriction on template |
---|
1095 | variable inferencing). |
---|
1096 | One alternative that enables this case, while still limiting the possible |
---|
1097 | type variable bindings is to say that at least one argument must bind to its |
---|
1098 | type parameter exactly. |
---|
1099 | In this case, both calls to `add` would have the set `{ T = int, T = short }` |
---|
1100 | for candidate bindings, and would have to check both, as well as checking that |
---|
1101 | `short` could convert to `int` or vice-versa. |
---|
1102 | |
---|
1103 | It is worth noting here that parameterized types generally bind their type |
---|
1104 | parameters exactly anyway, so these "restrictive" semantics only restrict a |
---|
1105 | small minority of calls; for instance, in the example following, there isn't a |
---|
1106 | sensible way to type the call to `ptr-add`: |
---|
1107 | |
---|
1108 | forall(otype T | { T ?+?(T, T) }) |
---|
1109 | void ptr-add( T* rtn, T* x, T* y ) { |
---|
1110 | *rtn = *x + *y; |
---|
1111 | } |
---|
1112 | |
---|
1113 | int main() { |
---|
1114 | int i, j = 2; |
---|
1115 | short s = 3; |
---|
1116 | ptr-add(&i, &j, &s); // ERROR &s is not an int* |
---|
1117 | } |
---|
1118 | |
---|
1119 | I think there is some value in providing library authors with the |
---|
1120 | capability to express "these two parameter types must match exactly". |
---|
1121 | This can be done without restricting the language's expressivity, as the `add` |
---|
1122 | case above can be made to work under the strictest type variable binding |
---|
1123 | semantics with any addition operator in the system by changing its signature |
---|
1124 | as follows: |
---|
1125 | |
---|
1126 | forall( otype T, otype R, otype S | { R ?+?(T, S); } ) |
---|
1127 | R add(T x, S y) { return x + y; } |
---|
1128 | |
---|
1129 | Now, it is somewhat unfortunate that the most general version here is more |
---|
1130 | verbose (and thus that the path of least resistence would be more restrictive |
---|
1131 | library code); however, the breaking case in the example code above is a bit |
---|
1132 | odd anyway - explicitly taking two variables of distinct types and relying on |
---|
1133 | C's implicit conversions to do the right thing is somewhat bad form, |
---|
1134 | especially where signed/unsigned conversions are concerned. |
---|
1135 | I think the more common case for implicit conversions is the following, |
---|
1136 | though, where the conversion is used on a literal: |
---|
1137 | |
---|
1138 | short x = 40; |
---|
1139 | short y = add(x, 2); |
---|
1140 | |
---|
1141 | One option to handle just this case would be to make literals implicitly |
---|
1142 | convertable to match polymorphic type variables, but only literals. |
---|
1143 | The example above would actually behave slightly differently than `x + 2` in |
---|
1144 | C, though, casting the `2` down to `short` rather than the `x` up to `int`, a |
---|
1145 | possible demerit of this scheme. |
---|
1146 | |
---|
1147 | The other question to ask would be which conversions would be allowed for |
---|
1148 | literals; it seems rather odd to allow down-casting `42ull` to `char`, when |
---|
1149 | the programmer has explicitly specified by the suffix that it's an unsigned |
---|
1150 | long. |
---|
1151 | Type interpretations of literals in C are rather complex (see [1]), but one |
---|
1152 | reasonable approach would be to say that un-suffixed integer literals could be |
---|
1153 | interpreted as any type convertable from int, "u" suffixed literals could be |
---|
1154 | interpreted as any type convertable from "unsigned int" except the signed |
---|
1155 | integer types, and "l" or "ll" suffixed literals could only be interpreted as |
---|
1156 | `long` or `long long`, respectively (or possibly that the "u" suffix excludes |
---|
1157 | the signed types, while the "l" suffix excludes the types smaller than |
---|
1158 | `long int`, as in [1]). |
---|
1159 | Similarly, unsuffixed floating-point literals could be interpreted as `float`, |
---|
1160 | `double` or `long double`, but "f" or "l" suffixed floating-point literals |
---|
1161 | could only be interpreted as `float` or `long double`, respectively. |
---|
1162 | I would like to specify that character literals can only be interpreted as |
---|
1163 | `char`, but the wide-character variants and the C practice of typing character |
---|
1164 | literals as `int` means that would likely break code, so character literals |
---|
1165 | should be able to take any integer type. |
---|
1166 | |
---|
1167 | [1] http://en.cppreference.com/w/c/language/integer_constant |
---|
1168 | |
---|
1169 | With the possible exception of the `add` case above, implicit conversions to |
---|
1170 | the function types of assertions can handle most of the expected behaviour |
---|
1171 | from C. |
---|
1172 | However, implicit conversions cannot be applied to match variable assertions, |
---|
1173 | as in the following example: |
---|
1174 | |
---|
1175 | forall( otype T | { int ?<?(T, T); T ?+?(T, T); T min; T max; } ) |
---|
1176 | T clamp_sum( T x, T y ) { |
---|
1177 | T sum = x + y; |
---|
1178 | if ( sum < min ) return min; |
---|
1179 | if ( max < sum ) return max; |
---|
1180 | return sum; |
---|
1181 | } |
---|
1182 | |
---|
1183 | char min = 'A'; |
---|
1184 | double max = 100.0; |
---|
1185 | //int val = clamp_sum( 'X', 3.14 ); // ERROR (1) |
---|
1186 | |
---|
1187 | char max = 'Z' |
---|
1188 | char val = clamp_sum( 'X', 3.14 ); // MATCH (2) |
---|
1189 | double val = clamp_sum( 40.9, 19.9 ); // MAYBE (3) |
---|
1190 | |
---|
1191 | In this example, the call to `clamp_sum` at (1) doesn't compile, because even |
---|
1192 | though there are compatible `min` and `max` variables of types `char` and |
---|
1193 | `double`, they need to have the same type to match the constraint, and they |
---|
1194 | don't. |
---|
1195 | The (2) example does compile, but with a behaviour that might be a bit |
---|
1196 | unexpected given the "usual arithmetic conversions", in that both values are |
---|
1197 | narrowed to `char` to match the `min` and `max` constraints, rather than |
---|
1198 | widened to `double` as is usual for mis-matched arguments to +. |
---|
1199 | The (3) example is the only case discussed here that would require the most |
---|
1200 | permisive type binding semantics - here, `T` is bound to `char`, to match the |
---|
1201 | constraints, and both the parameters are narrowed from `double` to `char` |
---|
1202 | before the call, which would not be allowed under either of the more |
---|
1203 | restrictive binding semantics. |
---|
1204 | However, the behaviour here is unexpected to the programmer, because the |
---|
1205 | return value will be `(double)'A' /* == 60.0 */` due to the conversions, |
---|
1206 | rather than `60.8 /* == 40.9 + 19.9 */` as they might expect. |
---|
1207 | |
---|
1208 | Personally, I think that implicit conversions are not a particularly good |
---|
1209 | language design, and that the use-cases for them can be better handled with |
---|
1210 | less powerful features (e.g. more versatile rules for typing constant |
---|
1211 | expressions). |
---|
1212 | However, though we do need implicit conversions in monomorphic code for C |
---|
1213 | compatibility, I'm in favour of restricting their usage in polymorphic code, |
---|
1214 | both to give programmers some stronger tools to express their intent and to |
---|
1215 | shrink the search space for the resolver. |
---|
1216 | Of the possible binding semantics I've discussed, I'm in favour of forcing |
---|
1217 | polymorphic type variables to bind exactly, though I could be talked into |
---|
1218 | allowing literal expressions to have more flexibility in their bindings, or |
---|
1219 | possibly loosening "type variables bind exactly" to "type variables bind |
---|
1220 | exactly at least once"; I think the unrestricted combination of implicit |
---|
1221 | conversions and polymorphic type variable binding unneccesarily multiplies the |
---|
1222 | space of possible function resolutions, and that the added resolution options |
---|
1223 | are mostly unexpected and therefore confusing and not useful to user |
---|
1224 | programmers. |
---|
1225 | |
---|
1226 | ## Appendix A: Partial and Total Orders ## |
---|
1227 | The `<=` relation on integers is a commonly known _total order_, and |
---|
1228 | intuitions based on how it works generally apply well to other total orders. |
---|
1229 | Formally, a total order is some binary relation `<=` over a set `S` such that |
---|
1230 | for any two members `a` and `b` of `S`, `a <= b` or `b <= a` (if both, `a` and |
---|
1231 | `b` must be equal, the _antisymmetry_ property); total orders also have a |
---|
1232 | _transitivity_ property, that if `a <= b` and `b <= c`, then `a <= c`. |
---|
1233 | If `a` and `b` are distinct elements and `a <= b`, we may write `a < b`. |
---|
1234 | |
---|
1235 | A _partial order_ is a generalization of this concept where the `<=` relation |
---|
1236 | is not required to be defined over all pairs of elements in `S` (though there |
---|
1237 | is a _reflexivity_ requirement that for all `a` in `S`, `a <= a`); in other |
---|
1238 | words, it is possible for two elements `a` and `b` of `S` to be |
---|
1239 | _incomparable_, unable to be ordered with respect to one another (any `a` and |
---|
1240 | `b` for which either `a <= b` or `b <= a` are called _comparable_). |
---|
1241 | Antisymmetry and transitivity are also required for a partial order, so all |
---|
1242 | total orders are also partial orders by definition. |
---|
1243 | One fairly natural partial order is the "subset of" relation over sets from |
---|
1244 | the same universe; `{ }` is a subset of both `{ 1 }` and `{ 2 }`, which are |
---|
1245 | both subsets of `{ 1, 2 }`, but neither `{ 1 }` nor `{ 2 }` is a subset of the |
---|
1246 | other - they are incomparable under this relation. |
---|
1247 | |
---|
1248 | We can compose two (or more) partial orders to produce a new partial order on |
---|
1249 | tuples drawn from both (or all the) sets. |
---|
1250 | For example, given `a` and `c` from set `S` and `b` and `d` from set `R`, |
---|
1251 | where both `S` and `R` both have partial orders defined on them, we can define |
---|
1252 | a ordering relation between `(a, b)` and `(c, d)`. |
---|
1253 | One common order is the _lexicographical order_, where `(a, b) <= (c, d)` iff |
---|
1254 | `a < c` or both `a = c` and `b <= d`; this can be thought of as ordering by |
---|
1255 | the first set and "breaking ties" by the second set. |
---|
1256 | Another common order is the _product order_, which can be roughly thought of |
---|
1257 | as "all the components are ordered the same way"; formally `(a, b) <= (c, d)` |
---|
1258 | iff `a <= c` and `b <= d`. |
---|
1259 | One difference between the lexicographical order and the product order is that |
---|
1260 | in the lexicographical order if both `a` and `c` and `b` and `d` are |
---|
1261 | comparable then `(a, b)` and `(c, d)` will be comparable, while in the product |
---|
1262 | order you can have `a <= c` and `d <= b` (both comparable) which will make |
---|
1263 | `(a, b)` and `(c, d)` incomparable. |
---|
1264 | The product order, on the other hand, has the benefit of not prioritizing one |
---|
1265 | order over the other. |
---|
1266 | |
---|
1267 | Any partial order has a natural representation as a directed acyclic graph |
---|
1268 | (DAG). |
---|
1269 | Each element `a` of the set becomes a node of the DAG, with an arc pointing to |
---|
1270 | its _covering_ elements, any element `b` such that `a < b` but where there is |
---|
1271 | no `c` such that `a < c` and `c < b`. |
---|
1272 | Intuitively, the covering elements are the "next ones larger", where you can't |
---|
1273 | fit another element between the two. |
---|
1274 | Under this construction, `a < b` is equivalent to "there is a path from `a` to |
---|
1275 | `b` in the DAG", and the lack of cycles in the directed graph is ensured by |
---|
1276 | the antisymmetry property of the partial order. |
---|
1277 | |
---|
1278 | Partial orders can be generalized to _preorders_ by removing the antisymmetry |
---|
1279 | property. |
---|
1280 | In a preorder the relation is generally called `<~`, and it is possible for |
---|
1281 | two distict elements `a` and `b` to have `a <~ b` and `b <~ a` - in this case |
---|
1282 | we write `a ~ b`; `a <~ b` and not `a ~ b` is written `a < b`. |
---|
1283 | Preorders may also be represented as directed graphs, but in this case the |
---|
1284 | graph may contain cycles. |
---|
1285 | |
---|
1286 | ## Appendix B: Building a Conversion Graph from Un-annotated Single Steps ## |
---|
1287 | The short answer is that it's impossible. |
---|
1288 | |
---|
1289 | The longer answer is that it has to do with what's essentially a diamond |
---|
1290 | inheritance problem. |
---|
1291 | In C, `int` converts to `unsigned int` and also `long` "safely"; both convert |
---|
1292 | to `unsigned long` safely, and it's possible to chain the conversions to |
---|
1293 | convert `int` to `unsigned long`. |
---|
1294 | There are two constraints here; one is that the `int` to `unsigned long` |
---|
1295 | conversion needs to cost more than the other two (because the types aren't as |
---|
1296 | "close" in a very intuitive fashion), and the other is that the system needs a |
---|
1297 | way to choose which path to take to get to the destination type. |
---|
1298 | Now, a fairly natural solution for this would be to just say "C knows how to |
---|
1299 | convert from `int` to `unsigned long`, so we just put in a direct conversion |
---|
1300 | and make the compiler smart enough to figure out the costs" - given that the |
---|
1301 | users can build an arbitrary graph of conversions, this needs to be handled |
---|
1302 | anyway. |
---|
1303 | We can define a preorder over the types by saying that `a <~ b` if there |
---|
1304 | exists a chain of conversions from `a` to `b`. |
---|
1305 | This preorder corresponds roughly to a more usual type-theoretic concept of |
---|
1306 | subtyping ("if I can convert `a` to `b`, `a` is a more specific type than |
---|
1307 | `b`"); however, since this graph is arbitrary, it may contain cycles, so if |
---|
1308 | there is also a path to convert `b` to `a` they are in some sense equivalently |
---|
1309 | specific. |
---|
1310 | |
---|
1311 | Now, to compare the cost of two conversion chains `(s, x1, x2, ... xn)` and |
---|
1312 | `(s, y1, y2, ... ym)`, we have both the length of the chains (`n` versus `m`) |
---|
1313 | and this conversion preorder over the destination types `xn` and `ym`. |
---|
1314 | We could define a preorder by taking chain length and breaking ties by the |
---|
1315 | conversion preorder, but this would lead to unexpected behaviour when closing |
---|
1316 | diamonds with an arm length of longer than 1. |
---|
1317 | Consider a set of types `A`, `B1`, `B2`, `C` with the arcs `A->B1`, `B1->B2`, |
---|
1318 | `B2->C`, and `A->C`. |
---|
1319 | If we are comparing conversions from `A` to both `B2` and `C`, we expect the |
---|
1320 | conversion to `B2` to be chosen because it's the more specific type under the |
---|
1321 | conversion preorder, but since its chain length is longer than the conversion |
---|
1322 | to `C`, it loses and `C` is chosen. |
---|
1323 | However, taking the conversion preorder and breaking ties or ambiguities by |
---|
1324 | chain length also doesn't work, because of cases like the following example |
---|
1325 | where the transitivity property is broken and we can't find a global maximum: |
---|
1326 | |
---|
1327 | `X->Y1->Y2`, `X->Z1->Z2->Z3->W`, `X->W` |
---|
1328 | |
---|
1329 | In this set of arcs, if we're comparing conversions from `X` to each of `Y2`, |
---|
1330 | `Z3` and `W`, converting to `Y2` is cheaper than converting to `Z3`, because |
---|
1331 | there are no conversions between `Y2` and `Z3`, and `Y2` has the shorter chain |
---|
1332 | length. |
---|
1333 | Also, comparing conversions from `X` to `Z3` and to `W`, we find that the |
---|
1334 | conversion to `Z3` is cheaper, because `Z3 < W` by the conversion preorder, |
---|
1335 | and so is considered to be the nearer type. |
---|
1336 | By transitivity, then, the conversion from `X` to `Y2` should be cheaper than |
---|
1337 | the conversion from `X` to `W`, but in this case the `X` and `W` are |
---|
1338 | incomparable by the conversion preorder, so the tie is broken by the shorter |
---|
1339 | path from `X` to `W` in favour of `W`, contradicting the transitivity property |
---|
1340 | for this proposed order. |
---|
1341 | |
---|
1342 | Without transitivity, we would need to compare all pairs of conversions, which |
---|
1343 | would be expensive, and possibly not yield a minimal-cost conversion even if |
---|
1344 | all pairs were comparable. |
---|
1345 | In short, this ordering is infeasible, and by extension I believe any ordering |
---|
1346 | composed solely of single-step conversions between types with no further |
---|
1347 | user-supplied information will be insufficiently powerful to express the |
---|
1348 | built-in conversions between C's types. |
---|
1349 | |
---|
1350 | ## Appendix C: Proposed Prelude Changes ## |
---|
1351 | **TODO** Port Glen's "Future Work" page for builtin C conversions. |
---|
1352 | **TODO** Move discussion of zero_t, unit_t here. |
---|
1353 | |
---|
1354 | It may be desirable to have some polymorphic wrapper functions in the prelude |
---|
1355 | which provide consistent default implementations of various operators given a |
---|
1356 | definition of one of them. |
---|
1357 | Naturally, users could still provide a monomorphic overload if they wished to |
---|
1358 | make their own code more efficient than the polymorphic wrapper could be, but |
---|
1359 | this would minimize user effort in the common case where the user cannot write |
---|
1360 | a more efficient function, or is willing to trade some runtime efficiency for |
---|
1361 | developer time. |
---|
1362 | As an example, consider the following polymorphic defaults for `+` and `+=`: |
---|
1363 | |
---|
1364 | forall(otype T | { T ?+?(T, T); }) |
---|
1365 | lvalue T ?+=? (T *a, T b) { |
---|
1366 | return *a = *a + b; |
---|
1367 | } |
---|
1368 | |
---|
1369 | forall(otype T | { lvalue T ?+=? (T*, T) }) |
---|
1370 | T ?+? (T a, T b) { |
---|
1371 | T tmp = a; |
---|
1372 | return tmp += b; |
---|
1373 | } |
---|
1374 | |
---|
1375 | Both of these have a possibly unneccessary copy (the first in copying the |
---|
1376 | result of `*a + b` back into `*a`, the second copying `a` into `tmp`), but in |
---|
1377 | cases where these copies are unavoidable the polymorphic wrappers should be |
---|
1378 | just as performant as the monomorphic equivalents (assuming a compiler |
---|
1379 | sufficiently clever to inline the extra function call), and allow programmers |
---|
1380 | to define a set of related operators with maximal concision. |
---|
1381 | |
---|
1382 | **TODO** Look at what Glen and Richard have already written for this. |
---|
1383 | |
---|
1384 | ## Appendix D: Feasibility of Making void* Conversions Explicit ## |
---|
1385 | C allows implicit conversions between `void*` and other pointer types, as per |
---|
1386 | section 6.3.2.3.1 of the standard. |
---|
1387 | Making these implicit conversions explicit in Cforall would provide |
---|
1388 | significant type-safety benefits, and is precedented in C++. |
---|
1389 | A weaker version of this proposal would be to allow implicit conversions to |
---|
1390 | `void*` (as a sort of "top type" for all pointer types), but to make the |
---|
1391 | unsafe conversion from `void*` back to a concrete pointer type an explicit |
---|
1392 | conversion. |
---|
1393 | However, `int *p = malloc( sizeof(int) );` and friends are hugely common |
---|
1394 | in C code, and rely on the unsafe implicit conversion from the `void*` return |
---|
1395 | type of `malloc` to the `int*` type of the variable - obviously it would be |
---|
1396 | too much of a source-compatibility break to disallow this for C code. |
---|
1397 | We do already need to wrap C code in an `extern "C"` block, though, so it is |
---|
1398 | technically feasible to make the `void*` conversions implicit in C but |
---|
1399 | explicit in Cforall. |
---|
1400 | Also, for calling C code with `void*`-based APIs, pointers-to-dtype are |
---|
1401 | calling-convention compatible with `void*`; we could read `void*` in function |
---|
1402 | signatures as essentially a fresh dtype type variable, e.g: |
---|
1403 | |
---|
1404 | void* malloc( size_t ) |
---|
1405 | => forall(dtype T0) T0* malloc( size_t ) |
---|
1406 | void qsort( void*, size_t, size_t, int (*)( const void*, const void* ) ) |
---|
1407 | => forall(dtype T0, dtype T1, dtype T2) |
---|
1408 | void qsort( T0*, size_t, size_t, int (*)( const T1*, const T2* ) ) |
---|
1409 | |
---|
1410 | This would even allow us to leverage some of Cforall's type safety to write |
---|
1411 | better declarations for legacy C API functions, like the following wrapper for |
---|
1412 | `qsort`: |
---|
1413 | |
---|
1414 | extern "C" { // turns off name-mangling so that this calls the C library |
---|
1415 | // call-compatible type-safe qsort signature |
---|
1416 | forall(dtype T) |
---|
1417 | void qsort( T*, size_t, size_t, int (*)( const T*, const T* ) ); |
---|
1418 | |
---|
1419 | // forbid type-unsafe C signature from resolving |
---|
1420 | void qsort( void*, size_t, size_t, int (*)( const void*, const void* ) ) |
---|
1421 | = delete; |
---|
1422 | } |
---|