| 63 | --------------------------- |
| 64 | === Nonextensible records with polymorphic selection & update === |
| 65 | |
| 66 | The ideas in "first class record types" still work in the case of nonextensible records. Using a simplified version of Labels #2104 we can implement truly polymorphic selection and update, which would be more expressive than TDNR and wouldn't need a whole new type resolution mechanism. Here is a concrete proposal: |
| 67 | |
| 68 | 1. Introduce a built-in class `Label`, whose members are strings at the type level. We need a notation for them; I will use double single quotes, so `''string''` is treated as if it was defined by |
| 69 | {{{ |
| 70 | data ''string'' |
| 71 | |
| 72 | instance Label ''string'' |
| 73 | }}} |
| 74 | This has global scope, so `''string''` is the same type in all modules. You can't define other instances of `Label`. |
| 75 | |
| 76 | 2. Define a class (in a library somewhere) |
| 77 | {{{ |
| 78 | class Label n => Contains r n where |
| 79 | type Field r n :: * |
| 80 | select :: r -> n -> Field r n |
| 81 | update :: r -> n -> Field r n -> r |
| 82 | }}} |
| 83 | 3. Declarations with field labels such as |
| 84 | {{{ |
| 85 | data C = F {l1 :: t1, l2 :: t2} | G {l2 :: t2} |
| 86 | }}} |
| 87 | are syntactic sugar for |
| 88 | {{{ |
| 89 | data C = F t1 t2 | G t2 |
| 90 | |
| 91 | instance Contains C ''l1'' where |
| 92 | Field C ''l1'' = t1 |
| 93 | select (F x y) _ = x |
| 94 | update (F x y) _ x' = F x' y |
| 95 | |
| 96 | instance Contains C ''l2'' where |
| 97 | Field C ''l2'' = t2 |
| 98 | select (F x y) _ = y |
| 99 | select (G y) _ = y |
| 100 | update (F x y) _ y' = F x y' |
| 101 | update (G y) _ y' = G y' |
| 102 | }}} |
| 103 | 4. Selector functions only need to be defined once, however many types they are used in |
| 104 | {{{ |
| 105 | l1 :: Contains r ''l1'' => r -> Field r ''l1'' |
| 106 | l1 = select r (undefined ::''l1'') |
| 107 | |
| 108 | l2 :: Contains r ''l2'' => r -> Field r ''l2'' |
| 109 | l2 = select r (undefined ::''l2'') |
| 110 | }}} |
| 111 | 5. Constructors are exactly as they are currently. I can't see any use for polymorphic constructors when records are nonextensible. |
| 112 | |
| 113 | 6. Updates such as |
| 114 | {{{ |
| 115 | r {l1 = x} |
| 116 | }}} |
| 117 | are syntactic sugar for |
| 118 | {{{ |
| 119 | update r (undefined::''l1'') x |
| 120 | }}} |