Knowledge

Flow-sensitive typing

Source 📝

978:). My goal was to ensure that all use of references should be absolutely safe, with checking performed automatically by the compiler. But I couldn't resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years. 216:, a type of an expression is determined by the types of the sub-expressions that compose it. However, in flow-sensitive typing, an expression's type may be updated to a more specific type if it follows an operation that validates its type. Validating operations can include type predicates, imperative updates, and control flow. 661:
and making up for terser code, easier to read and modify. It achieves this is in a different way, it allows to match the type of a structure, extract data out of it at the same time by declaring new variable. As such, it reduces the ceremony around type casting and value extraction. Pattern matching
590:
From a Programming Languages perspective, it's reasonable to say that flow-sensitive typing is the feature that finally made it possible to build usable type-safe programming languages with union types and without rampant dynamic checking. Until this point, attempts to add this feature to languages
925:
In a statically typed language, the advantage of pattern matching over flow-sensitive typing is that the type of a variable always stays the same: it does not change depending on control flow. When writing down the pattern to be matched, a new variable is declared that will have the new type.
614:
Typed JavaScript observed that in "scripting" languages, flow-typing depends on more than conditional predicates; it also depends on state and control flow. This style has since been adopted in languages like
974:
I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object oriented language (
591:
such as Scheme generally resulted in intractably large type representations. One example of a system with limited support for union types is Wright and Cartwright's "Soft Scheme."
1206: 851:// try to type cast "Node" into "MulNode", and create the variables "left" and "right" of type "Node". 788:// try to type cast "Node" into "AddNode", and create the variables "left" and "right" of type "Node". 1161: 572:
It can also help language implementers provide implementations that execute dynamic languages faster by predicting the type of objects statically.
1064: 1450: 1821: 1455: 1184: 1138: 1445: 1440: 168: 746:// try to type cast "Node" into "NegNode", and create the variable "n" of type "Node". 713:// try to type cast "Node" into "IntNode", and create the variable "i" of type "int". 58: 1428: 1329: 969: 607:), is also based on occurrence typing. Shortly after Typed Scheme, David J. Pearce independently reinvented flow-typing in 1091: 943: 1606: 1579: 1117: 1696: 1501: 1433: 1395: 854:// If that works, then return the multiplication of evaluating the "left" and "right" nodes 639: 643: 616: 608: 604: 600: 432: 230: 202: 1268: 1596: 1526: 1374: 1851: 1486: 791:// If that works, then return the addition of evaluating the "left" and "right" nodes 182: 1474: 161: 1882: 1784: 1736: 1648: 1626: 1621: 1549: 1415: 1369: 132: 1658: 1322: 1068: 1811: 1726: 914:// no "default" because the compiler knows all the possible cases have been enumerated 1554: 1410: 1364: 1045: 76: 38: 54: 1872: 1544: 1519: 154: 1887: 1346: 663: 8: 1877: 1816: 1794: 1721: 1574: 1566: 1315: 1224: 603:, was the first type system with this feature. Its successor, Typed Racket (a dialect of 72: 638:, that have a limited form of this feature that only applies to nullable types, such as 1799: 1779: 1731: 1706: 1491: 1460: 1246: 1686: 1616: 1591: 1405: 1400: 117: 1831: 1716: 1514: 1003: 991: 654: 1836: 1701: 1653: 1586: 1027: 554: 137: 127: 63: 666:
because all the cases can be enumerated and statically checked by the compiler.
1789: 1611: 1601: 1509: 749:// If that works, then return the negation of evaluating the "n" node 635: 558: 550: 112: 102: 67: 1095: 1866: 1711: 238:// Object? means the variable "name" is of type Object or else null 213: 122: 97: 1668: 1643: 631: 584: 580: 206: 142: 1007: 1846: 1841: 1691: 1638: 1465: 576: 562: 198: 81: 33: 19: 549:
This technique coupled with type inference reduces the need for writing
1751: 1746: 1663: 1631: 1536: 1479: 1139:"Ceylon - Quick introduction - Typesafe null and flow-sensitive typing" 965: 620: 1182: 1826: 1804: 1761: 1756: 1423: 1379: 1338: 658: 566: 1741: 624: 975: 657:
reaches the same goals as flow-sensitive typing, namely reducing
423:
Hello, world! Hello, object 1! Hello, John Doe! String.size is 8
1287: 1183:
Avik Chaudhuri; Basil Hosmer; Gabriel Levi (18 November 2014).
1162:"TypeScript 1.4 sneak peek: union types, type guards, and more" 1307: 1285: 587:—the null reference inventor—as "the billion dollar mistake" 1028:"The Design and Implementation of Typed Scheme | POPL, 2008" 476:// Since the type cast did not fail, `obj` must be a String! 301:// and it is possible to call String methods on the variable 1359: 1354: 944:"The Inconvenient Truth About Dynamic vs. Static Typing" 716:// If that works, then return the value of "i" 569:
and makes for terser code, easier to read and modify.
996:
ACM Transactions on Programming Languages and Systems
340:// "name" now has type Object in this block 286:// "name" now has type String in this block 1118:"Typing Local Control and State Using Flow Analysis" 1286:Gavin Bierman and Brian Goetz (19 September 2023). 990:Wright, Andrew; Cartwright, Robert (1 Jan 1997). 1864: 1185:"Flow, a new static type checker for JavaScript" 989: 1089: 1062: 630:There are also a few languages that don't have 1159: 1323: 970:"Null References: The Billion Dollar Mistake" 464:// A type cast fails if `obj` is not a String 162: 1330: 1316: 964: 941: 169: 155: 992:"A practical soft type system for scheme" 662:works best when used in conjunction with 310:" String.size is ``name.size``" 1865: 1288:"JEP 441: Pattern Matching for switch" 1207:"Design with nullable reference types" 1311: 1063:David J. Pearce (22 September 2010). 1160:Ryan Cavanaugh (18 November 2014). 1065:"On Flow-Sensitive Types in Whiley" 349:"Hello, object ``name``!" 13: 594: 14: 1899: 1090:David J. Pearce (8 April 2012). 669:See this example mock for Java: 599:Typed Scheme, a type system for 579:and can prevent problems due to 1279: 1261: 1239: 1217: 1199: 1176: 1153: 942:Lukas Eder (11 December 2014). 649: 233:which illustrates the concept: 205:depends on its position in the 1337: 1131: 1110: 1083: 1056: 1038: 1020: 983: 958: 935: 1: 1396:Arbitrary-precision or bignum 929: 229:See the following example in 1094:. whiley.org. Archived from 1067:. whiley.org. Archived from 512:' is a string of length 295:"Hello, ``name``!" 7: 553:for all variables or to do 544: 219: 183:programming language theory 10: 1904: 1164:. blogs.msdn.microsoft.com 214:statically typed languages 1770: 1737:Strongly typed identifier 1679: 1565: 1535: 1500: 1388: 1345: 1269:"The Lobster Type System" 426: 370:"Hello, world!" 224: 671: 437: 235: 1812:Parametric polymorphism 1247:"Type Checks and Casts" 1092:"Whiley - Flow Typing" 575:Finally, it increases 39:Strong vs. weak typing 1046:"5 Occurrence Typing" 1008:10.1145/239912.239917 201:where the type of an 187:flow-sensitive typing 1050:docs.racket-lang.org 664:algebraic data types 557:, like is seen with 431:See this example in 412:"John Doe" 1817:Primitive data type 1722:Recursive data type 1575:Algebraic data type 1451:Quadruple precision 1273:aardappel.github.io 1187:. code.facebook.com 420:and which outputs: 1780:Abstract data type 1461:Extended precision 1420:Reduced precision 1211:docs.microsoft.com 536:"Mooooo" 1860: 1859: 1592:Associative array 1456:Octuple precision 1141:. ceylon-lang.org 559:dynamic languages 195:occurrence typing 179: 178: 1895: 1883:Program analysis 1832:Type constructor 1717:Opaque data type 1649:Record or Struct 1446:Double precision 1441:Single precision 1332: 1325: 1318: 1309: 1308: 1303: 1302: 1300: 1298: 1283: 1277: 1276: 1265: 1259: 1258: 1256: 1254: 1249:. kotlinlang.org 1243: 1237: 1236: 1234: 1232: 1227:. kotlinlang.org 1221: 1215: 1214: 1203: 1197: 1196: 1194: 1192: 1180: 1174: 1173: 1171: 1169: 1157: 1151: 1150: 1148: 1146: 1135: 1129: 1128: 1126: 1124: 1114: 1108: 1107: 1105: 1103: 1098:on 11 March 2016 1087: 1081: 1080: 1078: 1076: 1071:on 11 March 2016 1060: 1054: 1053: 1042: 1036: 1035: 1024: 1018: 1017: 1015: 1014: 987: 981: 980: 962: 956: 955: 953: 951: 939: 921: 918: 915: 912: 909: 906: 903: 900: 897: 894: 891: 888: 885: 882: 879: 876: 873: 870: 867: 864: 861: 858: 855: 852: 849: 846: 843: 840: 837: 834: 831: 828: 825: 822: 819: 816: 813: 810: 807: 804: 801: 798: 795: 792: 789: 786: 783: 780: 777: 774: 771: 768: 765: 762: 759: 756: 753: 750: 747: 744: 741: 738: 735: 732: 729: 726: 723: 720: 717: 714: 711: 708: 705: 702: 699: 696: 693: 690: 687: 684: 681: 678: 675: 655:Pattern matching 551:type annotations 540: 537: 534: 531: 528: 525: 522: 519: 516: 513: 510: 507: 504: 501: 498: 495: 492: 489: 486: 483: 480: 477: 474: 471: 468: 465: 462: 459: 456: 453: 450: 447: 444: 441: 416: 413: 410: 407: 404: 401: 398: 395: 392: 389: 386: 383: 380: 377: 374: 371: 368: 365: 362: 359: 356: 353: 350: 347: 344: 341: 338: 335: 332: 329: 326: 323: 320: 317: 314: 311: 308: 305: 302: 299: 296: 293: 290: 287: 284: 281: 278: 275: 272: 269: 266: 263: 260: 257: 254: 251: 248: 245: 242: 239: 171: 164: 157: 90:Minor categories 47:Major categories 26:General concepts 16: 15: 1903: 1902: 1898: 1897: 1896: 1894: 1893: 1892: 1863: 1862: 1861: 1856: 1837:Type conversion 1772: 1766: 1702:Enumerated type 1675: 1561: 1555:null-terminated 1531: 1496: 1384: 1341: 1336: 1306: 1296: 1294: 1284: 1280: 1267: 1266: 1262: 1252: 1250: 1245: 1244: 1240: 1230: 1228: 1223: 1222: 1218: 1205: 1204: 1200: 1190: 1188: 1181: 1177: 1167: 1165: 1158: 1154: 1144: 1142: 1137: 1136: 1132: 1122: 1120: 1116: 1115: 1111: 1101: 1099: 1088: 1084: 1074: 1072: 1061: 1057: 1044: 1043: 1039: 1026: 1025: 1021: 1012: 1010: 988: 984: 963: 959: 949: 947: 946:. blog.jooq.org 940: 936: 932: 923: 922: 919: 916: 913: 910: 907: 904: 901: 898: 895: 892: 889: 886: 883: 880: 877: 874: 871: 868: 865: 862: 859: 856: 853: 850: 847: 844: 841: 838: 835: 832: 829: 826: 823: 820: 817: 814: 811: 808: 805: 802: 799: 796: 793: 790: 787: 784: 781: 778: 775: 772: 769: 766: 763: 760: 757: 754: 751: 748: 745: 742: 739: 736: 733: 730: 727: 724: 721: 718: 715: 712: 709: 706: 703: 700: 697: 694: 691: 688: 685: 682: 679: 676: 673: 652: 646:, and Lobster. 597: 595:Implementations 547: 542: 541: 538: 535: 532: 529: 526: 523: 520: 517: 514: 511: 508: 505: 502: 499: 496: 493: 490: 487: 484: 481: 478: 475: 472: 469: 466: 463: 460: 457: 454: 451: 448: 445: 442: 439: 429: 424: 418: 417: 414: 411: 408: 405: 402: 399: 396: 393: 390: 387: 384: 381: 378: 375: 372: 369: 366: 363: 360: 357: 354: 351: 348: 345: 342: 339: 336: 333: 330: 327: 324: 321: 318: 315: 312: 309: 306: 303: 300: 297: 294: 291: 288: 285: 282: 279: 276: 273: 270: 267: 264: 261: 258: 255: 252: 249: 246: 243: 240: 237: 227: 222: 175: 12: 11: 5: 1901: 1891: 1890: 1885: 1880: 1875: 1858: 1857: 1855: 1854: 1849: 1844: 1839: 1834: 1829: 1824: 1819: 1814: 1809: 1808: 1807: 1797: 1792: 1790:Data structure 1787: 1782: 1776: 1774: 1768: 1767: 1765: 1764: 1759: 1754: 1749: 1744: 1739: 1734: 1729: 1724: 1719: 1714: 1709: 1704: 1699: 1694: 1689: 1683: 1681: 1677: 1676: 1674: 1673: 1672: 1671: 1661: 1656: 1651: 1646: 1641: 1636: 1635: 1634: 1624: 1619: 1614: 1609: 1604: 1599: 1594: 1589: 1584: 1583: 1582: 1571: 1569: 1563: 1562: 1560: 1559: 1558: 1557: 1547: 1541: 1539: 1533: 1532: 1530: 1529: 1524: 1523: 1522: 1517: 1506: 1504: 1498: 1497: 1495: 1494: 1489: 1484: 1483: 1482: 1472: 1471: 1470: 1469: 1468: 1458: 1453: 1448: 1443: 1438: 1437: 1436: 1431: 1429:Half precision 1426: 1416:Floating point 1413: 1408: 1403: 1398: 1392: 1390: 1386: 1385: 1383: 1382: 1377: 1372: 1367: 1362: 1357: 1351: 1349: 1343: 1342: 1335: 1334: 1327: 1320: 1312: 1305: 1304: 1278: 1260: 1238: 1216: 1198: 1175: 1152: 1130: 1109: 1082: 1055: 1037: 1019: 1002:(1): 87--152. 982: 968:(2009-08-25). 957: 933: 931: 928: 672: 651: 648: 636:nullable types 596: 593: 546: 543: 438: 428: 425: 422: 236: 226: 223: 221: 218: 177: 176: 174: 173: 166: 159: 151: 148: 147: 146: 145: 140: 135: 130: 125: 120: 115: 110: 108:Flow-sensitive 105: 100: 92: 91: 87: 86: 85: 84: 79: 70: 61: 49: 48: 44: 43: 42: 41: 36: 28: 27: 23: 22: 9: 6: 4: 3: 2: 1900: 1889: 1886: 1884: 1881: 1879: 1876: 1874: 1871: 1870: 1868: 1853: 1850: 1848: 1845: 1843: 1840: 1838: 1835: 1833: 1830: 1828: 1825: 1823: 1820: 1818: 1815: 1813: 1810: 1806: 1803: 1802: 1801: 1798: 1796: 1793: 1791: 1788: 1786: 1783: 1781: 1778: 1777: 1775: 1769: 1763: 1760: 1758: 1755: 1753: 1750: 1748: 1745: 1743: 1740: 1738: 1735: 1733: 1730: 1728: 1725: 1723: 1720: 1718: 1715: 1713: 1712:Function type 1710: 1708: 1705: 1703: 1700: 1698: 1695: 1693: 1690: 1688: 1685: 1684: 1682: 1678: 1670: 1667: 1666: 1665: 1662: 1660: 1657: 1655: 1652: 1650: 1647: 1645: 1642: 1640: 1637: 1633: 1630: 1629: 1628: 1625: 1623: 1620: 1618: 1615: 1613: 1610: 1608: 1605: 1603: 1600: 1598: 1595: 1593: 1590: 1588: 1585: 1581: 1578: 1577: 1576: 1573: 1572: 1570: 1568: 1564: 1556: 1553: 1552: 1551: 1548: 1546: 1543: 1542: 1540: 1538: 1534: 1528: 1525: 1521: 1518: 1516: 1513: 1512: 1511: 1508: 1507: 1505: 1503: 1499: 1493: 1490: 1488: 1485: 1481: 1478: 1477: 1476: 1473: 1467: 1464: 1463: 1462: 1459: 1457: 1454: 1452: 1449: 1447: 1444: 1442: 1439: 1435: 1432: 1430: 1427: 1425: 1422: 1421: 1419: 1418: 1417: 1414: 1412: 1409: 1407: 1404: 1402: 1399: 1397: 1394: 1393: 1391: 1387: 1381: 1378: 1376: 1373: 1371: 1368: 1366: 1363: 1361: 1358: 1356: 1353: 1352: 1350: 1348: 1347:Uninterpreted 1344: 1340: 1333: 1328: 1326: 1321: 1319: 1314: 1313: 1310: 1293: 1289: 1282: 1274: 1270: 1264: 1248: 1242: 1226: 1225:"Null Safety" 1220: 1212: 1208: 1202: 1186: 1179: 1163: 1156: 1140: 1134: 1119: 1113: 1097: 1093: 1086: 1070: 1066: 1059: 1051: 1047: 1041: 1033: 1029: 1023: 1009: 1005: 1001: 997: 993: 986: 979: 977: 972:. InfoQ.com. 971: 967: 961: 945: 938: 934: 927: 670: 667: 665: 660: 656: 647: 645: 641: 637: 633: 628: 626: 622: 618: 612: 610: 606: 602: 592: 588: 586: 583:, labeled by 582: 581:null pointers 578: 573: 570: 568: 565:. It reduces 564: 560: 556: 552: 436: 434: 421: 234: 232: 217: 215: 210: 208: 204: 200: 196: 192: 189:(also called 188: 184: 172: 167: 165: 160: 158: 153: 152: 150: 149: 144: 141: 139: 136: 134: 133:Substructural 131: 129: 126: 124: 121: 119: 116: 114: 111: 109: 106: 104: 101: 99: 96: 95: 94: 93: 89: 88: 83: 80: 78: 74: 71: 69: 65: 62: 60: 56: 53: 52: 51: 50: 46: 45: 40: 37: 35: 32: 31: 30: 29: 25: 24: 21: 18: 17: 1873:Type systems 1617:Intersection 1295:. Retrieved 1291: 1281: 1272: 1263: 1251:. Retrieved 1241: 1229:. Retrieved 1219: 1210: 1201: 1189:. Retrieved 1178: 1166:. Retrieved 1155: 1143:. Retrieved 1133: 1121:. Retrieved 1112: 1100:. Retrieved 1096:the original 1085: 1073:. Retrieved 1069:the original 1058: 1049: 1040: 1031: 1022: 1011:. Retrieved 999: 995: 985: 973: 960: 948:. Retrieved 937: 924: 668: 653: 650:Alternatives 634:but do have 629: 613: 598: 589: 585:C.A.R. Hoare 574: 571: 555:type casting 548: 430: 419: 228: 211: 207:control flow 194: 190: 186: 180: 118:Intersection 107: 20:Type systems 1888:Type theory 1847:Type theory 1842:Type system 1692:Bottom type 1639:Option type 1580:generalized 1466:Long double 1411:Fixed point 1297:14 November 1292:openjdk.org 1123:14 November 632:union types 577:type safety 563:duck typing 503:"' 199:type system 191:flow typing 82:Duck typing 34:Type safety 1878:Data types 1867:Categories 1752:Empty type 1747:Type class 1697:Collection 1654:Refinement 1632:metaobject 1480:signedness 1339:Data types 1032:dl.acm.org 1013:2024-05-04 966:Tony Hoare 930:References 621:TypeScript 203:expression 128:Refinement 77:structural 1827:Subtyping 1822:Interface 1805:metaclass 1757:Unit type 1727:Semaphore 1707:Exception 1612:Inductive 1602:Dependent 1567:Composite 1545:Character 1527:Reference 1424:Minifloat 1380:Bit array 659:verbosity 567:verbosity 561:that use 103:Dependent 1852:Variable 1742:Top type 1607:Equality 1515:physical 1492:Rational 1487:Interval 1434:bfloat16 1253:11 March 1231:11 March 1191:11 March 1168:11 March 1145:11 March 1102:11 March 1075:11 March 950:11 March 625:Facebook 545:Benefits 220:Examples 98:Abstract 68:inferred 64:Manifest 1795:Generic 1771:Related 1687:Boolean 1644:Product 1520:virtual 1510:Address 1502:Pointer 1475:Integer 1406:Decimal 1401:Complex 1389:Numeric 976:ALGOL W 860:MulNode 797:AddNode 755:NegNode 722:IntNode 497:println 197:) is a 143:Session 113:Gradual 73:Nominal 59:dynamic 1785:Boxing 1773:topics 1732:Stream 1669:tagged 1627:Object 1550:String 698:switch 695:return 644:Kotlin 627:Flow. 617:Ceylon 609:Whiley 605:Racket 601:Scheme 521:" 494:length 473:String 433:Kotlin 427:Kotlin 328:exists 274:String 250:Object 231:Ceylon 225:Ceylon 138:Unique 123:Latent 55:Static 1680:Other 1664:Union 1597:Class 1587:Array 1370:Tryte 908:right 884:-> 878:right 845:right 821:-> 815:right 770:-> 737:-> 530:hello 443:hello 406:hello 394:hello 382:hello 364:print 343:print 304:print 289:print 244:hello 1800:Kind 1762:Void 1622:List 1537:Text 1375:Word 1365:Trit 1360:Byte 1299:2023 1255:2016 1233:2016 1193:2016 1170:2016 1147:2016 1125:2016 1104:2016 1077:2016 952:2016 902:eval 893:left 887:eval 875:Node 869:left 866:Node 857:case 839:eval 830:left 824:eval 812:Node 806:left 803:Node 794:case 776:eval 761:Node 752:case 719:case 683:Node 677:eval 623:and 388:null 358:else 331:name 319:else 277:name 256:name 241:void 75:vs. 66:vs. 57:vs. 1659:Set 1355:Bit 1004:doi 728:int 674:int 509:obj 488:obj 479:val 467:obj 455:Any 449:obj 440:fun 212:In 193:or 181:In 1869:: 1290:. 1271:. 1209:. 1048:. 1030:. 1000:19 998:. 994:. 917:}; 911:); 848:); 785:); 642:, 640:C# 619:, 611:. 515:$ 506:$ 470:as 435:: 415:); 403:); 391:); 373:); 352:); 322:if 313:); 298:); 271:is 265:if 209:. 185:, 1331:e 1324:t 1317:v 1301:. 1275:. 1257:. 1235:. 1213:. 1195:. 1172:. 1149:. 1127:. 1106:. 1079:. 1052:. 1034:. 1016:. 1006:: 954:. 920:} 905:( 899:* 896:) 890:( 881:) 872:, 863:( 842:( 836:+ 833:) 827:( 818:) 809:, 800:( 782:n 779:( 773:- 767:) 764:n 758:( 743:; 740:i 734:) 731:i 725:( 710:{ 707:) 704:n 701:( 692:{ 689:) 686:n 680:( 539:) 533:( 527:} 524:) 518:l 500:( 491:. 485:= 482:l 461:{ 458:) 452:: 446:( 409:( 400:1 397:( 385:( 379:} 376:} 367:( 361:{ 355:} 346:( 337:{ 334:) 325:( 316:} 307:( 292:( 283:{ 280:) 268:( 262:{ 259:) 253:? 247:( 170:e 163:t 156:v

Index

Type systems
Type safety
Strong vs. weak typing
Static
dynamic
Manifest
inferred
Nominal
structural
Duck typing
Abstract
Dependent
Flow-sensitive
Gradual
Intersection
Latent
Refinement
Substructural
Unique
Session
v
t
e
programming language theory
type system
expression
control flow
statically typed languages
Ceylon
Kotlin

Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.