947:– that is, those two type expressions are understood to denote the same type. In fact, most theories of equirecursive types go further and essentially specify that any two type expressions with the same "infinite expansion" are equivalent. As a result of these rules, equirecursive types contribute significantly more complexity to a type system than isorecursive types do. Algorithmic problems such as type checking and
977:
1200:
in C, are replaced with their definition at compile time. (Type synonyms are not "real" types; they are just "aliases" for convenience of the programmer.) But if this is attempted with a recursive type, it will loop infinitely because no matter how many times the alias is substituted, it still refers
50:
An important application of recursion in computer science is in defining dynamic data structures such as Lists and Trees. Recursive data structures can dynamically grow to an arbitrarily large size in response to runtime requirements; in contrast, a static array's size requirements must be set at
230:(its children). This definition is elegant and easy to work with abstractly (such as when proving theorems about properties of trees), as it expresses a tree in simple terms: a list of one type, and a pair of two types.
951:
are more difficult for equirecursive types as well. Since direct comparison does not make sense on an equirecursive type, they can be converted into a canonical form in O(n log n) time, which can easily be compared.
185:
This indicates that non-empty list of type E contains a data member of type E, and a reference to another List object for the rest of the list (or a null reference to indicate that this is the end of the list).
247:
and a list of trees (its children). This definition is more compact, but somewhat messier: a tree consists of a pair of one type and a list another, which require disentangling to prove results about.
562:
There are two forms of recursive types: the so-called isorecursive types, and equirecursive types. The two forms differ in how terms of a recursive type are introduced and eliminated.
854:
517:
772:
557:
895:
597:
941:
684:
647:
1220:
Another way to see it is that a level of indirection (the algebraic data type) is required to allow the isorecursive type system to figure out when to
1488:
1859:
1493:
1483:
1478:
1466:
1367:
686:
indicates that all instances of Z are replaced with Y in X) are distinct (and disjoint) types with special term constructs, usually called
1332:
1020:
1315:
987:
1617:
1734:
1539:
1471:
1433:
233:
This mutually recursive definition can be converted to a singly recursive definition by inlining the definition of a forest:
77:
1634:
1564:
1412:
1084:
67:
1889:
1002:
1644:
1512:
955:
Isorecursive types capture the form of self-referential (or mutually referential) type definitions seen in nominal
998:
1822:
1774:
1686:
1664:
1659:
1587:
1453:
1095:
flag is used or it's a record or variant), or
Haskell; so, for example the following Haskell types are illegal:
1696:
1360:
960:
777:
478:
701:
1849:
1764:
1252:
530:
1592:
1448:
1407:
1402:
1285:
43:
for values that may contain other values of the same type. Data of recursive types are usually viewed as
1582:
1557:
205:
254:, the tree and forest data types can be mutually recursively defined as follows, allowing empty trees:
963:. In functional programming languages, isorecursive types (in the guise of datatypes) are common too.
1915:
1384:
1237:
1144:
Instead, they must be wrapped inside an algebraic data type (even if they only has one constructor):
20:
1910:
1854:
1832:
1612:
1604:
1524:
1353:
1242:
871:
573:
55:
1290:
208:, which can be defined mutually recursively in terms of a forest (a list of trees). Symbolically:
1837:
1817:
1769:
1744:
1529:
1498:
523:
represent the Zero and Succ data constructors. Zero takes no arguments (thus represented by the
1724:
1654:
1629:
1443:
1438:
1869:
1754:
1552:
857:
444:
201:
195:
73:
1874:
1739:
1691:
1624:
1338:
956:
1827:
1649:
1639:
1547:
1247:
948:
900:
652:
606:
44:
1904:
1749:
437:
1305:
Revisiting iso-recursive subtyping | Proceedings of the ACM on
Programming Languages
68:
Recursion (computer science) § Recursive data structures (structural recursion)
1706:
1681:
1284:"Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types".
959:
programming languages, and also arise in type-theoretic semantics of objects and
1884:
1879:
1729:
1676:
1503:
1037:, recursion is allowed in type aliases. Thus, the following example is allowed.
695:
433:
251:
1789:
1784:
1701:
1669:
1574:
1517:
1034:
1864:
1842:
1799:
1794:
1461:
1417:
1376:
524:
40:
127:
containing an 'a' (the "head" of the list) and another list (the "tail").
1779:
1304:
520:
1197:
1316:(More) Recursive Type Aliases - Announcing TypeScript 3.7 - TypeScript
1005:. Statements consisting only of original research should be removed.
336:
In
Haskell, the tree and forest data types can be defined similarly:
1088:
440:α may appear in the type T and stands for the entire type itself.
1397:
1349:
123:
This indicates that a list of a's is either an empty list or a
1392:
970:
1345:
130:
Another example is a similar singly linked type in Java:
994:
436:, a recursive type has the general form μα.T where the
1083:
However, recursion is not allowed in type synonyms in
527:) and Succ takes another Nat (thus another element of
903:
874:
780:
704:
655:
609:
576:
533:
481:
54:
Sometimes the term "inductive data type" is used for
1808:
1717:
1603:
1573:
1538:
1426:
1383:
935:
889:
848:
766:
678:
641:
591:
551:
511:
16:Data type that refers to itself in its definition
204:. The most important basic example of this is a
1201:to itself, e.g. "Bad" will grow indefinitely:
1361:
8:
868:Under equirecursive rules, a recursive type
570:With isorecursive types, the recursive type
1368:
1354:
1346:
447:) may be defined by the Haskell datatype:
218:consists of a list of trees, while a tree
1289:
1021:Learn how and when to remove this message
922:
902:
873:
849:{\displaystyle unroll:\mu \alpha .T\to T}
835:
779:
738:
703:
665:
654:
628:
608:
575:
532:
512:{\displaystyle nat=\mu \alpha .1+\alpha }
480:
1264:
767:{\displaystyle roll:T\to \mu \alpha .T}
1271:
443:For example, the natural numbers (see
552:{\displaystyle \mu \alpha .1+\alpha }
58:which are not necessarily recursive.
7:
1196:This is because type synonyms, like
200:Data types can also be defined by
196:Mutual recursion § Data types
14:
975:
930:
907:
843:
820:
814:
749:
746:
723:
698:between them. To be precise:
673:
659:
636:
613:
475:In type theory, we would say:
243:consists of a pair of a value
222:consists of a pair of a value
1:
1434:Arbitrary-precision or bignum
890:{\displaystyle \mu \alpha .T}
592:{\displaystyle \mu \alpha .T}
190:Mutually recursive data types
1001:the claims made and adding
1932:
519:where the two arms of the
193:
65:
1775:Strongly typed identifier
1146:
1097:
1039:
449:
338:
256:
132:
82:
1850:Parametric polymorphism
1331:Harper, Robert (1998),
1253:Node (computer science)
967:Recursive type synonyms
937:
891:
850:
768:
680:
643:
599:and its expansion (or
593:
553:
513:
1334:Datatype Declarations
938:
892:
851:
769:
681:
644:
594:
554:
514:
194:Further information:
21:programming languages
1238:Recursive definition
901:
872:
856:, and these two are
778:
702:
653:
649:(where the notation
607:
574:
531:
479:
211:f: , ..., t] t: v f
56:algebraic data types
1855:Primitive data type
1760:Recursive data type
1613:Algebraic data type
1489:Quadruple precision
1243:Algebraic data type
864:Equirecursive types
37:inductive data type
33:inductively-defined
29:recursively-defined
25:recursive data type
1818:Abstract data type
1499:Extended precision
1458:Reduced precision
986:possibly contains
933:
897:and its unrolling
887:
846:
764:
676:
639:
589:
566:Isorecursive types
549:
509:
72:An example is the
1898:
1897:
1630:Associative array
1494:Octuple precision
1211:(Int, (Int, Bad))
1031:
1030:
1023:
988:original research
936:{\displaystyle T}
858:inverse functions
679:{\displaystyle X}
642:{\displaystyle T}
27:(also known as a
1923:
1870:Type constructor
1755:Opaque data type
1687:Record or Struct
1484:Double precision
1479:Single precision
1370:
1363:
1356:
1347:
1342:
1337:, archived from
1318:
1313:
1307:
1302:
1296:
1295:
1293:
1281:
1275:
1269:
1216:
1212:
1208:
1204:
1192:
1189:
1186:
1183:
1180:
1177:
1174:
1171:
1168:
1165:
1162:
1159:
1156:
1153:
1150:
1140:
1137:
1134:
1131:
1128:
1125:
1122:
1119:
1116:
1113:
1110:
1107:
1104:
1101:
1094:
1079:
1076:
1073:
1070:
1067:
1064:
1061:
1058:
1055:
1052:
1049:
1046:
1043:
1026:
1019:
1015:
1012:
1006:
1003:inline citations
979:
978:
971:
942:
940:
939:
934:
926:
896:
894:
893:
888:
855:
853:
852:
847:
839:
773:
771:
770:
765:
742:
685:
683:
682:
677:
669:
648:
646:
645:
640:
632:
598:
596:
595:
590:
558:
556:
555:
550:
518:
516:
515:
510:
471:
468:
465:
462:
459:
456:
453:
445:Peano arithmetic
423:
420:
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:
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:
202:mutual recursion
181:
178:
175:
172:
169:
166:
163:
160:
157:
154:
151:
148:
145:
142:
139:
136:
119:
116:
113:
110:
107:
104:
101:
98:
95:
92:
89:
86:
1931:
1930:
1926:
1925:
1924:
1922:
1921:
1920:
1901:
1900:
1899:
1894:
1875:Type conversion
1810:
1804:
1740:Enumerated type
1713:
1599:
1593:null-terminated
1569:
1534:
1422:
1379:
1374:
1330:
1327:
1322:
1321:
1314:
1310:
1303:
1299:
1283:
1282:
1278:
1270:
1266:
1261:
1234:
1214:
1210:
1206:
1202:
1194:
1193:
1190:
1187:
1184:
1181:
1178:
1175:
1172:
1169:
1166:
1163:
1160:
1157:
1154:
1151:
1148:
1142:
1141:
1138:
1135:
1132:
1129:
1126:
1123:
1120:
1117:
1114:
1111:
1108:
1105:
1102:
1099:
1092:
1081:
1080:
1077:
1074:
1071:
1068:
1065:
1062:
1059:
1056:
1053:
1050:
1047:
1044:
1041:
1027:
1016:
1010:
1007:
992:
980:
976:
969:
957:object-oriented
899:
898:
870:
869:
866:
776:
775:
700:
699:
694:, that form an
651:
650:
605:
604:
572:
571:
568:
529:
528:
477:
476:
473:
472:
469:
466:
463:
460:
457:
454:
451:
430:
425:
424:
421:
418:
415:
412:
409:
406:
403:
400:
397:
394:
391:
388:
385:
382:
379:
376:
373:
370:
367:
364:
361:
358:
355:
352:
349:
346:
343:
340:
334:
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:
237:
236:t: v , ..., t]
212:
198:
192:
183:
182:
179:
176:
173:
170:
167:
164:
161:
158:
155:
152:
149:
146:
143:
140:
137:
134:
121:
120:
117:
114:
111:
108:
105:
102:
99:
96:
93:
90:
87:
84:
70:
64:
45:directed graphs
17:
12:
11:
5:
1929:
1927:
1919:
1918:
1913:
1903:
1902:
1896:
1895:
1893:
1892:
1887:
1882:
1877:
1872:
1867:
1862:
1857:
1852:
1847:
1846:
1845:
1835:
1830:
1828:Data structure
1825:
1820:
1814:
1812:
1806:
1805:
1803:
1802:
1797:
1792:
1787:
1782:
1777:
1772:
1767:
1762:
1757:
1752:
1747:
1742:
1737:
1732:
1727:
1721:
1719:
1715:
1714:
1712:
1711:
1710:
1709:
1699:
1694:
1689:
1684:
1679:
1674:
1673:
1672:
1662:
1657:
1652:
1647:
1642:
1637:
1632:
1627:
1622:
1621:
1620:
1609:
1607:
1601:
1600:
1598:
1597:
1596:
1595:
1585:
1579:
1577:
1571:
1570:
1568:
1567:
1562:
1561:
1560:
1555:
1544:
1542:
1536:
1535:
1533:
1532:
1527:
1522:
1521:
1520:
1510:
1509:
1508:
1507:
1506:
1496:
1491:
1486:
1481:
1476:
1475:
1474:
1469:
1467:Half precision
1464:
1454:Floating point
1451:
1446:
1441:
1436:
1430:
1428:
1424:
1423:
1421:
1420:
1415:
1410:
1405:
1400:
1395:
1389:
1387:
1381:
1380:
1375:
1373:
1372:
1365:
1358:
1350:
1344:
1343:
1326:
1323:
1320:
1319:
1308:
1297:
1276:
1263:
1262:
1260:
1257:
1256:
1255:
1250:
1248:Inductive type
1245:
1240:
1233:
1230:
1147:
1098:
1040:
1029:
1028:
983:
981:
974:
968:
965:
949:type inference
932:
929:
925:
921:
918:
915:
912:
909:
906:
886:
883:
880:
877:
865:
862:
845:
842:
838:
834:
831:
828:
825:
822:
819:
816:
813:
810:
807:
804:
801:
798:
795:
792:
789:
786:
783:
763:
760:
757:
754:
751:
748:
745:
741:
737:
734:
731:
728:
725:
722:
719:
716:
713:
710:
707:
675:
672:
668:
664:
661:
658:
638:
635:
631:
627:
624:
621:
618:
615:
612:
588:
585:
582:
579:
567:
564:
548:
545:
542:
539:
536:
508:
505:
502:
499:
496:
493:
490:
487:
484:
450:
429:
426:
339:
257:
235:
210:
191:
188:
133:
83:
63:
60:
51:compile time.
15:
13:
10:
9:
6:
4:
3:
2:
1928:
1917:
1914:
1912:
1909:
1908:
1906:
1891:
1888:
1886:
1883:
1881:
1878:
1876:
1873:
1871:
1868:
1866:
1863:
1861:
1858:
1856:
1853:
1851:
1848:
1844:
1841:
1840:
1839:
1836:
1834:
1831:
1829:
1826:
1824:
1821:
1819:
1816:
1815:
1813:
1807:
1801:
1798:
1796:
1793:
1791:
1788:
1786:
1783:
1781:
1778:
1776:
1773:
1771:
1768:
1766:
1763:
1761:
1758:
1756:
1753:
1751:
1750:Function type
1748:
1746:
1743:
1741:
1738:
1736:
1733:
1731:
1728:
1726:
1723:
1722:
1720:
1716:
1708:
1705:
1704:
1703:
1700:
1698:
1695:
1693:
1690:
1688:
1685:
1683:
1680:
1678:
1675:
1671:
1668:
1667:
1666:
1663:
1661:
1658:
1656:
1653:
1651:
1648:
1646:
1643:
1641:
1638:
1636:
1633:
1631:
1628:
1626:
1623:
1619:
1616:
1615:
1614:
1611:
1610:
1608:
1606:
1602:
1594:
1591:
1590:
1589:
1586:
1584:
1581:
1580:
1578:
1576:
1572:
1566:
1563:
1559:
1556:
1554:
1551:
1550:
1549:
1546:
1545:
1543:
1541:
1537:
1531:
1528:
1526:
1523:
1519:
1516:
1515:
1514:
1511:
1505:
1502:
1501:
1500:
1497:
1495:
1492:
1490:
1487:
1485:
1482:
1480:
1477:
1473:
1470:
1468:
1465:
1463:
1460:
1459:
1457:
1456:
1455:
1452:
1450:
1447:
1445:
1442:
1440:
1437:
1435:
1432:
1431:
1429:
1425:
1419:
1416:
1414:
1411:
1409:
1406:
1404:
1401:
1399:
1396:
1394:
1391:
1390:
1388:
1386:
1385:Uninterpreted
1382:
1378:
1371:
1366:
1364:
1359:
1357:
1352:
1351:
1348:
1341:on 1999-10-01
1340:
1336:
1335:
1329:
1328:
1324:
1317:
1312:
1309:
1306:
1301:
1298:
1292:
1291:10.1.1.4.2276
1287:
1280:
1277:
1273:
1268:
1265:
1258:
1254:
1251:
1249:
1246:
1244:
1241:
1239:
1236:
1235:
1231:
1229:
1227:
1223:
1218:
1199:
1145:
1096:
1090:
1086:
1038:
1036:
1025:
1022:
1014:
1004:
1000:
996:
990:
989:
984:This section
982:
973:
972:
966:
964:
962:
958:
953:
950:
946:
927:
923:
919:
916:
913:
910:
904:
884:
881:
878:
875:
863:
861:
859:
840:
836:
832:
829:
826:
823:
817:
811:
808:
805:
802:
799:
796:
793:
790:
787:
784:
781:
761:
758:
755:
752:
743:
739:
735:
732:
729:
726:
720:
717:
714:
711:
708:
705:
697:
693:
689:
670:
666:
662:
656:
633:
629:
625:
622:
619:
616:
610:
602:
586:
583:
580:
577:
565:
563:
560:
546:
543:
540:
537:
534:
526:
522:
506:
503:
500:
497:
494:
491:
488:
485:
482:
448:
446:
441:
439:
438:type variable
435:
427:
337:
255:
253:
248:
246:
242:
234:
231:
229:
226:and a forest
225:
221:
217:
209:
207:
203:
197:
189:
187:
131:
128:
126:
81:
79:
75:
69:
61:
59:
57:
52:
48:
46:
42:
38:
34:
30:
26:
22:
1759:
1655:Intersection
1339:the original
1333:
1311:
1300:
1279:
1267:
1225:
1221:
1219:
1195:
1143:
1082:
1032:
1017:
1011:January 2024
1008:
985:
954:
944:
867:
691:
687:
600:
569:
561:
474:
442:
431:
335:
249:
244:
240:
238:
232:
227:
223:
219:
215:
213:
199:
184:
129:
124:
122:
71:
53:
49:
36:
32:
28:
24:
19:In computer
18:
1916:Type theory
1885:Type theory
1880:Type system
1730:Bottom type
1677:Option type
1618:generalized
1504:Long double
1449:Fixed point
1272:Harper 1998
696:isomorphism
434:type theory
252:Standard ML
1911:Data types
1905:Categories
1790:Empty type
1785:Type class
1735:Collection
1692:Refinement
1670:metaobject
1518:signedness
1377:Data types
1259:References
1207:(Int, Bad)
1035:TypeScript
995:improve it
66:See also:
1865:Subtyping
1860:Interface
1843:metaclass
1795:Unit type
1765:Semaphore
1745:Exception
1650:Inductive
1640:Dependent
1605:Composite
1583:Character
1565:Reference
1462:Minifloat
1418:Bit array
1286:CiteSeerX
1093:-rectypes
999:verifying
928:α
914:α
911:μ
879:α
876:μ
841:α
827:α
824:μ
815:→
806:α
803:μ
756:α
753:μ
750:→
744:α
730:α
727:μ
634:α
620:α
617:μ
601:unrolling
581:α
578:μ
547:α
538:α
535:μ
525:unit type
507:α
498:α
495:μ
214:A forest
125:cons cell
76:type, in
41:data type
1890:Variable
1780:Top type
1645:Equality
1553:physical
1530:Rational
1525:Interval
1472:bfloat16
1232:See also
1198:typedefs
1091:(unless
521:sum type
259:datatype
1833:Generic
1809:Related
1725:Boolean
1682:Product
1558:virtual
1548:Address
1540:Pointer
1513:Integer
1444:Decimal
1439:Complex
1427:Numeric
1325:Sources
1085:Miranda
993:Please
961:classes
239:A tree
78:Haskell
62:Example
39:) is a
1823:Boxing
1811:topics
1770:Stream
1707:tagged
1665:Object
1588:String
1288:
1226:unroll
1051:number
692:unroll
428:Theory
416:Forest
383:Forest
371:Forest
331:forest
328:'a
319:'a
301:forest
298:'a
292:forest
289:'a
283:'a
262:'a
1718:Other
1702:Union
1635:Class
1625:Array
1408:Tryte
1185:->
1136:->
1089:OCaml
945:equal
353:Empty
271:Empty
156:value
135:class
1838:Kind
1800:Void
1660:List
1575:Text
1413:Word
1403:Trit
1398:Byte
1224:and
1222:roll
1188:Fine
1182:Bool
1170:Fine
1167:data
1164:Good
1158:Pair
1152:Good
1149:data
1139:Evil
1133:Bool
1127:Evil
1124:type
1100:type
1072:Tree
1066:tree
1057:Tree
1045:Tree
1042:type
943:are
774:and
690:and
688:roll
467:Succ
461:Zero
452:data
404:Tree
398:Cons
380:data
359:Node
344:Tree
341:data
322:tree
313:Cons
277:Node
265:tree
206:tree
174:next
171:>
165:<
162:List
147:>
141:<
138:List
112:List
103:Cons
88:List
85:data
74:list
23:, a
1697:Set
1393:Bit
1215:...
1203:Bad
1176:Fun
1161:Int
1118:Bad
1112:Int
1103:Bad
1063:let
1033:In
997:by
559:).
470:Nat
455:Nat
432:In
392:Nil
307:Nil
295:and
250:In
97:Nil
35:or
1907::
1228:.
1217:.
1213:→
1209:→
1205:→
1087:,
1078:];
860:.
603:)
541:.1
501:.1
316:of
280:of
80::
47:.
31:,
1369:e
1362:t
1355:v
1294:.
1274:.
1191:)
1179:(
1173:=
1155:=
1130:=
1121:)
1115:,
1109:(
1106:=
1075:=
1069::
1060:;
1054:|
1048:=
1024:)
1018:(
1013:)
1009:(
991:.
931:]
924:/
920:T
917:.
908:[
905:T
885:T
882:.
844:]
837:/
833:T
830:.
821:[
818:T
812:T
809:.
800::
797:l
794:l
791:o
788:r
785:n
782:u
762:T
759:.
747:]
740:/
736:T
733:.
724:[
721:T
718::
715:l
712:l
709:o
706:r
674:]
671:Z
667:/
663:Y
660:[
657:X
637:]
630:/
626:T
623:.
614:[
611:T
587:T
584:.
544:+
504:+
492:=
489:t
486:a
483:n
464:|
458:=
422:)
419:a
413:(
410:)
407:a
401:(
395:|
389:=
386:a
377:)
374:a
368:,
365:a
362:(
356:|
350:=
347:a
325:*
310:|
304:=
286:*
274:|
268:=
245:v
241:t
228:f
224:v
220:t
216:f
180:}
177:;
168:E
159:;
153:E
150:{
144:E
118:)
115:a
109:(
106:a
100:|
94:=
91:a
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.