| | 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 | }}} |
