Extensible Records

[Claus Reinke]

>> Hugs.Trex> :t let f opts x = (opt1="default"|opts) in f
>> let {...} in f :: a\opt1 => Rec a -> b -> Rec (opt1 :: [Char] | a)
> 
> This completely loses the aim of optional arguments: with this type,  
> the argument 'opts' cannot have a field 'opt1' (as shown by the  
> context 'a\opt1'). The type we want should say that 'opts' cannot  
> have any fields except 'opt1' (though that is optional). Flex cannot  
> express this type.

ok, then i misunderstood what you wanted to demonstrate with
that example. but then this part doesn't seem to need any extensible
records at all, in fact 'cannot have any fields except' requires non-
extensibility. the standard type for optional things is Maybe thing, 
and if you want a record of optional things, a record with default 
value Nothing in each field, updated only on the fields you want
to pass a value in, will do fine.
 
> What I meant by "Flex-like" systems is that they can only extend  
> record types by fixed fields. 

thanks, i find the explanation more helpful than the name.
there are already too many variations around, so unless there
is a concrete implementation/specification, as in the case of 
Trex, Daan's system (i think he actually had several, so i should
say 'Daan's scoped labels'), or Oleg's, your's and my libraries, 
it might be better to specify the features.

> As well as the usual extraction and  
> deletion of fields, I want first-class operators:
> 
> (+:) :: r `Disjoint` s => r -> s -> r :+: s
> x +: y is the concatenation of two records x and y, under the  
> condition that they have no fields in common
> r :+: s is the type of x +: y, assuming x::r and y::s

this is a fairly complex operation, part of which includes a
generalisation of the 'lacks' predicate in Trex to sets of labels, 
to catch common errors at the price of additional complexity.

until i saw Daan's system, i would have agreed that this kind
of disjointness/lacks guarantee was necessary for a useable
record type system, but i'm no longer convinced that the 
additional complexity (not just in implementation, but in types)
is worth it. but that is just one example of why we might 
need several design alternatives - no single system to please
everyone all the time!-)
 
> (|:) :: r `Subrecord` s => s -> r -> s
> x |: y is the update of x by y, under the condition that every field  
> of y is a field of x of the same type
> the type of x |: y is the same as the type of x

i agree that something like this is useful (i should add it to
my own code some time).
 
> The conditions on the types of these operators are important, as they  
> catch common errors. For example, if a function 'f' has optional  
> arguments 'opt1::x1, ... optn::xn' you want 'f {optt1 = val}' to give  
> a type error because you've misspelled 'opt1', not simply to ignore  
> it. In other words, you need a condition that the fields of the  
> record argument of f are a subset of {opt1, .., optn}.

again, that is achievable even with haskell's labelled fields, as it
specifically rules out record extension as a programmer error.

for a full record system, there are two parts of the problem:
- opening closed record types to extension
- closing extensible record types to prevent extension

you argue that the second step is necessary, and suggest a 
generalisation of systems like Trex, Daan argued that a 
surprisingly large subset of practical problems can be 
addressed with the first step alone.

since the second step isn't entirely for free (those 'lacks'
and 'Disjoint' predicates keep piling up), there is something
to be said for offering both the step 1 and the step 1+2
systems.

there are several other features in which both kinds of
system go beyond haskell's labelled fields, but many of
those we might be able to agree on?-)

> These operators can be defined using type families: download the code  
> from
> http://homepage.ntlworld.com/b.hilken/files/Records.hs
> This code would only need minimal extensions to GHC to make it  
> completely useable.

i still have your original announcement in my inbox!-) i just
haven't got around to it yet, because i wanted to translate
my own system to type functions first, and other things keep
getting in the way..

>>.. (type sharing).. 
> I believe this issue is completely independent of records. Exactly  
> the same problem would arise if the same datatype with the same  
> constructors was defined in two different modules. To solve this we  
> need a mechanism whereby identically defined types in different  
> modules can be identified.

indeed. record labels just raise the urgency of the issue as
a real problem in programming practice.

> but I am strongly biased in favour of my own records system!

who isn't?-) that is exactly why none of the systems have made
it into haskell so far. and why we should allow for multiple options
if we want to go any further than the numerous previous attempts.

claus