diff --git a/EHC/figs/conflict-lattice.fig b/EHC/figs/conflict-lattice.fig new file mode 100644 index 000000000..67317e062 --- /dev/null +++ b/EHC/figs/conflict-lattice.fig @@ -0,0 +1,32 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1425 2175 1050 2925 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1050 3225 2025 3975 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3525 3225 2400 3975 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3225 2175 3600 2925 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1650 2025 3075 2025 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1200 3075 3450 3075 +4 0 0 50 -1 0 12 0.0000 4 135 90 3150 2100 1\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 1500 2100 0\001 +4 0 0 50 -1 0 12 0.0000 4 135 150 900 3150 1-\001 +4 0 0 50 -1 0 12 0.0000 4 135 195 3600 3150 1+\001 +4 0 0 50 -1 0 12 0.0000 4 75 90 2175 4200 *\001 diff --git a/EHC/figs/specific-lattice.fig b/EHC/figs/specific-lattice.fig new file mode 100644 index 000000000..76d78160c --- /dev/null +++ b/EHC/figs/specific-lattice.fig @@ -0,0 +1,26 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2250 3150 2625 2775 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2250 3825 2250 3525 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3300 3150 2925 2775 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3300 3825 3300 3525 +4 0 0 50 -1 0 12 0.0000 4 135 90 3300 4050 1\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 2250 4050 0\001 +4 0 0 50 -1 0 12 0.0000 4 135 195 2175 3450 1+\001 +4 0 0 50 -1 0 12 0.0000 4 135 150 3225 3450 1-\001 +4 0 0 50 -1 0 12 0.0000 4 75 90 2775 2850 *\001 diff --git a/EHC/figs/unq-graph.fig b/EHC/figs/unq-graph.fig index b2c5cda6a..a88def3a2 100644 --- a/EHC/figs/unq-graph.fig +++ b/EHC/figs/unq-graph.fig @@ -15,6 +15,9 @@ Single 1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 300 300 1650 1275 1950 1275 1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 1275 300 300 3750 1275 4050 1275 1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 300 300 3750 3450 4050 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 225 225 1650 1275 1875 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 225 225 2250 2325 2475 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 225 225 3750 3450 3975 3450 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 0 0 1.00 60.00 120.00 1950 1275 3450 1275 @@ -29,14 +32,20 @@ Single 3825 3150 3825 1575 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 0 0 1.00 60.00 120.00 - 2325 2625 2925 3000 + 2930 2992 3455 3292 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 2775 2850 2925 2850 2925 3000 2775 3000 2775 2850 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 0 0 1.00 60.00 120.00 - 3150 2625 2925 3000 + 2475 2550 2775 2850 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 0 0 1.00 60.00 120.00 - 2925 3000 3450 3300 + 3114 2523 2889 2823 4 0 0 50 -1 0 16 0.0000 4 120 105 1575 1350 a\001 4 0 0 50 -1 0 16 0.0000 4 165 120 3675 1350 b\001 4 0 0 50 -1 0 16 0.0000 4 165 120 3225 2400 d\001 4 0 0 50 -1 0 16 0.0000 4 120 105 3675 3525 e\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3900 2475 h\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3375 1800 h\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 2850 1800 h\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 2625 1200 s\001 diff --git a/EHC/figs/unq-graph2.fig b/EHC/figs/unq-graph2.fig new file mode 100644 index 000000000..41cde0393 --- /dev/null +++ b/EHC/figs/unq-graph2.fig @@ -0,0 +1,70 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +6 2175 2250 2325 2400 +4 0 0 50 -1 0 16 0.0000 4 120 105 2175 2400 c\001 +-6 +6 6000 2250 6150 2400 +4 0 0 50 -1 0 16 0.0000 4 120 105 6000 2400 c\001 +-6 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3300 2325 300 300 3300 2325 3600 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 300 300 2250 2325 2550 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 300 300 1650 1275 1950 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 1275 300 300 3750 1275 4050 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 300 300 3750 3450 4050 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 225 225 1650 1275 1875 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 225 225 2250 2325 2475 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 225 225 3750 3450 3975 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 225 225 5475 1275 5700 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 300 300 5475 1275 5775 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6075 2325 225 225 6075 2325 6300 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6075 2325 300 300 6075 2325 6375 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7200 1875 225 225 7200 1875 7425 1875 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7200 1875 300 300 7200 1875 7500 1875 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1950 1275 3450 1275 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3466 1448 2491 2123 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3600 1575 3450 2025 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3825 3150 3825 1575 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2930 2992 3455 3292 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 2775 2850 2925 2850 2925 3000 2775 3000 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2475 2550 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3114 2523 2889 2823 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5625 1575 5925 2025 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6900 2025 6375 2250 +4 0 0 50 -1 0 16 0.0000 4 120 105 1575 1350 a\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3675 1350 b\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3225 2400 d\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 3675 3525 e\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3900 2475 h\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3375 1800 h\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 5400 1350 a\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 7125 1950 e\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 2850 1800 h\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 5625 1875 s\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 6600 2025 h\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 2625 1200 s\001 diff --git a/EHC/figs/unq-graph3.fig b/EHC/figs/unq-graph3.fig new file mode 100644 index 000000000..b6f6f91bf --- /dev/null +++ b/EHC/figs/unq-graph3.fig @@ -0,0 +1,74 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +6 2175 2250 2325 2400 +4 0 0 50 -1 0 16 0.0000 4 120 105 2175 2400 c\001 +-6 +6 6600 1200 6750 1350 +4 0 0 50 -1 0 16 0.0000 4 120 105 6600 1350 c\001 +-6 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3300 2325 300 300 3300 2325 3600 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 300 300 2250 2325 2550 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 300 300 1650 1275 1950 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 1275 300 300 3750 1275 4050 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 300 300 3750 3450 4050 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 225 225 1650 1275 1875 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 225 225 2250 2325 2475 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 225 225 3750 3450 3975 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 225 225 5475 1275 5700 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 300 300 5475 1275 5775 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6675 1275 225 225 6675 1275 6900 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6666 1277 300 300 6666 1277 6966 1277 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6066 2552 300 300 6066 2552 6366 2552 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6063 2554 225 225 6063 2554 6288 2554 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1950 1275 3450 1275 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3466 1448 2491 2123 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3600 1575 3450 2025 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3825 3150 3825 1575 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2930 2992 3455 3292 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 2775 2850 2925 2850 2925 3000 2775 3000 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2475 2550 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3114 2523 2889 2823 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 6000 1800 6150 1800 6150 1950 6000 1950 6000 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5625 1575 6000 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6450 1500 6150 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6075 1950 6075 2250 +4 0 0 50 -1 0 16 0.0000 4 120 105 1575 1350 a\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3675 1350 b\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3225 2400 d\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 3675 3525 e\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3900 2475 h\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3375 1800 h\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 5400 1350 a\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 2850 1800 h\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 2625 1200 s\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 5625 1800 s\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 6000 2625 e\001 diff --git a/EHC/figs/unq-graph4.fig b/EHC/figs/unq-graph4.fig new file mode 100644 index 000000000..f1a29a420 --- /dev/null +++ b/EHC/figs/unq-graph4.fig @@ -0,0 +1,114 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +6 2175 2250 2325 2400 +4 0 0 50 -1 0 16 0.0000 4 120 105 2175 2400 c\001 +-6 +6 6600 1200 6750 1350 +4 0 0 50 -1 0 16 0.0000 4 120 105 6600 1350 c\001 +-6 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3300 2325 300 300 3300 2325 3600 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 300 300 2250 2325 2550 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 300 300 1650 1275 1950 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 1275 300 300 3750 1275 4050 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 300 300 3750 3450 4050 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 225 225 1650 1275 1875 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 225 225 2250 2325 2475 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 225 225 3750 3450 3975 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 225 225 5475 1275 5700 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 300 300 5475 1275 5775 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6675 1275 225 225 6675 1275 6900 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6666 1277 300 300 6666 1277 6966 1277 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6066 2552 300 300 6066 2552 6366 2552 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6063 2554 225 225 6063 2554 6288 2554 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7945 1998 225 225 7945 1998 8170 1998 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 9171 2012 225 225 9171 2012 9396 2012 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7955 2001 300 300 7955 2001 8255 2001 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 9170 2016 300 300 9170 2016 9470 2016 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7951 1070 300 300 7951 1070 8251 1070 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7947 1082 225 225 7947 1082 8172 1082 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8580 3285 300 300 8580 3285 8880 3285 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8577 3294 225 225 8577 3294 8802 3294 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1950 1275 3450 1275 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3466 1448 2491 2123 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3600 1575 3450 2025 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3825 3150 3825 1575 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2930 2992 3455 3292 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 2775 2850 2925 2850 2925 3000 2775 3000 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2475 2550 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3114 2523 2889 2823 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 6000 1800 6150 1800 6150 1950 6000 1950 6000 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5625 1575 6000 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6450 1500 6150 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6075 1950 6075 2250 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5775 1275 6375 1275 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6300 2325 6600 1575 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8100 2280 8475 2505 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8947 2212 8647 2512 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 8505 2505 8655 2505 8655 2655 8505 2655 8505 2505 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8580 2670 8580 2970 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 7950 1380 7950 1680 +2 1 1 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6075 1875 7455 1875 +4 0 0 50 -1 0 16 0.0000 4 120 105 1575 1350 a\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3675 1350 b\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3225 2400 d\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 3675 3525 e\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3900 2475 h\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3375 1800 h\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 5400 1350 a\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 2850 1800 h\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 2625 1200 s\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 6000 2625 e\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 6000 1200 s\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 6450 2175 h\001 +4 0 0 50 -1 0 16 0.0000 4 165 90 7905 2085 f\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 9135 2115 c\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 8520 3360 e\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 7890 1140 a\001 +4 0 0 50 -1 0 16 0.0000 4 120 90 7770 1605 s\001 +4 0 0 50 -1 0 12 0.0000 4 180 600 1845 3345 graph G\001 +4 0 0 50 -1 0 12 0.0000 4 180 585 5715 3090 graph R\001 +4 0 0 50 -1 0 12 0.0000 4 180 600 7770 2820 graph X\001 diff --git a/EHC/figs/unq-graph5.fig b/EHC/figs/unq-graph5.fig new file mode 100644 index 000000000..cceac7cd5 --- /dev/null +++ b/EHC/figs/unq-graph5.fig @@ -0,0 +1,52 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +6 6600 1200 6750 1350 +4 0 0 50 -1 0 16 0.0000 4 120 105 6600 1350 c\001 +-6 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 300 300 5475 1275 5775 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6066 2552 300 300 6066 2552 6366 2552 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6063 2554 225 225 6063 2554 6288 2554 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6666 1277 300 300 6666 1277 6966 1277 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6035 407 225 225 6035 407 6260 407 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6053 404 300 300 6053 404 6353 404 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8625 375 300 300 8625 375 8925 375 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8625 375 225 225 8625 375 8850 375 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8688 1800 225 225 8688 1800 8913 1800 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8691 1800 300 300 8691 1800 8991 1800 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 6000 1800 6150 1800 6150 1950 6000 1950 6000 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6450 1500 6150 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6075 1950 6075 2250 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5625 1575 6000 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6300 600 6525 975 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5850 675 5625 975 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 8550 1050 8700 1050 8700 1200 8550 1200 8550 1050 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8625 675 8625 1050 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8625 1200 8625 1500 +4 0 0 50 -1 0 16 0.0000 4 120 105 6000 450 a\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 5400 1350 b\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 6000 2625 d\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 8625 1875 b\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 8550 450 a\001 diff --git a/EHC/figs/unq-graph6.fig b/EHC/figs/unq-graph6.fig new file mode 100644 index 000000000..dc5841a36 --- /dev/null +++ b/EHC/figs/unq-graph6.fig @@ -0,0 +1,104 @@ +#FIG 3.2 +Landscape +Center +Inches +Letter +100.00 +Single +-2 +1200 2 +6 2175 2250 2325 2400 +4 0 0 50 -1 0 16 0.0000 4 120 105 2175 2400 c\001 +-6 +6 6435 1980 6585 2130 +4 0 0 50 -1 0 16 0.0000 4 120 105 6435 2130 c\001 +-6 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3300 2325 300 300 3300 2325 3600 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 300 300 2250 2325 2550 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 300 300 1650 1275 1950 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 1275 300 300 3750 1275 4050 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 300 300 3750 3450 4050 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1650 1275 225 225 1650 1275 1875 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 2250 2325 225 225 2250 2325 2475 2325 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3750 3450 225 225 3750 3450 3975 3450 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 225 225 5475 1275 5700 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5475 1275 300 300 5475 1275 5775 1275 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6075 3375 300 300 6075 3375 6375 3375 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6064 3366 225 225 6064 3366 6289 3366 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6509 2035 300 300 6509 2035 6809 2035 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5416 2132 300 300 5416 2132 5716 2132 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8358 3219 300 300 8358 3219 8658 3219 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7858 1926 300 300 7858 1926 8158 1926 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 7863 1918 225 225 7863 1918 8088 1918 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8362 3218 225 225 8362 3218 8587 3218 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 6512 2039 225 225 6512 2039 6737 2039 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 5420 2126 225 225 5420 2126 5645 2126 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8852 1889 300 300 8852 1889 9152 1889 +1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 8859 1888 225 225 8859 1888 9084 1888 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 1950 1275 3450 1275 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3466 1448 2491 2123 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3600 1575 3450 2025 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3825 3150 3825 1575 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2930 2992 3455 3292 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 2775 2850 2925 2850 2925 3000 2775 3000 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 2475 2550 2775 2850 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 3114 2523 2889 2823 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 6000 2625 6150 2625 6150 2775 6000 2775 6000 2625 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6075 2775 6075 3075 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 6450 2325 6150 2625 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5632 2389 6007 2614 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 5400 1575 5400 1800 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 7875 2250 8250 2475 +2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 + 8250 2475 8400 2475 8400 2625 8250 2625 8250 2475 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8325 2625 8325 2925 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 0 0 1.00 60.00 120.00 + 8685 2160 8385 2460 +2 1 1 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 2 + 8265 2565 5205 720 +2 1 1 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 2 + 8265 2580 5730 4005 +4 0 0 50 -1 0 16 0.0000 4 120 105 1575 1350 a\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3225 2400 d\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 3675 3525 e\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3900 2475 h\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 3375 1800 h\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 5400 1350 a\001 +4 0 0 50 -1 0 12 0.0000 4 135 90 2850 1800 h\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 2625 1200 s\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 6000 3450 e\001 +4 0 0 50 -1 0 12 0.0000 4 90 90 5250 1725 s\001 +4 0 0 50 -1 0 16 0.0000 4 165 90 5325 2250 f\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 3675 1350 b\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 7815 2010 a\001 +4 0 0 50 -1 0 16 0.0000 4 120 105 8325 3315 c\001 +4 0 0 50 -1 0 16 0.0000 4 165 120 8805 1965 b\001 diff --git a/EHC/lhs2TeX/afp.fmt b/EHC/lhs2TeX/afp.fmt index a325341d0..09aea476b 100644 --- a/EHC/lhs2TeX/afp.fmt +++ b/EHC/lhs2TeX/afp.fmt @@ -65,10 +65,11 @@ %format (Dot(x)(y)(z)) = "{" x "}_{" y "}^{" z "}" %format (Delta(x)) = "{\delta_{" x "}}" -%format (Annot(x)(y)) = "{" x "}^{\delta_{" y "}}" -%format (Sup(x)(y)) = "{" x "}^{" y "}" -%format (Sub(x)(y)) = "{" x "}_{" y "}" +%format (Annot(x)(y)) = "{{" x "}^{\delta_{" y "}}}" +%format (Sup(x)(y)) = "{{" x "}^{" y "}}" +%format (Sub(x)(y)) = "{{" x "}_{" y "}}" %format (Card(x)(y)) = "{{" x "} \bowtie {" y "}}" +%format (SCard(x)(z)(y)) = "{{" x "} \bowtie^{" z "} {" y "}}" %format restr = "\backslash " @@ -408,3 +409,17 @@ %format Usage = "\jmath" %format UpperBound = "\imath" %format LowerBound = "\ell" +%format leq = "\sqsubseteq" +%format leqB = "\sqsubseteq_B" +%format leqL = "\sqsubseteq_L" +%format leqU = "\sqsubseteq_U" +%format leqC = "\sqsubseteq_C" +%format leqS = "\sqsubseteq_S" +%format leqX = "\sqsubseteq_X" +%format leqZ = "\sqsubseteq_Z" +%format leqM = "\sqsubseteq_M" +%format leqP = "\sqsubseteq_P" +%format leqQ = "\sqsubseteq_Q" +%format join = "\sqcup" +%format ConstrSet = zeta +%format bottom = "\bot" diff --git a/EHC/mk/config.mk b/EHC/mk/config.mk index 75693aea3..dc038f7cc 100644 --- a/EHC/mk/config.mk +++ b/EHC/mk/config.mk @@ -13,20 +13,20 @@ EH_VERSION := $(EH_VERSION_MAJOR).$(EH_VERSION_MINOR) # TOPABS_PREFIX : absolute prefix/pathname to top dir ### Unix -EXEC_SUFFIX := -PATH_SEP := / -PATHS_SEP := : -PATHS_SEP_COL := : -STRIP_CMD := strip -TOPABS_PREFIX := $(shell pwd)/ - -### WinXX -#EXEC_SUFFIX := .exe +#EXEC_SUFFIX := #PATH_SEP := / -#PATHS_SEP := ; +#PATHS_SEP := : #PATHS_SEP_COL := : -#STRIP_CMD := strip -#TOPABS_PREFIX := c:/whatever/ +#STRIP_CMD := strip +#TOPABS_PREFIX := $(shell pwd)/ + +### WinXX +EXEC_SUFFIX := .exe +PATH_SEP := / +PATHS_SEP := ; +PATHS_SEP_COL := : +STRIP_CMD := strip +TOPABS_PREFIX := c:/EHC/ ### remaining config # which version (usually v1 = current, v2 == under development) diff --git a/EHC/mk/shared.mk b/EHC/mk/shared.mk index 125d0a843..71540fce8 100644 --- a/EHC/mk/shared.mk +++ b/EHC/mk/shared.mk @@ -30,7 +30,7 @@ FILTER_NONEMP_FILES := $(BINABS_PREFIX)filterOutEmptyFiles # lhs2TeX LHS2TEX_ENV := $(LHS2TEX) -LHS2TEX_CMD := LHS2TEX=".$(PATHS_SEP)../../$(FMT_SRC_PREFIX)$(PATHS_SEP)$(LHS2TEX_ENV)" lhs2TeX +LHS2TEX_CMD := LHS2TEX=".$(PATHS_SEP)../../$(FMT_SRC_PREFIX)$(PATHS_SEP)$(LHS2TEX_ENV)" lhs2TeX +RTS -K20M -RTS # latex LATEX_ENV := $(TEXINPUTS) diff --git a/EHC/text/LitAdm.bib b/EHC/text/LitAdm.bib index 0517916a9..3371ff60e 100644 --- a/EHC/text/LitAdm.bib +++ b/EHC/text/LitAdm.bib @@ -64,7 +64,7 @@ @inproceedings{diatchki02hask-module @article{martelli82eff-unif-alg , eprint = {papers/martelli82eff-unif-alg.pdf} , title = {{An Efficient Unification Algorithm}} , author = {Martelli, Alberto and Montanari, Ugo} , journal = {ACM TOPLAS} , month = {April} , pages = {258 - 282} , number = {2} , volume = {4} , year = {1982} , url = {http://doi.acm.org/10.1145/357162.357169} , howpublished = {\verb|http://doi.acm.org/10.1145/357162.357169|}} @inproceedings{kanellakis91unification , eprint = {papers/kanellakis91unification.pdf} , title = {{Unification and {ML}-Type Reconstruction}} , author = {Kanellakis, Paris C. and Mairson, Harry G.} , booktitle = {Computational Logic - Essays in Honor of Alan Robinson} , year = {1991 } , url = {http://citeseer.nj.nec.com/kanellakis91unification.html} , howpublished = {\verb|http://citeseer.nj.nec.com/kanellakis91unification.html|}} @inproceedings{botlan03ml-power-f , eprint = {papers/botlan03ml-power-f.pdf} , title = {{ML-F, Raising ML to the Power of System F}} , author = {Botlan, Le, Didier and R\'emy, Didier} , booktitle = {ICFP} , year = {2003} , url = {http://citeseer.nj.nec.com/564799.html} , howpublished = {\verb|http://citeseer.nj.nec.com/564799.html|}} -@misc{peytonjones04pract-inf-rank , eprint = {papers/peytonjones04pract-inf-rank.pdf} , title = {{Practical type inference for arbitrary-rank types}} , author = {Peyton Jones, Simon and Shields, Mark} , year = {2004} , url = {http://research.microsoft.com/Users/simonpj/papers/putting/index.htm} , howpublished = {\verb|http://research.microsoft.com/Users/simonpj/papers/putting/index.htm|}} +@misc{peytonjones04pract-inf-rank , eprint = {papers/peytonjones04pract-inf-rank.pdf} , title = {{Practical type inference for arbitrary-rank types}} , author = {Peyton Jones, Simon L. and Shields, Mark} , year = {2004} , url = {http://research.microsoft.com/Users/simonpj/papers/putting/index.htm} , howpublished = {\verb|http://research.microsoft.com/Users/simonpj/papers/putting/index.htm|}} @techreport{gaster96poly-ext-rec-var , eprint = {papers/gaster96poly-ext-rec-var.pdf} , title = {{A Polymorphic Type System for Extensible Records and Variants}} , author = {Gaster, Benedict R. and Jones, Mark P.} , institution = {Languages and Programming Group, Department of Computer Science, Nottingham} , school = {Languages and Programming Group, Department of Computer Science, Nottingham} , month = {November} , number = {NOTTCS-TR-96-3} , year = {1996} , url = {http://citeseer.nj.nec.com/gaster96polymorphic.html} , howpublished = {\verb|http://citeseer.nj.nec.com/gaster96polymorphic.html|}} @inproceedings{shields01first-class-mod , eprint = {papers/shields01first-class-mod.pdf} , title = {{First-class Modules for Haskell}} , author = {Shields, Mark and Peyton Jones, Simon} , booktitle = {Ninth International Conference on Foundations of Object-Oriented Languages (FOOL 9), Portland, Oregon} , month = {December} , year = {2001} , url = {http://www.cse.ogi.edu/~mbs/pub/first_class_modules/} , howpublished = {\verb|http://www.cse.ogi.edu/~mbs/pub/first_class_modules/|}} @book{plasmeijer01clean-rep-2 , eprint = {papers/plasmeijer01clean-rep-2.pdf} , title = {{The Concurrent Clean Language Report (draft)}} , author = {Plasmeijer, Rinus and Eekelen, Marko van} , publisher = {Department of Software Technology, University of Nijmegen} , year = {2001} , url = {http://www.cs.kun.nl/~clean/contents/body_contents.html} , howpublished = {\verb|http://www.cs.kun.nl/~clean/contents/body_contents.html|}} diff --git a/EHC/text/RulerUniquenessExamples.crul b/EHC/text/RulerUniquenessExamples.crul index 630c58977..685af3e5e 100644 --- a/EHC/text/RulerUniquenessExamples.crul +++ b/EHC/text/RulerUniquenessExamples.crul @@ -151,7 +151,7 @@ ruleset prog.base scheme prog "Program type rule" = view U1 = judge E : expr = gam :- e : uty ~> cs judge P : unpack = uty === { _ , delta } - judge F : flowPrimWeak = cs.f === { (1,*,1) =>= delta } + judge F : flowPrimWeak = cs.f === { ((1,"(Card(*)(*))",1)) =>= delta } judge C : check = cs.f cs judge K : consistency = - @@ -164,6 +164,7 @@ ruleset expr.base scheme expr "Expression type rules" = - judge R : expr = gam :- n : Ty_Int view U1 = + judge A : arbitrary = delta - judge R : expr | uty = Ty_Int..delta @@ -172,6 +173,7 @@ ruleset expr.base scheme expr "Expression type rules" = - judge R : expr = gam :- n : Ty_Int view UX = + judge F : fresh = delta - judge R : expr | uty = Ty_Int..delta @@ -247,11 +249,9 @@ ruleset expr.base scheme expr "Expression type rules" = judge B : expr | uty = Ty_Int..b | cs = cs.b - judge C1 : flowPrim2 = cs.c1 === {c.ref =>= a.ref} - judge C2 : flowPrim2 = cs.c2 === {c.ref =>= b.ref} - judge P1 : unpackTup = a === { a.ref, _ } - judge P2 : unpackTup = b === { b.ref, _ } - judge P3 : unpackTup = c === { c.ref, _ } + judge C1 : flowPrim2 = cs.c1 === {c =>= a} + judge C2 : flowPrim2 = cs.c2 === {c =>= b} + judge F : fresh = c - judge R : expr | cs = cs.c1 cs.c2 cs.a cs.b @@ -293,16 +293,14 @@ ruleset expr.base scheme expr "Expression type rules" = judge A : expr | uty = uty.a | cs = cs.a - judge C : match = uty.f <=> (uty.a.1 ->..(delta.1) uty.r) - judge C2 : freshAnnot = uty.r ~> uty - judge C3 : match = uty.a.1 <=> uty.a - judge T1 : unpack = uty === { ty , delta.top } - judge M1 : mkFlow = cs.md === delta.top =>= delta - judge M2 : mkFlow = cs.ma === uty.a.1 =>= uty.a - judge M3 : mkFlow = cs.mr === uty =>= uty.r + judge C : match = uty.f <=> (uty.p ->..(delta.f) uty) + judge C3 : match = ty.p <=> ty.a + judge T1 : unpack = uty === { ty , delta } + judge M1 : flowPrimWeak = cs.md === { delta =>= delta.f } + judge M2 : flow = :- uty.p =>= uty.a ~> cs.ma - judge R : expr - | cs = cs.md cs.ma cs.mr cs.a cs.f + | cs = cs.md cs.ma cs.a cs.f view L = judge F : expr = gam.f :- f : (ty.a -> ty) judge A : expr = gam.a :- a : ty.a @@ -314,27 +312,30 @@ ruleset expr.base scheme expr "Expression type rules" = - judge R : expr = gam :- (\x -> b) : (ty.x -> ty) view U1 = + judge A : arbitrary = delta judge B : expr = (x :-> ty.x + gam) :- b : uty ~> cs.b - judge S1 : gather = x :- b ~> ({ x.1:uty.1.a1, "...", x.n:uty.n.an }) + judge S1 : gather = x :- b ~> ({ x.1:"(Sub(Sup(utau)(Sub(a)(1)))(1))", "...", x.n:"(Sub(Sup(utau)(Sub(a)(n)))(n))" }) judge P : unpack = uty.x === { _, a } - judge S2 : sum = cs.sum === { sum <= a } + judge S2 : sum = cs.gat === { sum <= a } - judge R : expr | uty = uty.x ->..delta uty - | cs = cs.sum cs.b + | cs = cs.gat cs.b view EX = judge B : expr = (x :-> ty.x + gam) :- b : ty - judge R : expr = gam :- (\x -> b) : (ty.x -> ty) view UX = - judge B : expr = (x :-> ty.x + gam) :- b : uty ~> cs.b - judge S1 : gather = x :- b ~> ({ x.1:uty.1.a1, "...", x.n:uty.n.an }) + judge F : fresh = delta + judge B : expr = (x :-> ty.x + gam) :- b : uty.b ~> cs.b + judge M : flow = :- uty =>= uty.b ~> cs.r + judge S1 : gather = x :- b ~> ({ x.1:"(Sub(Sup(utau)(Sub(a)(1)))(1))", "...", x.n:"(Sub(Sup(utau)(Sub(a)(n)))(n))" }) judge P : unpack = uty.x === { _, a } judge S2 : sum = cs.sum === { sum <= a } - judge R : expr | uty = uty.x ->..delta uty - | cs = cs.sum cs.b + | cs = cs.sum cs.r cs.b view L = judge B : expr = (x :-> ty.x + gam) :- b : ty - @@ -342,8 +343,8 @@ ruleset expr.base scheme expr "Expression type rules" = rule e.let "Let" = view EL = - judge E : expr = gam :- expr : ty.expr - judge B : expr = (x.m :-> ty.expr + gam) :- body : ty + judge E : expr = gam :- expr : ty.x + judge B : expr = (x.m :-> ty.x + gam) :- body : ty - judge R : expr = gam :- (let.m x "=" expr in body) : ty view UL = @@ -351,8 +352,9 @@ ruleset expr.base scheme expr "Expression type rules" = | uty = uty.e | cs = cs.e | bcs = bcs.e - judge B : expr = (x.m :-> uty.expr + gam) :- body : uty ~> cs.b , bcs.b - judge C1 : gather = x :- (expr, body) ~> ({ x.1:uty.1.a1, "...", x.n:uty.n.an }) + judge A : freshAnnot = uty.e ~> uty.x + judge B : expr = (x.m :-> uty.x + gam) :- body : uty ~> cs.b , bcs.b + judge C1 : gather = x :- (expr, body) ~> ({ x.1:"(Sub(Sup(utau)(Sub(a)(1)))(1))", "...", x.n:"(Sub(Sup(utau)(Sub(a)(n)))(n))" }) judge P : unpack = uty.x === {_ , delta } judge S : sum = cs.sum === { sum <= delta } - @@ -389,6 +391,11 @@ ruleset expr.base scheme expr "Expression type rules" = | cs = cs.gc cs.tc cs.ec cs.g cs.t cs.e | bcs = bcs.g bcs.t bcs.e +relation arbitrary = + view B = + holes [ x : Nm ] + judgespec x + judgeuse tex x " arbitrary" relation lookup = view B = @@ -435,7 +442,7 @@ relation flow = judgespec :- utyA =>= utyB ~> cs judgeuse tex :-..flow utyA =>= utyB ~> cs -ruleset flow.base scheme flow "Flow type rules" = +ruleset flow.base scheme flow "Coercion generating type rules" = rule int "Int" = view U1 = judge F : flowPrim = cs === { a =>= b } @@ -474,6 +481,11 @@ relation consistency = judgespec judgeuse tex "all tripples consistent" +relation fresh = + view B = + holes [ delta : Dummy ] + judgespec delta + judgeuse tex delta " |fresh|" diff --git a/EHC/text/uniqueness/TopicIntroduction.cltex b/EHC/text/uniqueness/TopicIntroduction.cltex index 16f355895..ee553b8ba 100644 --- a/EHC/text/uniqueness/TopicIntroduction.cltex +++ b/EHC/text/uniqueness/TopicIntroduction.cltex @@ -115,7 +115,8 @@ of values that are used at most once, is the focus of this master's thesis. ranges over all elements of the list, and each element gets the same property, although given our intuition of the definition of |fibs|, lower numbers are used much more than higher numbers, since the lower numbers are used to obtain a higher number. The approximation makes it easier to deal with usage properties, hence usage analyses are defined in - terms of type systems, at the cost of accuracy. In practice this is not much of a problem: if a programmer uses a list, + terms of type systems, at the cost of accuracy (see Figure~\ref{fig.ListRep} for an example why types cannot cannot + differentiate between individual bits of memory). In practice this is not much of a problem: if a programmer uses a list, then the elements of this list are typically used in a similar way, otherwise the programmer would have used two lists or another data type. @@ -145,7 +146,7 @@ of values that are used at most once, is the focus of this master's thesis. In practice, a linear type system mixes linear type and non-linear types, demanding the environment restrictions on linear types, and no restrictions for non-linear types (see the type systems given - by Wadler~\cite{wadler90linear} for more information). In this thesis, we use a richer representation than just + by Wadler~\cite{wadler90linear} for more information). In this master's thesis, we use a richer representation than just linear and non-linear to represent uniqueness properties (Section~\ref{sect.Annotations}), but assume that linear types are annotated with a |1| (i.e. |(Sup(Int)(1))|), and non-linear types with a |*| (i.e. |(Sup(Int)(*))|). diff --git a/EHC/text/uniqueness/TopicNoBindings.cltex b/EHC/text/uniqueness/TopicNoBindings.cltex index ce11c1614..e0ca25ebe 100644 --- a/EHC/text/uniqueness/TopicNoBindings.cltex +++ b/EHC/text/uniqueness/TopicNoBindings.cltex @@ -1,7 +1,5 @@ %%[main -%format sumtuples = "\sum_{i}" - \chapter{Lambda-calculus without bindings} \label{chapt.NoBindings} @@ -37,7 +35,7 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma \subsection{Annotations} \label{sect.Annotations} - + We consider for a moment what a usage property actually is. During the execution of a program, there are \emph{values} in memory and there are \emph{names} bound to values. These names are actually present in memory as \emph{pointers} to a value\footnote{Unless the value is unboxed, then the name only exists conceptually.}. @@ -55,11 +53,15 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma the same value, it also represents a value that is used more than once, even though this value is used only once via |x|. Similary, |(Sub(x)(2))| represents a value that is used more than once. These are two different properties for a name: a propery that describes the usage of a value via a name, and a property that describes the entire usage of a value represented by a name. - - This concept of names can be generalized to expressions (via referential transparency). Suppose that |v| is a value represented by an - expression |E|. There is a difference between a usage property that specifies that |v| is used a number of times through |E|, and - the property that specifies how often |v| is used in total. - + + This concept of names can be generalized to expressions (via referential transparency: an unevaluated expression in a \emph{thunk}, of which + the memory is later replaced by the actual value). Suppose that |v| is a value represented by an + expression |E|. + + An important observation is that there is a difference between a usage property that specifies that |v| is used a number of times + via |E|, and the property that specifies how often |v| is used in total. An analysis typically focusses on one of of these two + usage properties. + For uniqueness typing as defined in Clean, only usage properties of values are important. In Clean, a unique type represents a value that is used at most once. For each name |x| with a unique type, we know that the corresponding value is used at most once. For example, the value represented by |x| is used at most once in |(\x -> const (Sub(x)(5)) (Sub(x)(6))) 3|, but this property does not specify that @@ -67,14 +69,14 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma one of the names, that it will not be used via any of the other names. This is sufficient for destructive updates optimisations. Code that performs destructive updates can be generated for any operation on a value that is used at most once, because at most one of these operations will be performed during a program execution. - + However, there are optimisations that benefit from knowing that a value is used exactly once. A value that is used exactly once, can be safely pre-evaluated before passing it to a function. Or a function that is used exactly once, can be inlined safely, always resulting into better performing code and a smaller code size.Futhermore, an expression that will not be used at all, can be omitted. These are realistic and beneficial optimisations, thus for our analysis, we support both types of usage properties. - + We define the \emph{cardiality}~\cite{jur} property of a type as follows: - + %%[[wrap=code (Card(Usage)(Usage)) %%] @@ -99,7 +101,7 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma is used at most once, which is slightly less demanding. Our approach can verify both uniqueness properties and strictness properties. Although our focus is on uniqueness properties, we consider strictness as well, since we get it almost for free with our approach. We still call our approach uniqueness typing, but it is technically more than that. - + A cardinality property is attached to type constructors as \emph{cardinality annotation}. Cardinality originates from set theory where it is defined as the number of elements in a set. Some authors use the word cardinality as alternative for arity. Our definition of cardinality is unrelated to arity, which is the reason why we stress the difference here. @@ -118,18 +120,18 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma Chapter~\ref{chapt.Polyvariant}). Unfortunately, we cannot easily formulate the conditions of when an annotation is correct or not. We have to check two things: does the annotation fit with related annotations (the context), and does the annotation fit with the actual uses of the value. With context we mean that if two types are unified, - that their annotations also unify. For example, a value with cardinality |(Card(1)(1))| cannot be passed to a function that + that their annotations also unify. For example, a value with cardinality |(Card(1)(1))| cannot be passed to a function that has |(Card(onemin)(1))| cardinality for its parameter, because the function does not guarantee that the value will always be used. With the actual uses of the value, we mean the guaranteed upper and lower bound on the number of times the value will be evaluated or referenced. For example, a value that is referenced at least once cannot have the cardinality annotation |(Card(0)(0))|. We have - sufficient information for the context check (which is basically a form of unification), but insufficient information for the - the check on the usages. - - We therefore ask the programmer to specify the upper and lower bound as well. The types in an expression are - thus annotated with three (!) annotations: A cardinality annotation, a lower-bound usage-count annotation, - and an upper-bound usage-count annotation. The lower-bound usage-count annotation tells us that a value is at - least used a certain number of times, and the upper-bound usage-count annotation tells us that a value is at most - used a certain number of times. The usage-check demands that the cardinality annotation \emph{fits} with these + sufficient information for the context check (which is basically a form of unification, and checks the right-hand side of the cardinality annotation), but insufficient information for the + the check on the usages (the left-hand side of the cardinality annotation). + + We therefore ask the programmer to specify an upper and lower bound on the type of an expression (or name). The types in an expression are + thus annotated with three (!) annotations: A cardinality annotation, a lower-bound usage-count annotation, and an upper-bound usage-count annotation. + The lower-bound usage-count annotation tells us that a value is at + least used a certain number of times via the expression, and the upper-bound usage-count annotation tells us that a value is at most + used a certain number of times via the expression. The usage-check demands that left-hand side of the cardinality annotation \emph{fits} with these bounds~\ref{code.FitsInBounds}). The upper and lower bound can be verified by means of an analysis, which in turn means that we can verify the cardinality annotations. @@ -225,7 +227,8 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma is strictly necessary: %%[[wrap=code - (\x -> x) 3 + (\x -> x) 3 -- original expression + (((\(x :: Int) -> x :: Int) :: Int -> Int) (3 :: Int)) :: Int -- typed expression (((\(x :: (Sup(Sub(Int)(a))(*))) -> x :: (Sup(Sub(Int)(b))(1))) :: (Sup(Sub(Int)(c))(*)) (Sup(Sub(->)(d))(*)) (Sup(Sub(Int)(e))(1))) (3 :: (Sup(Sub(Int)(f))(*)))) :: (Sup(Sub(Int)(g))(1)) %%] @@ -307,26 +310,24 @@ solving. In the remainder of the chapter, we treat these aspects in a more forma The second annotation is the cardinality annotation, specifying that the value is strict, meaning that it is used one or more times. The third annotation is the upper-bound usage-count annotation, which specifies that the value is at most used an arbitrary number of times. This triple is consistent if the cardinality annotation - fits the two bounds and the cardinaltiy annotat - -the lower bound - is smaller or equal than the cardinality annotation, and the cardinalt annotation is smaller or equal to the upper bound. - The smaller or equal relation is defined between the three types of annotations in the obvious way, and - consistency for a triple is defined in Figure~\ref{code.FitsInBounds}. + fits the two bounds (Figure~\ref{code.FitsInBounds}) and the left-hand side of the cardinality annotation does not conflict with the right-hand side + of the cardinality annotation (Section~\ref{sect.TpAnnConstr}). For the above example, a possible annotation is: %%[[wrap=code - ( ( (\x y -> ( ( y :: (Sup(Int)((1, 1, 1))) - + x :: (Sup(Int)((1, oneplus, *))) - ) :: (Sup(Int)((1, 1, 1)))) - + x :: (Sup(Int)((1, oneplus, *))) - ) :: (Sup(Int)((1, 1, 1))) - ) :: (Sup(Int)((1, oneplus, *))) (Sup(->)((1, 1, 1))) (Sup(Int)((1, 1, 1))) (Sup(->)((1, 1, 1))) (Sup(Int)((1, 1, 1)))) - (3 :: (Sup(Int)((1, oneplus, *))))) - ) :: (Sup(Int)((1, 1, 1))) (Sup(->)((1, 1, 1))) (Sup(Int)((1, 1, 1)))) - (4 :: (Sup(Int)((1, 1, 1)))) - ) :: (Sup(Int)((1, 1, 1))) + ( ( ( \(x :: (Sup(Int)((1, (Card(1)(oneplus)), *)))) -> + \(y :: (Sup(Int)((1, (Card(1)(1)), *)))) -> + ( ( y :: (Sup(Int)((1, (Card(1)(1)), 1))) + + x :: (Sup(Int)((1, (Card(1)(oneplus)), *))) + ) :: (Sup(Int)((1, (Card(1)(1)), 1)))) + + x :: (Sup(Int)((1, (Card(1)(oneplus)), *))) + ) :: (Sup(Int)((1, (Card(1)(1)), 1))) + ) :: (Sup(Int)((1, (Card(1)(oneplus)), *))) (Sup(->)((1, (Card(1)(1)), 1))) (Sup(Int)((1, (Card(1)(1)), 1))) (Sup(->)((1, (Card(1)(1)), 1))) (Sup(Int)((1, (Card(1)(1)), 1)))) + (3 :: (Sup(Int)((1, (Card(1)(oneplus)), *)))) + ) :: (Sup(Int)((1, (Card(1)(1)), 1))) (Sup(->)((1, (Card(1)(1)), 1))) (Sup(Int)((1, (Card(1)(1)), 1)))) + (4 :: (Sup(Int)((1, (Card(1)(1)), 1)))) + ) :: (Sup(Int)((1, (Card(1)(1)), 1))) %%] This looks quite intimidating, but that is just because there are a lot of types involved and the @@ -343,7 +344,7 @@ the lower bound constraints are satisfied, the annotations are correct and the program is correctly typed according to the uniqueness type system. - As a side note, in order to keep the explanation compact, we are a bit + As an aside, in order to keep the explanation compact, we are a bit sloppy in distinguishing identifiers, values and types. For example, if we talk about the upper bound of a function, we intend the upper-bound usage-count annotation on the type constructor associated with the value representing the function. Or when we talk about the cardinality of an expression, we actually mean how @@ -356,41 +357,42 @@ the lower bound start with the entire program (expression): %%[[wrap=code - ( ... ) :: (Sup(Int)(((Sup(1)(1)), (Sup(1)(2)), (Sup(1)(3))))) + ( ... ) :: (Sup(Int)(((Sup(1)(1)), (SCard(1)(2)(1)), (Sup(1)(3))))) %%] The result of the entire expression is exactly used once. However, we are allowed to be less accurate for the result - of the entire expression. Any usage value that is consistent is allowed. We generate the constraint |(1, *, 1) (Sub(=>=)(s)) ((Sup(1)(1)), (Sup(1)(2)), (Sup(1)(3)))|. This constraint specifies that the lower bound + of the entire expression. Any usage value that is consistent is allowed. We generate the constraint |(1, (Card(1)(*)), 1) (Sub(=>=)(s)) ((Sup(1)(1)), (SCard(1)(2)(1)), (Sup(1)(3)))|. This constraint specifies that the lower bound is at most |1|, the upper bound is at least |1|, and the cardinality annotation can be anything as long as it is consistent with - the two bounds in the triple. The subscript |s| indicates that the usage annotation is ignored in this constraint. A |=>=| constraint - without the |s| suffix is encountered later in the example. The generated constraint expresses what we know about the result of the entire expression. We call this - constraint a flow or propagation constraint, because with some imagination, it `pushes' values on the - left-hand side to the right-hand side. We often call a |=>=| constraint a coercion, which is explained in the next - section. + the two bounds in the triple. The subscript |s| indicates that the cardinality annotation is ignored in this + constraint. A |=>=| constraint without the |s| suffix is encountered later in the example. The generated constraint expresses what + we know about the result of the entire expression. We call this constraint a flow or propagation constraint, because with some + imagination, it `pushes' values on the left-hand side to the right-hand side. We often call a |=>=| constraint a coercion, which + is explained in the next section. One step into the expression, an application is encountered: %%[[wrap=code - (( ... :: (Sup(Int)(((Sup(1)(4)), (Sup(1)(5)), (Sup(1)(6))))) (Sup(->)(((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9))))) (Sup(Int)(((Sup(1)(10)), (Sup(1)(11)), (Sup(1)(12)))))) (4 :: (Sup(Int)(((Sup(1)(13)), (Sup(1)(14)), (Sup(1)(15))))))) :: (Sup(Int)(((Sup(1)(16)), (Sup(1)(17)), (Sup(1)(18))))) + (( ... :: (Sup(Int)(((Sup(1)(4)), (SCard(1)(5)(1)), (Sup(1)(6))))) (Sup(->)(((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9))))) (Sup(Int)(((Sup(1)(10)), (SCard(1)(11)(1)), (Sup(1)(12)))))) (4 :: (Sup(Int)(((Sup(1)(13)), (SCard(1)(14)(1)), (Sup(1)(15))))))) :: (Sup(Int)(((Sup(1)(16)), (SCard(1)(17)(1)), (Sup(1)(18))))) %%] Several constraints are generated for a function application: \begin{itemize} \item The function application and the function. The number of usages of the function depends on the number of usages of the - function application. We generate the constraint |((Sup(1)(16)), (Sup(1)(17)), (Sup(1)(18))) (Sub(=>=)(s)) ((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9)))|. + function application. We generate the constraint |((Sup(1)(16)), (SCard(1)(17)(1)), (Sup(1)(18))) (Sub(=>=)(s)) ((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9)))|. The lower bound of the function (|(Sup(1)(7))|) is at most the lower bound of the function application (|(Sup(1)(16))|). The upper bound of the function (|(Sup(1)(18))|) is at least the upper bound of the function application (|(Sup(1)(9))|). The constraint expresses precisely how often the function is used, if we know how often the function application itself is used. - The cardinality annotations are unrelated, since the memory occupied by the function has nothing to do with the memory + The cardinality annotations are unrelated, since the memory occupied by the closure (function) is unrelated to the memory occupied by the result of the function. \item The function application and result of the function. The number of uses of the result of the function application depends on - how often the function application itself is used. We generate the constraint |((Sup(1)(16)), (Sup(1)(17)), (Sup(1)(18))) =>= ((Sup(1)(10)), (Sup(1)(11)), (Sup(1)(12)))|. + how often the function application itself is used. We generate the constraint |((Sup(1)(16)), (SCard(1)(17)(1)), (Sup(1)(18))) =>= ((Sup(1)(10)), (SCard(1)(11)(1)), (Sup(1)(12)))|. The lower bound of the result of the function (|(Sup(1)(10))|) is at most the lower bound of the function application (|(Sup(1)(16))|). The upper bound of - the result of the function function (|(Sup(1)(18))|) is at least the upper bound of the function application (|(Sup(1)(11))|). The cardinality annotation (|(Sup(1)(12))|) - of the result of the function should be equal (modulo coercion) to the cardinality annotation of the function application (|(Sup(1)(17))|). + the result of the function function (|(Sup(1)(18))|) is at least the upper bound of the function application (|(Sup(1)(12))|). The cardinality annotation (|(SCard(1)(11)(1))|) + of the result of the function should be equal (modulo coercion/weakening) to the cardinality annotation of the function application (|(SCard(1)(17)(1))|), since they + represent the same value (via referential transparancy). \item The function and the argument of the function application. The uses of the argument of the function - application depend on the annotations of the parameter of the function. We generate the constraint |((Sup(1)(4)), (Sup(1)(5)), (Sup(1)(6))) =>= ((Sup(1)(13)), (Sup(1)(14)), (Sup(1)(15)))|. + application depend on the annotations of the parameter of the function. We generate the constraint |((Sup(1)(4)), (SCard(1)(5)(1)), (Sup(1)(6))) =>= ((Sup(1)(13)), (SCard(1)(14)(1)), (Sup(1)(15)))|. The semantics of the constraint capture the relations between the three annotations on the type of the function parameter and the type of the argument value. \end{itemize} @@ -402,41 +404,40 @@ the lower bound The function expression is again an application: %%[[wrap=code - ( ... :: (Sup(Int)(((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21))))) (Sup(->)(((Sup(1)(22)), (Sup(1)(23)), (Sup(1)(24))))) ((Sup(Int)(((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27))))) (Sup(->)(((Sup(1)(28)), (Sup(1)(29)), (Sup(1)(30))))) (Sup(Int)(((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33))))))) - (3 :: (Sup(Int)(((Sup(1)(34)), (Sup(oneplus)(35)), (Sup(*)(36)))))) - :: (Sup(Int)(((Sup(1)(4)), (Sup(1)(5)), (Sup(1)(6))))) (Sup(->)(((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9))))) (Sup(Int)(((Sup(1)(10)), (Sup(1)(11)), (Sup(1)(12))))) + ( ... :: (Sup(Int)(((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21))))) (Sup(->)(((Sup(1)(22)), (SCard(1)(23)(1)), (Sup(1)(24))))) ((Sup(Int)(((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27))))) (Sup(->)(((Sup(1)(28)), (SCard(1)(29)(1)), (Sup(1)(30))))) (Sup(Int)(((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33))))))) + (3 :: (Sup(Int)(((Sup(1)(34)), (SCard(oneplus)(35)(oneplus)), (Sup(*)(36)))))) + :: (Sup(Int)(((Sup(1)(4)), (SCard(1)(5)(1)), (Sup(1)(6))))) (Sup(->)(((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9))))) (Sup(Int)(((Sup(1)(10)), (SCard(1)(11)(1)), (Sup(1)(12))))) %%] This is basically the same situation as above, except with one important difference. The type of the result of the function application is a function. Its type has more than one type constructor, and multiple triples of annotations. Each type constructor in one type has a corresponding type constructor in the other type. The |=>=| constraint is generated - between triples attached on corresponding type constructors. This way we check annotations that specify - usages of the same regions of a value. The direction of the |=>=| constraint depends on co-variance and contra-variance. The - direction is reversed for |=>=| constraint between |contra-variant| type constructors. The reason is that co-variant type - constructors correspond to values for which the annotation require some property (``I must be used exactly once''), whereas + between triples attached on corresponding type constructors. This way we check annotations that represent the same values. The direction of the |=>=| constraint depends on co-variance and contra-variance. The + direction is reversed for |=>=| constraints between \emph{contra-variant} type constructors. The reason is that a co-variant type + constructor corresponds to values for which the annotation requires some property (``I must be used exactly once''), whereas contra-variant type constructors correspond to values for which the annotations provide some property (``I am used exactly once''), which is essentially the inverse direction. See Peyton Jones~\cite{peytonjones04pract-inf-rank} for an elaborate explanation - on co-variance and contra-variance and subtyping. + on co-variance, contra-variance, and subtyping. Applying the same reasoning as with the previous function application, we generate the following constraints: %%[[wrap=code - ((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9))) (Sub(=>=)(s)) ((Sup(1)(22)), (Sup(1)(23)), (Sup(1)(24))) -- use of the function - ((Sup(1)(10)), (Sup(1)(11)), (Sup(1)(12))) =>= ((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33))) -- use of the function value (resulting Int, co-variant) - ((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9))) =>= ((Sup(1)(28)), (Sup(1)(29)), (Sup(1)(30))) -- use of the function value (function type, co-variant) - ((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27))) =>= ((Sup(1)(4)), (Sup(1)(5)), (Sup(1)(6))) -- use of the function value (argument Int, contra-variant) - ((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21))) =>= ((Sup(1)(34)), (Sup(oneplus)(35)), (Sup(*)(36))) -- use of the argument + ((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9))) (Sub(=>=)(s)) ((Sup(1)(22)), (SCard(1)(23)(1)), (Sup(1)(24))) -- use of the function + ((Sup(1)(10)), (SCard(1)(11)(1)), (Sup(1)(12))) =>= ((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33))) -- use of the function value (resulting Int, co-variant) + ((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9))) =>= ((Sup(1)(28)), (SCard(1)(29)(1)), (Sup(1)(30))) -- use of the function value (function type, co-variant) + ((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27))) =>= ((Sup(1)(4)), (SCard(1)(5)(1)), (Sup(1)(6))) -- use of the function value (argument Int, contra-variant) + ((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21))) =>= ((Sup(1)(34)), (SCard(oneplus)(35)(oneplus)), (Sup(*)(36))) -- use of the argument %%] - This leaves to analyse the function of the function application, and the argument of the function application. The argument + Still to analyse are the function of the function application, and the argument of the function application. The argument is again an |Int| expression, which does not result in constraints, so we proceed with the function expression. The function expression is a lambda abstraction: %%[[wrap=code - ( \(x :: (Sup(Int)(((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21)))))) (y :: (Sup(Int)(((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27)))))) -> ... y :: (Sup(Int)(((Sup(1)(37)), (Sup(1)(38)), (Sup(1)(39))))) ... (Sub(x)(1)) :: (Sup(Int)(((Sup(1)(40)), (Sup(oneplus)(41)), (Sup(*)(42))))) ... (Sub(x)(2)) :: (Sup(Int)(((Sup(1)(43)), (Sup(oneplus)(44)), (Sup(*)(45))))) - ) :: (Sup(Int)(((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21))))) (Sup(->)(((Sup(1)(22)), (Sup(1)(23)), (Sup(1)(24))))) ((Sup(Int)(((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27))))) (Sup(->)(((Sup(1)(28)), (Sup(1)(29)), (Sup(1)(30))))) (Sup(Int)(((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33)))))) + ( \(x :: (Sup(Int)(((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21)))))) (y :: (Sup(Int)(((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27)))))) -> ... y :: (Sup(Int)(((Sup(1)(37)), (SCard(1)(38)(1)), (Sup(1)(39))))) ... (Sub(x)(1)) :: (Sup(Int)(((Sup(1)(40)), (SCard(1)(41)(oneplus)), (Sup(*)(42))))) ... (Sub(x)(2)) :: (Sup(Int)(((Sup(1)(43)), (SCard(1)(44)(oneplus)), (Sup(*)(45))))) + ) :: (Sup(Int)(((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21))))) (Sup(->)(((Sup(1)(22)), (SCard(1)(23)(1)), (Sup(1)(24))))) ((Sup(Int)(((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27))))) (Sup(->)(((Sup(1)(28)), (SCard(1)(29)(1)), (Sup(1)(30))))) (Sup(Int)(((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33)))))) %%] For a lambda abstraction, we perform two tasks: analyze the body of the lambda abstraction, and @@ -454,15 +455,15 @@ the lower bound With only one use-site of |y|, and two use-sites of |x|, the constraints are: %%[[wrap=code - ((Sup(1)(40)), (Sup(oneplus)(41)), (Sup(*)(42))) \*/ ((Sup(1)(43)), (Sup(oneplus)(44)), (Sup(*)(45))) <= ((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21))) -- for x - ((Sup(1)(37)), (Sup(1)(38)), (Sup(1)(39))) <= ((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27))) -- for y + ((Sup(1)(40)), (SCard(1)(41)(oneplus)), (Sup(*)(42))) \*/ ((Sup(1)(43)), (SCard(1)(44)(oneplus)), (Sup(*)(45))) <= ((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21))) -- for x + ((Sup(1)(37)), (SCard(1)(38)(1)), (Sup(1)(39))) <= ((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27))) -- for y %%] The function body remains to be checked. The function body consists of the additions: %%[[wrap=code - ((y :: (Sup(Int)(((Sup(1)(37)), (Sup(1)(38)), (Sup(1)(39)))))) + ((Sub(x)(1)) :: (Sup(Int)(((Sup(1)(40)), (Sup(oneplus)(41)), (Sup(*)(42))))))) :: (Sup(Int)(((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48))))) - ((( ... ) :: (Sup(Int)(((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48)))))) + ((Sub(x)(2)) :: (Sup(Int)(((Sup(1)(43)), (Sup(oneplus)(44)), (Sup(*)(45))))))) :: (Sup(Int)(((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33)))))) + ((y :: (Sup(Int)(((Sup(1)(37)), (SCard(1)(38)(1)), (Sup(1)(39)))))) + ((Sub(x)(1)) :: (Sup(Int)(((Sup(1)(40)), (SCard(oneplus)(41)(oneplus)), (Sup(*)(42))))))) :: (Sup(Int)(((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48))))) + ((( ... ) :: (Sup(Int)(((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48)))))) + ((Sub(x)(2)) :: (Sup(Int)(((Sup(1)(43)), (SCard(oneplus)(44)(oneplus)), (Sup(*)(45))))))) :: (Sup(Int)(((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33)))))) %%] The addition operator uses both the arguments at least as many times as the result is used. The default operational @@ -472,53 +473,59 @@ the lower bound upper-bound annotations of the result of the expression. The cardinality annotation on the result of the addition may be any value that fits the two bounds. For the relation between the arguments of the addition and the result of the addition, we generate a weaker version of the |=>=| constraint that ignores the cardinality annotation, but does not - ignore the two bounds: |(Sub(=>=)(s))|, with the |s| of 'soft'. When we want to stress the difference between these - two |=>=| constraints, we write the normal |=>=| constraint as |(Sub(=>=)(h))|, with the |h| of 'hard'. + ignore the two bounds: |(Sub(=>=)(s))|, with the |s| of \emph{soft}. When we want to stress the difference between these + two |=>=| constraints, we write the normal |=>=| constraint as |(Sub(=>=)(h))|, with the |h| of \emph{hard}. The following constraints relate the result of the additions properly to the arguments of the addition: %%[[wrap=code - ((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(37)), (Sup(1)(38)), (Sup(1)(39))) - ((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(40)), (Sup(oneplus)(41)), (Sup(*)(42))) - ((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48))) - ((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(43)), (Sup(oneplus)(44)), (Sup(*)(45))) + ((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(37)), (SCard(1)(38)(1)), (Sup(1)(39))) + ((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(40)), (SCard(1)(41)(oneplus)), (Sup(*)(42))) + ((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48))) + ((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(43)), (SCard(1)(44)(oneplus)), (Sup(*)(45))) %%] \subsection{Checking the constraints} The final part of this example is to verify that the constraints hold. We show by an example how we interpret - the constraints. We define when a constraint hold more precisely in Section~\ref{Sect.CheckingConstraints}. We assume that - the triples are already checked for consistency, meaning that the usage annotation fits between the upper and - lower bound. The following table lists the constraints and their interpretation (see Figure~\ref{splitFunc} for the definition of |properSplit|): + the constraints. We define when a constraint holds more precisely in Section~\ref{Sect.CheckingConstraints}. We assume that + the triples are already checked for consistency, meaning that the cardinality annotation fits between the upper and + lower bound, and that the cardianltiy annotation itself is consistent. A cardinality annotation is consistent if the + left-hand side does not conflict with the right-hand side. The following table lists the constraints and their + interpretation (see Figure~\ref{splitFunc} for the definition of |isSplit|): \begin{tabular}{llllr} constraint & lower bound & usage & upper bound & holds \\ \hline - |(1, *, 1) (Sub(=>=)(s)) ((Sup(1)(1)), (Sup(1)(2)), (Sup(1)(3)))| & |1 >= (Sup(1)(1))| & & |1 <= (Sup(1)(3))| & OK \\ - |((Sup(1)(16)), (Sup(1)(17)), (Sup(1)(18))) (Sub(=>=)(s)) ((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9)))| & |(Sup(1)(16)) >= (Sup(1)(7))| & & |(Sup(1)(18)) <= (Sup(1)(9))| & OK \\ - |((Sup(1)(16)), (Sup(1)(17)), (Sup(1)(18))) =>= ((Sup(1)(10)), (Sup(1)(11)), (Sup(1)(12)))| & |(Sup(1)(16)) >= (Sup(1)(10))| & |(Sup(1)(17)) <= (Sup(1)(11))| & |(Sup(1)(18)) <= (Sup(1)(12))| & OK \\ - |((Sup(1)(4)), (Sup(1)(5)), (Sup(1)(6))) =>= ((Sup(1)(13)), (Sup(1)(14)), (Sup(1)(15)))| & |(Sup(1)(4)) >= (Sup(1)(13))| & |(Sup(1)(5)) <= (Sup(1)(14))| & |(Sup(1)(6)) <= (Sup(1)(15))| & OK \\ - |((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9))) (Sub(=>=)(s)) ((Sup(1)(22)), (Sup(1)(23)), (Sup(1)(24)))| & |(Sup(1)(7)) >= (Sup(1)(22))| & & |(Sup(1)(9)) <= (Sup(1)(24))| & OK \\ - |((Sup(1)(10)), (Sup(1)(11)), (Sup(1)(12))) =>= ((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33)))| & |(Sup(1)(10)) >= (Sup(1)(31))| & |(Sup(1)(11)) <= (Sup(1)(32))| & |(Sup(1)(12)) <= (Sup(1)(33))| & OK \\ - |((Sup(1)(7)), (Sup(1)(8)), (Sup(1)(9))) =>= ((Sup(1)(28)), (Sup(1)(29)), (Sup(1)(30)))| & |(Sup(1)(7)) >= (Sup(1)(28))| & |(Sup(1)(8)) <= (Sup(1)(29))| & |(Sup(1)(9)) <= (Sup(1)(30))| & OK \\ - |((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27))) =>= ((Sup(1)(4)), (Sup(1)(5)), (Sup(1)(6)))| & |(Sup(1)(25)) >= (Sup(1)(4))| & |(Sup(1)(26)) <= (Sup(1)(5))| & |(Sup(1)(27)) <= (Sup(1)(6))| & OK \\ - |((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21))) =>= ((Sup(1)(34)), (Sup(oneplus)(35)), (Sup(*)(36)))| & |(Sup(1)(19)) >= (Sup(1)(34))| & |(Sup(oneplus)(20)) <= (Sup(oneplus)(35))| & |(Sup(*)(20)) <= (Sup(*)(36))| & OK \\ - |((Sup(1)(40)), (Sup(oneplus)(41)), (Sup(*)(42))) \*/ ((Sup(1)(43)), (Sup(oneplus)(44)), (Sup(*)(45)))| & |(Sup(1)(40)) `max` (Sup(1)(43)) >= (Sup(1)(19))| & |properSplit {(Sup(oneplus)(41)), (Sup(oneplus)(44))} (Sup(oneplus)(20))| & |(Sup(1)(42)) + (Sup(1)(45)) <= (Sup(1)(21))| & OK \\ - | <= ((Sup(1)(19)), (Sup(oneplus)(20)), (Sup(*)(21)))| & & & & \\ - |((Sup(1)(37)), (Sup(1)(38)), (Sup(1)(39))) <= ((Sup(1)(25)), (Sup(1)(26)), (Sup(1)(27)))| & |(Sup(1)(37)) >= (Sup(1)(25))| & |properSplit {(Sup(1)(38))} (Sup(1)(26))| & |(Sup(1)(39)) <= (Sup(1)(27))| & OK \\ - |((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(37)), (Sup(1)(38)), (Sup(1)(39)))| & |(Sup(1)(46)) >= (Sup(1)(37))| & & |(Sup(1)(48)) <= (Sup(1)(39))| & OK \\ - |((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(40)), (Sup(oneplus)(41)), (Sup(*)(42)))| & |(Sup(1)(46)) >= (Sup(1)(40))| & & |(Sup(1)(48)) <= (Sup(*)(42))| & OK \\ - |((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(46)), (Sup(1)(47)), (Sup(1)(48)))| & |(Sup(1)(31)) >= (Sup(1)(46))| & & |(Sup(1)(33)) <= (Sup(1)(48))| & OK \\ - |((Sup(1)(31)), (Sup(1)(32)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(43)), (Sup(oneplus)(44)), (Sup(*)(45)))| & |(Sup(1)(13)) >= (Sup(1)(43))| & & |(Sup(1)(33)) <= (Sup(*)(45))| & OK \\ + |(1, *, 1) (Sub(=>=)(s)) ((Sup(1)(1)), (SCard(1)(2)(1)), (Sup(1)(3)))| & |1 leqL (Sup(1)(1))| & & |1 <= (Sup(1)(3))| & OK \\ + |((Sup(1)(16)), (SCard(1)(17)(1)), (Sup(1)(18))) (Sub(=>=)(s)) ((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9)))| & |(Sup(1)(16)) leqL (Sup(1)(7))| & & |(Sup(1)(18)) leqU (Sup(1)(9))| & OK \\ + |((Sup(1)(16)), (SCard(1)(17)(1)), (Sup(1)(18))) =>= ((Sup(1)(10)), (SCard(1)(11)(1)), (Sup(1)(12)))| & |(Sup(1)(16)) leqL (Sup(1)(10))| & |(SCard(1)(17)(1)) leqC (SCard(1)(11)(1))| & |(Sup(1)(18)) leqU (Sup(1)(12))| & OK \\ + |((Sup(1)(4)), (SCard(1)(5)(1)), (Sup(1)(6))) =>= ((Sup(1)(13)), (SCard(1)(14)(1)), (Sup(1)(15)))| & |(Sup(1)(4)) leqL (Sup(1)(13))| & |(SCard(1)(5)(1)) leqC (SCard(1)(14)(1))| & |(Sup(1)(6)) leqU (Sup(1)(15))| & OK \\ + |((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9))) (Sub(=>=)(s)) ((Sup(1)(22)), (SCard(1)(23)(1)), (Sup(1)(24)))| & |(Sup(1)(7)) leqL (Sup(1)(22))| & & |(Sup(1)(9)) leqU (Sup(1)(24))| & OK \\ + |((Sup(1)(10)), (SCard(1)(11)(1)), (Sup(1)(12))) =>= ((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33)))| & |(Sup(1)(10)) leqL (Sup(1)(31))| & |(SCard(1)(11)(1)) leqC (SCard(1)(32)(1))| & |(Sup(1)(12)) leqU (Sup(1)(33))| & OK \\ + |((Sup(1)(7)), (SCard(1)(8)(1)), (Sup(1)(9))) =>= ((Sup(1)(28)), (SCard(1)(29)(1)), (Sup(1)(30)))| & |(Sup(1)(7)) leqL (Sup(1)(28))| & |(SCard(1)(8)(1)) leqC (SCard(1)(29)(1))| & |(Sup(1)(9)) leqU (Sup(1)(30))| & OK \\ + |((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27))) =>= ((Sup(1)(4)), (SCard(1)(5)(1)), (Sup(1)(6)))| & |(Sup(1)(25)) leqL (Sup(1)(4))| & |(SCard(1)(26)(1)) leqC (SCard(1)(5)(1))| & |(Sup(1)(27)) leqU (Sup(1)(6))| & OK \\ + |((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21))) =>= ((Sup(1)(34)), (SCard(oneplus)(35)(oneplus)), (Sup(*)(36)))| & |(Sup(1)(19)) leqL (Sup(1)(34))| & |(SCard(oneplus)(20)(oneplus)) leqC (SCard(oneplus)(35)(oneplus))| & |(Sup(*)(20)) leqU (Sup(*)(36))| & OK \\ + |((Sup(1)(40)), (SCard(1)(41)(oneplus)), (Sup(*)(42))) \*/ ((Sup(1)(43)), (SCard(1)(44)(oneplus)), (Sup(*)(45)))| & |(Sup(1)(40)) `max` (Sup(1)(43)) leqL (Sup(1)(19))| & |{(Sub(1)(41)), (Sub(1)(44))} `isSplit` (Sub(oneplus)(20)) && (Sub(oneplus)(20)) === (Sub(oneplus)(20)) === (Sub(oneplus)(20)))| & |(Sup(1)(42)) + (Sup(1)(45)) leqU (Sup(1)(21))| & OK \\ + | <= ((Sup(1)(19)), (SCard(oneplus)(20)(oneplus)), (Sup(*)(21)))| & & & & \\ + |((Sup(1)(37)), (SCard(1)(38)(1)), (Sup(1)(39))) <= ((Sup(1)(25)), (SCard(1)(26)(1)), (Sup(1)(27)))| & |(Sup(1)(37)) leqL (Sup(1)(25))| & |{(Sub(1)(38))} `isSplit` (Sub(1)(26)) && (Sub(1)(38)) === (Sub(1)(26))| & |(Sup(1)(39)) leqU (Sup(1)(27))| & OK \\ + |((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(37)), (SCard(1)(38)(1)), (Sup(1)(39)))| & |(Sup(1)(46)) leqL (Sup(1)(37))| & & |(Sup(1)(48)) leqU (Sup(1)(39))| & OK \\ + |((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48))) (Sub(=>=)(s)) ((Sup(1)(40)), (SCard(1)(41)(oneplus)), (Sup(*)(42)))| & |(Sup(1)(46)) leqC (Sup(1)(40))| & & |(Sup(1)(48)) leqU (Sup(*)(42))| & OK \\ + |((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(46)), (SCard(1)(47)(1)), (Sup(1)(48)))| & |(Sup(1)(31)) leqL (Sup(1)(46))| & & |(Sup(1)(33)) leqU (Sup(1)(48))| & OK \\ + |((Sup(1)(31)), (SCard(1)(32)(1)), (Sup(1)(33))) (Sub(=>=)(s)) ((Sup(1)(43)), (SCard(1)(44)(oneplus)), (Sup(*)(45)))| & |(Sup(1)(13)) leqL (Sup(1)(43))| & & |(Sup(1)(33)) leqU (Sup(*)(45))| & OK \\ \end{tabular} - All constraints are satisfied, so the annotated program is properly annotated. But this is not the only annotated program that satisfies the - above constraints. For example, set all annotations to |*| and verify that constraints still hold. However, set - some annotations to |0| to find out that not all combinations are allowed. In the next chapter, we determine - a least solution to the constraints, which means a least upper bound, a highest lower bound, and a most precise - usage annotation. + The relation |leqL| should be interpreted as the relation |>=| on natural numers. The relation |leqU| as |<=| on natural numbers. The |leqC| + relation is somewhat complicated. For the left component in the cardinality annotation, the |leqC| relation specifies 'is more specific', + and for the right component the relation is equality modulo coercion. We cover these relations in more detail in Section~\ref{sect.TpAnnConstr}. + + All constraints are satisfied, so the program was properly annotated. But this is only one of the annotated programs that satisfies the + above constraints. For example, take |0| for all lower bounds, |(Card(*)(*))| for all cardinalities, and |*| for all upper bounds and verify that + the constraints are satisfied. However, set lower bounds to |0|, cardinalities to |(Card(0)(0))|, and upper bounds to |0|, and verify that some + constraints are violated. - The remainder of this chapter delves more precisely into each subject that is encountered in this section. + In the next chapter, we determine a least solution to the constraints, which means a least upper bound, a highest lower bound, + and a most precise usage annotation. The remainder of this chapter delves more precisely into subjects encountered in this section. \section{Language} \label{sect.ExprLanguage} @@ -545,7 +552,12 @@ the lower bound %%] We assume that all programs are correctly typed according to the type - system in Figure~\ref{RulerUniquenessExamples.E.expr.base}. + system in Figure~\ref{RulerUniquenessExamples.E.expr.base}. In this specification of the type + system, |Gamma| is the evironments that constains a type for each identifier + in scope, and |tau| represents types. An integer expression has type |Int|. The type of a variable is recorded in the + environment. The result and operands of an addition are |Int|s. When applying a function to a value, the parameter + type and argument type should unify. Finally, a lambda abstraction brings the type of an identifier in scope, which + means into the environment |Gamma| of the body. \rulerCmdUse{RulerUniquenessExamples.E.expr.base} @@ -558,71 +570,249 @@ the lower bound attached to type constructors: %%[[wrap=code - utau ::= Sup(Int)((low,use,up)) -- tycon int (Int) - | Sup((->))((low,use,up)) -- tycon arrow (Arrow) - | utau utau -- type application (App) + utau ::= Sup(Int)((LowerBound,c,UpperBound))) -- tycon int + | Sup(->)((LowerBound,c,UpperBound)) -- tycon arrow + | utau utau -- type application + + c ::= (Card(Usage)(Usage)) -- cardinality annotation + LowerBound ::= 1 | 0 -- lower-bound usage-count annotation + UpperBound ::= 0 | 1 | * -- upper-bound usage-count annotation + Usage ::= 0 | onemin | 1 | oneplus | * -- cardinality annotation +%%] + + Why annotate the type constructors? Types describe the structure of a value in + a concise way. A type constructor corresponds with a certain area of memory. + For example, the |Int| type constructor represents all bits of an integer value. + But in |List Int| (algebraic data types are introduced later in this master's thesis, Chapter~\ref{chapt.DataTypes}), + the |List| type constructor represents the spine of a list, and the |Int| type constructor + represents each element of the list (Figure~\ref{fig.ListRep}). + +\begin{figure} +\caption{Representation of a |List| in memory} +\label{fig.ListRep} +\includegraphics[width=12cm]{list-rep} +\end{figure} + + Each bit of the list belongs to a single type constructor, the \emph{corresponding} + type constructor. The cardinality of a single bit, is the cardinality of the + corresponding type constructor. Or, the other way around, the cardinality of a + type constructor is the \emph{join} over all the cardinalities of the bits that correspond + to the type constructor. So, the reason is that the type constructors allow us to specify + cardinalities of bits in a concise way, although we loose the ability give different + cardinalities to bits represented by the same type constructor. + + A related question is: why is the arrow type constructor annotated? There are + several reasons. From a practical view considering code generation: functions + are also values: \emph{closures}. Such a value is represented by an area of + memory, and can have a cardinality like any other value. From a more + theoretical point of view, functions that are used exactly once have the property that they can + be safely inlined~\cite{Wansbrough:PhDThesis}. So, the arrow type constructor + requires an annotation as well. + + \subsection{The annotations} + \label{sect.partialorderings} + + The lower-bound usage-count annotation |LowerBound| on a type constructor of a type originating from + expression |E|, specifies that the value of |E| is used at least |0| or |1| times via + |E|. A lower bound of |0| means that there is no guarantee that the value is used via |E|. + The |LowerBound| values are totally ordered with |1 leqL 0|\footnote{All the |leq| relations that we define are partial orders.}. Note that the + relation |leqL| corresponds to the relation |>=| if the |LowerBound| values are considered natural + numbers. We use this relation later to specify that when we know that |E| uses its value at least + once, that we are allowed to forget it and think that we do not have any guarantee about how often + the value of |E| is used. The definition of lower bound values can be generalised to lower + bounds up to some value |k|, but we will not complicate this description with this generalisation. + + The upper-bound usage-count annotation |UpperBound| is the dual to the lower-bound usage-count + annotation. It specifies that the value of |E| is used at most |0|, |1|, or |*| times via + |E|. An upper bound of |0| means that the value of |E| is never used via |E|. An upper bound of + |1| specifies that |E| used its value at most once. It can occur that the value of |E| is never + used via |E|, but an upper bound of |1| does not guarantee that. However, it does guarantee that + |E| is not used twice or thrice via |E|. Finally, an upper bound of |*| means that the value of + |E| is used an arbitrary number of times via |E|, but probably twice or more. The |UpperBound| + values are totally ordered with: |0 leqU 1| and |1 leqU *|. + The |<=| relation on natural numbers corresponds to the above relation. The above relation is used in + the checks to allow relaxation of an upper bound to a higher upper bound. + + The cardinality annotation consists of two |Usage| values. The left |Usage| value defines the + usage of the value via |E|, and the right |Usage| value defines the total usage of the + value. The left |Usage| value must fit the two bounds (Figure~\ref{code.FitsInBounds}). The + right |Usage| value is at most as specific as the left |Usage| value. + + We define several orderings on |Usage| values. We start with an ordering that is used in + the definition for consistency of cardinality annotations. If |a leqX b| then |a| does not + conflict with |b|. There is a conflict when the left |Usage| value specifies that the + value is used at least |k| times and the right |Usage| value specifies that the value is + used strictly less than |k| times. For example, |a = 1| and |b = 0| conflict. The following + partial order defines when two values do not conflict (see Figure~\ref{fig.conflict}): + +%%[[wrap=code + 0 leqX onemin + 0 leqX oneplus + 1 leqX oneplus + onemin leqX oneplus + onemin leqX * + oneplus leqX * +%%] + +\begin{figure} +\caption{The does-not-conflict semi-lattice} +\label{fig.conflict} +\begin{center} +\includegraphics{conflict-lattice} +\end{center} +\end{figure} + + If the left-hand side of a cardinality annotation is |*|, then the only possibility is + |*| for the right-hand side. If we do not know the usage of one particular occurrence + of some value, then we neither know it for the aggregation of all occurrences. Another + interesting example is |onemin leqX oneplus|. A specific occurrence of a value can + be used at most time, but then it is still possible that the value is in total + guaranteed to be used more than once. + + Furthermore, we have a partial order for checking that one |Usage| value is more + specific than another |Usage| value. If |a leqQ b|, then |a| is more specific than + |b|. It is defined as follows (see also Figure~\ref{fig.specificness}): - low ::= 0 | 1 -- lower-bound usage-count annotation - use ::= 0 | onemin | 1 | oneplus | * -- cardinality annotation - up ::= 0 | 1 | * -- upper-bound usage-count annotation +%%[[wrap=code + 0 leqQ onemin + onemin leqQ * + 1 leqQ oneplus + oneplus leqQ * %%] - The lower-bound usage-count annotation specifies that a value represented - by the annotated type constructor, is at least used |0| or |1| times. The - upper-bound usage-annotation specifies that a value represented by the annotated type constructor, - is at most used |0|, |1|, or an arbitrary number of times. The cardinality annotation specifies a - usage property for a value. For example, the cardinality annotation |onemin| means - that the corresponding value is at most used once. +\begin{figure} +\caption{A semi-lattice on specificness of |Usage| values} +\label{fig.specificness} +\begin{center} +\includegraphics{specific-lattice} +\end{center} +\end{figure} - When we write that a variable is \emph{used}, we actually mean that the memory that - is represented by the value is touched, either for reading or for writing. If a - value has a lower-bound usage count of |1|, then we know that its memory is - at least touched once. If it has an upper-bound usage count of |0|, the memory - is never touched, altough there may be references to it during program execution. Such - references are never evaluated though. + The above ordering is used in Chapter~\ref{Chapt.Polyvariance} to specify which right-hand side + values of a cardinality annotation are preferable over others. |Usage| values of |0| and + |1| are preferable over |onemin| or |*| because it is more precise. - Why annotate the type constructors? Consider how a value is represented in - memory. The type constructors of a type partition the memory representation - of a value. Each area of memory for a certain value is associated with a - single type constructor in the corresponding type. We get the usage - properties of an area of memory by looking at the annotations on the - corresponding type constructor. + Similar to|leqQ| is |leqP|, which also specify that one |Usage| value is more specific + than another |Usage| value, but then for the left-hand side values of cardinality annotations: - Another question is: why is the arrow type constructor annotated? There are - several reasons. From a practical view considering code generation: functions - are also values: \emph{closures}. Such a value is represented by an area of - memory, and can be unique or shared like any other value. From a more - theoretical point of view, unique functions have the property that they can - be safely inlined~\cite{Wansbrough:PhDThesis}. So, the arrow type constructor is - annotated as well, like any other value. - - A type constructor gets a triple with three annotations: a lower-bound usage-count annotation, - a cardinality annotation, and an upper-bound usage-count annotation. The values of - the two bound annotations are totally ordered (|0 <= 1 <= *|). Cardinality annotations are partially - ordered, but almost incomparable: |0 <= 0, onemin <= onemin, onemin <= *, 1 <= 1, oneplus <= oneplus, * <= *|. Only - a value that is at most used once can be weakened to a value that is used an arbitrary number - of times. This is where the term coercion comes from. The fact that a value is used at most once - may be forgotten, but can require the insertion of some coercion function, depending on the - optimizations of the back-end. For example, the code generator can choose to generate code that - allocates values that are used at most once on a compile-time garbage-collected heap, and insert a - coercion functionthat moves the value to a runtime garbage-collected heap when the restriction - that a value is used at most once is forgotten. - - A triple is consistent if the cardinality annotation fits into the boundaries given by the two boundary - annotations. See Figure~\ref{code.FitsInBounds} for a specification of a cardinality - annotation fitting between the two boundary annotations. +%%[[wrap=code + 0 leqP * + onemin leqP * + 1 leqP * + oneplus leqP * +%%] + + The rationale behind this ordering is that the join between two left-hand side + values of a cardinality annotation, does not violate the lower bound and upper bound corresponding + to these values. + + Furthermore, we define an ordering for coercions on the right-hand side |Usage| values of + a cardinality annotation. A value with a total usage of |u| may be relaxed into a + value with total usage |u'| (denoted by |u' leqZ u|) if there is a coercion function that changes a value + with usage of |u| to a value with usage |u'|, such that optimisations of the compiler + are still valid. + + For example, we can coerce a value with total usage of |onemin| to + a value with total usage of |*| by means of the identity function if we assume that + the the compiler only uses cardinality annotations to insert code for destructive + updates on unique values. The reason for this particular example is that due to the + fact that the coercion is the first use of the value, that there can only be unused + references (besides the coercion) to the value that consider it to be used at most once. + And after the coercion, any active reference assumes that the value is used in an + arbitrary way, such that no inplace updates can be performed on it. On the other hand, + if the compiler generates code that allocates values with a total usage of |onemin| on + a special compile-time garbage collected heap, then such a coercion is not allowed, + unless there is an coercion function inserted into the generated code that copies the + value to a normal garbage collected heap. + + So, it depends on optimisations of the compiler and the availability of coercion function, + to allow certain coercions between right-hand side annotations of cardinality annotations. + Therefore, by default |leqZ| is an equality relation, but we assume that it can be a + subset of the |leqS| with left and right arguments swapped. Note that |a leqZ b| defines + that the total usage |b| can be relaxed by coercion in total usage |a|. This is the inverse direction compared to the other + orderings in this section. This is intential: the two bound annotations and the + left-hand side value of a cardinality annotation combine usage information of individual + occurrences of a value into usage information about the total usage of some value. Subsequently, + this aggregate result is passed back to the individual occurrences via the right-hand side + value of the cardinality annotations. We are only allowed to forget some property about the + total usage of a value, if our uses of the value do not conflict with optimized uses of the + value at other places, possibly by doing some additional administrative work (the coercion). + + We define a similar ordering as the ordering above for left-hand side of a cardinality + annotation is relaxed. If |a leqS b|, then |a| can be relaxed to |b|. This ordering + is typically an equality relation, unless a relaxation does not conflict with optimisations + of the backend or can be resolved using a coercion function. + + Or in other words: we can relax the left-hand side of a cardinality annotation only + to |*|. However, there is an important restriction here: if we make a relaxation for + one particular occurrence of some value, then we must make this relaxation for all + anotations of this particular occurrence. For example, + + Finally, we define an ordering to verify that the right-hand side of a + cardinality annotation does not conflict with the left-hand side of a cardinality + annotation: + +%%[[wrap=code + leqB :: LowerBound -> UpperBound -> Bool + 0 leqB _ = True + 1 leqB u = 1 leqU u + _ leqB _ = False +%%] + + The orderings on the left-hand side and right-hand side of a cardinality annotation can be + combined into a single ordering on cardinality annotations as a whole: + +%%[[wrap=code + (Card(a)(b)) leqC (Card(c)(d)) + = a leqS c + && b leqZ d + && a leqB b + && c leqB d +%%] + + \subsection{Triple consistency} + + A triple is consistent if the left-hand side of the cardinality annotation fits into the boundaries given by the two boundary + annotations, and the left-hand side of the cardinality annotation is consistent with the right-hand side. See Figure~\ref{code.FitsInBounds} for a specification. + We do not allow a |Usage| value that might violate the bounds. For example, the |Usage| value |oneplus| is not allowed when the upper bound is |0| or |1|, because + `at least zero' or 'at least once' does not guarantee that the upper bound is violated. We make one exception to this rule for |*|. + It always fits the bounds. We know that once |*| has been derived for an individual occurrence of a value, that the value in total + will have a |Usage| value of |*|. Nowhere in the program can guarantees be made about a value with |Usage| value of |*|, so the + bounds can be ignored for this value. Strictly speaking, this is not required: we could enforce a stronger notion of fitting and require that the boundaries itself are relaxed to + |0| for the lower bound or |*| for the upper bound when the |Usage| value is |*|. However, in Chapter~\ref{chapt.Polyvariant}, we present an + approach that infers the annotations, and the above relaxation allows us to infer lower and upper bounds seperately from the cardinality annotations + (Figure~\ref{code.iterate}). \begin{figure} - \caption{Consistency of tripples} + \caption{Consistency of triples} \label{code.FitsInBounds} %%[[wrap=code - fits (0, 0, 0) = True - fits (1, 1, 1) = True - fits (1, oneplus, h) = h >= 1 - fits (_, onemin, 1) = True - fits (l, *, h) = l <= h - fits (_, _, _) = False + trippleConsistent (a, (Card(b)(c)), d) + = a `leftFit` b + && b `rightFit` d + && b leqX c + && a leqB d +%%] +\\ +%%[[wrap=code + leftFit :: LowerBound -> Usage -> Bool + leftFit 0 _ = True -- bound gives no info + leftFit _ * = True -- `don't know' fits bounds + leftFit 1 1 = True + leftFit 1 oneplus = True + leftFit _ _ = False +%%] +\\ +%%[[wrap=code + rightFit :: Usage -> UpperBound -> Bool + rightFit _ * = True -- bound gives no info + rightFit * _ = True -- `don't know' fits bounds + rightFit 0 1 = True + rightFit 1 1 = True + rightFit onemin 1 = True + rightFit 0 0 = True + rightFit _ _ = False %%] \end{figure} @@ -635,21 +825,22 @@ the lower bound There are three types of constraints for the type system in this chapter: %%[[wrap=code - constr ::= (low,use,up) =>= (low,use,up) -- coercion - | (low,use,up) (Sub(=>=)(s)) (low,use,up) -- coercion (ignores use) - | (low,use,up) \*/ ... \*/ (low,use,up) <= (low,use,up) -- aggregation + constr ::= (LowerBound,c,UpperBound) =>= (LowerBound,c,UpperBound) -- coercion + | (LowerBound,c,UpperBound) (Sub(=>=)(s)) (LowerBound,c,UpperBound) -- coercion (ignores use) + | (LowerBound,c,UpperBound) \*/ ... \*/ (LowerBound,c,up) <= (LowerBound,c,UpperBound) -- aggregation %%] As demonstrated in the examples, the coercion constraint (|=>=|) is used to propagate usage - information. It specifies that the lower bound on the left-hand side is greater - than the lower bound on the right-hand side. Vice versa, it specifies that - the upper bound on the left-hand side is smaller than the upper bound on the - right-hand side. Finally, it specifies that the two cardinality values are equal, - unless the left-hand side can be coerced into the right-hand side. + information. It specifies that the lower bound on the left-hand side is greater or equal + than the lower bound on the right-hand side (|left \leqL right|). Vice versa, it specifies that + the upper bound on the left-hand side is smaller or equal to the upper bound on the + right-hand side (|left \leqU right|). Finally, it specifies how the cardianlity annotations + are relaxed: for the left-hand side |Usage| value from left to right, and for the right-hand side + |Usage| value from right to left. In the last case only when there is a coercion. With the coercion constraint, we essentially check that all boundary information is properly propagated from outermost expression to innermost expression, from - body to parameters. The usages of values bound to identifiers, are treated separately + body to parameters. The cardinalities of values bound to identifiers are treated separately for each use-site of an identifier and added to each other by using the aggregation constraint |\*/|. Section~\ref{Sect.CheckingConstraints} describes how the constraints are checked. @@ -665,7 +856,8 @@ the lower bound \rulerCmdUse{RulerUniquenessExamples.U1.prog.base} The type rule for the whole program (Figure~\ref{RulerUniquenessExamples.U1.prog.base}) states that the resulting expression has a lower and upper bound of |1|. By assuming - that all the triples are consistent, this means that the resulting expression can have an arbitrary usage value (except not 0). We pattern + that all the triples are consistent, this means that the resulting expression is allowed to have a cardinality of which the left-hand side + is either |1| or |*|, although the total cardinality may be any |Usage| value except |0|. We pattern match on the annotated type of the expression to obtain the annotation |delta| on the outermost type constructor and generate a constraint that specifies that the lower bound is at least |1| and the upper bound is at most |1|. This constraint, and the constraints gathered from the expression itself, must be satisfied for the program to be valid according to @@ -674,18 +866,26 @@ the lower bound Types are written in two ways in the type rules. A type written as |utau| has annotations. A type written as |tau| has no annotations. We sometimes write |(Sub(tau)(a))| to refer to the unannotated version of |(Sub(utau)(a))|. A |utau| is also denoted as |Sup(tau)(delta)|, where |delta| is the outermost\footnote{In this chapter, this is the - triple on the outermost type constructor of the type expression. In the presence of data type, this is the outermost + triple on the outermost type constructor of the type expression. In the presence of algebraic data types, this is the outermost annotation on the result-kind of the type expression.} annotation. + The structure of the type rules of Figure~\ref{RulerUniquenessExamples.U1.expr.base} is as follows. |Gamma| represents an environment that contains bindings from identifier to (unannotated) + type. The |e| stands for an expression with the annotated type |utau|. Finally |zeta| stands for a set of generated constraints. + + A few words on syntax: we write |(Sub(zeta)(1)) (Sub(zeta)(2))| to denote a constraint set obtained by taking the union of + |(Sub(zeta)(1))| with |(Sub(zeta)(2))|. We write |(Sub(tau)(a)) <=> (Sub(tau)(b))| for the unification of |(Sub(tau)(a))| + with |(Sub(tau)(b))|. Finally, unbound identifiers such as |delta| in the |Var| and |Lam| rule, specify that there are + no limitations on that identifier. + \rulerCmdUse{RulerUniquenessExamples.U1.expr.base} - Constraints for an expression are gathered by a traversal over the expression, as is described by Figure~\ref{RulerUniquenessExamples.U1.expr.base}. + Constraints for an expression are gathered by a syntax directed traversal over the expression. The case for integers is the easiest: integers can be produced for any usage annotation and nothing has to be checked for them. We neither have to check anything for the use-sites of identifiers, since we deal with these identifiers in the case for lambda abstraction. The case for integer addition is slightly more complicated. Aside from consistency, there are no demands on the uniqueness component of the result of the addition. On the other hand, we check that the upper and lower bound annotations of the parameters are - properly propagation from result of the addition to the arguments of the addition. For that, a |(Sub(=>=)(s))| constraint is generated + properly propagated from result of the addition to the arguments of the addition. For that, a |(Sub(=>=)(s))| constraint is generated between the triple on the result type and the triples on the argument types. The function application is perhaps the most difficult case in the uniqueness type system. Three things have to be done: check @@ -699,7 +899,7 @@ the lower bound function result and result, are properly connected. Note that variance plays a role here: the direction of an argument of a function is the opposite to the result of the function. Suppose that a function |f| is passed to function |g| as parameter, then |g| applies the function, and passes some argument |x|. Propagation is from |x|, to the parameter of |g|, and inside |g| to the result-value of |g|. The - flow of boundaries and usage information for such an annotation is the other way around than the usual flow. In Figure~\ref{RulerUniquenessExamples.U1.flow.base} we list the + propagation of boundaries and usage information for such an annotation is the other way around than the usual flow. In Figure~\ref{RulerUniquenessExamples.U1.flow.base} we list the type rules that walk over the type and generate the |=>=|-constraints for each two corresponding annotations in the proper direction. \rulerCmdUse{RulerUniquenessExamples.U1.flow.base} @@ -723,7 +923,7 @@ the lower bound %%[[wrap=code satisfied :: Check satisfied (a =>= b) = a `coercionSatisfied` b -satisfied (a (Sub(=>=)(s)) b) = a `weakCoercionSatisfied` b +satisfied (a (Sub(=>=)(s)) b) = a `softCoercionSatisfied` b satisfied ((Sub(a)(1)) \*/ ... \*/ (Sub(a)(2)) <= a) = [(Sub(a)(1)) ... (Sub(a)(n))] `aggregationSatisfied` a %%] @@ -736,9 +936,12 @@ satisfied ((Sub(a)(1)) \*/ ... \*/ (Sub(a)(2)) <= a) = [(Sub(a)(1)) ... (Sub(a %%[[wrap=code coercionSatisfied (a, b, c) (d, e, f) - = a >= d && e <= b && c <= f -weakCoercionSatisfied (a, b, c) (d, e, f) - = a >= d && c <= f + = a leqL d + && b leqC e + && c leqU f +softCoercionSatisfied (a, b, c) (d, e, f) + = a leqL d + && c leqU f %%] This constraint is generated in such a way that we may weaken what we know of the @@ -751,20 +954,25 @@ weakCoercionSatisfied (a, b, c) (d, e, f) \subsection{Aggregation constraint} For the aggregation constraint, we conservatively approximate the upper and lower bound. Things - are a bit more complicated for the cardinality annotation. We check that the usage annotation - is properly split up to the individual use sites (Figure~\ref{splitFunc}). We mean with this that if a value - is linear, that one use site is linear and all the other use sites are not used at all. - Figure~\ref{code.sumsat} defines when an aggregation constraint is satisfied. + are a bit more complicated for the cardinality annotation. We check that the left-hand side of the cardinality annotation + is properly split up to the individual use sites (Figure~\ref{splitFunc}) and that the right-hand side is equal for + all use-sites. We mean with this that if a value is linear, that the left-hand side of the cardinality annotation is + linear for one use site, and not used for the other use sites. For the right-hand side of the cardinality, we check that + that all use-sites consider the total usage of the value to be linear. See Figure~\ref{code.sumsat} for the + definition. \begin{figure} \caption{The isSplit function.} \label{splitFunc} - %%[[wrap=code isSplit as 0 = all (== 0) as -isSplit as 1 = let (eq0, neq0) = partition (== 0) as - in length neq0 == 1 && head neq0 == 1 -isSplit as oneplus = length as > 0 && any (== oneplus) as && all (/= 0) as && all (/= 1) as +isSplit as 1 = let (eq0, neq0) = partition (== 0) as + in length neq0 == 1 + && head neq0 == 1 +isSplit as oneplus = length as > 0 + && any (== oneplus) as + && all (/= 0) as + && all (/= 1) as isSplit as onemin = all (== onemin) as isSplit as * = all (== *) as %%] @@ -773,12 +981,12 @@ isSplit as * = all (== *) as \begin{figure} \caption{aggregation constraint satisfaction} \label{code.sumsat} - %%[[wrap=code -aggregationSatisfied [((Sub(a)(1)), (Sub(b)(1)), (Sub(c)(1))), ..., ((Sub(a)(b)), (Sub(b)(n)), (Sub(c)(n)))] (a, b, c) - = (Sub(a)(1)) `max` ... `max` (Sub(a)(n)) >= a - && (Sub(c)(1)) + ... + (Sub(c)(n)) <= c +aggregationSatisfied [((Sub(a)(1)), (Card(Sub(b)(1))(Sub(c)(1))), (Sub(d)(1))), ..., ((Sub(a)(n)), (Card(Sub(b)(n))(Sub(c)(n))), (Sub(d)(n)))] (a, (Card(b)(c)), d) + = (Sub(a)(1)) `max` ... `max` (Sub(a)(n)) leqL a && isSplit [(Sub(b)(1)), ..., (Sub(b)(n))] b + && (Sub(c)(1)) === ... === (Sub(c)(n)) + && (Sub(d)(1)) + ... + (Sub(d)(n)) leqU d %%] \end{figure} @@ -796,16 +1004,34 @@ aggregationSatisfied [((Sub(a)(1)), (Sub(b)(1)), (Sub(c)(1))), ..., ((Sub(a)(b)) lower bounds instead of the maximum (note the duality here). We discuss this subject in Chapter~\ref{chapt.Parallel}. +\section{Strictness?} + + As we mentioned in Chapter~\ref{chapt.Introduction}, we can also infer strictness with our approach. Strictness is + defined as follows: consider a function |f = \x -> ...| and the application |r = f bottom|. If reduction of |r| to + weak-head normal form results into |bottom|, then |f| is strict in |x|. + + After performing the analysis that we explained in this chapter, we know from some parameters that they are + used. This information almost tells us that the parameters are strict, but not entirely: in our analysis it is + possible that we consider a value used because the result of the function is reduced further than weak-head + normal form. + + But, we can obtain strictness properties of a function |f| with result type |r|. Suppose we only have the expression + of |f|. If we use |(1, (Card(1)(oneplus)), 1)| for the outermost annotation on |r| and |(0, (Card(0)(0)), 0)| for + all other annotations of |r|, and expect a valid annotation, then |f| is strict in those parameters that can have a + cardinality annotation with |oneplus| or |1| as left-hand side value. An optimisation is that we can |seq| the + parameters before applying them to the function. The annotations on the types further specify how deep the + |seq| function can evaluate the value. + \section{Conclusion} We showed in this chapter what we mean with uniqueness typing, be it with a simple language. Our approach - consists of a set of type rules that specify when a program is correctly annotated with coercion annotations. - We turn this problem into a constraint satisfaction problem, which gives us a separation between the + consists of a set of type rules that specify when a program is correctly annotated with cardinality annotations. + We turned this problem into a constraint satisfaction problem, which gives us a separation between the gathering of the constraint and the checking of them. In the next chapter, we show that the - constraints also allow us to \emph{infer} coercion annotations, instead of requiring that they are supplied + constraints also allow us to \emph{infer} cardinality annotations, instead of requiring that they are supplied by the programmer. - In this chapter, we also told that usage annotations are not sufficient. We required lower-bound and upper-bound annotations - as well. In the next chapter, we switch to inferring uniqueness properties, and there we infer these bounds as well. + In this chapter, we also told that cardinality annotations are not sufficient. We required lower-bound and upper-bound annotations + as well. In the next chapter, we switch to inferring cardinality properties, and there we infer these bounds as well. %%] diff --git a/EHC/text/uniqueness/TopicPolyvariant.cltex b/EHC/text/uniqueness/TopicPolyvariant.cltex index 3c13fe04e..33dc46cb4 100644 --- a/EHC/text/uniqueness/TopicPolyvariant.cltex +++ b/EHC/text/uniqueness/TopicPolyvariant.cltex @@ -3,7 +3,7 @@ \chapter{Polyvariant analysis with monomorphic bindings} \label{chapt.Polyvariant} -In the previous chapter, we generate constrains from an annotated program, and call the annotations valid if and only if +In the previous chapter, we generate constraints from an annotated program, and call the annotations valid if and only if the constraints are satisfied. In this chapter, we take a closer look at the constraints. We take a validly typed, but not annotated, program and decorate the type constructors with \emph{cardinality variables} |delta| instead of concrete annotations. Then we generate the set of constraints, which now contain variables instead of concrete values. A solution @@ -12,15 +12,15 @@ a whole family of solutions. In this chapter, we discuss a technique that infers constraints (Section~\ref{sect.TheMinimalSolution}). To make this chapter slightly more challenging, we add a monomorphic and non-recursive |let| to the expression language defined -in Chapter~\ref{chapt.NoBindings}. With the existence of cardinality variables, we turn the analysis into a polyvariant analysis, which +in Chapter (Section~\ref{chapt.NoBindings}). With the existence of cardinality variables, we turn the analysis into a polyvariant analysis, which means that we infer a most general uniqueness typing for a binding, and allow different instantiations for each use of an identifier. This chapter is organized as follows. We illustrate the concept of cardinality inference by an example. -Then we go into the concept of the type inference process~\ref{sect.TheInferencer}. We follow this up with a discussion about +Then we go into the concept of the type inference process (Section~\ref{sect.TheInferencer}). We follow this up with a discussion about the addition of bindings to the expression language, and consequently the concept of binding groups and instantiation~\ref{sect.Instantiation}. The constraints play an important role here, but we go to yet another representation: -the constraints are rewritten to a graph-representation on which we can perform graph rewriting~\ref{sect.Rewriting} to +the constraints are rewritten to a graph-representation on which we can perform graph reduction (Section~\ref{sect.Rewriting}) to simplify the constraints. @@ -28,36 +28,35 @@ simplify the constraints. \label{sect.ExamplePoly} A type can now have cardinality variables as annotations. Upper and lower-bound cardinality annotations do not exist anymore, -but are used internally by the constraint solver. The following example demonstrates some annotated types and constraint +but are used internally by the inferencer. The following example demonstrates some annotated types and constraint sets: %%[[wrap=code f :: forall (Delta(1)) . (Annot(Int)(1)) -g :: forall (Delta(1)) . (Annot(Int)(1)), onemin =>= (Delta(1)) +g :: forall (Delta(1)) . (Annot(Int)(1)), (Card(onemin,*)) =>= (Delta(1)) h :: forall (Delta(2)) . (Annot(Int)(2)) (Annot(->)(2)) (Annot(Int)(2)) -j :: forall (Delta(3))(Delta(4))(Delta(5)) . (Annot(Int)(4)) (Annot(->)(3)) (Annot(Int)(5)), (Delta(5)) =>= (Delta(4)), (Delta(5)) =>= (Delta(3)) +j :: forall (Delta(3))(Delta(4))(Delta(5)) . (Annot(Int)(4)) (Annot(->)(3)) (Annot(Int)(5)), (Delta(5)) =>= (Delta(4)), (Delta(5)) (Sub(=>=)(s)) (Delta(3)) %%] All cardinality variables are universally quantified, but are constrained by a constraint set. For example, |f| represents -a value with a type that has an unconstrained annotation |(Delta(1))|. This annotation can be instantiated with any of -the five cardinality annotations. The annotation on the type of |g| can only be |(Sub(Int)(onemin))| and |(Sub(Int)(*))|, -since the annotations |0|, |oneplus| and |1| are not allowed according to the constraint (Section~\ref{Sect.CheckingConstraints}). -The type of |h| corresponds to a function that may have any of the five cardinality values as long as the function, the argument, -and the result type have the same cardinality value. The three annotations of the type of |j| can have any cardinality value -as long as the two coercions are satisfied. +a value with a type that has an unconstrained annotation |(Delta(1))|. This annotation can be instantiated with any consistent +cardinalty value. The annotation on the type of |g| can only be |(Card(onemin)(*))|, or |(Card(*)(*))|, since the +constraint disalows other combinations (Section~\ref{Sect.CheckingConstraints}). The type of |h| corresponds to a function +that may have any of the five cardinality values as long as the function, the argument, and the result type have the same cardinality value. +The three annotations on the type of |j| can have any cardinality value as long as the two coercions are satisfied. We annotate a program with cardinality variables, perform the constraint gathering of the previous chapter, and -perform cardinality inference on the constraints. +perform cardinality inference on the constraints. We remark that a cardinality annotation is a cardinality +variable (i.e. |delta|), and a concrete cardinality annotation is a cardinality value (i.e. |(Card(1)(*))|). -The first step is to take a typed program and annotate it: +The first step in this process is to take a typed program and annotate it with fresh annotations: %%[[wrap=code (\x -> x) 3 ((\(x :: Int) -> x :: Int) :: Int -> Int) (3 :: Int) :: Int %%] -Each type constructor in the types is annotated with a fresh -cardinality variable (the |x| parameter gets its annotation from +Each type constructor in the types is annotated with a fresh cardinality variable (the |x| parameter gets its annotation from the type of the function). %%[[wrap=code @@ -65,35 +64,42 @@ the type of the function). ((\(x :: (Annot(Int)(1))) -> x :: (Annot(Int)(2))) :: (Annot(Int)(3)) (Annot(->)(4)) (Annot(Int)(5))) (3 :: (Annot(Int)(6))) :: (Annot(Int)(7)) %%] -Constraint gathering of Section~\ref{Sect.ConstraintGathering} results into the following constraints: +Constraint gathering of Section~\ref{Sect.ConstraintGathering} results in the following constraints: %%[[wrap=code -(1,bottom,0) (Sub(=>=)(s)) (Delta(7)) -- root of the expression -(Delta(7)) =>= (Delta(5)) -- function application to function result -(Delta(7)) (Sub(=>=)(s)) (Delta(4)) -- function application to function spine -(Delta(3)) =>= (Delta(6)) -- function parameter to function type -(Delta(5)) =>= (Delta(2)) -- function result to function body -(Delta(2)) <= (Delta(1)) -- aggregation of use-sites of |x| -(Delta(1)) =>= (Delta(3)) -- parameter to function +(1,(Card(1)(*)),0) (Sub(=>=)(s)) (Delta(7)) -- root of the expression +(Delta(7)) =>= (Delta(5)) -- function application to function result +(Delta(7)) (Sub(=>=)(s)) (Delta(4)) -- function application to function spine +(Delta(3)) =>= (Delta(6)) -- function parameter to function type +(Delta(5)) =>= (Delta(2)) -- function result to function body +(Delta(2)) <= (Delta(1)) -- aggregation of use-sites of |x| +(Delta(1)) =>= (Delta(3)) -- parameter to function %%] These constraints specify a whole family of solutions. A solution is a substitution that maps each cardinality -variable to a cardinality value and satisfies the constraints. The substitution that maps |*| to each -cardinality variable always satisfies the constraint. But in this case is a substitution that maps |1| or -|oneplus| to each cardinality variable also consistent with the constraints. Annotate the program with corresponding -upper and lower bound annotations and apply the constraint checking of the previous chapter if in doubt. - -The above constraints are passed to the constraint solver, which finds the least solution to the constraints. With a least -solution we mean a solution that is as specific as possible for each cardinality annotation. The annotations |1| and +variable to a cardinality value and satisfies the constraints. The substitution that maps each +cardinality variable to |(Card(*)(*))| always satisfies the constraint. But in this case, a substitution that maps +each cardinality variable to |(Card(1)(1))|, |(Card(1)(oneplus))|, or |(Card(oneplus)(oneplus))|, also satisfies +the constraints. Annotate the program with corresponding upper and lower bound annotations and apply the constraint +checking of the previous chapter if in doubt. + +The above constraints are passed to the inferencer (we call it the constraint solver), which infers the least solution to +the constraints. With a least Solution we mean a solution that is as specific as possible for each cardinality annotation +(see the ordering |leqS| in Section~\ref{sect.TpAnnConstr}). The |Usage| values |1| and |0| are the most specific (and mutual exclusive), the annotations |onemin| and |oneplus| annotations are in between (also -mutual exclusive) and |*| is the least specific annotation. There is exactly one least solution to the constraints. See -Section~\ref{sect.TheMinimalSolution} for a proof. Keep in mind that this solution is still a conservative approximation +mutual exclusive) and |*| is the least specific |Usage| value. There is exactly one least solution to the constraints (see +Section~\ref{sect.TheMinimalSolution} for a proof). Keep in mind that this solution is still a conservative approximation of the actual usage of a value. We obtain the solution as follows. Based upon the constraints, a lower and an upper bound is inferred for each cardinality -annotation. Then the most specific cardinality annotation that fits the bounds is chosen for each cardinality variable. Then -we check for each constraint if the cardinality values agree with the constraint, otherwise the cardinality values are made -less specific until they fit the constraints. This process is repeated until all cardinality values fit. +annotation. After the lower and upper bounds are inferred, we choose the most specific |Usage| value for both |Usage| +values of the cardinality annotations. We then relax (make them less specific according to |leqS|) the left-hand side and +right-hand side of the cardinality values independendly until they satisfy the constraints. A relaxation of the +left-hand side possibly leads to a relaxation of the right-hand side to keep the cardinality value consistent +(see |leqB| in Section~\ref{sect.partialorderings}). Satisfying one constraint by relaxing one of the |Usage| values of +a cardinality annotation, can cause a need for relaxation of the cardinalities of another constraint. This process is repeated +until all cardinality values satisfies the constraints. This process terminates since we cannot relax |Usage| values +beyond |*|. The upper and lower bound are obtained in a similar way. An initial substitution is created that maps the lower bound of each cardinality variable to |1|. Each coercion constraint that is not satisfied has a higher lower bound in the substitution @@ -101,8 +107,8 @@ for the right-hand side than the left-hand side. The constraint becomes satisfie right-hand side to the lower-bound of the left-hand side. An aggregation constraint that is not satisfied, becomes satisfied by changing the right-hand side to the result of the computation of the left-hand side. This process is repeated until all constraints are satisfied. The same process is performed for the right-hand side, except that we start with the -value |0|. Performing this approach on the constraints of the example results into lower-bound values of all |1| (none -of the constraints are satisfied to start with), and an upper bound values of |1| (some work had to be done for this one). +value |0|. Performing this approach on the constraints of the example results in lower-bound values of all |1| (none +of the constraints are satisfied to start with), and upper bound values of |1| (some work had to be done for this one). The most specific cardinality value that fits (Figure~\ref{code.FitsInBounds}) an upper bound and lower bound of |1|, is the value |1| (linear). A cardinality of |1| satisfies all the above constraints. The substitution |S (Delta(i)) = 1|, with |1 <= i <= 7| @@ -112,12 +118,11 @@ is a least solution to the constraints of the above example. \section{Cardinality variables and type rules} \label{sect.UniquenessVariables} -In contrast to previous chapter where the type constructors are annotated by a triple of annotations, we now only +In contrast to the previous chapter where the type constructors are annotated by a triple of annotations, we now only annotate the type constructors with a fresh cardinality variable. The example -in Section~\ref{sect.ExamplePoly} showed several types annotated with such cardinality variables. In this thesis, we -often refer to cardinality variables as cardinality annotations. +in Section~\ref{sect.ExamplePoly} showed several types annotated with such cardinality variables. -Consider the following expression with types at every place: +Consider the following expression with types of every identifier and subexpression: %%[[wrap=code let (f :: Int -> Int) = (\x :: Int -> (x :: Int) + (1 :: Int) :: Int) :: Int -> Int @@ -136,44 +141,49 @@ As demonstrated in Chapter~\ref{chapt.NoBindings}, the constraints between annot variables are properly connected to each other. The above approach allows cardinality coercions everywhere in the abstract syntax tree. A cardinality coercion allows -a relaxation of an established cardinality result to a weaker variant. For example, we can coerce a value with cardinality -|onemin| to a value with cardinality |*| by forgetting that the value is used at most once. Depending on the code -generator, an coercion function needs to be inserted, for example to move the value from one heap to another. But, there -is some redundancy between annotations on some types. For example, a parameter of a function can use the cardinality -variables of the enclosing function for its annotated type. It does not need fresh cardinality variables. There is no -need to put a coercion at the use sites of identifiers. Another redundancy is that in the binding |x = f 3|, it is possible -to coerce the result of |f| at the function application, but also at the place where the result of |f| is bound to |x|, or even both. -Coercions lead to additional code insertion in the program, depending on the code generator. We therefore want to -limit the number of coercions that can be inserted, and restrict it to clearly defined places. - -We can restrict the places where cardinality coercions are inserted, to two places: the argument of function applications and -the right hand side of a binding to an identifier, without reducing the quality of the cardinality inference. At the other places, -an annotated type can be constructed by using the cardinality variables occurring on type constructors in types of the -subexpressions. - -Compare the difference with the following example and the previous example: +a relaxation of an established cardinality result to a weaker variant. For example, we can coerce a value with a total +|usage| value of |onemin| to a value with a total usage of |*| by forgetting that the value is used at most once in total, +if optimisations do not conflict with this coercion and possibly requires a coercion to be applied to the value at the +moment of relaxation. There is some redundancy between annotations on some types. For example, a parameter of a function can use the cardinality +variables of the enclosing function for its annotated type. It does not need fresh cardinality variables. Since we allow a +coercion from argument to parameter, there is no need for a coercion from parameter to use-site of the parameter in the body +of the function. Similary, for a function application like such as |f 3|, it is possible to coerce the result of |f| at the +function application. However, the result of |f 3| can be used at three places: as argument of a function application, as +body of a lambda, or as right-hand side of a |let| binding (later in this chapter). In case it is used as argument to another function application (i.e. |g (f 3)|), then the function +application of |g| already allows an coercion. In case it is used as the body of lambda, we already allow a coercion from the type of +the body to the type of the result of the lambda. Finally, we also already allow a coercion of the right-hand side of a +|let|. So, a coercion of the result of a function at a function application is redundant. Coercions possibly lead to additional +code depending on the code generator. We therefore want to limit the number +of coercions that can be inserted, and restrict it to clearly defined places. Therefore, we restrict coercion to the three +places mentioned above. This has no influence on the quality of the inference process. It leads to +fewer coercion constraints and fewer annotations, which is beneficial for the performance of the compiler and possibly the +performance of the program itself. + +Consider the difference between the following example and the previous example: %%[[wrap=code -let (f :: (Annot(Int)(1)) (Annot(->)(2)) (Annot(Int)(3))) = (\(x :: (Annot(Int)(1))) -> (x :: (Annot(Int)(4))) + (1 :: (Annot(Int)(5))) :: (Annot(Int)(3))) :: (Annot(Int)(1)) (Annot(->)(2)) (Annot(Int)(3)) -in (f :: (Annot(Int)(6)) (Annot(->)(7)) (Annot(Int)(8))) (1 :: (Annot(Int)(9))) :: (Annot(Int)(10)) +let (f :: (Annot(Int)(1)) (Annot(->)(2)) (Annot(Int)(3))) = (\(x :: (Annot(Int)(1))) -> (x :: (Annot(Int)(4))) + (1 :: (Annot(Int)(5))) :: (Annot(Int)(6))) :: (Annot(Int)(1)) (Annot(->)(2)) (Annot(Int)(3)) +in (f :: (Annot(Int)(7)) (Annot(->)(8)) (Annot(Int)(9))) (1 :: (Annot(Int)(10))) :: (Annot(Int)(11)) %%] -With this strategy, less different cardinality annotations are used compared with the annotation strategy above. +With this strategy, fewer different cardinality annotations are used compared with the annotation strategy above. The difference is that we allow coercions only at restricted places. The result is less constraints and less -coercion variables, which results into better performance of the inferencer. To scale up to typing big real-life +coercion variables, which results in better performance of the inferencer. To scale up to typing big real-life programs, a cardinality inferencer can decide to reduce accuracy for certain unimportant pieces of a program, by limiting the coercions and reusing cardinality variables even more, to reduce the number of -annotations severely, thus preventing choking up on the number of annotations (Section~\ref{sect.FutureWork}). +annotations severely, thus preventing choking on the number of annotations (Section~\ref{sect.FutureWork}). Limiting coercions can also positively impact runtime performance, depending on the additional code that is inserted for it, and what the code-improvements are up to the point of the coercion. -Take a look at the example again. The types at the use-site of an identifier are freshly annotated, but this has nothing to -do with coercions. The reason for freshly annotating the use-sites of an identifier is because we treat each use of an -identifier independently, and combine the results at the definition site with the aggregation constraint. +Take a look at the example again. The types at the use-site of an identifier are freshly annotated, but this is unrelated +to coercions. The reason for freshly annotating the use-sites of an identifier is because we treat each use of an +identifier independently, and combine the results at the definition site with the aggregation constraint. For similar +reasons are integer expressions and the spine of a lambda freshly annotated: we can produce integers and functions +for any cardinality annotation. Figure~\ref{RulerUniquenessExamples.UX.expr.base} lists the type rules for the uniqueness type system with cardinality inference. The constraint -generation remained virtually the same. The notable changes are the places where a normal type is freshly annotated to -an annotated type with cardinality variables. The result of the inference process are annotated types for each expression, +generation remained virtually the same. The notable changes are the places where identifiers are freshly annotated, and a reduction in the +number of coercion constraints. The result of the inference process are annotated types for each expression, and a substitution. The substitution maps each cardinality variable to a cardinality value. \rulerCmdUse{RulerUniquenessExamples.UX.expr.base} @@ -182,14 +192,28 @@ and a substitution. The substitution maps each cardinality variable to a cardina \section{The inferencer} \label{sect.TheInferencer} -The question that now remains is: how to obtain the substitution that maps a cardinality value to a cardinality -variable. Since we have a finite number of cardinality variables, and a finite number of cardinality values, an obvious -approach is to iterate through all combinations, and pick the least solution from the combinations that satisfy the constraints. -This is not a feasible approach in practice. +The question that now remains is: how to obtain the substitution that assigns a cardinality value to a cardinality +variable? Since we have a finite number of cardinality variables and a finite number of cardinality values, an obvious +approach is to iterate through all combinations, and pick a least solution from the combinations that satisfy the constraints. +A least solution is a lowest value in the ordering |leqM| such that the cardinality values satisfy the constraints: + +%%[[wrap=code +((Sub(c)(1)), ..., (Sub(c)(n))) leqM ((Sub(d)(1)), ..., (Sub(d)(n))) + = (Sub(c)(1)) leqC (Sub(d)(1)) + && ... + && (Sub(c)(n)) leqC (Sub(d)(n)) +%%] + +Although it is not obvious from the definition |leqM|, we show in Section~\ref{sect.TheMinimalSolution} that there is only one least solution +to a set of constrains. Unfortunately, the above approach is not feasible in practice. The problem is for |n| annotations, there are +$5^n$ combinations, which is not feasible to calculate in practice. -We first compute with an fixpoint computation the upper and lower bounds. Then choose the most specific cardinality value -that fits the bounds. With a fixpoint computation, the cardinality values are relaxed to less specific values until the -constraints are all satisfied. That means three fixpoint computations on the same constraint set, each time with a +Fortuantely, there is no need to compute all possible combinations. Due to the orderings defined on the cardinalities, +upper bound and lower bounds, we can use a fixpoint computation to obtain a least fixpoint. Actually, we need three +of these computations: one for the lower bound, one for the upper bound, and one for the cardinalities. We first +compute the lower and upper bounds. Then choose for each cardinality the most specific cardinality that fits with +the two bounds. The third iteration process relaxes the cardinalities according to |leqC|, until all constraints +are satisfied. This means that there are three fixpoint computations on the same constraint set, each time with a different solving function. Figure~\ref{code.fixSolve} gives an overview of the implementation. \begin{figure} @@ -205,12 +229,17 @@ infer cs %%] \\ %%[[wrap=code -bestFit :: LBound -> UBound -> Cardinality -bestFit 0 0 = 0 -bestFit 1 1 = 1 -bestFit 1 _ = oneplus -bestFit _ 1 = onemin -bestFit _ _ = * +bestFit :: LowerBound -> UpperBound -> c +bestFit l u + = let z = l `bestFitAux` u + in (Card(z)(z)) + where + bestFitAux :: LowerBound -> UpperBound -> Usage + bestFitAux 0 0 = 0 + bestFitAux 1 1 = 1 + bestFitAux 1 _ = oneplus + bestFitAux _ 1 = onemin + bestFitAux _ _ = * %%] \\ %%[[wrap=code @@ -224,7 +253,7 @@ worklistFix solveF cs initial iter (c : cs) subst = let c1 = subst `apply` c c2 = solveF c1 - subst' = c2 `improve` subst + subst' = c2 `update` subst in if subst' == subst then iter cs subst' else iter ((c `lookup` deps) ++ cs) subst' @@ -232,25 +261,26 @@ worklistFix solveF cs initial \end{figure} The fixpoint iteration proceeds as follows. We start with the best possible substitution, which is the -lowest value in the ordering defined on the values where the substitutions are mapped to. If one -particular value |v| does not satisfy the constraint, then |v| is too low and we select a value -|v' >= v| such that |v| is as small as possible, but satisfies the constraint. Such a value |v| is -always found because the biggest value in the ordering always satisfies the constraints. It is possible that -satisfying one constraint makes another constraint not satisfied. Such a constraint is visited again, -which causes the substitution to increase to make it satisfied. After several iterations back and -forth the constraints, the values do not change anymore and the iteration process terminates. The -iteration process always terminates because the substitution needs to grow in order for the -iteration to continue and the substitution cannot grow beyond the point where each variable -is mapped to the maximum value. When the fixpoint procedure terminates, we say that a least -fixpoint is reached. +lowest value in the ordering. If one particular value |v| does not satisfy a constraint, then |v| is +too low in the ordering and we select a value v', with |v leq v'| and v' as low as possible in the +ordering and satisfies the constraint. We relaxed |v| to |v'|, since |v'| can only be higher in the +ordering. Such a value can alawys be found since the orderings are finite join-semilattices, wich +implies there is a value |t| such that |v leq t| for any |x|. It is possible that satisfying one constraint +makes another constraint not satisfied. Processing the constraints once is called an iteration, and we +repeat iterations until the substitution does not change anymore. If a substitution does not change, then +no relaxations took place, which implies that all constraints are satisfied. Futhermore, the number of +relaxations is limited, since we have a finite substitution of which the value for each variable can +be relaxed a finite number of times. A property of the fixpoint procedure is that a least fixpoint is +reached after the process terminates. For our constraints and their interpretation, there is only one such least fixpoint, and it is the optimal solution to the constraint set (Section~\ref{sect.TheMinimalSolution}). This approach is fast: when the constraints are topologically ordered, with the left-hand side(s) as dependency on the right-hand-side, and a special treatment -for constraints that form a cycle, at most 5 iterations are required for the upper bound computation: 3+1 iterations (in the worst case) to get |*| everywhere in the substitution, and one -iteration to discover that nothing changed. With an implementation by means of a worklist algorithm, it takes even less +for constraints that form a cycle (a change of the substitution of a variable in a cycle is directly propagated to the substitution of the +other variables in the cycle), at most four iterations are required for the upper bound computation: three iterations (in the worst case) to get |*| everywhere in the substitution, and one +iteration to discover that the substitution did not change. With an implementation by means of a worklist algorithm, it takes even less time in practice, due to several reasons, including that the constraints represented as a graph (Section~\ref{sect.Rewriting}) -is sparse. The worklist version takes a single constraint, ensures that it is satisfied, and +are sparse. The worklist version takes a single constraint, ensures that it is satisfied, and if it changes the substitution, adds all dependent constraints on the stack of constraints to process. See Figure~\ref{code.fixSolve} for the worklist implementation. @@ -259,18 +289,18 @@ Figure~\ref{code.iterate} lists the solve functions. The worklist function appli substitution to a constraint, such that the solve function gets a constraint with concrete values filled in for the variables. The solve function returns the constraint with possibly increased values for the variables. The worklist function takes these values out of the constraint -again and improves the substitution with it. Over and over again until the substitution does not +again and updates the substitution with it. This happens over and over again until the substitution does not change anymore. Compare these functions with the constraint checking functions of Section~\ref{Sect.CheckingConstraints}. The solve functions are similar to the constraint checking functions, which is not surprising since the iteration functions just increase values until they fit. -The solve functions for the lower bound and the upper bound are fairly straightforward. The solve function for -cardinality values requires some explanation. The |join| function relaxes a cardinality if the two cardinalities do not fit. -For example, if one of the cardinalities specifies that some value has cardinality |0|, and the other specifies that it -has cardinality |oneplus|, then we relax the value to |oneplus|, which is less specific. A special variant of the |join| function -is used to only increase the left-hand side if the right-hand side cannot be coerced to it. The cases for the aggregation -constraint specify that a cardinality value needs to be split up in a proper way. For example, if the cardinality of the -result is |1|, then there must be one occurrence with cardinality |1| and all the other occurrences cardinality |0|. +Figure~\ref{code.iterate} lists the solve functions. The solve functions for the lower bound and the upper bound are fairly straightforward. +The |beta| in the coercion constraint means that we do not differentiate between soft and hard coercion constraints for the lower and +upper bounds. The solve function for cardinality values requires some explanation. The |increase| function minimally relaxes both |Usage| parameters +until they coerce into each other. The |split| function relaxes |Usage| values minimally until usages are properly split over the individual +occurrences. This means for example that if we know that the combined occurrences are used in total exactly once, then once of the occurrences must +be used exactly once and the others not. If we know that the total is used more than once, then one of the individual occurrences must be used +more than once and the others can be arbitrarily used. \begin{figure} \caption{Solve functions} @@ -293,38 +323,43 @@ upperSolveF ((Sub(a)(1)) \*/ ... \*/ (Sub(a)(n)) <= a) %%] \\ %%[[wrap=code -cardSolveF c@(a (Sub(=>=)(s)) b) -- weak constraint ignores cardinality - = c -cardSolveF (a (Sub(=>=)(h)) b) - = let z = a `leftJoin` b - z' = a `join` b - in z (Sub(=>=)(h)) z' - where - leftJoin * -1 = -1 -- coercion - leftJoin a b = join a b -cardSolveF c@(0 \*/ ... \*/ 0 <= 0) -- all 0 +cardSolveF c@(_ (Sub(=>=)(s)) _) -- soft constraint ignores cardinality = c -cardSolveF c@((Sub(a)(1)) \*/ ... \*/ (Sub(a)(n)) <= 1) -- one exactly 1 and the rest all 0 +cardSolveF ((Card(a)(b)) (Sub(=>=)(h)) (Card(c)(d))) + = let (a1, c1) = increase (leqP) (leqS) a c + (b1, d1) = increase (leqQ) (leqZ) b d + b2 = a1 `(Sub(join)(leqX))` b1 + d2 = c1 `(Sub(join)(leqX))` d1 + in ((Card(a1)(b2)) (Sub(=>=)(h)) (Card(c1)(d2))) +cardSolveF ((Card(Sub(a)(1))(Sub(b)(1))) \*/ ... \*/ (Card(Sub(a)(n))(Sub(b)(1))) <= (Card(a)(b))) + = let ((Sub(a1)(1)), ..., (Sub(a1)(n)), a1) = split ((Sub(a)(1)), ..., (Sub(a)(b)), a) + (Sub(b1)(1)) = (Sub(a1)(1)) `(Sub(join)(leqX))` (Sub(b)(1)) + ... + (Sub(b1)(n)) = (Sub(a1)(n)) `(Sub(join)(leqX))` (Sub(b)(n)) + b1 = a1 `(Sub(join)(leqX))` b + b2 = (Sub(b1)(1)) `(Sub(join)(leqQ))` ... `(Sub(join)(leqQ))` (Sub(b1)(n)) + in ((Card(Sub(a1)(1))(b2)) \*/ ... \*/ (Card(Sub(a1)(n))(b2)) <= (Card(a1)(b2))) +%%] +\\ +%%[[wrap=code +split c@(0, ..., 0, 0) -- all exactly 0 + = c +split c@((Sub(a)(1)), ..., (Sub(a)(n)), 1) -- one exactly 1, the others exactly 0 | length neq0 == 1 && head neq0 == 1 = c where - (_, neq0) = partition (== 0) [(Sub(a)(1)) ... (Sub(a)(n))] - -cardSolveF ((Sub(a)(1)) \*/ ... \*/ (Sub(a)(n)) <= a) -- all 1+ or all 1- or all * - = let z = (Sub(a)(1)) `join` ... `join` (Sub(a)(n)) - in (z \*/ ... \*/ z <= z) + (_, neq0) = partition (== 0) [(Sub(a)(1)), ..., (Sub(a)(n))] +split ((Sub(a)(1)), ..., (Sub(a)(n)), a) -- all 1+ or all 1- or all * + = let z = (Sub(a)(1)) `(Sub(join)(leqP))` ... `(Sub(join)(leqP))` (Sub(a)(n)) `(Sub(join)(leqP))` a + in (z, ..., z, z) %%] \\ %%[[wrap=code -join * _ = * -join _ * = * -join oneplus onemin = * -join onemin oneplus = * -join oneplus _ = oneplus -join _ oneplus = oneplus -join onemin _ = oneplus -join _ onemin = oneplus -join _ _ = * +increase relaxR coercionR a b + = (Sub(min)((leqQ, leqQ))) [ (a', b') | a' <- Usage, b' <- Usage + , a `relaxR` a' + , b `relaxR` b' + , a `coercionR` b' ] %%] \end{figure} @@ -364,8 +399,8 @@ join _ _ = * So, taking the minimum of two solutions gives another solution. With this fact, we prove that there can only be one least solution. Assume that the opposite is the case, such that |P| and |Q| are different least solutions. In order for |P| and |Q| - to be different, there must be some annotation |(Sub(delta)(0))| for which |Q((Sub(delta)(0))) < P((Sub(delta)(0)))|. The - other way around as well, but we do not need that here. Consider the + to be different, there must be some annotation |(Sub(delta)(0))| for which |Q((Sub(delta)(0))) < P((Sub(delta)(0)))| (the + other way around as well, but we do not need that here). Consider the solution obtained by taking the minimum from |P| and |Q|: |M === P `min` Q|. For each annotation |delta|, |M(delta) <= P(delta)|. But for |(Sub(delta)(0))|, |M((Sub(delta)(0))) = Q((Sub(delta)(0))) < P((Sub(delta)(0)))|. This means that |M| is a smaller solution that |P|. Thus |P| cannot be a least solution, and that there is only @@ -381,8 +416,8 @@ In Chapter~\ref{chapt.NoBindings} we showed how to gather the constraints. In th uniqueness types given the constraints, using a fixpoint iteration approach. We are now going to make life a bit interesting by supporting a non-recursive |let|. This will complicate -the inferencer, especially since we are paving a way to support a polymorphic and recursive |let| for -Chapter~\ref{chapt.Recursion} and Chapter~\ref{chapt.Polymorphic}. A gentle warning: make sure you have a feeling +the inferencer, especially since we are paving the way to support a polymorphic and recursive |let| for +Chapter~\ref{chapt.Recursion} in Chapter~\ref{chapt.Polymorphic}. A gentle warning: make sure you have a feeling of the inference process up to this point, otherwise subsequent sections and chapters will be difficult to understand! @@ -423,10 +458,10 @@ type rule: \end{center} We can apply the same strategy for the uniqueness type system. A set of constraints $S$ is inferred for |expr_def|. For each use -of |id|, $S$ is copied as the constraint set of the identifier. To show why this approach works, remember that referential -transparency allows to substitute an identifier by its definition. +of |id|, $S$ is copied as the constraint set of the identifier. To show why this approach works, remember that beta-reduction +allows us to substitute an identifier by its definition. -Suppose the occurrences |1..n| of |id| in |body_expr| are replaced by |def_expr|, to |(Sub(inst_expr)(1))..(Sub(inst_expr)(n))|. +Suppose the occurrences |1..n| of |id| in |body_expr| are replaced by |def_expr| to |(Sub(inst_expr)(1))..(Sub(inst_expr)(n))|. In other words, in the expression: %%[[wrap=code @@ -434,10 +469,10 @@ let id = def_expr in ... (Sub(id)(1)) ... (Sub(id)(n)) ... %%] -The definition for |id| is inlined: +The definition for |id| is inlined to (beta-reduction): %%[[wrap=code -... (Sub(inst_expr(1)) ... (Sub(inst_expr(n)) ... +... (Sub(inst_expr)(1)) ... (Sub(inst_expr)(n)) ... %%] We now compare the constraint sets resulting from constraint gathering on |def_expr| and each |(Sub(inst_expr)(i))|. The constraint @@ -448,35 +483,38 @@ is due to the fresh annotations of the types occurring in |(Sub(inst_expr)(1)).. There is one other difference in the constraint set of the whole expression. If |def_expr| uses some identifier |x| from an outer binding group, then the |x| occurs |n| times more often in the inlined version. The corresponding aggregation constraint will be |n| times bigger. We solve this difference with a trick: when instantiating the constraint set of |def_expr|, the cardinality variables -occurring on the use-site-types of identifiers are not given fresh variables, unless they are an argument or result of a function. -This gives us |n| of the smaller aggregation constraints, slightly different, but gives a conservative result towards the |n| times as big aggregation -constraint. - -The following example explains it in a more intuitive way: +occurring on the use-site-types of identifiers are not given fresh variables (unless they are an argument or result of a function, but that +is not important for this explanation). This gives us |n| of the smaller aggregation constraints, slightly different, but gives a +conservative result towards the |n| times as big aggregation constraint, as the following example shows: %%[[wrap=code let x = ... -in (x ... x) ... (x ... x) + y = x ... x +in y ... y %%] %%[[wrap=code let x = ... - y = x ... x -in y ... y +in (x ... x) ... (x ... x) %%] -We note here that computing the bounds through |y| gives bounds for |x| that are conservative to bounds computed directly from -the four usages of |x|. - -The cardinality variables that may not be replaced by a fresh cardinality variable, are called the \emph{sacred variables} -or sacred annotations. These sacred variables are the annotations on the definition-site types of identifiers and the -annotations on use-site types of identifiers that are in scope for a binding group. These sacred variables are collected and +In the version where |y| is inlined, we compute the bounds of |x| directly. In the inlined version, the bound of |x| are +computed from the bounds of |y|. This potentially leads to a less accurate, but conservative result, since we already +approximate the bounds of |y|. This means that the constraint set that we obtain by separately analysing |y| and +inserting this constraint set at each use-site of |y|, gives solutions that are equal, or conservatively less +accurate, compared to solutions obtained from analysing an expression without a |let|. + +The \emph{sacred variables}, or sacred annotations, are those cardinality variables that may not be replaced by a fresh +cardinality variable. These sacred variables are the annotations on the definition-site types of identifiers and the +annotations on use-site types of identifiers that are in scope for a binding group. Basically, the sacred annotations +are the annotations on identifiers that are directly influenced and visible by the binding group. The number of sacred +annotation variables is linear in the size of the abstract syntax tree. The sacred variables are collected and passed to the inferencer. We omit this detail in the type rules. The type scheme has an additional result |omega|, which represents the constraints of a binding group: \rulerCmdUse{RulerUniquenessExamples.UL.expr.base.scheme} -The inferencer performs the constraint duplication. In the gathered constraint set, we insert a placeholder to represent the +The inferencer performs the constraint duplication. In the inferred constraint set, we insert a placeholder to represent the constraints that are to be inserted, by means of the following constraint: %%[[wrap=code @@ -509,88 +547,121 @@ For the |let|, we have the following type rule: The term \emph{binding group} refers to the bindings of the |let|. We assume that each |let| is numbered. This number identifies the binding group. In EH, each |let| only contains a single binding group, but technically speaking, the |let| -can be partitioned into multiple binding groups (such as in Haskell), without invalidating this text. +can be partitioned in multiple binding groups (such as in Haskell). Binding groups are nested. Binding group |A| is a +parent of binding group |B| if and only if the |let| of |B| occurs in the expression of the identifier of the |let| of +|A|. The body of the |let| belongs to the same binding group of the encloding expression. An identifier in binding group +|C| is also in binding group |D| if and only if |D| is |C|, or is a parent of |C|. Two identifiers are in the same binding group if +and only if the binding group of one identifier is the parent of the binding group of the other +identifier. A binding group is outermost if it has no parent. + +The type rule for the |let| specifies that a compiler performs two tasks for a |let|: generate a constraint to +aggregate the cardinalities of individual occurrences of the identifier bound to the |let|, and collect constraints +of the binding group. -Similarly to the discussion of parameters of a function, we need to aggregate the individual uses of an identifier in -a subexpression, resulting in the generation of an aggregation constraint for each binding. The second task of the |let| is -to gather the constraint for the bindings. The input to the type inferencer is a constraint set for each binding -group. +In the end, a result of the constraint gathering phase is a set of constraints for each binding group. These constraints +are passed to the inferencer. The inferencer combines the individual results computes a least substitution. \section{The inferencer revisited} \label{sect.Instantiation} + The inferencer processes the constraint sets of binding groups in the order such that if $A$ is a constraint set containing an |Inst| constraint referencing binding group $B$, then $B$ is processed before $A$. In other words: the binding groups are processed in the order specified by a topological sort on the dependency graph -between constraints. Since the binding groups are non-recursive, it is guaranteed that when the inferencer +between constraint sets. Since the binding groups are non-recursive, it is guaranteed that when the inferencer processes a binding group, that all the binding groups it depends on are already processed. The processing of a binding group consists essentially of getting rid of the |Inst| constraints, and replace them by normal constraints. Then, we end up with a normal constraint set again, and can continue with -the uniqueness inference as specified in the first part of this chapter. However, replacing the |Inst| +the cardinality inference as specified in the first part of this chapter. However, replacing the |Inst| constraint by the constraint set of the corresponding binding group, tends to let the number of constraints -explode (Section~\ref{sect.Rewriting}). We take a different approach, by converting each constraint set to an equivalent +explode. We take a different approach, by converting each constraint set to an equivalent graph representation: the \emph{constraint graph}. By simplifying the graph, it becomes small enough for practical -use (Section~\ref{sect.Rewriting}. +use (Section~\ref{sect.Rewriting}). -The graph representation is straightforward. It is a directed graph with the cardinality variables as nodes and the constraints as directed edges -between the nodes. The constraint |a =>= b| is translated to a directed edge\footnote{There are two variants of the |=>=| constraint. This is only a slight, but not interesting, complication, so we leave it out of this description.} from node |a| to node |b|. The constraint -|(Sub(a)(1)) \+/ ... \+/ (Sub(a)(n)) <= b| is translated to a hyper edge from nodes |(Sub(a)(1)), ..., (Sub(a)(n))| to -node |b|. The inference of the substitution is analogous to the inference on the constraint set, except that now -the edges of the graph are traversed instead of the constraints. +The graph representation of a constraint set |Cs| is obtained as follows. Let $G = (V, E, H)$ be a directed graph with +vertices $V$, edges $E$, and hyper edges $H$. The vertices of $G$ are the cardinality annotations of |Cs|: |delta `elem` V| if and only +if |delta `isAnnotation` Cs|. The labelled edges of $G$ are the coercion constraints of |Cs|: +|E((Delta(1)), (Delta(2))) = beta| if and only if |((Delta(1)) (Sub(=>=)(beta)) (Delta(2))) `elem` Cs|. The labelled hyper edges of $G$ are aggregation +constraints of |Cs|: |H [(Delta(1)), ..., (Delta(n))] = (delta, Nothing)| if and only if +|((Delta(1)) \*/ ... \*/ (Delta(n)) <= delta) `elem` Cs|. This |Nothing| value is a label on the block +symbol of a hyper edge. We come back to this value later. -As an example of the above approach, take the following constraint set: +As an example of the above approach, take the following constraint set (we make an explicit difference between the +soft and hard versions of the coercion constraints): %%[[wrap=code -a =>= b -b =>= c -b =>= d +a (Sub(=>=)(s)) b +b (Sub(=>=)(h)) c +b (Sub(=>=)(h)) d c \*/ d <= e -e =>= b +e (Sub(=>=)(h)) b %%] -The representation as a graph is: +The variables |a..e| become vertices in the graph. The coercion constraints become the edges and the aggregation +constraints become hyper edges. Suppose that the variables |a|, |c|, and |e| are sacred cardinality +variables. We visually represent sacred vertices with a double circle, and normal vertices with just a single circle. +This results in the graph: \begin{center} -\includegraphics[width=6cm]{unq-graph} +\includegraphics{unq-graph} \end{center} -The variables |a..e| are the nodes in the graph. The coercion constraints are the edges and the aggregation -constraint is a hyper edge. To calculate an upper bound substitution from initial substitution |S(a) = 1, S(delta) = 0, delta `elem` [b..e]|, +To calculate an upper bound substitution from initial substitution |S(a) = 1, S(delta) = 0, delta `elem` [b..e]|, we iterate over the (hyper) edges of the graph. The edge between |a| and |b|, combined with the substitution |S(a) = 1|, force |S(b)| to |1|. |S(b) = 1| forces both |S(c)| and |S(d)| to |1|. The hyper edge combines |S(c) = 1| and |S(d) = 1|, resulting in |*|, and forces |S(b)| to |*|. Repeating the above procedure forces |S(c)| and |S(d)| to |*|. The hyper edge combines |S(c) = *| and |S(d) = *| in |*| for |S(b)|, which is already the case. None of the edges in the graph change the substitution anymore, and the iteration stops with a final substitution S', with |S'(a) = 1, S'(delta) = *, delta `elem` [b..e]|. -Back to the inferencer. The inferencer applies the following steps: +Figure~\ref{fig.graphinferencer} gives an overview of inferencer. The inferencer applies the following steps: \begin{itemize} \item Convert the constraints, excluding |Inst| constraints, of each binding group to a constraint graph. -\item For binding group |p|, with an |Inst q l| constraint, instantiate binding group |q| into |p|, with +\item For binding group |p|, with an |Inst q l| constraint, instantiate binding group graph |Q| into |P|, with definition-site cardinality variables replaced by use-site cardinality variables, as specified by |l|. What -basically happens is that for each node in |q|, a fresh node is inserted in |p|, except when it occurs -in |l|. Then each edge in |q| is inserted in |p|, taking the corresponding node in |p|. +basically happens is that for each vertex in |Q|, a fresh vertex is inserted in |P|, except when it occurs +in |l|. Then each edge in |Q| is inserted in |P|, taking the corresponding vertex in |P|. \item Perform a fixpoint cardinality inference on the constraint graph of the outermost binding group. \end{itemize} -The last step results into a cardinality substitution for each cardinality variable occurring in types +\begin{figure} +\caption{Overview of the inferencer} +\label{fig.graphinferencer} + +%%[[wrap=code +inferSubst constrSets + = let deps = [(i, j, c) | (i, cs) <- constrSets, c@(Inst j _) <- insts cs] + order = topsort deps + initial = [(i, csToGraph cs) | (i, cs) <- constrSets] + graphs = foldr instantiate initial order + in infer (outermost graphs) + where + instantiate (to, from, (Inst _ tups)) graphs + = let src = fresh (sacred to) tups (to `lookup` graphs) + dst = (from `lookup` graphs) `union` src + dst' = reduce dst + in (to, dst') `insert` graphs +%%] +\end{figure} + +The last step results in a cardinality substitution for each cardinality variable occurring in types of the outermost binding group of the program. It does not directly give a substitution for another binding group, since the substitution is potentially different for each use of an identifier occurring in such a binding group. We can construct such a definition-site substitution from a use-site substitution. Suppose we know the cardinality substitution $R$ for binding group |k|, and |k| contains the use-site of an identifier |x| -of binding group |j|. We can construct the substitution $S$ for the upper bound and the substitution $W$ for the lower bound -from $R$ by translating the guarantees that cardinality values of $R$ give, to upper and lower bounds. -Take the upper bound substitution $S$ as example. Take $S$ such that it maps to |0| for each cardinality variable of |j|, +defined in binding group |j|. We can construct the substitution $S$ for the upper bound and the substitution $W$ for the lower bound +from $R$ by translating the guarantees that left-hand side |Usage| values of cardinality values of $R$ give to upper and lower bounds. +Consider an upper bound substitution $S$ for example. Take $S$ such that it maps to |0| for each cardinality variable of |j|, except for the cardinality variables mentioned by the |Inst| constraint. These we set to a value determined by the -cardinality use-site counterpart in $R$. If the cardinality is |0|, the upper bound is |0|, for |onemin| and |1| the -upper bound is |1|, and otherwise |*|. By feeding $S$ as initial substitution into the inferencer for the fixpoint +cardinality of the use-site counterpart in $R$. If the left-hand side cardinality value is |0|, the upper bound is |0|, and +for |onemin| and |1| the upper bound is |1|, and otherwise |*|. By feeding $S$ as initial substitution to the inferencer for the fixpoint computations on the constraint graph of |j|, we get a final substitution for the upper bound of each cardinality variable of |j|. This allows us to get a use-site dependent typing for a binding-group, which can be exploited by a code generator that performs code specialization. -\section{Graph rewriting} +\section{Graph reduction} \label{sect.Rewriting} \label{sect.Rewrite} \label{sect.Strategies} @@ -606,118 +677,150 @@ in let inc4 = \x -> inc1 (inc1 (inc1 (inc1 x)) %%] With constraint duplication, the size of the graph corresponding to |inc16| is at least four times as big as the graph of |inc4|, and at least -sixteen times as big as the graph of |inc1|. - -By applying several reduction strategies, we end up with a graph that is considerably smaller. A lot of intermediate nodes can be -dropped. The reason is that only the sacred variables matter. These are all use-site and definition-site cardinality variables in scope of -the binding group. The other cardinality variables (for example, those as a result of a coercion in a function application, or the fresh variables resulting from instantiations) are intermediates. A constraint graph can be converted into an -equivalent constraint graph with all intermediate cardinality variables eliminated, resulting only in constraints (or edges in the -constraint graph) between the cardinality variables on the types of an identifier or the mono variables. - -The theoretical maximum number of constraints between these sacred cardinality variables is only dependent on the -number of variables, which in turn only depends on the size of the types in question, and the number of uses -of an identifier. Without elimination, the number of constraints depend on the amount of duplication, which can easily -cause the number of constraints to explode, as the example shows. With the elimination of intermediate cardinality variables, and $n$ -sacred cardinality variables, the theoretical maximum number of normal edges is $O(n^2)$, but the theoretical number -of hyper edges is still high: $O(n!)$. In practice, these numbers are not reached. A cardinality variable represents -memory, and memory in a program is largely independent. The constraint graphs are sparse, with the number of -constraints proportional to the number of cardinality variables. - -There are two moments to rewrite a constraint graph. Just before instantiation of a constraint graph, and after -all instantiations are done. In the first case, the graph is specialized to only those cardinality variables that are -used in the new binding group, to prevent ending up with graphs that explode in size due to the structure of -an expression. For second case, the graph consists of the nodes and edges coming from the constraint set -of the binding group, and all nodes and edges coming from (rewritten) graphs of other binding groups. This -graph can have some redundancy, and by applying a set of rewrite rules, we reduce this graph. A smaller -graph of the second case, makes the procedure to obtain graphs of the first case, faster. We discuss both -reduction moments in more detail. - -\subsection{Reducing instantiation graphs} +sixteen times as big as the graph of |inc1|. The reason is that only the sacred variables matter. These are all use-site and definition-site cardinality variables in scope of +the binding group. The other cardinality variables, for example, those taken freshly when instantiating a constraint graph, are +intermediates. The vertices corresponding to sacred cardinalities are sacred vertices. The other vertices are intermediates. We present +a reduction strategy that removes all intermediates from the graph, and preserves the substitution that the graph represents. + +The theoretical maximum number of constraints between these sacred vertices is only dependent on the +number of sacred vertices, which are in turn only dependent on the size of the abstract syntax tree. Without reduction, the number of +constraints depend on the amount of duplication, which can easily +cause the number of constraints to explode, as the example shows. With the reduction of intermediate vertices, and $n$ +sacred vertices, the theoretical maximum number of normal edges is $O(n^2)$, but the theoretical number +of hyper edges is still high: $O(n!)$. In practice, these numbers are not reached. The constraint graphs are +sparse, with the number of edges proportial (on average) to the number of vertices. The reason is that the +sacred annotations corresponds to values, and evaluation of some value depends typically on only a few +other values. Futhermore, there are only a few hyper edges with many sources (those related to functions that +are used a lot, such as prelude functions), but most identifiers in a program have only a hand ful of +occurrences. + +\subsection{Reduction of intermediates} \label{sect.RedInstGraphs} -We reduce the graph of a binding group just before instantiating it. The cardinality variables that have a -counterpart in the destination graph, are not reduced, they are sacred. The other cardinality -variables are intermediates and are eliminated. - -Suppose $G$ represents the original graph, and suppose that $G$ does not contain any hyper edges. Further, -suppose that $H$ is the reduced graph. Only simple paths in $G$ between sacred -cardinality variables matter for the reduction to $H$. Each simple path in $G$, not containing sacred -cardinality variables as intermediate nodes, between -sacred cardinality variables can be replaced by a single edge between the cardinality variables in $H$, since -|p =>= ... (Sub(s)(i)) ... =>= q| equals |p =>= q|, as long as each cardinality variable |(Sub(s)(i))| -is not a sacred cardinality variable. A path in $G$ between sacred cardinality variables with a sacred -cardinality variable in between, does not matter, since |p =>= ... =>= r =>= ... =>= q| equals -|p =>= r, r =>= q|, which are already present in $H$ by the above procedure. - -But, a constraint graph can contain hyper edges. Suppose that $G$ has hyper edges, and that we construct -a graph $F$ from $G$, such that $F$ only consists of all simple paths from $G$, on which there is a hyper edge, and no sacred cardinality -variables as intermediate nodes, and only sacred cardinality variables at both ends. A hyper edge in $F$ -can have less branches than in $G$, if some branch is not on a path to a sacred uniqueness variable. -Now, if we union the graphs $F$ and $H$, we have a graph on which cardinality inference results into the -same solution for the sacred cardinality variables, as cardinality inference gives for $G$. - -Graph $F$ can be reduced further. We would like to end up with only the hyper edges between sacred cardinality -variables. However, this does not work, because there can be an intermediate cardinality variable between -a sacred cardinality variable and a hyper edge connected by a coercion, which cannot be eliminated. We can -reduce from $F$ each intermediate node not connected by a hyper edge. Due to this construction, each -normal edge contains exactly one sacred cardinality variable, and the other uniqueness variable is connected -to a hyper edge. Call this graph $F'$. The number of nodes in $F'$ is therefore proportional to the number -of hyper edges between the sacred cardinality variables. - -The graph we use for instantiation is the union between $H$ and $F'$. This graph is considered to be in -normal form. - -If we look at the constraint sets of -which both graphs are a representation, then the constraint set of $H$ consists of the coercion constraints -between sacred cardinality variables. $F'$ consists of the aggregation constraints between sacred cardinality -variables, with an occasional coercion. For example, suppose that |a|, |b|, and |c| are -sacred uniqueness variables. Then the constraint set of which $F'$ is a representation, can contain -constraints like |a \*/ b <= c|, but also |a =>= a', b =>= b', c' =>= c, a' \*/ b' <= c'|. - -The graph can be reduced a bit further by eliminating subsumed hyper edges, or in other words, -subsumed |\*/| constraints. For example, suppose that we have |a \*/ b \*/ c <= d| and -|a \*/ b <= d|, then |a \*/ b <= d| is subsumed by |a \*/ b \*/ c <= d|, and can be erased. But, the -procedure of to obtain $F'$ already combined some hyper edges if they existed on the same path, such -that most hyper edges range over different sets of sacred cardinality variables, which means that -subsumed hyper edges do not exist often, and the elimination does not contribute enough to the size -of the graph to be worthwhile. - -Removal of subsumed non-hyper edges, on the other hand, is worth-while. Imagine the following -situation: |a =>= c, a =>= b, b =>= c|, where |a|, |b|, and |c| are sacred annotation variables. The -constraint |a =>= c| is not required in this case, it is subsumed by |a =>= b, b =>= c|, due to transitivity. -Due to the top-down pushing of annotations, the constraints are visually like long threads from the -annotations on the root of the expression to the annotations on the inner expressions. The procedure in this -section, in fact, inserts an edge |a =>= c| if there are edges |a =>= b| and |b =>= c|. Preventing the -insertion of |a =>= c| thus saves quite some edges. - -In the next subsection, we discuss a reduction procedure that makes the graph of the binding group smaller, -such the procedure of this section works faster. The reduction procedure of this subsection has to be -performed for each instantiation, so if we can save time on this procedure, it helps to improve the -speed of the compiler. In fact, after the procedure of the next subsection has reduced the graph, -we can apply the procedure of this subsection once to this graph, taking all the cardinality -variables on all types of the bindings of the binding group as sacred annotations. Then all the -path-finding work has to be done once (reducing the reduction work for instantiation to taking -a subgraph of the reduced graph, containing only those components that have annotations occurring -on the type of the binding that is instantiated), instead of each time again for an instantiation. -This saves time for binding groups with high dependencies between the identifiers, or when the -identifiers are used a lot. - -\subsection{Reducing binding group graphs} - -The constraint graph of a binding group is constructed by converting the constraints to their -graph representation, followed by the insertion of nodes and edges from instantiated graphs for -each |Inst| constraint. The resulting graph has several opportunities for reduction, such as -reducing a sequence of edges to a single edge, but most of these opportunities arise only in -subsequent chapters. The main motivation for reduction of this graph is to lower the size of -the graph to improve the performance of instantiations and fixpoint computations on the graph. +Figure~\ref{fig.graphinferencer} mentioned the function |reduce|. We describe the implementation of this function +in this section. This is an important function: it ensures that graphs do not explode due to constraint duplication. + +We take the graph |G = ((Sub(N)(G)), (Sub(E)(G)))| (encountered above) as example: + +\begin{center} +\includegraphics{unq-graph} +\end{center} + +From this graph, we construct a reduced graph |R| that does not have the vertices |b| and |d|. We take a two step approach: +first we created a reduced graph |K| that contains only normal edges, and then a reduced graph |L| that contains +only hyper edges. The reduced graph |R| is the union of |K| and |L|. + +We start with the reduced graph |K=((Sub(V)(K)),(Sub(E)(K)),emptyset)|. This reduced graph only contains the +sacred vertices of |G|: |(Sub(V)(K)) = [ v `elem` (Sub(V)(G)) || v sacred ]|. The set of edges |(Sub(E)(K))| +is defined as follows: + +%%[[wrap=code +[ ((Delta(1)),(Delta(2)), h) `elem` (Sub(E)(K)) || (Delta(1)) `hardPath` (Delta(2)) ] +[ ((Delta(1)),(Delta(2)), s) `elem` (Sub(E)(K)) || (Delta(1)) `softPath` (Delta(2)) && not ((Delta(1)) `softPath` (Delta(2))) ] +%%] + +There is a hard path between |x| and |y| (|x /= y|) if there is a simple path between |x| and |y| that: +\begin{itemize} +\item Contains no sacred vertices except |x| and |y|. +\item All edges are labelled with |h|. +\end{itemize} + +Similary, a soft path between |x| and |y| (|x /= y|) if there is a simple path between |x| and |y| that: +\begin{itemize} +\item Contains no sacred vertices except |x| and |y|. +\item Has an edge labelled with |s|. +\end{itemize} + +The idea behind these two definitions is that a soft edge is overruled by a hard edge. + +When we look at the example, we see that there is only a soft path between |a| and |c|. There is +a hard path between |e| and |c| (via |b|). The result is: + +\begin{center} +\includegraphics{unq-graph2} +\end{center} + +Now the graph |L=((Sub(V)(L)),emptyset,(Sub(H)(L)))| containing only hyper edges. This reduced graph only contains the +sacred vertices of |G|: |(Sub(V)(L)) = [ v `elem` (Sub(V)(G)) || v sacred ]|. The set of hyper edges |(Sub(H)(L))| +is defined as follows: + +|(Sub(H)(L)) [(Delta(1)), ..., (Delta(n))] = (delta, eta)|, if: + +\begin{itemize} +\item |delta| is a sacred vertex. +\item Each |(Delta(i))| is a sacred vertex. +\item There is a path P between |(Delta(i))| and |delta| in |G|, not containing any other sacred vertices. +\item P traverses a hyper edge (possibly more). The hyper edge |HG| is the hyper edge closest to |delta|. +\item |eta| is the |eta| of |HG| if all the vertices |(Delta(i))| are the sources of |HG|. Otherwise |eta| is + the value |Just X| where |X| is a constraint graph that describes how |(Delta(1)) ... (Delta(n))| + are combined into |delta|. +\end{itemize} + +Before we talk about the graph |X|, we consider the example again. There is a path from both |a| end |c| to +|e| traversing a hyper edge. We therefore expect |L| to be: + +\begin{center} +\includegraphics{unq-graph3} +\end{center} + +Unfortunately, there is a coercion (actually two) between |a| and the source vertex |d| on +the hyper edge in |G|. The problem is that the hyper edge can force some value for the substitution of +|d| which is relaxed by the coercion before it reaches |a|. If we blindly connect |a| to the hyper edge +(as in the example), then the hyper edge can force the value directly on |a|, which is not the case +with the original graph |G|. Or formulated in terms of constraints, there is a difference between +|a (Sub(=>=)(s)) d, d \+/ c <= e| and |a \+/ c <= e|. + +Even worse, consider a slightly different graph: + +\begin{center} +\includegraphics{unq-graph5} +\end{center} + +A reduction from the left graph to the right graph gives a constraint graph that results into +wrong solutions! This is where |eta = Just X| enters the picture. We store a graph on a hyper +egde (|HL|) in |L| that describes how the sources of |HL| are combined. This is basically a subgraph +of |G| representing |HL|. When performing a solve step for |HL|, the inferencer +either applies the solve step for an aggregation constraint (|eta = Nothing|), or recurses on the +graph |X| (|eta = Just X|). In that case, the inferencer temporarily extends the substitution with +initial values for the vertices in |X| that are not on |HL|. + +We construct the constraint graph |X = ((Sub(V)(X)),(Sub(E)(X)))| as follows. We first construct +a graph |X1| which is a subgraph of |G| such that it contains only vertices and edges on simple +paths from |(Delta(i))| to |delta| that traverse hyper edge |HG|. In other words, it is just +the part of |G| that is related to the hyper edge that we are inserting into |L|. The second step +is that we clone |X1| to |X2| with a fresh variable on each vertex of |X2|, except for the +source and destination vertices of |HL|. Now comes the trick: we mark all source +and destination vertices of hyper edges in |X2| sacred and recursively reduce |X2| to |X|. Since +all sources and destinations of the hyper edges are marked as sacred, reduction of this graph does +not recurse futher, but create a small graph that connects the sources of |HL| properly to the destination of |HL|. + +Applying this approach on the running example of this section, gives us the following graphs for |L| and |X|: + +\begin{center} +\includegraphics{unq-graph5} +\end{center} + +The last step is to take the union between |K| and |L| to obtain: + +\begin{center} +\includegraphics{unq-graph4} +\end{center} + + +\subsection{Preprocessing reductions} + +The reduction approach of the previous section is an effective reduction strategy. A downside is +that the reduction strategy involves a lot of path-finding. We therefore preprocess the graph +with a series of simple, but efficient, reduction techniques aimed to lower the number of +vertices and paths in the graph, such that the actual reduction strategy performs better. Again, some cardinality variables may not be eliminated. The sacred cardinality variables can have counter part in the destination graph during instantiation and should not be eliminated. The -other variables can be eliminated, since their values can be reconstructed once we have a substitution for the +other variables are allowed to be eliminated, since their values can be reconstructed once we have a substitution for the sacred variables, by filling in the values in the original graph, and performing the fixpoint computation again, as we discussed earlier in this chapter. -A simple elimination strategy is splitting the constraint graph into connected components, +A simple elimination strategy is splitting the constraint graph in connected components, and dropping those components without a sacred cardinality variable. These components cannot influence the substitution on sacred cardinality variables, since there is no path to them. This strategy is only effective when there are multiple, independent (mutual exclusive), bindings in a binding group. @@ -730,56 +833,50 @@ are discussed, which can cause cycles in the constraint graph. A cycle in the co reduced to all sacred nodes in the cycle, or to an arbitrary node if there are no sacred nodes in the cycle. The edges of a singleton cycle, \emph{self edges}, can be removed entirely. -There is an effective rewrite strategy that can be applied in this chapter. Each non-sacred node |u| that +There is an effective reduction strategy that can be applied in this chapter. Each non-sacred node |u| that is not connected by hyper edges, can be eliminated. For each pair of nodes |a| and |b|, such that there exists an edge |a| to |u|, and an edge from |u| to |b|, create an edge from |a| to |b|. Then remove -|u| and the corresponding edges from the graph. This strategy replaces intermediate nodes from the graph, -or in terms of constraint sets, removes redundant cardinality nodes from the graph. - -A final rewrite strategy that we discuss makes use of upper and lower bound information. By applying the -fixpoint substitution computations for the lower and upper bound on the constraint graph, we can get bounds -for the cardinality variables. Take the upper bound values for example. Most of these values will still be |0|, -since these values depend largely on the usage of the binding group. But constraints from annotations of the user -(Section~\ref{sect.Signatures}), or ways to deal with a module system (Chapter~\ref{chapt.BeyondEH}), can give -some information that allow |*| to be inferred as an upper bound. If we also get a lower bound value of |0|, we -know that the two substitutions do not change anymore, and that the only possible cardinality annotation is |*|. -Suppose that this is the case for node |n|. Then for each node |m| with an edge from |m| to |n|, we know that +|u| and the corresponding edges from the graph. This strategy removes some of the intermediate nodes, +but not all of them (but that is where the reduction of previous section is used for). + +A final reduction strategy that we discuss makes use of upper and lower bound information. By applying the +fixpoint substitution computations for the lower and upper bound on the constraint graph (while the graph +is being constructed), we can get bounds for the cardinality variables. Take the upper bound values for example. Most +of these values will still be |0|, since these values depend largely on the usage of the binding group. But constraints +from annotations of the user (Section~\ref{sect.Signatures}), or ways to deal with a module system (Chapter~\ref{chapt.BeyondEH}), +can give some information that allow |*| to be inferred as an upper bound. If we also get a lower bound value of |0|, we +know that the two substitutions do not change anymore, and that the only possible cardinality annotation is |(Card(*)(*))|. +Suppose that this is the case for vertex |n|. Then for each vertex |m| with an edge from |m| to |n|, we know that |m| also has a lower bound substitution of |0| and an upper bound substitution of |*|, and a corresponding -cardinality value of |*|, because that is the result of one solve step on this the edge from |m| to |n|. In +cardinality value of |(Card(*)(*))|, because that is the result of one solve step on this the edge from |m| to |n|. In that case, we can remove the edge from |m| to |n| from the constraint graph. This approach disconnects nodes from the graph for which we already know that we cannot optimize the corresponding values. -All the rewrites strategies discussed in this subsection have the property that they can be implemented in an efficient way. This +All the reduction strategies discussed in this subsection have the property that they can be implemented in an efficient way. This is important, since the performance of the procedure in Subsection~\ref{sect.RedInstGraphs} depends largely on the size of the graph that it gets as input. -Note that we did not discuss reduction strategies for hyper edges. There are two reasons, the first -reason is that they do not form much of a problem in practice, due to the reduction work of -Subsection~\ref{sect.RedInstGraphs}. The other reason is related to the first, in the sense that due to -the low priority of this subject, it remains still a research problem to properly reduce hyper -edges in a way that offers improvements in practice. - \subsection{Remarks about graph reduction} -The concept of sacred cardinality variables, or sacred nodes, is important. The number of sacred -cardinality variables is a subset of all cardinality variables involved, especially when -there are a lot of places where coercions occur (which creates intermediates). The reduction strategies -that we discussed, rewrite the graphs such that the size of the graph is proportional to the -number of sacred cardinality variables. This helps to improve the performance of the compiler -on real-life programs. The number of sacred cardinality variables is basically an indicator of -the required processing time of the type system. To take this a step further, by +The concept of sacred cardinality variables, or sacred vertices, is important. The number of sacred +cardinality variables is a subset of all cardinality variables involved, especially where +instantiations occur (which creates intermediates). The reduction strategies +that we discussed, reduce the graphs such that the size is determined by the number of sacred +vertices instead of the amount of constraint duplication (which would be a severe problem otherwise). +This helps to improve the performance of the compiler on real-life programs. The number of sacred cardinality +variables is basically an indicator of the required processing time of the type system. To take this a step further, by controlling the number of cardinality variables, a compiler could trade accuracy conservatively for compilation speed. For example, the use-site types can be replaced by definition-site types, reducing the number of cardinality annotations severely, but also reducing the quality of the inference for these types. In Chapter~\ref{chapt.DataTypes} we introduce data types, which leads to an explosion of sacred cardinality variables, and we discuss several ways to allow control -over the number of cardinality variables, and thus to control the size of the uniqueness graphs, and +over the number of cardinality variables, and thus to control the size of the constraint graphs, and the performance of the compiler. \section{Conclusion} -The inferencing of cardinality annotations on types is rather indirect. The typing problem is translated into a constraint problem, which +The inferencing of cardinality annotations on types is rather indirect. The typing problem is translated in a constraint problem, which is turn is converted to a graph problem. This can be rather overkill at first thought, but it allows a certain separation of concerns and abstraction, which is further exploited in subsequent chapters. However, in this chapter, we already use this separation to allow non-recursive and monomorphic |let|-bindings in the expression language.