Commit 5eb9423
Name-based implicits in Effekt (#1380)
This implements implicits similar to
> Daan Leijen, Tim Whiting: Syntactic Implicit Parameters with Static
Overloading
It also implements their use to get source positions in the code.
### Syntax and Intended Behaviour
Putting a `?` in front of a value/block parameter makes it potentially
implicit. If *trailing* implicit parameters are missing, an argument is
generated as follows (e.g.):
- value argument called `$x`: `$x`
- value argument called `sourcePosition`:
`SourcePosition("somefilename.effekt",10,3,10,6)` (corresponding to the
source position of the called function, ~~without~~ with argument list)
- value argument called `callId`: A statically unique integer for *this*
call (unique within an Effekt compiler run).
- value argument of type `(...) => ... at {...}`: instantiated to `box
{...}` with whatever the block argument would be instantiated to.
- block argument called `$foo` of type `(A){B=>C} => D` : `{ (a: A){b: B
=> C} => $foo(a){b} }` (eta-expanded to allow for this call to also
receive implicit arguments)
- block argument with an interface type, called `$x`: `$x`
### Implementation strategy
- In `Namer`,
- find the set of all implicit parameters that any of the overloads
could require (i.e. for all functions of that name, all implicit
parameters) and generate the source for them already.
- then name-resolve them, but collect errors and just store them (for
now)
- in `Typer`,
- instantiate the arguments (i.e., currently, hardcoded copy of the
block literal and corresponding annotations, or just copying them),
refreshing them and typechecking them against their respective
parameters
- only happens if at this point, no errors were reported in this case
(otherwise, aborts)
- annotate the instantiated arguments
- in `ExplicitCapabilities`, actually change the source to pass the
annotated arguments explicitly.
### TODO and limitations
- [x] ~~Check if this works for more than the existing examples (find at
least the worst bugs)~~ The tests should be testing a good part of
possible uses now.
- [x] This *will* cause *Typer* to run indefinitely or stack-overflow if
the search is not terminated by a type/name error. We could try to catch
those cases somehow, but this is nontrivial (and will reject valid
programs).
- Opinions?
- The recursion is ~~quite indirect (and not actual recursion) in typer,
and~~ (we can check for recursive uses when checking implicit arguments
after instantiating them - this is separate now anyway) at a point where
we don't necessarily have the concrete types (due to unification), so
checking for "decreasing type size" or similar is potentially hard.
- Now aborts if, at the same name, we have 10 levels where the expected
type does not get smaller.
- [x] Syntax bikeshedding
- [ ] If merging this, we might want to change #1381 / #1123 s.t. they
provide only the definitions for base and recursive cases (not for all
types used etc).
---------
Co-authored-by: Jonathan Immanuel Brachthäuser <jonathan.brachthaeuser@uni-tuebingen.de>1 parent 7e5beee commit 5eb9423
60 files changed
Lines changed: 1167 additions & 93 deletions
File tree
- examples
- neg/name-based-implicits
- pos/name-based-implicits
- tour
- libraries/common
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
130 | 130 | | |
131 | 131 | | |
132 | 132 | | |
| 133 | + | |
133 | 134 | | |
134 | 135 | | |
135 | 136 | | |
| |||
472 | 473 | | |
473 | 474 | | |
474 | 475 | | |
| 476 | + | |
475 | 477 | | |
476 | 478 | | |
477 | 479 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
7 | 7 | | |
8 | 8 | | |
9 | 9 | | |
10 | | - | |
| 10 | + | |
11 | 11 | | |
12 | 12 | | |
13 | 13 | | |
| 14 | + | |
14 | 15 | | |
15 | 16 | | |
16 | 17 | | |
17 | 18 | | |
| 19 | + | |
18 | 20 | | |
19 | 21 | | |
20 | 22 | | |
| |||
337 | 339 | | |
338 | 340 | | |
339 | 341 | | |
| 342 | + | |
340 | 343 | | |
341 | 344 | | |
342 | 345 | | |
| |||
347 | 350 | | |
348 | 351 | | |
349 | 352 | | |
| 353 | + | |
350 | 354 | | |
351 | 355 | | |
352 | 356 | | |
| |||
364 | 368 | | |
365 | 369 | | |
366 | 370 | | |
| 371 | + | |
367 | 372 | | |
368 | 373 | | |
369 | 374 | | |
| |||
445 | 450 | | |
446 | 451 | | |
447 | 452 | | |
| 453 | + | |
| 454 | + | |
| 455 | + | |
| 456 | + | |
| 457 | + | |
| 458 | + | |
| 459 | + | |
| 460 | + | |
| 461 | + | |
| 462 | + | |
| 463 | + | |
| 464 | + | |
| 465 | + | |
| 466 | + | |
| 467 | + | |
| 468 | + | |
| 469 | + | |
| 470 | + | |
| 471 | + | |
| 472 | + | |
| 473 | + | |
| 474 | + | |
| 475 | + | |
| 476 | + | |
| 477 | + | |
| 478 | + | |
| 479 | + | |
| 480 | + | |
| 481 | + | |
| 482 | + | |
| 483 | + | |
| 484 | + | |
| 485 | + | |
| 486 | + | |
| 487 | + | |
| 488 | + | |
| 489 | + | |
| 490 | + | |
| 491 | + | |
| 492 | + | |
| 493 | + | |
448 | 494 | | |
449 | 495 | | |
450 | 496 | | |
| |||
491 | 537 | | |
492 | 538 | | |
493 | 539 | | |
494 | | - | |
| 540 | + | |
495 | 541 | | |
496 | 542 | | |
497 | 543 | | |
498 | 544 | | |
499 | 545 | | |
500 | 546 | | |
501 | 547 | | |
| 548 | + | |
| 549 | + | |
502 | 550 | | |
503 | 551 | | |
504 | 552 | | |
| |||
551 | 599 | | |
552 | 600 | | |
553 | 601 | | |
| 602 | + | |
554 | 603 | | |
555 | 604 | | |
556 | 605 | | |
557 | 606 | | |
558 | 607 | | |
559 | 608 | | |
| 609 | + | |
560 | 610 | | |
561 | 611 | | |
562 | 612 | | |
563 | 613 | | |
564 | 614 | | |
565 | 615 | | |
566 | | - | |
| 616 | + | |
567 | 617 | | |
568 | 618 | | |
569 | 619 | | |
| |||
666 | 716 | | |
667 | 717 | | |
668 | 718 | | |
669 | | - | |
| 719 | + | |
670 | 720 | | |
671 | 721 | | |
672 | 722 | | |
673 | 723 | | |
674 | 724 | | |
675 | | - | |
| 725 | + | |
676 | 726 | | |
677 | 727 | | |
678 | 728 | | |
679 | 729 | | |
680 | 730 | | |
681 | | - | |
| 731 | + | |
682 | 732 | | |
683 | 733 | | |
684 | 734 | | |
| |||
719 | 769 | | |
720 | 770 | | |
721 | 771 | | |
722 | | - | |
| 772 | + | |
723 | 773 | | |
724 | 774 | | |
725 | 775 | | |
| |||
1081 | 1131 | | |
1082 | 1132 | | |
1083 | 1133 | | |
1084 | | - | |
| 1134 | + | |
| 1135 | + | |
| 1136 | + | |
| 1137 | + | |
| 1138 | + | |
1085 | 1139 | | |
1086 | 1140 | | |
1087 | 1141 | | |
| |||
1092 | 1146 | | |
1093 | 1147 | | |
1094 | 1148 | | |
1095 | | - | |
| 1149 | + | |
| 1150 | + | |
| 1151 | + | |
| 1152 | + | |
| 1153 | + | |
1096 | 1154 | | |
1097 | 1155 | | |
1098 | 1156 | | |
| |||
1116 | 1174 | | |
1117 | 1175 | | |
1118 | 1176 | | |
1119 | | - | |
| 1177 | + | |
1120 | 1178 | | |
1121 | 1179 | | |
1122 | 1180 | | |
| |||
1170 | 1228 | | |
1171 | 1229 | | |
1172 | 1230 | | |
1173 | | - | |
| 1231 | + | |
| 1232 | + | |
1174 | 1233 | | |
1175 | 1234 | | |
1176 | 1235 | | |
| |||
1184 | 1243 | | |
1185 | 1244 | | |
1186 | 1245 | | |
1187 | | - | |
| 1246 | + | |
| 1247 | + | |
1188 | 1248 | | |
1189 | 1249 | | |
1190 | 1250 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
195 | 195 | | |
196 | 196 | | |
197 | 197 | | |
| 198 | + | |
| 199 | + | |
| 200 | + | |
198 | 201 | | |
199 | 202 | | |
200 | 203 | | |
| |||
331 | 334 | | |
332 | 335 | | |
333 | 336 | | |
334 | | - | |
335 | | - | |
| 337 | + | |
| 338 | + | |
336 | 339 | | |
337 | 340 | | |
338 | 341 | | |
| |||
345 | 348 | | |
346 | 349 | | |
347 | 350 | | |
348 | | - | |
| 351 | + | |
349 | 352 | | |
350 | 353 | | |
351 | 354 | | |
| |||
931 | 934 | | |
932 | 935 | | |
933 | 936 | | |
934 | | - | |
| 937 | + | |
935 | 938 | | |
936 | 939 | | |
937 | 940 | | |
| |||
1284 | 1287 | | |
1285 | 1288 | | |
1286 | 1289 | | |
1287 | | - | |
| 1290 | + | |
1288 | 1291 | | |
1289 | 1292 | | |
1290 | 1293 | | |
| |||
1654 | 1657 | | |
1655 | 1658 | | |
1656 | 1659 | | |
1657 | | - | |
| 1660 | + | |
1658 | 1661 | | |
1659 | 1662 | | |
1660 | 1663 | | |
| |||
1688 | 1691 | | |
1689 | 1692 | | |
1690 | 1693 | | |
1691 | | - | |
| 1694 | + | |
| 1695 | + | |
1692 | 1696 | | |
1693 | 1697 | | |
1694 | 1698 | | |
1695 | | - | |
| 1699 | + | |
| 1700 | + | |
1696 | 1701 | | |
1697 | 1702 | | |
1698 | 1703 | | |
| |||
1712 | 1717 | | |
1713 | 1718 | | |
1714 | 1719 | | |
1715 | | - | |
| 1720 | + | |
| 1721 | + | |
1716 | 1722 | | |
1717 | 1723 | | |
1718 | 1724 | | |
1719 | | - | |
| 1725 | + | |
| 1726 | + | |
1720 | 1727 | | |
1721 | 1728 | | |
1722 | 1729 | | |
| |||
0 commit comments