Typos in my last message: the identifier "field" should be "Field" throughout, and "undef" should be "undefined". Here is the corrected version: Nonextensible records with polymorphic selectors. ================================================= 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 automatically an instance of Label, and you can't define other instances. 2. Define a class (in a library somewhere) class Label n => Contains r n where type Field r n :: * select :: r -> n -> Field r n update :: r -> n -> Field r n -> r 3. Declarations with field labels such as data C = F {l1 :: t1, l2 :: t2} | G {l2 :: t2} are syntactic sugar for data C = F t1 t2 | G t2 instance Contains C ''l1'' where Field C ''l1'' = t1 select (F x y) _ = x update (F x y) _ x' = F x' y instance Contains C ''l2'' where Field C ''l2'' = t2 select (F x y) _ = y select (G y) _ = y update (F x y) _ y' = F x y' update (G y) _ y' = G y' 4. Selector functions only need to be defined once, however many types they are used in l1 :: Contains r ''l1'' => r -> Field r ''l1'' l1 = select r (undefined ::''l1'') l2 :: Contains r ''l2'' => r -> Field r ''l2'' l2 = select r (undefined ::''l2'') 5. Constructors are exactly as before 6. Updates such as r {l1 = x} are syntactic sugar for update r (undefined::''l1'') x ===================================================== Sorry about that. Barney.